# HG changeset patch
# User berghofe
# Date 1272975088 -7200
# Node ID f36588af1ba18c9b3eec7776a7ed235f73242664
# Parent  084470c3cea22e156eed8c912aee135c99ee3b61
Turned Sem into an inductive definition.

diff -r 084470c3cea2 -r f36588af1ba1 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Tue May 04 12:29:22 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Tue May 04 14:11:28 2010 +0200
@@ -27,18 +27,19 @@
 
 types 'a sem = "'a => 'a => bool"
 
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (%s s'. s ~: b & (s=s'))"
-"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+  "Sem (Basic f) s (f s)"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "s \<in> b \<Longrightarrow> Sem c1 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 s s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) s s'"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) s s"
+| "s \<in> b \<Longrightarrow> Sem c s s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+   Sem (While b x c) s s'"
 
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (s' = f s)"
-"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s  : b --> Sem c1 s s') &
-                                      (s ~: b --> Sem c2 s s'))"
-"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+  "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
   "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
@@ -209,19 +210,18 @@
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (auto simp:Valid_def)
 
-lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==>
-       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> I \<and> s \<in> b \<longrightarrow> s' \<in> I \<Longrightarrow>
+    s \<in> I \<Longrightarrow> s' \<in> I \<and> s' \<notin> b"
+  using assms
+  by (induct "WHILE b INV {i} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
 apply (clarsimp simp:Valid_def)
-apply(drule iter_aux)
-  prefer 2 apply assumption
+apply(drule While_aux)
+  apply assumption
  apply blast
 apply blast
 done
diff -r 084470c3cea2 -r f36588af1ba1 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue May 04 12:29:22 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Tue May 04 14:11:28 2010 +0200
@@ -25,22 +25,23 @@
 
 types 'a sem = "'a option => 'a option => bool"
 
-consts iter :: "nat => 'a bexp => 'a sem => 'a sem"
-primrec
-"iter 0 b S = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
-"iter (Suc n) b S =
-  (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
+inductive Sem :: "'a com \<Rightarrow> 'a sem"
+where
+  "Sem (Basic f) None None"
+| "Sem (Basic f) (Some s) (Some (f s))"
+| "Sem Abort s None"
+| "Sem c1 s s'' \<Longrightarrow> Sem c2 s'' s' \<Longrightarrow> Sem (c1;c2) s s'"
+| "Sem (IF b THEN c1 ELSE c2 FI) None None"
+| "s \<in> b \<Longrightarrow> Sem c1 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "s \<notin> b \<Longrightarrow> Sem c2 (Some s) s' \<Longrightarrow> Sem (IF b THEN c1 ELSE c2 FI) (Some s) s'"
+| "Sem (While b x c) None None"
+| "s \<notin> b \<Longrightarrow> Sem (While b x c) (Some s) (Some s)"
+| "s \<in> b \<Longrightarrow> Sem c (Some s) s'' \<Longrightarrow> Sem (While b x c) s'' s' \<Longrightarrow>
+   Sem (While b x c) (Some s) s'"
 
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
-"Sem Abort s s' = (s' = None)"
-"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' =
- (case s of None \<Rightarrow> s' = None
-  | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
-"Sem(While b x c) s s' =
- (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
+inductive_cases [elim!]:
+  "Sem (Basic f) s s'" "Sem (c1;c2) s s'"
+  "Sem (IF b THEN c1 ELSE c2 FI) s s'"
 
 definition Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool" where
   "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
@@ -212,23 +213,20 @@
   \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
 by (fastsimp simp:Valid_def image_def)
 
-lemma iter_aux:
- "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
-  (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
-apply(unfold image_def)
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
+lemma While_aux:
+  assumes "Sem (WHILE b INV {i} DO c OD) s s'"
+  shows "\<forall>s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
+    s \<in> Some ` I \<Longrightarrow> s' \<in> Some ` (I \<inter> -b)"
+  using assms
+  by (induct "WHILE b INV {i} DO c OD" s s') auto
 
 lemma WhileRule:
  "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> Valid p (While b i c) q"
 apply(simp add:Valid_def)
 apply(simp (no_asm) add:image_def)
 apply clarify
-apply(drule iter_aux)
-  prefer 2 apply assumption
+apply(drule While_aux)
+  apply assumption
  apply blast
 apply blast
 done