--- a/src/HOL/IMP/Abs_Int0.thy Wed Jan 25 16:07:48 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy Thu Jan 26 09:52:47 2012 +0100
@@ -18,7 +18,7 @@
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
lemma aval'_sound: "s : \<gamma>\<^isub>f S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
-by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def lookup_def)
+by (induction a) (auto simp: gamma_num' gamma_plus' \<gamma>_st_def lookup_def)
end
@@ -58,8 +58,8 @@
function operating on states as functions. *}
lemma step_preserves_le:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; cs \<le> \<gamma>\<^isub>c ca \<rbrakk> \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' S' ca)"
-proof(induction cs arbitrary: ca S S')
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; c \<le> \<gamma>\<^isub>c c' \<rbrakk> \<Longrightarrow> step S c \<le> \<gamma>\<^isub>c (step' S' c')"
+proof(induction c arbitrary: c' S S')
case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
next
case Assign thus ?case
@@ -69,24 +69,24 @@
case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
by (metis le_post post_map_acom)
next
- case (If b cs1 cs2 P)
- then obtain ca1 ca2 Pa where
- "ca= IF b THEN ca1 ELSE ca2 {Pa}"
- "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+ case (If b c1 c2 P)
+ then obtain c1' c2' P' where
+ "c' = IF b THEN c1' ELSE c2' {P'}"
+ "P \<subseteq> \<gamma>\<^isub>o P'" "c1 \<le> \<gamma>\<^isub>c c1'" "c2 \<le> \<gamma>\<^isub>c c2'"
by (fastforce simp: If_le map_acom_If)
- moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
- moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
+ moreover have "post c1 \<subseteq> \<gamma>\<^isub>o(post c1' \<squnion> post c2')"
+ by (metis (no_types) `c1 \<le> \<gamma>\<^isub>c c1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+ moreover have "post c2 \<subseteq> \<gamma>\<^isub>o(post c1' \<squnion> post c2')"
+ by (metis (no_types) `c2 \<le> \<gamma>\<^isub>c c2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` by (simp add: If.IH subset_iff)
next
- case (While I b cs1 P)
- then obtain ca1 Ia Pa where
- "ca = {Ia} WHILE b DO ca1 {Pa}"
- "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+ case (While I b c1 P)
+ then obtain c1' I' P' where
+ "c' = {I'} WHILE b DO c1' {P'}"
+ "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "c1 \<le> \<gamma>\<^isub>c c1'"
by (fastforce simp: map_acom_While While_le)
- moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post ca1)"
- using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+ moreover have "S \<union> post c1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post c1')"
+ using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `c1 \<le> \<gamma>\<^isub>c c1'`, simplified]
by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
ultimately show ?case by (simp add: While.IH subset_iff)
qed
@@ -135,7 +135,7 @@
subsubsection "Ascending Chain Condition"
-hide_const acc
+hide_const (open) acc
abbreviation "strict r == r \<inter> -(r^-1)"
abbreviation "acc r == wf((strict r)^-1)"
@@ -392,5 +392,20 @@
apply(simp add: bot_acom assms(3))
done
+context Abs_Int_mono
+begin
+
+lemma AI_Some_measure:
+assumes "(strict{(x,y::'a). x \<sqsubseteq> y})^-1 <= measure m"
+and "\<forall>x y::'a. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m x = m y"
+shows "\<exists>c'. AI c = Some c'"
+unfolding AI_def
+apply(rule lpfpc_termination)
+apply(rule wf_subset[OF wf_measure measure_st[OF assms]])
+apply(erule mono_step'[OF le_refl])
+apply(rule strip_step')
+done
end
+
+end
--- a/src/HOL/IMP/Abs_Int0_const.thy Wed Jan 25 16:07:48 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_const.thy Thu Jan 26 09:52:47 2012 +0100
@@ -85,21 +85,18 @@
text{* Termination: *}
+definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
+
lemma measure_const:
- "(strict{(x::const,y). x \<sqsubseteq> y})^-1 \<subseteq>
- measure(%x. case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"
-by(auto split: const.splits)
+ "(strict{(x::const,y). x \<sqsubseteq> y})^-1 \<subseteq> measure m_const"
+by(auto simp: m_const_def split: const.splits)
lemma measure_const_eq:
- "\<forall> x y::const. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> (%x. case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0) x = (%x. case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0) y"
-by(auto split: const.splits)
-
-lemma acc_const_st: "Abs_Int0.acc{(x::const st,y). x \<sqsubseteq> y}"
-by(rule wf_subset[OF wf_measure measure_st[OF measure_const measure_const_eq]])
+ "\<forall> x y::const. x \<sqsubseteq> y \<and> y \<sqsubseteq> x \<longrightarrow> m_const x = m_const y"
+by(auto simp: m_const_def split: const.splits)
lemma "EX c'. AI_const c = Some c'"
-by(metis AI_def lpfpc_termination[OF acc_const_st, where f = "step_const \<top>",
- OF mono_step'[OF le_refl] strip_step'])
+by(rule AI_Some_measure[OF measure_const measure_const_eq])
subsubsection "Tests"
--- a/src/HOL/IMP/Abs_Int0_fun.thy Wed Jan 25 16:07:48 2012 +0100
+++ b/src/HOL/IMP/Abs_Int0_fun.thy Thu Jan 26 09:52:47 2012 +0100
@@ -314,8 +314,8 @@
by(simp add: \<gamma>_fun_def)
lemma step_preserves_le:
- "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; cs \<le> \<gamma>\<^isub>c ca \<rbrakk> \<Longrightarrow> step S cs \<le> \<gamma>\<^isub>c (step' S' ca)"
-proof(induction cs arbitrary: ca S S')
+ "\<lbrakk> S \<subseteq> \<gamma>\<^isub>o S'; c \<le> \<gamma>\<^isub>c c' \<rbrakk> \<Longrightarrow> step S c \<le> \<gamma>\<^isub>c (step' S' c')"
+proof(induction c arbitrary: c' S S')
case SKIP thus ?case by(auto simp:SKIP_le map_acom_SKIP)
next
case Assign thus ?case
@@ -325,24 +325,24 @@
case Semi thus ?case apply (auto simp: Semi_le map_acom_Semi)
by (metis le_post post_map_acom)
next
- case (If b cs1 cs2 P)
- then obtain ca1 ca2 Pa where
- "ca= IF b THEN ca1 ELSE ca2 {Pa}"
- "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1" "cs2 \<le> \<gamma>\<^isub>c ca2"
+ case (If b c1 c2 P)
+ then obtain c1' c2' P' where
+ "c' = IF b THEN c1' ELSE c2' {P'}"
+ "P \<subseteq> \<gamma>\<^isub>o P'" "c1 \<le> \<gamma>\<^isub>c c1'" "c2 \<le> \<gamma>\<^isub>c c2'"
by (fastforce simp: If_le map_acom_If)
- moreover have "post cs1 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs1 \<le> \<gamma>\<^isub>c ca1` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
- moreover have "post cs2 \<subseteq> \<gamma>\<^isub>o(post ca1 \<squnion> post ca2)"
- by (metis (no_types) `cs2 \<le> \<gamma>\<^isub>c ca2` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
+ moreover have "post c1 \<subseteq> \<gamma>\<^isub>o(post c1' \<squnion> post c2')"
+ by (metis (no_types) `c1 \<le> \<gamma>\<^isub>c c1'` join_ge1 le_post mono_gamma_o order_trans post_map_acom)
+ moreover have "post c2 \<subseteq> \<gamma>\<^isub>o(post c1' \<squnion> post c2')"
+ by (metis (no_types) `c2 \<le> \<gamma>\<^isub>c c2'` join_ge2 le_post mono_gamma_o order_trans post_map_acom)
ultimately show ?case using `S \<subseteq> \<gamma>\<^isub>o S'` by (simp add: If.IH subset_iff)
next
- case (While I b cs1 P)
- then obtain ca1 Ia Pa where
- "ca = {Ia} WHILE b DO ca1 {Pa}"
- "I \<subseteq> \<gamma>\<^isub>o Ia" "P \<subseteq> \<gamma>\<^isub>o Pa" "cs1 \<le> \<gamma>\<^isub>c ca1"
+ case (While I b c1 P)
+ then obtain c1' I' P' where
+ "c' = {I'} WHILE b DO c1' {P'}"
+ "I \<subseteq> \<gamma>\<^isub>o I'" "P \<subseteq> \<gamma>\<^isub>o P'" "c1 \<le> \<gamma>\<^isub>c c1'"
by (fastforce simp: map_acom_While While_le)
- moreover have "S \<union> post cs1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post ca1)"
- using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `cs1 \<le> \<gamma>\<^isub>c ca1`, simplified]
+ moreover have "S \<union> post c1 \<subseteq> \<gamma>\<^isub>o (S' \<squnion> post c1')"
+ using `S \<subseteq> \<gamma>\<^isub>o S'` le_post[OF `c1 \<le> \<gamma>\<^isub>c c1'`, simplified]
by (metis (no_types) join_ge1 join_ge2 le_sup_iff mono_gamma_o order_trans)
ultimately show ?case by (simp add: While.IH subset_iff)
qed
--- a/src/HOL/IMP/Abs_State.thy Wed Jan 25 16:07:48 2012 +0100
+++ b/src/HOL/IMP/Abs_State.thy Thu Jan 26 09:52:47 2012 +0100
@@ -12,8 +12,8 @@
datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname list"
-fun "fun" where "fun (FunDom f _) = f"
-fun dom where "dom (FunDom _ A) = A"
+fun "fun" where "fun (FunDom f xs) = f"
+fun dom where "dom (FunDom f xs) = xs"
definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
--- a/src/HOL/IMP/Collecting.thy Wed Jan 25 16:07:48 2012 +0100
+++ b/src/HOL/IMP/Collecting.thy Thu Jan 26 09:52:47 2012 +0100
@@ -152,8 +152,8 @@
definition CS :: "com \<Rightarrow> state set acom" where
"CS c = lfp (step UNIV) c"
-lemma mono_step_aux: "x \<le> y \<Longrightarrow> S \<subseteq> T \<Longrightarrow> step S x \<le> step T y"
-proof(induction x y arbitrary: S T rule: less_eq_acom.induct)
+lemma mono2_step: "c1 \<le> c2 \<Longrightarrow> S1 \<subseteq> S2 \<Longrightarrow> step S1 c1 \<le> step S2 c2"
+proof(induction c1 c2 arbitrary: S1 S2 rule: less_eq_acom.induct)
case 2 thus ?case by fastforce
next
case 3 thus ?case by(simp add: le_post)
@@ -164,7 +164,7 @@
qed auto
lemma mono_step: "mono (step S)"
-by(blast intro: monoI mono_step_aux)
+by(blast intro: monoI mono2_step)
lemma strip_step: "strip(step S c) = strip c"
by (induction c arbitrary: S) auto
--- a/src/HOL/IMP/Collecting1.thy Wed Jan 25 16:07:48 2012 +0100
+++ b/src/HOL/IMP/Collecting1.thy Thu Jan 26 09:52:47 2012 +0100
@@ -11,7 +11,7 @@
lemma step_preserves_le:
"\<lbrakk> step S cs = cs; S' \<subseteq> S; cs' \<le> cs \<rbrakk> \<Longrightarrow>
step S' cs' \<le> cs"
-by (metis mono_step_aux)
+by (metis mono2_step)
lemma steps_empty_preserves_le: assumes "step S cs = cs"
shows "cs' \<le> cs \<Longrightarrow> (step {} ^^ n) cs' \<le> cs"