From 78fe95f95fe51d50f696784035002c7951886c88 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Wed, 29 Dec 2021 08:04:23 +0000 Subject: [PATCH] Migration to Isabelle 2021-1 (based on afp-2021-12-28). --- .../Labeled_Stateful_Strands.thy | 2 +- Stateful_Protocol_Composition_and_Typing/Messages.thy | 8 +++++--- .../More_Unification.thy | 2 +- .../Stateful_Compositionality.thy | 4 ++-- .../Strands_and_Constraints.thy | 2 +- Stateful_Protocol_Composition_and_Typing/Typed_Model.thy | 2 +- .../document/root.tex | 1 + 7 files changed, 12 insertions(+), 9 deletions(-) diff --git a/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy b/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy index a7fe4d4..44120a9 100644 --- a/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy +++ b/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy @@ -485,7 +485,7 @@ lemma labeled_list_insert_eq_cases: "d \ set (unlabel D) \ List.insert d (unlabel D) = unlabel (List.insert (i,d) D)" "(i,d) \ set D \ List.insert d (unlabel D) = unlabel (List.insert (i,d) D)" unfolding unlabel_def -by (metis (no_types, hide_lams) List.insert_def image_eqI list.simps(9) set_map snd_conv, +by (metis (no_types, opaque_lifting) List.insert_def image_eqI list.simps(9) set_map snd_conv, metis in_set_insert set_zip_rightD zip_map_fst_snd) lemma labeled_list_insert_eq_ex_cases: diff --git a/Stateful_Protocol_Composition_and_Typing/Messages.thy b/Stateful_Protocol_Composition_and_Typing/Messages.thy index 6df19d3..55cffdf 100644 --- a/Stateful_Protocol_Composition_and_Typing/Messages.thy +++ b/Stateful_Protocol_Composition_and_Typing/Messages.thy @@ -110,7 +110,8 @@ using subterm_of_iff_subtermeq by blast subsection \The subterm relation is a partial order on terms\ -interpretation "term": order "(\)" "(\)" + +interpretation "term": ordering "(\)" "(\)" proof show "s \ s" for s :: "('a,'b) term" by (induct s rule: subterms.induct) auto @@ -137,10 +138,11 @@ proof } thus ?case by auto qed simp - thus "(s \ t) = (s \ t \ \(t \ s))" for s t :: "('a,'b) term" - by blast + show \s \ t \ s \ t\ for s t :: "('a,'b) term" .. qed +interpretation "term": order "(\)" "(\)" + by (rule ordering_orderI) (fact term.ordering_axioms) subsection \Lemmata concerning subterms and free variables\ lemma fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s_append: "fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s (F@G) = fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s F@fv_list\<^sub>p\<^sub>a\<^sub>i\<^sub>r\<^sub>s G" diff --git a/Stateful_Protocol_Composition_and_Typing/More_Unification.thy b/Stateful_Protocol_Composition_and_Typing/More_Unification.thy index d4b098f..e468348 100644 --- a/Stateful_Protocol_Composition_and_Typing/More_Unification.thy +++ b/Stateful_Protocol_Composition_and_Typing/More_Unification.thy @@ -1062,7 +1062,7 @@ proof unfolding range_vars_alt_def subst_compose_def by (auto simp add: subst_domain_def) { assume "x \ ?img \1" hence "x \ ?img \2" - by (metis (no_types, hide_lams) fv_in_subst_img Un_iff subst_compose_def + by (metis (no_types, opaque_lifting) fv_in_subst_img Un_iff subst_compose_def vt subsetCE subst_apply_term.simps(1) subst_sends_fv_to_img) } thus "x \ ?img \1 \ ?img \2" by auto diff --git a/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy b/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy index 848bc1b..3d0158a 100644 --- a/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy +++ b/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy @@ -1645,7 +1645,7 @@ proof - prefix_same_cases set_append suffix_def) hence "suffix [(m, receive\t\\<^sub>s\<^sub>t)] E'" "prefix E' A''" using *(1) prems(1,2) suffix_append[of "[(m,receive\t\\<^sub>s\<^sub>t)]" "constr Di" E'] *** - by (metis (no_types, hide_lams) Nil_suffix append_Nil2 in_set_conv_decomp rev_exhaust + by (metis (no_types, opaque_lifting) Nil_suffix append_Nil2 in_set_conv_decomp rev_exhaust snoc_suffix_snoc suffix_appendD, auto) then obtain F where "prefix F S" "E' \ set (tr\<^sub>p\<^sub>c F (filter (\d. d \ set Di) D))" @@ -1692,7 +1692,7 @@ proof - prefix_same_cases set_append suffix_def) hence "suffix [(m, receive\t\\<^sub>s\<^sub>t)] E'" "prefix E' A''" using *(1) prems(1,2) suffix_append[of "[(m,receive\t\\<^sub>s\<^sub>t)]" constr E'] *** - by (metis (no_types, hide_lams) Nil_suffix append_Nil2 in_set_conv_decomp rev_exhaust + by (metis (no_types, opaque_lifting) Nil_suffix append_Nil2 in_set_conv_decomp rev_exhaust snoc_suffix_snoc suffix_appendD, auto) then obtain F where "prefix F S" "E' \ set (tr\<^sub>p\<^sub>c F D)" using *(2) ** IH by metis diff --git a/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy b/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy index a88a358..a306d8c 100644 --- a/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy +++ b/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy @@ -1208,7 +1208,7 @@ next thus ?thesis using assms fv_strand_subst' unfolding subst_elim_def - by (metis (mono_tags, hide_lams) fv\<^sub>s\<^sub>e\<^sub>t.simps imageE mem_simps(8) subst_apply_term.simps(1)) + by (metis (mono_tags, opaque_lifting) fv\<^sub>s\<^sub>e\<^sub>t.simps imageE mem_simps(8) subst_apply_term.simps(1)) qed lemma strand_fv_subst_subset_if_subst_elim': diff --git a/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy b/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy index 675752a..54a5cab 100644 --- a/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy +++ b/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy @@ -2168,7 +2168,7 @@ proof - unfolding comp_tfr\<^sub>s\<^sub>e\<^sub>t_def Let_def by metis thus ?thesis using vars_term_disjoint_imp_unifier[OF var_rename_fv_set_disjoint[OF M_finite]] s0(1) t0(1) - unfolding s0(3) t0(3) by (metis (no_types, hide_lams) subst_subst_compose) + unfolding s0(3) t0(3) by (metis (no_types, opaque_lifting) subst_subst_compose) qed (use st_type_neq st(2,4) in auto) thus "\ s = \ t" when "\\. Unifier \ s t" by (metis that) qed diff --git a/Stateful_Protocol_Composition_and_Typing/document/root.tex b/Stateful_Protocol_Composition_and_Typing/document/root.tex index 8a462d0..fe9f1d6 100644 --- a/Stateful_Protocol_Composition_and_Typing/document/root.tex +++ b/Stateful_Protocol_Composition_and_Typing/document/root.tex @@ -1,5 +1,6 @@ \documentclass[10pt,DIV16,a4paper,abstract=true,twoside=semi,openright] {scrreprt} +\usepackage[T1]{fontenc} \usepackage[english]{babel} \usepackage[numbers, sort&compress]{natbib} \usepackage{isabelle,isabellesym}