Renamed upstream repository.

README.md

@@ -12,7 +12,7 @@ submitted (as an update of the Stateful Protocol Composition and Typing entry) a
 ## Installation
 
 ```console
-achim@logicalhacking:~$ isabelle build -D Stateful_Protocol_Composition_and_Typing.html
+achim@logicalhacking:~$ isabelle build -D Stateful_Protocol_Composition_and_Typing
 ```
 
 ## Authors
@@ -27,10 +27,10 @@ This project is licensed under a 3-clause BSD-style license.
 
 SPDX-License-Identifier: BSD-3-Clause
 
-## Master Repository
+## Upstream Repository
 
-The master git repository for this project is hosted by the [Software
+The upstream git repository, i.e., the single source of truth, for this project is hosted 
-Assurance & Security Research Team](https://logicalhacking.com) at
+by the [Software Assurance & Security Research Team](https://logicalhacking.com) at
 <https://git.logicalhacking.com/afp-mirror/Stateful_Protocol_Composition_and_Typing>.
 
 ## Publications

Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy

@@ -485,7 +485,7 @@ lemma labeled_list_insert_eq_cases:
   "d \<notin> set (unlabel D) \<Longrightarrow> List.insert d (unlabel D) = unlabel (List.insert (i,d) D)"
   "(i,d) \<in> set D \<Longrightarrow> 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:

Stateful_Protocol_Composition_and_Typing/Messages.thy

@@ -110,7 +110,8 @@ using subterm_of_iff_subtermeq by blast
 
 
 subsection \<open>The subterm relation is a partial order on terms\<close>
-interpretation "term": order "(\<sqsubseteq>)" "(\<sqsubset>)"
+
+interpretation "term": ordering "(\<sqsubseteq>)" "(\<sqsubset>)"
 proof
   show "s \<sqsubseteq> 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 \<sqsubset> t) = (s \<sqsubseteq> t \<and> \<not>(t \<sqsubseteq> s))" for s t :: "('a,'b) term"
+  show \<open>s \<sqsubset> t \<longleftrightarrow> s \<sqsubset> t\<close> for s t :: "('a,'b) term" ..
-    by blast
 qed
 
+interpretation "term": order "(\<sqsubseteq>)" "(\<sqsubset>)"
+  by (rule ordering_orderI) (fact term.ordering_axioms)
 
 subsection \<open>Lemmata concerning subterms and free variables\<close>
 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"

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 \<notin> ?img \<theta>1" hence "x \<in> ?img \<theta>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 \<in> ?img \<theta>1 \<union> ?img \<theta>2" by auto

Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy

@@ -1645,7 +1645,7 @@ proof -
                                        prefix_same_cases set_append suffix_def)
       hence "suffix [(m, receive\<langle>t\<rangle>\<^sub>s\<^sub>t)] E'" "prefix E' A''"
         using *(1) prems(1,2) suffix_append[of "[(m,receive\<langle>t\<rangle>\<^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' \<in> set (tr\<^sub>p\<^sub>c F (filter (\<lambda>d. d \<notin> set Di) D))"
@@ -1692,7 +1692,7 @@ proof -
                                        prefix_same_cases set_append suffix_def)
       hence "suffix [(m, receive\<langle>t\<rangle>\<^sub>s\<^sub>t)] E'" "prefix E' A''"
         using *(1) prems(1,2) suffix_append[of "[(m,receive\<langle>t\<rangle>\<^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' \<in> set (tr\<^sub>p\<^sub>c F D)" using *(2) ** IH by metis

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':

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 "\<Gamma> s = \<Gamma> t" when "\<exists>\<delta>. Unifier \<delta> s t" by (metis that)
   qed

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}