# HG changeset patch
# User nipkow
# Date 1327567967 -3600
# Node ID 3858dc8eabd880dc7e4ca93fd35ed9e8da529a70
# Parent  46c2c96f5d92f7690149f090708d196114336b64
tuned

diff -r 46c2c96f5d92 -r 3858dc8eabd8 src/HOL/IMP/Abs_Int0.thy
--- 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
diff -r 46c2c96f5d92 -r 3858dc8eabd8 src/HOL/IMP/Abs_Int0_const.thy
--- 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"
diff -r 46c2c96f5d92 -r 3858dc8eabd8 src/HOL/IMP/Abs_Int0_fun.thy
--- 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
diff -r 46c2c96f5d92 -r 3858dc8eabd8 src/HOL/IMP/Abs_State.thy
--- 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]"
 
diff -r 46c2c96f5d92 -r 3858dc8eabd8 src/HOL/IMP/Collecting.thy
--- 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
diff -r 46c2c96f5d92 -r 3858dc8eabd8 src/HOL/IMP/Collecting1.thy
--- 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"