Migration to Isabelle 2021-1 (based on afp-2021-12-28).
This commit is contained in:
parent
c3c1cafaa3
commit
e40cb5bbde
|
@ -228,7 +228,7 @@ lemma once_none_nxt_always_none: "alw (nxt (state_eq None)) (make_full_observati
|
||||||
by (simp add: alw_iff_sdrop del: sdrop.simps)
|
by (simp add: alw_iff_sdrop del: sdrop.simps)
|
||||||
|
|
||||||
lemma snth_sconst: "(\<forall>i. s !! i = h) = (s = sconst h)"
|
lemma snth_sconst: "(\<forall>i. s !! i = h) = (s = sconst h)"
|
||||||
by (metis funpow_code_def id_funpow sdrop_simps(1) sdrop_siterate siterate.simps(1) smap_alt smap_sconst snth.simps(1) stream.map_id)
|
by (auto simp add: sconst_alt sset_range)
|
||||||
|
|
||||||
lemma alw_sconst: "(alw (\<lambda>xs. shd xs = h) t) = (t = sconst h)"
|
lemma alw_sconst: "(alw (\<lambda>xs. shd xs = h) t) = (t = sconst h)"
|
||||||
by (simp add: snth_sconst[symmetric] alw_iff_sdrop)
|
by (simp add: snth_sconst[symmetric] alw_iff_sdrop)
|
||||||
|
|
|
@ -128,7 +128,7 @@ lemma sorted_hd_Min:
|
||||||
"sorted l \<Longrightarrow>
|
"sorted l \<Longrightarrow>
|
||||||
l \<noteq> [] \<Longrightarrow>
|
l \<noteq> [] \<Longrightarrow>
|
||||||
hd l = Min (set l)"
|
hd l = Min (set l)"
|
||||||
by (metis List.finite_set Min_eqI eq_iff hd_Cons_tl insertE list.set_sel(1) list.simps(15) sorted.simps(2))
|
by (metis List.finite_set Min_eqI eq_iff hd_Cons_tl insertE list.set_sel(1) list.simps(15) sorted_simps(2))
|
||||||
|
|
||||||
lemma hd_sort_Min: "l \<noteq> [] \<Longrightarrow> hd (sort l) = Min (set l)"
|
lemma hd_sort_Min: "l \<noteq> [] \<Longrightarrow> hd (sort l) = Min (set l)"
|
||||||
by (metis sorted_hd_Min set_empty set_sort sorted_sort)
|
by (metis sorted_hd_Min set_empty set_sort sorted_sort)
|
||||||
|
@ -214,7 +214,7 @@ lemma sorted_distinct_ffold_ord: assumes "sorted l"
|
||||||
using assms
|
using assms
|
||||||
apply (induct l arbitrary: b)
|
apply (induct l arbitrary: b)
|
||||||
apply simp
|
apply simp
|
||||||
by (metis distinct.simps(2) ffold_ord_cons fold_simps(2) sorted.simps(2))
|
by (metis distinct.simps(2) ffold_ord_cons fold_simps(2) sorted_simps(2))
|
||||||
|
|
||||||
lemma ffold_ord_fold_sorted: "ffold_ord f s b = fold f (sorted_list_of_fset s) b"
|
lemma ffold_ord_fold_sorted: "ffold_ord f s b = fold f (sorted_list_of_fset s) b"
|
||||||
by (metis exists_sorted_distinct_fset_of_list sorted_distinct_ffold_ord distinct_remdups_id sorted_list_of_fset_sort sorted_sort_id)
|
by (metis exists_sorted_distinct_fset_of_list sorted_distinct_ffold_ord distinct_remdups_id sorted_list_of_fset_sort sorted_sort_id)
|
||||||
|
|
|
@ -166,17 +166,17 @@ next
|
||||||
qed auto
|
qed auto
|
||||||
|
|
||||||
definition max_input :: "vname gexp \<Rightarrow> nat option" where
|
definition max_input :: "vname gexp \<Rightarrow> nat option" where
|
||||||
"max_input g = (let inputs = (enumerate_gexp_inputs g) in if inputs = {} then None else Some (Max inputs))"
|
"max_input g = (let inputs = enumerate_gexp_inputs g in if inputs = {} then None else Some (Max inputs))"
|
||||||
|
|
||||||
definition max_input_list :: "vname gexp list \<Rightarrow> nat option" where
|
definition max_input_list :: "vname gexp list \<Rightarrow> nat option" where
|
||||||
"max_input_list g = fold max (map (\<lambda>g. max_input g) g) None"
|
"max_input_list g = fold max (map max_input g) None"
|
||||||
|
|
||||||
lemma max_input_list_cons:
|
lemma max_input_list_cons:
|
||||||
"max_input_list (a # G) = max (max_input a) (max_input_list G)"
|
"max_input_list (a # G) = max (max_input a) (max_input_list G)"
|
||||||
apply (simp add: max_input_list_def)
|
apply (cases \<open>max_input a\<close>)
|
||||||
apply (cases "max_input a")
|
apply (simp_all add: max_input_list_def flip: Max.set_eq_fold)
|
||||||
apply (simp add: max_def_raw)
|
apply (metis (mono_tags, lifting) List.finite_set Max_insert Max_singleton bot_option_def finite_imageI max.assoc max_bot2)
|
||||||
by (metis (no_types, lifting) List.finite_set Max.insert Max.set_eq_fold fold_simps(1) list.set(2) max.assoc set_empty)
|
done
|
||||||
|
|
||||||
fun enumerate_regs :: "vname gexp \<Rightarrow> nat set" where
|
fun enumerate_regs :: "vname gexp \<Rightarrow> nat set" where
|
||||||
"enumerate_regs (Bc _) = {}" |
|
"enumerate_regs (Bc _) = {}" |
|
||||||
|
@ -233,12 +233,13 @@ proof-
|
||||||
qed
|
qed
|
||||||
|
|
||||||
definition max_reg_list :: "vname gexp list \<Rightarrow> nat option" where
|
definition max_reg_list :: "vname gexp list \<Rightarrow> nat option" where
|
||||||
"max_reg_list g = (fold max (map (\<lambda>g. max_reg g) g) None)"
|
"max_reg_list g = fold max (map max_reg g) None"
|
||||||
|
|
||||||
lemma max_reg_list_cons:
|
lemma max_reg_list_cons:
|
||||||
"max_reg_list (a # G) = max (max_reg a) (max_reg_list G)"
|
"max_reg_list (a # G) = max (max_reg a) (max_reg_list G)"
|
||||||
apply (simp add: max_reg_list_def)
|
apply (simp add: max_reg_list_def flip: Max.set_eq_fold)
|
||||||
by (metis (no_types, lifting) List.finite_set Max.insert Max.set_eq_fold fold.simps(1) id_apply list.simps(15) max.assoc set_empty)
|
apply (metis List.finite_set Max_insert bot_option_def empty_not_insert finite_imageI finite_insert insert_commute max.commute max_bot2)
|
||||||
|
done
|
||||||
|
|
||||||
lemma max_reg_list_append_singleton:
|
lemma max_reg_list_append_singleton:
|
||||||
"max_reg_list (as@[bs]) = max (max_reg_list as) (max_reg_list [bs])"
|
"max_reg_list (as@[bs]) = max (max_reg_list as) (max_reg_list [bs])"
|
||||||
|
@ -713,18 +714,7 @@ lemma length_padding: "length (padding n) = n"
|
||||||
by (induct n, auto)
|
by (induct n, auto)
|
||||||
|
|
||||||
lemma length_take_or_pad: "length (take_or_pad a n) = n"
|
lemma length_take_or_pad: "length (take_or_pad a n) = n"
|
||||||
proof(induct n)
|
by (induction n) (simp_all add: take_or_pad_def length_padding)
|
||||||
case 0
|
|
||||||
then show ?case
|
|
||||||
by (simp add: take_or_pad_def)
|
|
||||||
next
|
|
||||||
case (Suc n)
|
|
||||||
then show ?case
|
|
||||||
apply (simp add: take_or_pad_def)
|
|
||||||
apply standard
|
|
||||||
apply auto[1]
|
|
||||||
by (simp add: length_padding)
|
|
||||||
qed
|
|
||||||
|
|
||||||
fun enumerate_gexp_strings :: "'a gexp \<Rightarrow> String.literal set" where
|
fun enumerate_gexp_strings :: "'a gexp \<Rightarrow> String.literal set" where
|
||||||
"enumerate_gexp_strings (Bc _) = {}" |
|
"enumerate_gexp_strings (Bc _) = {}" |
|
||||||
|
|
|
@ -134,22 +134,22 @@ next
|
||||||
case 3
|
case 3
|
||||||
then show ?case
|
then show ?case
|
||||||
apply simp
|
apply simp
|
||||||
by (metis (no_types, hide_lams) plus_trilean.simps(1) plus_trilean.simps(4) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(4) times_trilean.simps(5) trilean.exhaust)
|
by (metis (no_types, opaque_lifting) plus_trilean.simps(1) plus_trilean.simps(4) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(4) times_trilean.simps(5) trilean.exhaust)
|
||||||
next
|
next
|
||||||
case "4_1"
|
case "4_1"
|
||||||
then show ?case
|
then show ?case
|
||||||
apply simp
|
apply simp
|
||||||
by (metis (no_types, hide_lams) plus_trilean.simps(1) plus_trilean.simps(5) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(4) times_trilean.simps(5) times_trilean.simps(6) times_trilean.simps(7) trilean.exhaust)
|
by (metis (no_types, opaque_lifting) plus_trilean.simps(1) plus_trilean.simps(5) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(4) times_trilean.simps(5) times_trilean.simps(6) times_trilean.simps(7) trilean.exhaust)
|
||||||
next
|
next
|
||||||
case "4_2"
|
case "4_2"
|
||||||
then show ?case
|
then show ?case
|
||||||
apply simp
|
apply simp
|
||||||
by (metis (no_types, hide_lams) plus_trilean.simps(1) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(6) times_trilean.simps(7) trilean.exhaust)
|
by (metis (no_types, opaque_lifting) plus_trilean.simps(1) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(6) times_trilean.simps(7) trilean.exhaust)
|
||||||
next
|
next
|
||||||
case 5
|
case 5
|
||||||
then show ?case
|
then show ?case
|
||||||
apply simp
|
apply simp
|
||||||
by (metis (no_types, hide_lams) plus_trilean.simps(1) plus_trilean.simps(6) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(4) times_trilean.simps(5) times_trilean.simps(6) times_trilean.simps(7) trilean.exhaust)
|
by (metis (no_types, opaque_lifting) plus_trilean.simps(1) plus_trilean.simps(6) plus_trilean.simps(7) times_trilean.simps(1) times_trilean.simps(4) times_trilean.simps(5) times_trilean.simps(6) times_trilean.simps(7) trilean.exhaust)
|
||||||
qed
|
qed
|
||||||
|
|
||||||
instance
|
instance
|
||||||
|
@ -254,7 +254,7 @@ lemma maybe_not_eq: "(\<not>? x = \<not>? y) = (x = y)"
|
||||||
|
|
||||||
lemma de_morgans_1:
|
lemma de_morgans_1:
|
||||||
"\<not>? (a \<or>? b) = (\<not>?a) \<and>? (\<not>?b)"
|
"\<not>? (a \<or>? b) = (\<not>?a) \<and>? (\<not>?b)"
|
||||||
by (metis (no_types, hide_lams) add.commute invalid_maybe_and maybe_and_idempotent maybe_and_one maybe_not.elims maybe_not.simps(1) maybe_not.simps(3) maybe_not_invalid maybe_or_zero plus_trilean.simps(1) plus_trilean.simps(4) times_trilean.simps(1) times_trilean_commutative trilean.exhaust trilean.simps(6))
|
by (metis (no_types, opaque_lifting) add.commute invalid_maybe_and maybe_and_idempotent maybe_and_one maybe_not.elims maybe_not.simps(1) maybe_not.simps(3) maybe_not_invalid maybe_or_zero plus_trilean.simps(1) plus_trilean.simps(4) times_trilean.simps(1) times_trilean_commutative trilean.exhaust trilean.simps(6))
|
||||||
|
|
||||||
lemma de_morgans_2:
|
lemma de_morgans_2:
|
||||||
"\<not>? (a \<and>? b) = (\<not>?a) \<or>? (\<not>?b)"
|
"\<not>? (a \<and>? b) = (\<not>?a) \<or>? (\<not>?b)"
|
||||||
|
|
|
@ -27,18 +27,12 @@ declare less_eq_vname_def [simp]
|
||||||
|
|
||||||
instance
|
instance
|
||||||
apply standard
|
apply standard
|
||||||
apply (metis (full_types) dual_order.asym less_eq_vname_def less_vname.simps(2) less_vname.simps(3) less_vname.simps(4) vname.exhaust)
|
apply (auto elim: less_vname.elims)
|
||||||
apply simp
|
|
||||||
subgoal for x y z
|
subgoal for x y z
|
||||||
apply (induct x y rule: less_vname.induct)
|
apply (cases x; cases y; cases z)
|
||||||
apply (metis less_eq_vname_def less_vname.elims(2) less_vname.elims(3) vname.simps(4))
|
apply simp_all
|
||||||
apply simp
|
done
|
||||||
apply (metis less_eq_vname_def less_trans less_vname.elims(3) less_vname.simps(3) vname.simps(4))
|
done
|
||||||
by (metis le_less_trans less_eq_vname_def less_imp_le_nat less_vname.elims(2) less_vname.simps(4) vname.simps(4))
|
|
||||||
apply (metis dual_order.asym less_eq_vname_def less_vname.elims(2) less_vname.simps(3) less_vname.simps(4))
|
|
||||||
subgoal for x y
|
|
||||||
by (induct x y rule: less_vname.induct, auto)
|
|
||||||
done
|
|
||||||
end
|
end
|
||||||
|
|
||||||
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