Prove termination of new cut_memory

ContractSem.thy

@@ -365,4 +365,35 @@ done
 lemma program_sem_annotation_failure [simp] : "program_sem k con n InstructionAnnotationFailure = InstructionAnnotationFailure"
 by (induct_tac n; auto)
 
+lemma not_at_least_one :
+  "\<not> 1 \<le> (aa :: 256 word) \<Longrightarrow> aa = 0"
+apply(simp add:linorder_class.not_le)
+done
+
+lemma unat_suc : "unat (aa :: w256) = Suc n \<Longrightarrow> unat (aa - 1) = n"
+apply(case_tac "aa \<ge> 1")
+ apply(simp add: uint_minus_simple_alt)
+apply(drule not_at_least_one)
+apply(simp)
+done
+
+(* unat (1 + (aa - 1)) = Suc (unat(aa - 1)) *)
+
+
+lemma cut_memory_dom_nat :
+  "\<forall> a aa b. unat aa = n \<longrightarrow> cut_memory_dom (a, aa, b)"
+apply(induction n)
+ apply(clarify)
+ apply(rule cut_memory.domintros)
+ apply(simp add: unat_eq_0 uint_0_iff)
+apply(clarify)
+apply(rule cut_memory.domintros)
+apply(drule unat_suc)
+apply(auto)
+done
+
+termination cut_memory
+apply(auto simp add: cut_memory_dom_nat)
+done
+
 end

HoareTripleForInstructions.thy

@@ -1136,11 +1136,12 @@ lemma sep_ac:
  using sep_assoc by (simp add: sep_commute)
 
 lemma cut_memory_memory_range [simp] :
-  "\<forall> rest b. 
+  "\<forall> rest b n.
+   n = word_of_int (int (length lst)) \<longrightarrow>
    (memory_range b lst ** rest) (instruction_result_as_set c (InstructionContinue v))
-   \<longrightarrow> cut_memory b (length lst) (vctx_memory v) = lst"
+   \<longrightarrow> cut_memory b n (vctx_memory v) = lst"
 apply(induction lst)
- apply(simp add: cut_memory.simps sep_def)
+ apply(auto simp add: sep_def cut_memory.psimps)
 apply(auto)
 apply(drule_tac x = "memory8 b a ** rest" in spec)
 apply(drule_tac x = "b + 1" in spec)