Update to Isabelle2021-1 and AFP 2022-01-06

WebAssembly/ROOT

@@ -1,6 +1,5 @@
 session WebAssembly_Dev = "HOL-Library" +
   description "WebAssembly"
-  options [quick_and_dirty]
   sessions
     Native_Word
   theories

WebAssembly/Wasm_Ast.thy

@@ -1,4 +1,4 @@
-section {* WebAssembly Core AST *}
+section \<open>WebAssembly Core AST\<close>
 
 theory Wasm_Ast
   imports

WebAssembly/Wasm_Axioms.thy

@@ -1,4 +1,4 @@
-section {* Host Properties *}
+section \<open>Host Properties\<close>
 
 theory Wasm_Axioms imports Wasm begin
 

WebAssembly/Wasm_Base_Defs.thy

@@ -1,4 +1,4 @@
-section {* WebAssembly Base Definitions *}
+section \<open>WebAssembly Base Definitions\<close>
 
 theory Wasm_Base_Defs
   imports
@@ -202,7 +202,7 @@ definition word_rsplit_rev :: "'a::len word \<Rightarrow> 'b::len word list"
 lemma word_rsplit_rev_is: "word_rsplit_rev = rev \<circ> word_rsplit"
   using bin_rsplit_rev_is
   unfolding word_rsplit_def bin_rsplit_def word_rsplit_rev_def comp_def
-  by (metis (no_types, hide_lams) append_Nil fst_conv rev.simps(1) rev_map snd_conv)
+  by (metis (no_types, opaque_lifting) append_Nil fst_conv rev.simps(1) rev_map snd_conv)
 
 lift_definition serialise_i32 :: "i32 \<Rightarrow> bytes" is "word_rsplit_rev" .
 lift_definition serialise_i64 :: "i64 \<Rightarrow> bytes" is "word_rsplit_rev" .

WebAssembly/Wasm_Checker.thy

@@ -1,4 +1,4 @@
-section {* Executable Type Checker *}
+section \<open>Executable Type Checker\<close>
 
 theory Wasm_Checker imports Wasm_Checker_Types begin
 

WebAssembly/Wasm_Checker_Properties.thy

@@ -1,8 +1,8 @@
-section {* Correctness of Type Checker *}
+section \<open>Correctness of Type Checker\<close>
 
 theory Wasm_Checker_Properties imports Wasm_Checker Wasm_Properties begin
 
-subsection {* Soundness *}
+subsection \<open>Soundness\<close>
 
 lemma b_e_check_single_type_sound:
   assumes "type_update (Type x1) (to_ct_list t_in) (Type t_out) = Type x2"
@@ -818,7 +818,7 @@ proof -
     by simp
 qed
 
-subsection {* Completeness *}
+subsection \<open>Completeness\<close>
 
 lemma check_single_imp:
   assumes "check_single \<C> e ctn = ctm"

WebAssembly/Wasm_Checker_Types.thy

@@ -1,4 +1,4 @@
-section {* Augmented Type Syntax for Concrete Checker *}
+section \<open>Augmented Type Syntax for Concrete Checker\<close>
 
 theory Wasm_Checker_Types imports Wasm "HOL-Library.Sublist" begin
 
@@ -1035,7 +1035,7 @@ proof (cases c1)
       using ct_suffix_cons_ct_list[of "take (length cts - 3) cts" "[TSome x2]"]
             assms(3) c_types_agree.simps(2)[of ctm cm] ct_list_compat_ts_conv_eq
       unfolding ct_list_compat_def to_ct_list_def
-      by (metis (no_types, hide_lams) list.simps(8,9))
+      by (metis (no_types, opaque_lifting) list.simps(8,9))
     thus ?thesis
       using TSome outer_TAny
       by simp
@@ -1054,7 +1054,7 @@ next
       using ct_suffix_cons_ct_list[of "take (length cts - 3) cts" "[TSome x2]"]
             assms(3) c_types_agree.simps(2)[of ctm cm] ct_list_compat_ts_conv_eq
       unfolding ct_list_compat_def to_ct_list_def
-      by (metis (no_types, hide_lams) list.simps(8,9))
+      by (metis (no_types, opaque_lifting) list.simps(8,9))
     thus ?thesis
       using TSome TAny
       by simp
@@ -1071,7 +1071,7 @@ next
       using ct_suffix_cons_ct_list[of "take (length cts - 3) cts" "[TSome x2]"]
             assms(3) c_types_agree.simps(2)[of ctm cm] ct_list_compat_ts_conv_eq
       unfolding ct_list_compat_def to_ct_list_def
-      by (metis (no_types, hide_lams) list.simps(8,9))
+      by (metis (no_types, opaque_lifting) list.simps(8,9))
     thus ?thesis
       using TSome outer_TSome x_eq
       by simp

WebAssembly/Wasm_Properties.thy

@@ -1,8 +1,8 @@
-section {* Lemmas for Soundness Proof *}
+section \<open>Lemmas for Soundness Proof\<close>
 
 theory Wasm_Properties imports Wasm_Properties_Aux begin
 
-subsection {* Preservation *}
+subsection \<open>Preservation\<close>
 
 lemma t_cvt: assumes "cvt t sx v = Some v'" shows "t = typeof v'"
   using assms
@@ -1217,7 +1217,8 @@ lemma types_preserved_get_local:
 proof -
   have "(local \<C>)!i = typeof v"
     using assms(2,3)
-    by (metis (no_types, hide_lams) append_Cons length_map list.simps(9) map_append nth_append_length)
+    by (metis (no_types, opaque_lifting) append_Cons length_map list.simps(9) map_append
+        nth_append_length)
   hence "ts' = ts@[typeof v]"
     using assms(1) unlift_b_e[of s \<C> "[Get_local i]"] b_e_type_get_local
     by fastforce
@@ -1234,7 +1235,8 @@ lemma types_preserved_set_local:
 proof -
   have v_type:"(local \<C>)!i = typeof v"
     using assms(2,3)
-    by (metis (no_types, hide_lams) append_Cons length_map list.simps(9) map_append nth_append_length)
+    by (metis (no_types, opaque_lifting) append_Cons length_map list.simps(9) map_append
+        nth_append_length)
   obtain ts'' where ts''_def:"s\<bullet>\<C> \<turnstile> [$C v'] : (ts _> ts'')" 
                              "s\<bullet>\<C> \<turnstile> [$Set_local i] : (ts'' _> ts')"
     using e_type_comp assms
@@ -1590,7 +1592,7 @@ proof -
     done
 qed
 
-subsection {* Progress *}
+subsection \<open>Progress\<close>
 
 lemma const_list_no_progress:
   assumes "const_list es"
@@ -1673,34 +1675,30 @@ qed
 lemma trap_no_progress:
   assumes "es = [Trap]"
   shows "\<not>\<lparr>s;f;es\<rparr> \<leadsto> \<lparr>s';f';es'\<rparr>"
-proof -
-  {
-    assume "\<lparr>s;f;es\<rparr> \<leadsto> \<lparr>s';f';es'\<rparr>"
-    hence False
-      using assms
-    proof (induction rule: reduce.induct)
-      case (basic e e' s vs)
-      thus ?case
-      by (induction rule: reduce_simple.induct) auto
+proof (rule notI)
+  assume "\<lparr>s;f;es\<rparr> \<leadsto> \<lparr>s';f';es'\<rparr>"
+  thus False
+    unfolding assms
+  proof (induction s f "[Trap]" s' f' es' rule: reduce.induct)
+    case (basic e' s vs)
+    thus ?case
+      by (cases rule: reduce_simple.cases) simp_all
+  next
+    case (label s f es s' f' es' k lholed les')
+    show ?case
+      using label.hyps(3)
+    proof (cases rule: Lfilled.cases)
+      case (L0 vs es')
+      show ?thesis
+        using L0(2) label.hyps(1,2) empty_no_progress
+        by (auto simp add: Cons_eq_append_conv)
     next
-      case (label s f es s' f' es' k lholed les les')
-      show ?case
-        using label(2)
-        proof (cases rule: Lfilled.cases)
-          case (L0 vs es')
-          show ?thesis
-            using L0(2) label(1,4,5) empty_no_progress
-            by (auto simp add: Cons_eq_append_conv)
-        next
-          case (LN vs n es' l es'' k' lfilledk)
-          show ?thesis
-            using LN(2) label(5)
-            by (simp add: Cons_eq_append_conv)
-        qed
-    qed auto
-  }
-  thus ?thesis
-    by blast
+      case (LN vs n es' l es'' k' lfilledk)
+      show ?thesis
+        using LN(2) label.hyps(4)
+        by (simp add: Cons_eq_append_conv)
+    qed
+  qed auto
 qed
 
 lemma terminal_no_progress:

WebAssembly/Wasm_Properties_Aux.thy

@@ -1,4 +1,4 @@
-section {* Auxiliary Type System Properties *}
+section \<open>Auxiliary Type System Properties\<close>
 
 theory Wasm_Properties_Aux imports Wasm_Axioms begin
 

WebAssembly/Wasm_Soundness.thy

@@ -1,4 +1,4 @@
-section {* Soundness Theorems *}
+section \<open>Soundness Theorems\<close>
 
 theory Wasm_Soundness imports Main Wasm_Properties begin
 

WebAssembly/Wasm_Type_Printing.thy

@@ -27,6 +27,11 @@ Repeat all code equations explicitly again because the ones like @{const I32.int
 in export_code. Most of these are simply the original definitions, but we can also do some minor
 optimizations like in @{const int_shl} and others below.
 \<close>
+
+context
+  includes bit_operations_syntax
+begin
+
 lemma[code]: "int_clz (Abs_i32 x) = Abs_i32 (of_nat (word_clz x))"
   by (simp add: I32.int_clz_def int_clz_i32.abs_eq)
 lemma[code]: "int_ctz (Abs_i32 x) = Abs_i32 (of_nat (word_ctz x))"
@@ -171,6 +176,8 @@ lemma[code]: "int_ge_u (Abs_i64 x) (Abs_i64 y) \<longleftrightarrow> x \<ge> y"
 lemma[code]: "int_ge_s (Abs_i64 x) (Abs_i64 y) \<longleftrightarrow> signed.greater_eq x y"
   by (simp add: I64.int_ge_s_def int_ge_s_i64.abs_eq)
 
+end
+
 (* Sometimes to implement conversions we need to indirect through OCaml int types *)
 typedecl ocaml_i32
 typedecl ocaml_i64

WebAssembly/Wasm_Type_Word.thy

@@ -5,7 +5,7 @@ theory Wasm_Type_Word
     Wasm_Type_Abs
     "Word_Lib.Signed_Division_Word"
     "Word_Lib.More_Word_Operations"
-    Sshiftr
+    "Word_Lib.Reversed_Bit_Lists"
 begin
 
 lemma mult_inv_le: "(a::int) < 0 \<Longrightarrow> b \<ge> 0 \<Longrightarrow> a * b \<le> -b"
@@ -423,7 +423,7 @@ proof -
     hence sgn: "sgn a = sgn b" using of_int_0_le_iff of_int_le_0_iff by fastforce
     hence "a sdiv b = \<lfloor>rat_of_int a / rat_of_int b\<rfloor>"
       unfolding signed_divide_int_def
-      by (simp add: div_eq_sgn_abs floor_divide_of_int_eq)
+      by (auto simp add: div_eq_sgn_abs floor_divide_of_int_eq)
     thus ?thesis unfolding trunc using True by simp
   next
     case False