author blanchet Wed, 12 Sep 2012 00:20:37 +0200 changeset 49301 3577c7a2b306 parent 49300 c707df2e2083 child 49302 f5bd87aac224
```--- a/src/HOL/Codatatype/Examples/Process.thy	Wed Sep 12 00:20:37 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy	Wed Sep 12 00:20:37 2012 +0200
@@ -21,16 +21,7 @@

subsection {* Basic properties *}

-declare
-  process.inject[simp]
-  process.distinct[simp]
-  process.discs[simp]
-  process.sels[simp]
-  process.collapse[simp]
-  pre_process.pred_unfold[simp]
-
-lemmas process_exhaust =
-  process.exhaust[elim, case_names Action Choice]
+declare pre_process.pred_unfold[simp]

(* Constructors versus discriminators *)
theorem isAction_isChoice:
@@ -38,7 +29,7 @@
by (rule process.disc_exhaust) auto

theorem not_isAction_isChoice: "\<not> (isAction p \<and> isChoice p)"
-by (cases rule: process_exhaust[of p]) auto
+by (cases rule: process.exhaust[of p]) auto

subsection{* Coinduction *}
@@ -52,19 +43,19 @@
proof(intro mp[OF process.pred_coinduct, of \<phi>, OF _ phi], clarify)
fix p p'  assume \<phi>: "\<phi> p p'"
show "pre_process_pred (op =) \<phi> (process_unf p) (process_unf p')"
-  proof(cases rule: process_exhaust[of p])
+  proof(cases rule: process.exhaust[of p])
case (Action a q) note p = Action
-    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
-    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process_exhaust[of p'], auto)
+    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
+    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process.exhaust[of p'], auto)
have 0: "a = a' \<and> \<phi> q q'" using Act[OF \<phi>[unfolded p p']] .
have unf: "process_unf p = Inl (a,q)" "process_unf p' = Inl (a',q')"
unfolding p p' Action_def process.unf_fld by simp_all
show ?thesis using 0 unfolding unf by simp
next
case (Choice p1 p2) note p = Choice
-    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
+    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
then obtain p1' p2' where p': "p' = Choice p1' p2'"
-    by (cases rule: process_exhaust[of p'], auto)
+    by (cases rule: process.exhaust[of p'], auto)
have 0: "\<phi> p1 p1' \<and> \<phi> p2 p2'" using Ch[OF \<phi>[unfolded p p']] .
have unf: "process_unf p = Inr (p1,p2)" "process_unf p' = Inr (p1',p2')"
unfolding p p' Choice_def process.unf_fld by simp_all
@@ -82,19 +73,19 @@
proof(intro mp[OF process.pred_coinduct_upto, of \<phi>, OF _ phi], clarify)
fix p p'  assume \<phi>: "\<phi> p p'"
show "pre_process_pred (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_unf p) (process_unf p')"
-  proof(cases rule: process_exhaust[of p])
+  proof(cases rule: process.exhaust[of p])
case (Action a q) note p = Action
-    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
-    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process_exhaust[of p'], auto)
+    hence "isAction p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
+    then obtain a' q' where p': "p' = Action a' q'" by (cases rule: process.exhaust[of p'], auto)
have 0: "a = a' \<and> (\<phi> q q' \<or> q = q')" using Act[OF \<phi>[unfolded p p']] .
have unf: "process_unf p = Inl (a,q)" "process_unf p' = Inl (a',q')"
unfolding p p' Action_def process.unf_fld by simp_all
show ?thesis using 0 unfolding unf by simp
next
case (Choice p1 p2) note p = Choice
-    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process_exhaust[of p'], auto)
+    hence "isChoice p'" using iss[OF \<phi>] by (cases rule: process.exhaust[of p'], auto)
then obtain p1' p2' where p': "p' = Choice p1' p2'"
-    by (cases rule: process_exhaust[of p'], auto)
+    by (cases rule: process.exhaust[of p'], auto)
have 0: "(\<phi> p1 p1' \<or> p1 = p1') \<and> (\<phi> p2 p2' \<or> p2 = p2')" using Ch[OF \<phi>[unfolded p p']] .
have unf: "process_unf p = Inr (p1,p2)" "process_unf p' = Inr (p1',p2')"
unfolding p p' Choice_def process.unf_fld by simp_all```