It works \o/

Author: thestr4ng3r

Uppaal_Networks/AbsInt/AbsInt.thy

@@ -409,7 +409,7 @@ proof -
   from step_le this show ?thesis by force
 qed
 
-definition[simp, code]: "ai_loop \<equiv> finite_loop ai_step"
+definition[simp]: "ai_loop \<equiv> finite_loop ai_step"
 
 theorem ai_loop_correct: "collect_loop prog n (\<gamma>_map entry) \<le> \<gamma>_map (ai_loop prog n entry)"
 proof (induction n arbitrary: entry)
@@ -423,7 +423,7 @@ next
   thus ?case by simp
 qed
 
-definition[simp, code]: "ai_loop_fp \<equiv> finite_loop_fp ai_step"
+definition[simp]: "ai_loop_fp \<equiv> finite_loop_fp ai_step"
 
 theorem ai_loop_fp_correct: "collect_loop prog m (\<gamma>_map entry) \<le> \<gamma>_map (ai_loop_fp prog n entry)"
   by (metis (no_types, lifting) \<gamma>_map_mono ai_loop_correct ai_loop_def ai_loop_fp_def finite_loop_fp_supercomplete le_iff_sup le_sup_iff)

Uppaal_Networks/AbsInt/AbsInt_Final.thy

@@ -22,6 +22,16 @@ global_interpretation Abs_Int_Final: Smart_Base
     and \<gamma>_stack = "\<gamma>_stack_window n \<gamma>_word"
     and push = "push_stack_window n"
     and pop = "pop_stack_window n"
+  defines "final_step_base" = "Abs_Int_Final.step_smart_base"
+    and "final_step" = "Abs_Int_Final.step_smart"
+    and "final_astore_singleton" = "Abs_Int_Final.astore_singleton"
+    and "final_astore_multi" = "Abs_Int_Final.astore_multi"
+    and "final_astore" = "Abs_Int_Final.astore"
+    and "final_load" = "Abs_Int_Final.load"
+    and "final_cmp_op" = "Abs_Int_Final.cmp_op"
+    and "final_pop2" = "Abs_Int_Final.pop2"
+    and "final_pop2_push" = "Abs_Int_Final.pop2_push"
+    and "final_word_of" = "Abs_Int_Final.word_of"
 proof(standard, goal_cases)
   case (1 a b) then show ?case by (simp add: Word_Strided_Interval.mono_gamma) next
   case (3 a x) then show ?case by (simp add: Word_Strided_Interval.contains_correct) next
@@ -37,11 +47,10 @@ proof(standard, goal_cases)
   case (15 cx c b) then show ?case by (simp add: Word_Strided_Interval.mono_gamma window_pop_correct(2))
 qed auto
 
-definition[simp, code]: "final_loop_fp \<equiv> finite_loop_fp Abs_Int_Final.step_smart"
-theorem ai_loop_fp_correct: "collect_loop prog m (Abs_Int_Final.Smart.\<gamma>_map entry) \<le> Abs_Int_Final.Smart.\<gamma>_map (final_loop_fp prog n entry)" using Abs_Int_Final.Smart.ai_loop_fp_correct by simp
+definition[simp]: "final_loop_fp \<equiv> finite_loop_fp final_step"
+theorem ai_loop_fp_correct: "collect_loop prog m (Abs_Int_Final.Smart.\<gamma>_map entry) \<le> Abs_Int_Final.Smart.\<gamma>_map (final_loop_fp prog n entry)"
+  using Abs_Int_Final.Smart.ai_loop_fp_correct by simp
 
-lemma[code]: "HOL.equal (SM a) (SM b) = False" sorry
-
-export_code final_loop_fp in SML
+export_code final_loop_fp in SML module_name AbsInt_Final
 
 end

Uppaal_Networks/AbsInt/AbsInt_Refine.thy

@@ -56,7 +56,7 @@ code_datatype RSM RSMS
 definition "r_empty_map \<equiv> Mapping.empty::('a::bot) r_state_map"
 
 lemma r_bot[code]: "\<bottom> = RSM r_empty_map"
-  by (rule lookup_eq; simp add: lookup_default_empty r_empty_map_def)
+  by (rule state_map_eq_fwd; simp add: lookup_default_empty r_empty_map_def)
 
 lemma r_top[code]: "\<top> = RSMS SMTop" by simp
 
@@ -68,7 +68,7 @@ fun r_single :: "addr \<Rightarrow> 'a::absstate \<Rightarrow> 'a r_state_map" w
   "r_single k v = Mapping.update k v \<bottom>"
 
 lemma r_single[code]: "single k v = RSM (r_single k v)"
-  by (rule lookup_eq; simp add: bot_mapping_def lookup_default_empty lookup_default_update')
+  by (rule state_map_eq_fwd; simp add: bot_mapping_def lookup_default_empty lookup_default_update')
 
 lemma single_lookup: "lookup (single k v) k = v" by simp
 
@@ -117,7 +117,7 @@ proof -
 qed
 
 lemma r_merge_single[code]: "merge_single (RSM m) pc x = RSM (r_merge_single m pc x)"
-proof(rule lookup_eq)
+proof(rule state_map_eq_fwd)
   obtain mm where func: "RSM m = SM mm" using state_map_single_constructor by blast
   have "(if k = pc then x \<squnion> mm k else mm k) = lookup (RSM (r_merge_single m pc x)) k" for k
   proof(cases "k = pc")
@@ -462,7 +462,7 @@ proof (rule ccontr)
   from this obtain infpc where infpc: "infinite (slurp f prog ctx infpc)" by blast
   let ?slurpset = "{ost. \<exists>ipc op. prog ipc = Some op \<and> lookup ctx ipc \<noteq> \<bottom> \<and> lookup (f op ipc (lookup ctx ipc)) infpc = ost}"
   let ?aset = "{ipc. lookup ctx ipc \<noteq> \<bottom>}"
-  from assms(1) have finite_lookup: "finite ?aset" by (metis (full_types) domain.simps lookup.simps lookup_eq)
+  from assms(1) have finite_lookup: "finite ?aset" by (metis (full_types) domain.simps lookup.simps state_map_eq_fwd)
   let ?magic = "\<lambda>ipc. case prog ipc of None \<Rightarrow> None | Some op \<Rightarrow> Some (lookup (f op ipc (lookup ctx ipc)) infpc)"
   let ?youbet = "List.map_project ?magic ?aset"
   from finite_lookup have finite: "finite ?youbet" using map_project_finite by blast
@@ -483,7 +483,7 @@ proof (rule ccontr)
 qed
 
 lemma[code]: "finite_step_map (f::('a::absstate) astep) prog (RSM (Mapping tree)) = r_step_map f prog (RSM (Mapping tree))"
-proof(rule lookup_eq)
+proof(rule state_map_eq_fwd)
   fix pc
   let ?ctx = "RSM (Mapping tree)"
   let ?smf = "r_step_map_from f prog ?ctx"
@@ -605,6 +605,24 @@ proof (cases "finite_advance f prog st = \<top>")
   qed simp
 qed simp
 
+text\<open>Equality over state sets, necessary for ai_loop_fp\<close>
+
+lemma state_map_HOL_equal: "HOL.equal a b \<longleftrightarrow> (\<forall>k. lookup a k = lookup b k)"
+proof -
+  have "HOL.equal a b \<longleftrightarrow> a = b" by (rule HOL.equal_eq)
+  thus ?thesis using state_map_eq by blast
+qed
+
+lemma[code]: "HOL.equal (RSM a) (RSM b) \<longleftrightarrow> (\<forall>k \<in> (r_domain a \<union> r_domain b). r_lookup a k = r_lookup b k)"
+proof -
+  have "(\<forall>k. lookup (RSM a) k = lookup (RSM b) k) \<longleftrightarrow> (\<forall>k \<in> (r_domain a \<union> r_domain b). r_lookup a k = r_lookup b k)"
+    by (metis (mono_tags, lifting) UnI1 UnI2 mem_Collect_eq r_domain r_lookup)
+  moreover have "equal_class.equal (RSM a) (RSM b) = (\<forall>k. lookup (RSM a) k = lookup (RSM b) k)" by (rule state_map_HOL_equal)
+  ultimately show ?thesis by simp
+qed
+
+lemma[code]: "HOL.equal SMTop SMTop = True" by (rule HOL.equal_class.equal_refl)
+
 subsection \<open>Helper Refinement\<close>
 
 fun r_deep_merge_l :: "(addr * ('a::absstate)) list \<Rightarrow> 'a r_state_map \<Rightarrow> 'a r_state_map" where
@@ -683,6 +701,29 @@ proof -
   thus ?thesis by simp
 qed
 
+fun list_is_singleton :: "'a list \<Rightarrow> bool" where
+  "list_is_singleton [] = False" |
+  "list_is_singleton [_] = True" |
+  "list_is_singleton (x # y # r) = (x = y \<and> list_is_singleton (y # r))"
+
+lemma[code]: "is_singleton (set a) = list_is_singleton a"
+proof (induction a)
+  case Nil
+  then show ?case
+    by (simp add: is_singleton_def)
+next
+  case (Cons x yr)
+  then show ?case
+  proof (cases yr)
+    case Nil
+    then show ?thesis by simp
+  next
+    fix y r assume "yr = y # r"
+    then show ?thesis
+      by (metis empty_iff insert_absorb2 insert_iff is_singleton_the_elem list.simps(15) list_is_singleton.simps(3) local.Cons)
+  qed
+qed
+
 (***********)
 
 value "

Uppaal_Networks/AbsInt/AbsInt_Test.thy

@@ -1,11 +1,8 @@
 theory AbsInt_Test
   imports
     "HOL.String"
-    AbsInt_Refine
     Uppaal_Networks.UPPAAL_Asm_Show
-    Word_StridedInterval
-    Stack_Direct
-    State_Smart
+    AbsInt_Final
 begin
 
 instantiation toption :: ("show") "show"
@@ -84,11 +81,11 @@ definition "dumb_result \<equiv>
 definition "abs_res_str \<equiv> String.implode (show (DisplayCtx myprog dumb_result))"
 (*ML \<open>val _ = writeln (@{code abs_res_str})\<close>*)
 
-type_synonym si_state = "(strided_interval toption option, strided_interval toption option stack_direct) smart state_map"
+type_synonym si_state = "(strided_interval toption option, strided_interval toption option stack_window) smart state_map"
 
 definition "set_entry \<equiv> (merge_single \<bottom> 0 (Some (Smart \<bottom> \<bottom> BFalse)))::si_state"
-definition "set_result \<equiv> undefined (fetch_op myprog) 3 set_entry"
-definition "set_res_str \<equiv> String.implode (show (DisplayCtx myprog set_entry))"
+definition "set_result \<equiv> final_loop_fp (fetch_op myprog) 100 set_entry"
+definition "set_res_str \<equiv> String.implode (show (DisplayCtx myprog set_result))"
 ML \<open>val _ = writeln (@{code set_res_str})\<close>
 
 

Uppaal_Networks/AbsInt/Stack.thy

@@ -14,44 +14,5 @@ locale Abs_Stack =
   and push_correct: "c \<in> \<gamma>_stack b \<Longrightarrow> cx \<in> \<gamma>_word x \<Longrightarrow> (cx # c) \<in> \<gamma>_stack (push b x)"
   and pop_stack_correct:  "(cx # c) \<in> \<gamma>_stack b \<Longrightarrow> c \<in> \<gamma>_stack (snd (pop b))"
   and pop_return_correct: "(cx # c) \<in> \<gamma>_stack b \<Longrightarrow> cx \<in> \<gamma>_word (fst (pop b))"
-begin
-
-fun pop2 :: "'b \<Rightarrow> ('a * 'a * 'b)" where
-  "pop2 stack =
-    (let (a, astack) = pop stack;
-         (b, bstack) = pop astack
-    in (a, b, bstack))"
-lemma pop2_stack_correct: "(ca # cb # c) \<in> \<gamma>_stack b \<Longrightarrow> c \<in> \<gamma>_stack (snd (snd (pop2 b)))"
-  by (metis (no_types, lifting) Pair_inject case_prod_beta' pop2.elims pop_stack_correct prod.exhaust_sel)
-
-lemma pop2_return_b_correct: "(ca # cb # c) \<in> \<gamma>_stack b \<Longrightarrow> cb \<in> \<gamma>_word (fst (snd (pop2 b)))"
-proof -
-  assume ass: "(ca # cb # c) \<in> \<gamma>_stack b"
-  hence i: "(cb # c) \<in> \<gamma>_stack (snd (pop b))" using pop_stack_correct by simp
-  have "snd (pop2 b) = pop (snd (pop b))"
-    by (metis (no_types, lifting) case_prod_beta' pop2.elims prod.exhaust_sel snd_conv)
-  from this i show "cb \<in> \<gamma>_word (fst (snd (pop2 b)))" using pop_return_correct by auto
-qed
-
-lemma pop2_return_a_correct: "(ca # cb # c) \<in> \<gamma>_stack b \<Longrightarrow> ca \<in> \<gamma>_word (fst (pop2 b))"
-  by (metis (no_types, lifting) case_prod_beta' fst_conv pop2.elims pop_return_correct)
-
-fun pop2_push :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b" where
-  "pop2_push f stack =
-    (let (a, b, rstack) = pop2 stack
-    in push rstack (f a b))"
-
-lemma[simp]: "pop2_push f stack =
-  push (snd (snd (pop2 stack))) (f (fst (pop2 stack)) (fst (snd (pop2 stack))))"
-  by (simp add: case_prod_beta)
-
-lemma pop2_push:
-  assumes
-    "\<And>x y a b. x \<in> \<gamma>_word a \<Longrightarrow> y \<in> \<gamma>_word b \<Longrightarrow> (cop x y) \<in> \<gamma>_word (f a b)"
-    "a # b # rcstack \<in> \<gamma>_stack iastack"
-  shows "(cop a b) # rcstack \<in> \<gamma>_stack (pop2_push f iastack)"
-  apply (simp add: case_prod_beta Let_def)
-  using assms by (meson pop_return_correct pop_stack_correct push_correct)
-end
 
 end