src/HOL/IMP/Abs_Int0.thy

 subsection "Orderings"
 
 declare order_trans[trans]
 
 class semilattice = semilattice_sup + top
-(* +
-assumes join_ge1 [simp]: "x \<le> x \<squnion> y"
-and join_ge2 [simp]: "y \<le> x \<squnion> y"
-and join_least: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
-begin
-
-lemma join_le_iff[simp]: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
-by (metis join_ge1 join_ge2 join_least order_trans)
-*)
-
-lemma le_join_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> (z::'a::semilattice_sup)"
-by (metis sup_ge1 sup_ge2 order_trans)
 
 
 instance "fun" :: (type, semilattice) semilattice ..
-(*
-definition top_fun where "top_fun = (\<lambda>x. \<top>)"
-
-lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
-by (simp add: join_fun_def)
-
-instance
-proof
-qed (simp_all add: le_fun_def)
-
-end
-*)
 
 instantiation option :: (order)order
 begin
 
 fun less_eq_option where

 next
   case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
 qed
 
 end
+
+lemma [simp]: "(Some x < Some y) = (x < y)"
+by(auto simp: less_le)
 
 instantiation option :: (order)bot
 begin
 
 definition bot_option :: "'a option" where

 fun aval' :: "aexp \<Rightarrow> 'av st \<Rightarrow> 'av" where
 "aval' (N i) S = num' i" |
 "aval' (V x) S = S x" |
 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
 
-(* Interpretation would be nicer but is impossible *)
-definition "step' = Step.Step
+definition "step' = Step
   (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S)))
   (\<lambda>b S. S)"
 
-lemma [simp]: "step' S (SKIP {P}) = (SKIP {S})"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (x ::= e {P}) =
-  x ::= e {case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(S(x := aval' e S))}"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (C1; C2) = step' S C1; step' (post C1) C2"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
-   IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2
-   {post C1 \<squnion> post C2}"
-by(simp add: step'_def Step.Step.simps)
-lemma [simp]: "step' S ({I} WHILE b DO {P} C {Q}) =
-  {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
-by(simp add: step'_def Step.Step.simps)
-
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = pfp (step' \<top>) (bot c)"
-
-
-lemma strip_step'[simp]: "strip(step' S C) = strip C"
-by(induct C arbitrary: S) (simp_all add: Let_def)
 
 
 abbreviation \<gamma>\<^isub>s :: "'av st \<Rightarrow> state set"
 where "\<gamma>\<^isub>s == \<gamma>_fun \<gamma>"
 

 text{* Soundness: *}
 
 lemma aval'_sound: "s : \<gamma>\<^isub>s S \<Longrightarrow> aval a s : \<gamma>(aval' a S)"
 by (induct a) (auto simp: gamma_num' gamma_plus' \<gamma>_fun_def)
 
-lemma in_gamma_update:
-  "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
+lemma in_gamma_update: "\<lbrakk> s : \<gamma>\<^isub>s S; i : \<gamma> a \<rbrakk> \<Longrightarrow> s(x := i) : \<gamma>\<^isub>s(S(x := a))"
 by(simp add: \<gamma>_fun_def)
 
+lemma gamma_Step_subcomm:
+  assumes "!!x e S. f1 x e (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (f2 x e S)"  "!!b S. g1 b (\<gamma>\<^isub>o S) \<subseteq> \<gamma>\<^isub>o (g2 b S)"
+  shows "Step f1 g1 (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (Step f2 g2 S C)"
+proof(induction C arbitrary: S)
+qed  (auto simp: mono_gamma_o assms)
+
 lemma step_step': "step (\<gamma>\<^isub>o S) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' S C)"
-proof(induction C arbitrary: S)
-  case SKIP thus ?case by auto
-next
-  case Assign thus ?case
-    by (fastforce intro: aval'_sound in_gamma_update split: option.splits)
-next
-  case Seq thus ?case by auto
-next
-  case If thus ?case by (auto simp: mono_gamma_o)
-next
-  case While thus ?case by (auto simp: mono_gamma_o)
-qed
+unfolding step_def step'_def
+by(rule gamma_Step_subcomm) (auto simp: aval'_sound in_gamma_update split: option.splits)
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
   assume 1: "pfp (step' \<top>) (bot c) = Some C"
   have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
   have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"  --"transfer the pfp'"
   proof(rule order_trans)
     show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
     show "... \<le> \<gamma>\<^isub>c C" by (metis mono_gamma_c[OF pfp'])
   qed
-  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
+  have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
   have "lfp c (step (\<gamma>\<^isub>o \<top>)) \<le> \<gamma>\<^isub>c C"
     by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o \<top>)", OF 3 2])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 

 
 lemma mono_update: "a \<le> a' \<Longrightarrow> S \<le> S' \<Longrightarrow> S(x := a) \<le> S'(x := a')"
 by(simp add: le_fun_def)
 
 lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
-            split: option.split)
-done
+unfolding step'_def
+by(rule mono2_Step) (auto simp: mono_update mono_aval' split: option.split)
 
 end
 
 text{* Problem: not executable because of the comparison of abstract states,
 i.e. functions, in the post-fixedpoint computation. *}