# HG changeset patch
# User nipkow
# Date 1327846587 -3600
# Node ID 42a01315d9986d43c272251f771b7db0db9be926
# Parent  25f081f779158dfb0cfad5a237a25832af584f18
removed accidental dependance of abstract interpreter on gamma

diff -r 25f081f77915 -r 42a01315d998 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sun Jan 29 10:34:02 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Sun Jan 29 15:16:27 2012 +0100
@@ -150,7 +150,7 @@
 text{* ACC for option type: *}
 
 lemma acc_option: assumes "acc {(x,y::'a::preord). x \<sqsubseteq> y}"
-shows "acc {(x,y::'a option). x \<sqsubseteq> y}"
+shows "acc {(x,y::'a::preord option). x \<sqsubseteq> y}"
 proof(auto simp: wf_eq_minimal)
   fix xo :: "'a option" and Qo assume "xo : Qo"
   let ?Q = "{x. Some x \<in> Qo}"
@@ -195,8 +195,8 @@
 qed
 
 lemma measure_st: assumes "(strict{(x,y::'a::SL_top). x \<sqsubseteq> y})^-1 <= measure m"
-and "\<forall>x y::'a. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m x = m y"
-shows "(strict{(S,S'::'a st). S \<sqsubseteq> S'})^-1 \<subseteq>
+and "\<forall>x y::'a::SL_top. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m x = m y"
+shows "(strict{(S,S'::'a::SL_top st). S \<sqsubseteq> S'})^-1 \<subseteq>
   measure(%fd. \<Sum>x| x\<in>set(dom fd) \<and> ~ \<top> \<sqsubseteq> fun fd x. m(fun fd x)+1)"
 proof-
   { fix S S' :: "'a st" assume "S \<sqsubseteq> S'" "~ S' \<sqsubseteq> S"
diff -r 25f081f77915 -r 42a01315d998 src/HOL/IMP/Abs_Int0_const.thy
--- a/src/HOL/IMP/Abs_Int0_const.thy	Sun Jan 29 10:34:02 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy	Sun Jan 29 15:16:27 2012 +0100
@@ -69,7 +69,7 @@
 interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 defines AI_const is AI and step_const is step' and aval'_const is aval'
-proof qed
+..
 
 
 subsubsection "Tests"
diff -r 25f081f77915 -r 42a01315d998 src/HOL/IMP/Abs_Int0_parity.thy
--- a/src/HOL/IMP/Abs_Int0_parity.thy	Sun Jan 29 10:34:02 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_parity.thy	Sun Jan 29 15:16:27 2012 +0100
@@ -114,7 +114,7 @@
 interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 defines aval_parity is aval' and step_parity is step' and AI_parity is AI
-proof qed
+..
 
 
 subsubsection "Tests"
diff -r 25f081f77915 -r 42a01315d998 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Sun Jan 29 10:34:02 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Sun Jan 29 15:16:27 2012 +0100
@@ -77,14 +77,16 @@
 
 
 locale Val_abs1 =
- Val_abs1_gamma where \<gamma> = \<gamma>
- for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
-fixes filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
+  Val_abs1_gamma where \<gamma> = \<gamma>
+   for \<gamma> :: "'av::L_top_bot \<Rightarrow> val set" +
+fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
+and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
 and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
-assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
-  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
-and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
-  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> a1' \<and> n2 : \<gamma> a2'"
+assumes test_num': "test_num' n a = (n : \<gamma> a)"
+and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
+  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
+and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
+  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
 
 
 locale Abs_Int1 =
@@ -104,7 +106,7 @@
 subsubsection "Backward analysis"
 
 fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
-"afilter (N n) a S = (if n : \<gamma> a then S else None)" |
+"afilter (N n) a S = (if test_num' n a then S else None)" |
 "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
   let a' = lookup S x \<sqinter> a in
   if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
@@ -134,7 +136,7 @@
 
 lemma afilter_sound: "s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
 proof(induction e arbitrary: a S)
-  case N thus ?case by simp
+  case N thus ?case by simp (metis test_num')
 next
   case (V x)
   obtain S' where "S = Some S'" and "s : \<gamma>\<^isub>f S'" using `s : \<gamma>\<^isub>o S`
@@ -328,7 +330,7 @@
 
 lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
 apply(induction e arbitrary: r r' S S')
-apply(auto simp: Let_def split: option.splits prod.splits)
+apply(auto simp: test_num' Let_def split: option.splits prod.splits)
 apply (metis mono_gamma subsetD)
 apply(drule_tac x = "list" in mono_lookup)
 apply (metis mono_meet le_trans)
diff -r 25f081f77915 -r 42a01315d998 src/HOL/IMP/Abs_Int1_ivl.thy
--- a/src/HOL/IMP/Abs_Int1_ivl.thy	Sun Jan 29 10:34:02 2012 +0100
+++ b/src/HOL/IMP/Abs_Int1_ivl.thy	Sun Jan 29 15:16:27 2012 +0100
@@ -42,7 +42,7 @@
 "Some x + Some y = Some(x+y)" |
 "_ + _ = None"
 
-instance proof qed
+instance ..
 
 end
 
@@ -147,7 +147,7 @@
 "Some x - Some y = Some(x-y)" |
 "_ - _ = None"
 
-instance proof qed
+instance ..
 
 end
 
@@ -158,6 +158,7 @@
   "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(minus_ivl i1 i2)"
 by(auto simp add: minus_ivl_def \<gamma>_ivl_def split: ivl.splits option.splits)
 
+definition "test_num_ivl n ivl = contained_in ivl n"
 
 definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
   i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
@@ -205,32 +206,38 @@
 
 interpretation Val_abs1
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = test_num_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
   case goal1 thus ?case
+    by(auto simp add: test_num_ivl_def contained_in_def)
+next
+  case goal2 thus ?case
     by(auto simp add: filter_plus_ivl_def)
       (metis gamma_minus_ivl add_diff_cancel add_commute)+
 next
-  case goal2 thus ?case
+  case goal3 thus ?case
     by(cases a1, cases a2,
       auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
 interpretation Abs_Int1
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = test_num_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
 and step_ivl is step'
 and AI_ivl is AI
 and aval_ivl' is aval''
-proof qed
+..
 
 
 text{* Monotonicity: *}
 
 interpretation Abs_Int1_mono
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = test_num_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
   case goal1 thus ?case
@@ -247,38 +254,38 @@
 
 subsubsection "Tests"
 
-value [code] "show_acom_opt (AI_ivl test1_ivl)"
+value "show_acom_opt (AI_ivl test1_ivl)"
 
 text{* Better than @{text AI_const}: *}
-value [code] "show_acom_opt (AI_ivl test3_const)"
-value [code] "show_acom_opt (AI_ivl test4_const)"
-value [code] "show_acom_opt (AI_ivl test6_const)"
+value "show_acom_opt (AI_ivl test3_const)"
+value "show_acom_opt (AI_ivl test4_const)"
+value "show_acom_opt (AI_ivl test6_const)"
 
-value [code] "show_acom_opt (AI_ivl test2_ivl)"
-value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
+value "show_acom_opt (AI_ivl test2_ivl)"
+value "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test2_ivl))"
+value "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test2_ivl))"
+value "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test2_ivl))"
 
 text{* Fixed point reached in 2 steps. Not so if the start value of x is known: *}
 
-value [code] "show_acom_opt (AI_ivl test3_ivl)"
-value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
-value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom_opt (AI_ivl test3_ivl)"
+value "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
+value "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
 
 text{* Takes as many iterations as the actual execution. Would diverge if
 loop did not terminate. Worse still, as the following example shows: even if
 the actual execution terminates, the analysis may not. The value of y keeps
 decreasing as the analysis is iterated, no matter how long: *}
 
-value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
+value "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test4_ivl))"
 
 text{* Relationships between variables are NOT captured: *}
-value [code] "show_acom_opt (AI_ivl test5_ivl)"
+value "show_acom_opt (AI_ivl test5_ivl)"
 
 text{* Again, the analysis would not terminate: *}
-value [code] "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test6_ivl))"
+value "show_acom (((step_ivl \<top>)^^50) (\<bottom>\<^sub>c test6_ivl))"
 
 end
diff -r 25f081f77915 -r 42a01315d998 src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sun Jan 29 10:34:02 2012 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Sun Jan 29 15:16:27 2012 +0100
@@ -227,9 +227,10 @@
 
 interpretation Abs_Int2
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
+and test_num' = test_num_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 defines AI_ivl' is AI_wn
-proof qed
+..
 
 
 subsubsection "Tests"