--- a/src/HOL/IMP/Abs_Int0.thy Sat Apr 20 19:30:04 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Sat Apr 20 20:57:49 2013 +0200
@@ -102,7 +102,7 @@
by(simp add: bot_def)
-subsubsection "Post-fixed point iteration"
+subsubsection "Pre-fixpoint iteration"
definition pfp :: "(('a::order) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
"pfp f = while_option (\<lambda>x. \<not> f x \<le> x) f"
@@ -171,6 +171,9 @@
definition "step' = Step fa (\<lambda>b S. S)"
+lemma strip_step'[simp]: "strip(step' S C) = strip C"
+by(simp add: step'_def)
+
definition AI :: "com \<Rightarrow> 'av st option acom option" where
"AI c = pfp (step' \<top>) (bot c)"
@@ -257,6 +260,223 @@
by(rule mono2_Step)
(auto simp: mono_update mono_aval' fa_def split: option.split)
+lemma mono_step'_top: "C \<le> C' \<Longrightarrow> step' \<top> C \<le> step' \<top> C'"
+by (metis mono_step' order_refl)
+
+lemma AI_least_pfp: assumes "AI c = Some C" "step' \<top> C' \<le> C'" "strip C' = c"
+shows "C \<le> C'"
+by(rule pfp_bot_least[OF _ _ assms(2,3) assms(1)[unfolded AI_def]])
+ (simp_all add: mono_step'_top)
+
+end
+
+
+instantiation acom :: (type) vars
+begin
+
+definition "vars_acom = vars o strip"
+
+instance ..
+
+end
+
+lemma finite_Cvars: "finite(vars(C::'a acom))"
+by(simp add: vars_acom_def)
+
+
+subsubsection "Termination"
+
+lemma pfp_termination:
+fixes x0 :: "'a::order" and m :: "'a \<Rightarrow> nat"
+assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x < y \<Longrightarrow> m x > m y"
+and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<le> f x0"
+shows "\<exists>x. pfp f x0 = Some x"
+proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<le> f x"])
+ show "wf {(y,x). ((I x \<and> x \<le> f x) \<and> \<not> f x \<le> x) \<and> y = f x}"
+ by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
+next
+ show "I x0 \<and> x0 \<le> f x0" using `I x0` `x0 \<le> f x0` by blast
+next
+ fix x assume "I x \<and> x \<le> f x" thus "I(f x) \<and> f x \<le> f(f x)"
+ by (blast intro: I mono)
+qed
+
+
+locale Measure1_fun =
+fixes m :: "'av::{order,top} \<Rightarrow> nat"
+fixes h :: "nat"
+assumes h: "m x \<le> h"
+begin
+
+definition m_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("m\<^isub>s") where
+"m_s X S = (\<Sum> x \<in> X. m(S x))"
+
+lemma m_s_h: "finite X \<Longrightarrow> m_s X S \<le> h * card X"
+by(simp add: m_s_def) (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
+
+definition m_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
+"m_o X opt = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s X S)"
+
+lemma m_o_h: "finite X \<Longrightarrow> m_o X opt \<le> (h*card X + 1)"
+by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
+
+definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
+"m_c C = (\<Sum>i<size(annos C). m_o (vars C) (annos C ! i))"
+
+text{* Upper complexity bound: *}
+lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
+proof-
+ let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
+ have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))" by(simp add: m_c_def)
+ also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
+ apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
+ also have "\<dots> = ?a * (h * ?n + 1)" by simp
+ finally show ?thesis .
+qed
+
+end
+
+
+lemma le_iff_le_annos_zip: "C1 \<le> C2 \<longleftrightarrow>
+ (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<le> a2) \<and> strip C1 = strip C2"
+by(induct C1 C2 rule: less_eq_acom.induct) (auto simp: size_annos_same2)
+
+lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
+ strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
+by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
+
+
+text{* The predicates @{text "top_on_ty X a"} that follow describe that @{text a} is some object
+that maps all variables in @{text X} to @{term \<top>}.
+This is an important invariant for the termination proof where we argue that only
+the finitely many variables in the program change. That the others do not change
+follows because they remain @{term \<top>}. *}
+
+fun top_on_st :: "vname set \<Rightarrow> 'a::top st \<Rightarrow> bool" where
+"top_on_st X f = (\<forall>x\<in>X. f x = \<top>)"
+
+fun top_on_opt :: "vname set \<Rightarrow> 'a::top st option \<Rightarrow> bool" where
+"top_on_opt X (Some F) = top_on_st X F" |
+"top_on_opt X None = True"
+
+definition top_on_acom :: "vname set \<Rightarrow> 'a::top st option acom \<Rightarrow> bool" where
+"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on_opt X a)"
+
+lemma top_on_top: "top_on_opt X (\<top>::_ st option)"
+by(auto simp: top_option_def)
+
+lemma top_on_bot: "top_on_acom X (bot c)"
+by(auto simp add: top_on_acom_def bot_def)
+
+lemma top_on_post: "top_on_acom X C \<Longrightarrow> top_on_opt X (post C)"
+by(simp add: top_on_acom_def post_in_annos)
+
+lemma top_on_acom_simps:
+ "top_on_acom X (SKIP {Q}) = top_on_opt X Q"
+ "top_on_acom X (x ::= e {Q}) = top_on_opt X Q"
+ "top_on_acom X (C1;C2) = (top_on_acom X C1 \<and> top_on_acom X C2)"
+ "top_on_acom X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+ (top_on_opt X P1 \<and> top_on_acom X C1 \<and> top_on_opt X P2 \<and> top_on_acom X C2 \<and> top_on_opt X Q)"
+ "top_on_acom X ({I} WHILE b DO {P} C {Q}) =
+ (top_on_opt X I \<and> top_on_acom X C \<and> top_on_opt X P \<and> top_on_opt X Q)"
+by(auto simp add: top_on_acom_def)
+
+lemma top_on_sup:
+ "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2 \<Longrightarrow> top_on_opt X (o1 \<squnion> o2 :: _ st option)"
+apply(induction o1 o2 rule: sup_option.induct)
+apply(auto)
+done
+
+lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
+assumes "!!x e S. \<lbrakk>top_on_opt X S; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt X (f x e S)"
+ "!!b S. top_on_opt X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt X (g b S)"
+shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt X S; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (Step f g S C)"
+proof(induction C arbitrary: S)
+qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
+
+
+locale Measure_fun = Measure1_fun +
+assumes m2: "x < y \<Longrightarrow> m x > m y"
+begin
+
+lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
+by(auto simp: le_less m2)
+
+lemma m_s2_rep: assumes "finite(X)" and "S1 = S2 on -X" and "\<forall>x. S1 x \<le> S2 x" and "S1 \<noteq> S2"
+shows "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
+proof-
+ from assms(3) have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S2 x)" by (simp add: m1)
+ from assms(2,3,4) have "EX x:X. S1 x < S2 x"
+ by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
+ hence 2: "\<exists>x\<in>X. m(S1 x) > m(S2 x)" by (metis m2)
+ from setsum_strict_mono_ex1[OF `finite X` 1 2]
+ show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
+qed
+
+lemma m_s2: "finite(X) \<Longrightarrow> S1 = S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s X S1 > m_s X S2"
+apply(auto simp add: less_fun_def m_s_def)
+apply(simp add: m_s2_rep le_fun_def)
+done
+
+lemma m_o2: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
+ o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
+proof(induction o1 o2 rule: less_eq_option.induct)
+ case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
+next
+ case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h)
+next
+ case 3 thus ?case by (auto simp: less_option_def)
+qed
+
+lemma m_o1: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
+ o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
+by(auto simp: le_less m_o2)
+
+
+lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
+ C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
+proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
+ let ?X = "vars(strip C2)"
+ assume top: "top_on_acom (- vars(strip C2)) C1" "top_on_acom (- vars(strip C2)) C2"
+ and strip_eq: "strip C1 = strip C2"
+ and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
+ hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
+ apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
+ by (metis (lifting, no_types) finite_cvars m_o1 size_annos_same2)
+ fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
+ have topo1: "top_on_opt (- ?X) (annos C1 ! i)"
+ using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
+ have topo2: "top_on_opt (- ?X) (annos C2 ! i)"
+ using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
+ from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
+ by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
+ hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
+ show "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
+ < (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
+ apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
+qed
+
+end
+
+
+locale Abs_Int_fun_measure =
+ Abs_Int_fun_mono where \<gamma>=\<gamma> + Measure_fun where m=m
+ for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
+begin
+
+lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (step' \<top> C)"
+unfolding step'_def
+by(rule top_on_Step)
+ (auto simp add: top_option_def fa_def split: option.splits)
+
+lemma AI_Some_measure: "\<exists>C. AI c = Some C"
+unfolding AI_def
+apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on_acom (- vars C) C" and m="m_c"])
+apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
+apply(auto simp add: top_on_step' vars_acom_def)
+done
+
end
text{* Problem: not executable because of the comparison of abstract states,