From e40cb5bbde3bb783ac9f25037db63f12fba7faa2 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Fri, 31 Dec 2021 07:42:15 +0000 Subject: [PATCH] Migration to Isabelle 2021-1 (based on afp-2021-12-28). --- Extended_Finite_State_Machines/EFSM_LTL.thy | 2 +- Extended_Finite_State_Machines/FSet_Utils.thy | 4 +-- Extended_Finite_State_Machines/GExp.thy | 32 +++++++------------ Extended_Finite_State_Machines/Trilean.thy | 10 +++--- Extended_Finite_State_Machines/VName.thy | 16 +++------- .../document/root.tex | 1 + 6 files changed, 25 insertions(+), 40 deletions(-) diff --git a/Extended_Finite_State_Machines/EFSM_LTL.thy b/Extended_Finite_State_Machines/EFSM_LTL.thy index 2ffdbd1..00951b5 100644 --- a/Extended_Finite_State_Machines/EFSM_LTL.thy +++ b/Extended_Finite_State_Machines/EFSM_LTL.thy @@ -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) lemma snth_sconst: "(\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 (\xs. shd xs = h) t) = (t = sconst h)" by (simp add: snth_sconst[symmetric] alw_iff_sdrop) diff --git a/Extended_Finite_State_Machines/FSet_Utils.thy b/Extended_Finite_State_Machines/FSet_Utils.thy index 1e8eb7a..c54be68 100644 --- a/Extended_Finite_State_Machines/FSet_Utils.thy +++ b/Extended_Finite_State_Machines/FSet_Utils.thy @@ -128,7 +128,7 @@ lemma sorted_hd_Min: "sorted l \ 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 \ [] \ hd (sort l) = Min (set l)" 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 apply (induct l arbitrary: b) 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" by (metis exists_sorted_distinct_fset_of_list sorted_distinct_ffold_ord distinct_remdups_id sorted_list_of_fset_sort sorted_sort_id) diff --git a/Extended_Finite_State_Machines/GExp.thy b/Extended_Finite_State_Machines/GExp.thy index bfc58f1..be94bd0 100644 --- a/Extended_Finite_State_Machines/GExp.thy +++ b/Extended_Finite_State_Machines/GExp.thy @@ -166,17 +166,17 @@ next qed auto definition max_input :: "vname gexp \ 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 \ nat option" where - "max_input_list g = fold max (map (\g. max_input g) g) None" + "max_input_list g = fold max (map max_input g) None" lemma max_input_list_cons: "max_input_list (a # G) = max (max_input a) (max_input_list G)" - apply (simp add: max_input_list_def) - apply (cases "max_input a") - apply (simp add: max_def_raw) - by (metis (no_types, lifting) List.finite_set Max.insert Max.set_eq_fold fold_simps(1) list.set(2) max.assoc set_empty) + apply (cases \max_input a\) + apply (simp_all add: max_input_list_def flip: Max.set_eq_fold) + apply (metis (mono_tags, lifting) List.finite_set Max_insert Max_singleton bot_option_def finite_imageI max.assoc max_bot2) + done fun enumerate_regs :: "vname gexp \ nat set" where "enumerate_regs (Bc _) = {}" | @@ -233,12 +233,13 @@ proof- qed definition max_reg_list :: "vname gexp list \ nat option" where - "max_reg_list g = (fold max (map (\g. max_reg g) g) None)" + "max_reg_list g = fold max (map max_reg g) None" lemma max_reg_list_cons: "max_reg_list (a # G) = max (max_reg a) (max_reg_list G)" - apply (simp add: max_reg_list_def) - 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 (simp add: max_reg_list_def flip: Max.set_eq_fold) + 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: "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) lemma length_take_or_pad: "length (take_or_pad a n) = n" -proof(induct n) - 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 + by (induction n) (simp_all add: take_or_pad_def length_padding) fun enumerate_gexp_strings :: "'a gexp \ String.literal set" where "enumerate_gexp_strings (Bc _) = {}" | diff --git a/Extended_Finite_State_Machines/Trilean.thy b/Extended_Finite_State_Machines/Trilean.thy index 2f2db7a..8898cde 100644 --- a/Extended_Finite_State_Machines/Trilean.thy +++ b/Extended_Finite_State_Machines/Trilean.thy @@ -134,22 +134,22 @@ next case 3 then show ?case 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 case "4_1" then show ?case 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 case "4_2" then show ?case 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 case 5 then show ?case 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 instance @@ -254,7 +254,7 @@ lemma maybe_not_eq: "(\? x = \? y) = (x = y)" lemma de_morgans_1: "\? (a \? b) = (\?a) \? (\?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: "\? (a \? b) = (\?a) \? (\?b)" diff --git a/Extended_Finite_State_Machines/VName.thy b/Extended_Finite_State_Machines/VName.thy index ec953e8..185cc19 100644 --- a/Extended_Finite_State_Machines/VName.thy +++ b/Extended_Finite_State_Machines/VName.thy @@ -27,18 +27,12 @@ declare less_eq_vname_def [simp] instance 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 simp + apply (auto elim: less_vname.elims) subgoal for x y z - apply (induct x y rule: less_vname.induct) - apply (metis less_eq_vname_def less_vname.elims(2) less_vname.elims(3) vname.simps(4)) - apply simp - apply (metis less_eq_vname_def less_trans less_vname.elims(3) less_vname.simps(3) vname.simps(4)) - 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 + apply (cases x; cases y; cases z) + apply simp_all + done + done end end diff --git a/Extended_Finite_State_Machines/document/root.tex b/Extended_Finite_State_Machines/document/root.tex index bc1c425..bc70ce8 100644 --- a/Extended_Finite_State_Machines/document/root.tex +++ b/Extended_Finite_State_Machines/document/root.tex @@ -1,4 +1,5 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright]{scrreprt} +\usepackage[T1]{fontenc} \usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym}