Migration to Isabelle 2021-1 (based on afp-2021-12-28).
This commit is contained in:
parent
1f29340b1b
commit
7e2f942e0a
|
@ -71,7 +71,7 @@ lemma inconsistent_updates:
|
||||||
(\<exists>r' P. P (p2 $ r') \<and> (\<exists>y. p1 $ r' = Some y) \<and> \<not> P (p1 $ r')) \<Longrightarrow>
|
(\<exists>r' P. P (p2 $ r') \<and> (\<exists>y. p1 $ r' = Some y) \<and> \<not> P (p1 $ r')) \<Longrightarrow>
|
||||||
|
|
||||||
\<not> subsumes t2 r t1"
|
\<not> subsumes t2 r t1"
|
||||||
by (metis (no_types, hide_lams) option.simps(3) subsumes_def)
|
by (metis (no_types, opaque_lifting) option.simps(3) subsumes_def)
|
||||||
|
|
||||||
lemma bad_outputs:
|
lemma bad_outputs:
|
||||||
"\<exists>i. can_take_transition t1 i r \<and> evaluate_outputs t1 i r \<noteq> evaluate_outputs t2 i r \<Longrightarrow>
|
"\<exists>i. can_take_transition t1 i r \<and> evaluate_outputs t1 i r \<noteq> evaluate_outputs t2 i r \<Longrightarrow>
|
||||||
|
|
|
@ -139,7 +139,7 @@ proof(induct l)
|
||||||
next
|
next
|
||||||
case (Cons a l)
|
case (Cons a l)
|
||||||
then show ?case
|
then show ?case
|
||||||
by (metis sorted_Max_Cons Max_singleton hd_rev last.simps list.set(1) list.simps(15) sorted.simps(2))
|
by (metis sorted_Max_Cons Max_singleton hd_rev last.simps list.set(1) list.simps(15) sorted_simps(2))
|
||||||
qed
|
qed
|
||||||
|
|
||||||
lemma [code]: "fMax (fset_of_list (h#t)) = last (nativeSort (h#t))"
|
lemma [code]: "fMax (fset_of_list (h#t)) = last (nativeSort (h#t))"
|
||||||
|
|
|
@ -5,7 +5,7 @@ sets. All of the sets we need to use here are finite so we present an alternativ
|
||||||
basic set operations which generates much cleaner code.\<close>
|
basic set operations which generates much cleaner code.\<close>
|
||||||
|
|
||||||
theory Code_Target_Set
|
theory Code_Target_Set
|
||||||
imports "HOL-Library.Cardinality"
|
imports "HOL-Library.Code_Cardinality"
|
||||||
begin
|
begin
|
||||||
|
|
||||||
code_datatype set
|
code_datatype set
|
||||||
|
@ -19,7 +19,7 @@ declare eq_set_code(2) [code del]
|
||||||
declare eq_set_code(4) [code del]
|
declare eq_set_code(4) [code del]
|
||||||
declare List.subset_code [code del]
|
declare List.subset_code [code del]
|
||||||
declare inter_coset_fold [code del]
|
declare inter_coset_fold [code del]
|
||||||
declare Cardinality.subset'_code [code del]
|
declare Code_Cardinality.subset'_code [code del]
|
||||||
|
|
||||||
declare subset_eq [code]
|
declare subset_eq [code]
|
||||||
|
|
||||||
|
@ -38,7 +38,7 @@ lemma [code]: "insert x (set s) = (if x \<in> set s then set s else set (x#s))"
|
||||||
by auto
|
by auto
|
||||||
|
|
||||||
lemma [code]:
|
lemma [code]:
|
||||||
"Cardinality.subset' (set l1) (set l2) = ((list_all (\<lambda>x. List.member l2 x)) l1)"
|
"Code_Cardinality.subset' (set l1) (set l2) = ((list_all (\<lambda>x. List.member l2 x)) l1)"
|
||||||
by (meson in_set_member list.pred_set subset'_code(2))
|
by (meson in_set_member list.pred_set subset'_code(2))
|
||||||
|
|
||||||
end
|
end
|
||||||
|
|
|
@ -1,4 +1,5 @@
|
||||||
\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt}
|
\documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt}
|
||||||
|
\usepackage[T1]{fontenc}
|
||||||
\usepackage[english]{babel}
|
\usepackage[english]{babel}
|
||||||
\usepackage[numbers, sort&compress]{natbib}
|
\usepackage[numbers, sort&compress]{natbib}
|
||||||
\usepackage{isabelle,isabellesym}
|
\usepackage{isabelle,isabellesym}
|
||||||
|
|
Loading…
Reference in New Issue