fixed up some proof and made it so that it doesn't break when generat…

…ing a latex document of the proofs
Cheunglo · Jan 3, 2020 · d5c3057 · d5c3057
1 parent bd05b51
commit d5c3057
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 23 deletions.
diff --git a/WordArraySpec.thy b/WordArraySpec.thy
@@ -20,7 +20,7 @@ lemma take_drop_Suc:
   apply clarsimp
   by (metis Cons_nth_drop_Suc Suc_diff_Suc take_Suc_Cons)
 
-section \<open> wordarray_length specification \<close>
+section \<open> wordarray\_length specification \<close>
 
 definition w_length :: "u32 list \<Rightarrow> nat"
   where
@@ -32,7 +32,7 @@ lemma w_length_length_eq:
   "w_length xs = length xs"
   by (simp add: w_length_def)
 
-section \<open> wordarray_get specification \<close>
+section \<open> wordarray\_get specification \<close>
 
 definition w_get :: "u32 list \<Rightarrow> nat \<Rightarrow> u32"
   where
@@ -44,7 +44,7 @@ lemma w_get_get_eq:
   "i < length xs \<Longrightarrow> w_get xs i = xs ! i"
   by (simp add: w_get_def)
 
-section \<open> wordarray_put2 specification \<close>
+section \<open> wordarray\_put2 specification \<close>
 
 definition w_put :: "u32 list \<Rightarrow> nat \<Rightarrow> 
                       u32 \<Rightarrow> u32 list"
@@ -57,7 +57,7 @@ lemma w_put_listupdate_eq:
   "w_put xs i v= xs[i := v]"
   by (simp add: w_put_def)
 
-section \<open> wordarray_fold_no_break specification \<close>
+section \<open> wordarray\_fold\_no\_break specification \<close>
 
 definition w_fold :: "u32 list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (u32 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'a) \<Rightarrow> 
                       'a \<Rightarrow> 'b \<Rightarrow> 'a"
@@ -69,7 +69,7 @@ definition w_fold :: "u32 list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
     fold (\<lambda>x y. f x y obs)  
     (take (to - frm) (drop frm w)) acc)"
 
-subsection \<open>w_fold helper lemmas \<close>
+subsection \<open>w\_fold helper lemmas \<close>
 
 lemma w_fold_step: "\<lbrakk>frm < length xs; frm < to\<rbrakk> \<Longrightarrow>
   w_fold xs frm to f acc obsv = w_fold xs (Suc frm) to f (f (xs ! frm) acc obsv) obsv"
@@ -91,7 +91,7 @@ lemma w_fold_end:
   apply (simp add: w_fold_def)
   done
 
-subsection \<open> w_fold test \<close>
+subsection \<open> w\_fold test \<close>
 
 primrec summer :: "u32 \<Rightarrow> u32 \<Rightarrow> unit \<Rightarrow> u32" where
 "summer elem acc () = elem + acc"
@@ -110,7 +110,7 @@ lemma w_fold_fold_eq_slice:
   apply (simp add: w_fold_def)
   done
 
-section \<open> wordarray_fold specification \<close>
+section \<open> wordarray\_fold specification \<close>
 definition w_fold_break :: "u32 list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
                             (u32 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a, 'c) LoopResult ) \<Rightarrow> 
                             'a \<Rightarrow> 'b \<Rightarrow> ('a, 'c) LoopResult"
@@ -125,7 +125,7 @@ definition w_fold_break :: "u32 list \<Rightarrow> nat \<Rightarrow> nat \<Right
     (take (to - frm) (drop frm w)) (Iterate acc))"
 
 
-section \<open> wordarray_map_no_break specification \<close>
+section \<open> wordarray\_map\_no\_break specification \<close>
 
 definition w_map :: "u32 list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> (u32 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> u32 \<times> 'a) \<Rightarrow> 
                       'a \<Rightarrow> 'b \<Rightarrow> u32 list \<times> 'a"
@@ -141,7 +141,7 @@ definition w_map :: "u32 list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
         (take (to - frm) (drop frm w)) ([], acc)
      in ((take frm w) @ ys @ (drop to w), vacc))"
 
-subsection \<open> w_map helper lemmas \<close>
+subsection \<open> w\_map helper lemmas \<close>
 
 lemma w_map_bounds: 
   "to \<ge> length xs \<Longrightarrow> w_map xs frm to f acc obsv = w_map xs frm (length xs) f acc obsv"
@@ -346,7 +346,7 @@ lemma w_map_map_eq_whole:
   apply simp
   done
 
-section \<open> wordarray_map specification \<close>
+section \<open> wordarray\_map specification \<close>
 
 definition w_map_break :: "u32 list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
                       (u32 \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> (u32 \<times> 'a, 'c) LoopResult) \<Rightarrow> 

diff --git a/WordArrayT.thy b/WordArrayT.thy
@@ -91,9 +91,9 @@ lemmas frame_weaken = frame_weaken_w32 frame_weaken_w32_ptr
 
 lemmas frame_combine = frame_combine_w32 frame_combine_w32_ptr
 
-section \<open> Helper things \<close>
+section \<open> Helper Lemmas \<close>
 
-subsection \<open> misc pointer lemmas \<close>
+subsection \<open> Miscellaneous Pointer Lemmas \<close>
 
 lemma cptr_add_add[simp]:
   "p +\<^sub>p m +\<^sub>p n = p +\<^sub>p (m + n)"
@@ -156,7 +156,7 @@ lemma distinct_indices:
   apply (case_tac "n < m")
    apply (erule order_indices; clarsimp)
   by (metis linorder_neqE_nat order_indices)
-find_theorems "?a + ?b = ?a + ?c"
+
 subsection \<open> arrlist \<close>
 
 fun arrlist :: "('a :: c_type ptr \<Rightarrow> 'b) \<Rightarrow> ('a :: c_type ptr \<Rightarrow> bool) \<Rightarrow> 'b list \<Rightarrow> 'a ptr \<Rightarrow> bool"
@@ -234,7 +234,7 @@ lemma arrlist_all_nth:
   apply (erule to_arrlist)
   done
 
-section \<open> Word array abstraction \<close>
+section \<open> Word Array Abstraction \<close>
 
 definition u32list :: "lifted_globals \<Rightarrow> u32 list \<Rightarrow> u32 ptr \<Rightarrow> bool" 
   where
@@ -292,9 +292,9 @@ lemma \<alpha>_all_nth:
   apply (clarsimp simp: \<alpha>_def u32list_all_nth)
   done
 
-section \<open> refinement and frame proofs \<close>
+section \<open> Refinement and Frame Proofs \<close>
 
-subsection \<open> wordarray_get \<close>
+subsection \<open> wordarray\_get \<close>
 
 lemma wordarray_get_refinement:
   "\<lbrace>\<lambda>s. \<alpha> s xs w \<rbrace>
@@ -320,7 +320,7 @@ lemma wordarray_get_frame:
   apply (simp add: \<alpha>_def)
   done
 
-subsection \<open> wordarray_length \<close>
+subsection \<open> wordarray\_length \<close>
 
 lemma wordarray_length_refinement:
   "\<lbrace>\<lambda>s. \<alpha> s xs w\<rbrace>
@@ -344,7 +344,7 @@ lemma wordarray_length_frame:
   apply (clarsimp simp: frame_triv \<alpha>_def)
   done
 
-subsection \<open> wordarray_put2 \<close>
+subsection \<open> wordarray\_put2 \<close>
 
 lemma wordarray_same_address: 
   "\<lbrakk>\<alpha> s xs w; n < length xs; m < length xs\<rbrakk> \<Longrightarrow>
@@ -410,17 +410,17 @@ lemma wordarray_put_no_fail:
    apply (metis (full_types) \<alpha>_def int_unat u32list_all_nth w_length_def)
   by (simp add: word_less_nat_alt)
 
-subsection \<open> wordarray_fold_no_break \<close>
+subsection \<open> wordarray\_fold\_no\_break \<close>
 
 fun fold_dispatch :: "int \<Rightarrow> t3_C \<Rightarrow> word32"
   where
   "fold_dispatch n args = (if n = sint FUN_ENUM_mul_bod 
-                           then t3_C.acc_C args * t3_C.elem_C args 
-                           else t3_C.acc_C args + t3_C.elem_C args)"
+                           then t3_C.elem_C args * t3_C.acc_C args 
+                           else t3_C.elem_C args + t3_C.acc_C args)"
 
 definition f_n
   where  
-  "f_n \<equiv> (\<lambda>n a1 a2 a3. fold_dispatch (sint n) (t3_C a1 a2 a3))"
+  "f_n \<equiv> (\<lambda>n a1 a2 a3. fold_dispatch (sint n) (t3_C a2 a1 a3))"
 
 lemma unat_min: 
   "unat (min a b) = min (unat a) (unat b)"
@@ -529,7 +529,7 @@ lemma wordarray_fold_frame:
   done
 
 
-subsection \<open>wordarray_map\<close>
+subsection \<open> wordarray\_map\_no\_break \<close>
 
 
 fun map_dispatch :: "int \<Rightarrow> t6_C \<Rightarrow> word32 \<times> unit_t_C"