Expand eval_bool; add a method word_eqI_solve.

A number of proofs begin with word_eqI followed by some similar steps,
suggesting a 'word_eqI_solve' proof method, which is implemented here.

Many of these steps are standard, however a tricky part is that constants of
type 'nat' which encode a particular number of bits must often be unfolded.
This was done by expanding the eval_bool machinery to add eval_int_nat, which
tries to evaluate ints and nats.

Testing eval_int_nat revealed the need to improve the code generator setup
somewhat. The Arch locale contains many of the relevant constants, and they are
given global names via requalify_const, but the code generator doesn't know
about them. Some tweaks make them available. I *think* this is safe for
arch_split, as long as the proofs that derive from them are true in each
architecture.

lib/Eval_Bool.thy

@@ -18,35 +18,60 @@ begin
 text {* The eval_bool method/simproc uses the code generator setup to
 reduce terms of boolean type to True or False. Reducing booleans to
 True or False is nearly always desirable, and is a fairly good heuristic
-for when to make use of definitions/code-equations. *}
+for when to make use of definitions/code-equations.
+
+Additional simprocs exist to reduce other types.
+*}
 
 ML {*
-structure Eval_Bool = struct
+structure Eval_Simproc = struct
 
 exception Failure
 
-fun eval ctxt ct = let
+fun mk_constname_tab ts = fold Term.add_const_names ts []
+  |> Symtab.make_set
+
+fun is_built_from tab t = case Term.strip_comb t of
+    (Const (cn, _), ts) => Symtab.defined tab cn
+        andalso forall (is_built_from tab) ts
+  | _ => false
+
+fun eval tab ctxt ct = let
     val t = Thm.term_of ct
     val _ = Term.fold_aterms (fn Free _ => raise Failure
       | Var _ => raise Failure | _ => ignore) t ()
-    val is_bool = member (op aconv) [@{term True}, @{term False}]
-    val _ = not (is_bool t) orelse raise Failure
+    val _ = not (is_built_from tab t) orelse raise Failure
     val ev = the (try (Code_Simp.dynamic_conv ctxt) ct)
-  in if is_bool (Thm.term_of (Thm.rhs_of ev))
+  in if is_built_from tab (Thm.term_of (Thm.rhs_of ev))
     then SOME ev else NONE end
   handle Failure => NONE | Option => NONE
 
-val simproc = Simplifier.make_simproc @{context} "eval_bool"
-  { lhss = [@{term "b :: bool"}], proc = K eval }
+val eval_bool = eval (mk_constname_tab [@{term "True"}, @{term "False"}])
+val eval_nat = eval (mk_constname_tab [@{term "Suc 0"}, @{term "Suc 1"},
+    @{term "Suc 9"}])
+val eval_int = eval (mk_constname_tab [@{term "0 :: int"}, @{term "1 :: int"},
+    @{term "18 :: int"}, @{term "(-9) :: int"}])
+
+val eval_bool_simproc = Simplifier.make_simproc @{context} "eval_bool"
+  { lhss = [@{term "b :: bool"}], proc = K eval_bool }
+val eval_nat_simproc = Simplifier.make_simproc @{context} "eval_nat"
+  { lhss = [@{term "n :: nat"}], proc = K eval_nat }
+val eval_int_simproc = Simplifier.make_simproc @{context} "eval_int"
+  { lhss = [@{term "i :: int"}], proc = K eval_int }
 
 end
 *}
 
 method_setup eval_bool = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD'
-    (CHANGED o simp_tac (clear_simpset ctxt
-        addsimprocs [Eval_Bool.simproc])))\<close>
+    (CHANGED o full_simp_tac (clear_simpset ctxt
+        addsimprocs [Eval_Simproc.eval_bool_simproc])))\<close>
     "use code generator setup to simplify booleans in goals to True or False"
 
+method_setup eval_int_nat = \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD'
+    (CHANGED o full_simp_tac (clear_simpset ctxt
+        addsimprocs [Eval_Simproc.eval_nat_simproc, Eval_Simproc.eval_int_simproc])))\<close>
+    "use code generator setup to simplify nats and ints in goals to values"
+
 add_try_method eval_bool
 
 text {* Testing. *}
@@ -60,4 +85,51 @@ lemma
     \<and> sorted eval_bool_test_seq"
   by eval_bool
 
-end
+text {*
+A related gadget for installing constant definitions from locales
+as code equations. Useful where locales are being used to "hide"
+constants from the global state rather than to do anything tricky
+with interpretations.
+
+Installing the global definitions in this way will allow eval_bool
+etc to "see through" the hiding and decide questions about these
+constants.
+*}
+
+ML {*
+structure Add_Locale_Code_Defs = struct
+
+fun get_const_defs thy nm = Sign.consts_of thy
+  |> Consts.dest |> #constants
+  |> map fst
+  |> filter (fn s => case Long_Name.explode s of
+        [_, nm', _] => nm' = nm | _ => false)
+  |> map_filter (try (suffix "_def" #> Global_Theory.get_thm thy))
+
+fun setup nm thy = fold (fn t => Code.add_eqn_global (t, true))
+    (get_const_defs thy nm) thy
+
+end
+*}
+
+locale eval_bool_test_locale begin
+
+definition
+  "x == (12 :: int)"
+
+definition
+  "y == (13 :: int)"
+
+definition
+  "z = (x * y) + x + y"
+
+end
+
+setup {* Add_Locale_Code_Defs.setup "eval_bool_test_locale" *}
+
+setup {* Add_Locale_Code_Defs.setup "eval_bool_test_locale" *}
+
+lemma "eval_bool_test_locale.z > 150"
+  by eval_bool
+
+end

lib/HaskellLemmaBucket.thy

@@ -307,4 +307,25 @@ lemma findM_is_mapME:
   apply (simp add: liftE_bindE bind_assoc throwError_bind)
   done
 
+text {* Some word equalities can be solved by considering the
+problem bitwise.
+
+This is proven for all n < len_of TYPE ('a), which is different to
+running word_bitwise and expanding into an explicit list of bits.
+*}
+
+lemmas word_eqI_solve_simps = word_and_le1 word_or_zero le_word_or2
+  shiftL_nat word_FF_is_mask word_1FF_is_mask neg_mask_bang nth_ucast
+  linorder_not_less word_size minus_one_norm word_ops_nth_size
+  is_aligned_nth nth_w2p nth_shiftl nth_shiftr conj_comms
+  less_2p_is_upper_bits_unset
+
+method word_eqI_solve = solves \<open>rule word_eqI;
+  clarsimp simp: word_eqI_solve_simps;
+  (eval_int_nat; clarsimp simp: word_eqI_solve_simps)?;
+  fastforce simp: mask_def
+\<close>
+
+add_try_method word_eqI_solve
+
 end

lib/Word_Lib/Word_Lemmas.thy

@@ -2157,6 +2157,10 @@ lemma word_FF_is_mask:
   "0xFF = mask 8"
   by (simp add: mask_def)
 
+lemma word_1FF_is_mask:
+  "0x1FF = mask 9"
+  by (simp add: mask_def)
+
 lemma ucast_of_nat_small:
   "x < 2 ^ len_of TYPE('a) \<Longrightarrow> ucast (of_nat x :: 'a :: len word) = (of_nat x :: 'b :: len word)"
   apply (rule sym, subst word_unat.inverse_norm)
@@ -4727,6 +4731,14 @@ lemma upper_bits_unset_is_l2p:
   apply (drule word_power_increasing; simp add: word_len_min_2[simplified])
   done
 
+lemma less_2p_is_upper_bits_unset:
+  "((p::'a::len word) < 2 ^ n)
+    = (n < len_of TYPE('a) \<and> (\<forall>n' \<ge> n. n' < len_of TYPE('a) \<longrightarrow> \<not> p !! n'))"
+  apply (cases "n < len_of TYPE('a)")
+   apply (simp add: upper_bits_unset_is_l2p)
+  apply (simp add: power_overflow)
+  done
+
 lemma le_2p_upper_bits:
   "\<lbrakk> (p::'a::len word) \<le> 2^n - 1; n < len_of TYPE('a) \<rbrakk> \<Longrightarrow>
   \<forall>n'\<ge>n. n' < len_of TYPE('a) \<longrightarrow> \<not> p !! n'"

lib/Word_Lib/Word_Setup_32.thy

@@ -24,7 +24,7 @@ definition
   word_size :: "'a :: numeral" where
   "word_size \<equiv> 4"
 
-lemma word_bits_conv:
+lemma word_bits_conv[code]:
   "word_bits = 32" unfolding word_bits_def by simp
 
 lemma word_bits_word_size_conv:

lib/Word_Lib/Word_Setup_64.thy

@@ -24,7 +24,7 @@ definition
   word_size :: "'a :: numeral" where
   "word_size \<equiv> 8"
 
-lemma word_bits_conv:
+lemma word_bits_conv[code]:
   "word_bits = 64" unfolding word_bits_def by simp
 
 lemma word_bits_word_size_conv:

proof/invariant-abstract/ARM/ArchAcc_AI.thy

@@ -17,7 +17,6 @@ imports "../SubMonad_AI"
  "../../../lib/Crunch"
 begin
 
-
 context Arch begin global_naming ARM
 
 
@@ -306,21 +305,17 @@ crunch inv[wp]: get_master_pde P
 
 lemma ucast_mask_asid_low_bits [simp]:
   "ucast ((asid::word32) && mask asid_low_bits) = (ucast asid :: 10 word)"
-  apply (rule word_eqI)
-  apply (simp add: word_size nth_ucast asid_low_bits_def)
-  done
+  by word_eqI_solve
 
 
 lemma ucast_ucast_asid_high_bits [simp]:
   "ucast (ucast (asid_high_bits_of asid)::word32) = asid_high_bits_of asid"
-  apply (rule word_eqI)
-  apply (simp add: word_size nth_ucast asid_low_bits_def)
-  done
+  by word_eqI_solve
 
 
 lemma mask_asid_low_bits_ucast_ucast:
   "((asid::word32) && mask asid_low_bits) = ucast (ucast asid :: 10 word)"
-  by (rule word_eqI) (simp add: word_size nth_ucast asid_low_bits_def)
+  by word_eqI_solve
 
 
 lemma set_asid_pool_cur [wp]:
@@ -391,8 +386,7 @@ lemma pde_at_aligned_vptr:
     apply (rule shiftl_less_t2n)
      apply (rule shiftr_less_t2n')
       apply (simp add: pd_bits_def pageBits_def)
-      apply (rule word_eqI)
-      apply (simp add: word_size)
+      apply word_eqI_solve
      by (simp add: pd_bits_def pageBits_def)+
   apply simp
   done

proof/invariant-abstract/ARM/ArchInvariants_AI.thy

@@ -2373,4 +2373,8 @@ lemma valid_arch_tcb_lift:
   by (wp hoare_vcg_all_lift hoare_vcg_imp_lift; simp)
 
 end
+
+setup {* Add_Locale_Code_Defs.setup "ARM" *}
+setup {* Add_Locale_Code_Defs.setup "ARM_A" *}
+
 end

proof/invariant-abstract/ARM_HYP/ArchInvariants_AI.thy

@@ -2490,4 +2490,7 @@ lemma valid_arch_tcb_lift:
 
 end
 
+setup {* Add_Locale_Code_Defs.setup "ARM" *}
+setup {* Add_Locale_Code_Defs.setup "ARM_A" *}
+
 end

proof/invariant-abstract/Detype_AI.thy

@@ -1162,12 +1162,10 @@ lemma range_cover_plus_us:
 lemma mask_sub: "n \<le> m \<Longrightarrow> mask m - mask n = mask m && ~~ mask n"
   apply (simp add: field_simps)
   apply (subst word_plus_and_or_coroll)
-   apply (rule word_eqI,simp add:word_ops_nth_size)
-  apply (rule word_eqI, simp add: word_ops_nth_size word_size)
-  apply auto
+   apply word_eqI_solve
+  apply word_eqI_solve
   done
 
-
 lemma  neg_mask_diff_bound:
   "sz'\<le> sz \<Longrightarrow>(ptr && ~~ mask sz') - (ptr && ~~ mask sz) \<le> 2 ^ sz - 2 ^ sz'"
   (is "_ \<Longrightarrow> ?lhs \<le> ?rhs")
@@ -1177,9 +1175,8 @@ proof -
     apply (simp add: mask_out_sub_mask field_simps mask_and_mask min.absorb2)
     apply (simp add: mask_sub)
     apply (subst word_plus_and_or_coroll)
-     apply (rule word_eqI, simp add: word_size word_ops_nth_size)
-    apply (rule word_eqI, simp add: word_size word_ops_nth_size)
-    apply auto
+     apply word_eqI_solve
+    apply word_eqI_solve
     done
   also have "\<dots> \<le> ?rhs" using lt
     apply (simp add: mask_sub[symmetric])

proof/invariant-abstract/X64/ArchInvariants_AI.thy

@@ -3252,4 +3252,7 @@ lemma valid_arch_tcb_lift:
 
 end
 
+setup {* Add_Locale_Code_Defs.setup "X64" *}
+setup {* Add_Locale_Code_Defs.setup "X64_A" *}
+
 end