# HG changeset patch
# User traytel
# Date 1377007858 -7200
# Node ID c0217c4a6b2dae45d2bcb730c1e49155e862a747
# Parent  45a7bfd99b45ec4fbb06edfa68e0fb94a29628b0
tuned example

diff -r 45a7bfd99b45 -r c0217c4a6b2d src/HOL/BNF/Examples/Process.thy
--- a/src/HOL/BNF/Examples/Process.thy	Tue Aug 20 14:39:55 2013 +0200
+++ b/src/HOL/BNF/Examples/Process.thy	Tue Aug 20 16:10:58 2013 +0200
@@ -8,7 +8,7 @@
 header {* Processes *}
 
 theory Process
-imports "../BNF"
+imports Stream 
 begin
 
 codatatype 'a process =
@@ -38,81 +38,31 @@
 subsection{* Coinduction *}
 
 theorem process_coind[elim, consumes 1, case_names iss Action Choice, induct pred: "HOL.eq"]:
-assumes phi: "\<phi> p p'" and
-iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
-Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
-Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
-shows "p = p'"
-proof(intro mp[OF process.dtor_coinduct, of \<phi>, OF _ phi], clarify)
-  fix p p'  assume \<phi>: "\<phi> p p'"
-  show "pre_process_rel (op =) \<phi> (process_dtor p) (process_dtor 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)
-    have 0: "a = a' \<and> \<phi> q q'" using Act[OF \<phi>[unfolded p p']] .
-    have dtor: "process_dtor p = Inl (a,q)" "process_dtor p' = Inl (a',q')"
-    unfolding p p' Action_def process.dtor_ctor by simp_all
-    show ?thesis using 0 unfolding dtor 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)
-    then obtain p1' p2' where p': "p' = Choice p1' p2'"
-    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 dtor: "process_dtor p = Inr (p1,p2)" "process_dtor p' = Inr (p1',p2')"
-    unfolding p p' Choice_def process.dtor_ctor by simp_all
-    show ?thesis using 0 unfolding dtor by simp
-  qed
-qed
+  assumes phi: "\<phi> p p'" and
+  iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
+  Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
+  Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
+  shows "p = p'"
+  using assms
+  by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.discs(3))
 
 (* Stronger coinduction, up to equality: *)
 theorem process_strong_coind[elim, consumes 1, case_names iss Action Choice]:
-assumes phi: "\<phi> p p'" and
-iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
-Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> (\<phi> p p' \<or> p = p')" and
-Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
-shows "p = p'"
-proof(intro mp[OF process.dtor_strong_coinduct, of \<phi>, OF _ phi], clarify)
-  fix p p'  assume \<phi>: "\<phi> p p'"
-  show "pre_process_rel (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_dtor p) (process_dtor 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)
-    have 0: "a = a' \<and> (\<phi> q q' \<or> q = q')" using Act[OF \<phi>[unfolded p p']] .
-    have dtor: "process_dtor p = Inl (a,q)" "process_dtor p' = Inl (a',q')"
-    unfolding p p' Action_def process.dtor_ctor by simp_all
-    show ?thesis using 0 unfolding dtor 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)
-    then obtain p1' p2' where p': "p' = Choice p1' p2'"
-    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 dtor: "process_dtor p = Inr (p1,p2)" "process_dtor p' = Inr (p1',p2')"
-    unfolding p p' Choice_def process.dtor_ctor by simp_all
-    show ?thesis using 0 unfolding dtor by simp
-  qed
-qed
+  assumes phi: "\<phi> p p'" and
+  iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
+  Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> (\<phi> p p' \<or> p = p')" and
+  Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
+  shows "p = p'"
+  using assms
+  by (coinduct rule: process.strong_coinduct) (metis process.collapse(1,2) process.discs(3))
 
 
 subsection {* Coiteration (unfold) *}
 
 
 section{* Coinductive definition of the notion of trace *}
-
-(* Say we have a type of streams: *)
-
-typedecl 'a stream
-
-consts Ccons :: "'a \<Rightarrow> 'a stream \<Rightarrow> 'a stream"
-
-(* Use the existing coinductive package (distinct from our
-new codatatype package, but highly compatible with it): *)
-
 coinductive trace where
-"trace p as \<Longrightarrow> trace (Action a p) (Ccons a as)"
+"trace p as \<Longrightarrow> trace (Action a p) (a ## as)"
 |
 "trace p as \<or> trace q as \<Longrightarrow> trace (Choice p q) as"