--- a/src/HOL/Codatatype/Examples/Process.thy Sun Sep 09 21:22:31 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Process.thy Sun Sep 09 21:22:31 2012 +0200
@@ -21,13 +21,6 @@
subsection{* Setup for map, set, pred *}
-(* These should be eventually inferred from compositionality *)
-
-lemma pre_process_map[simp]:
-"pre_process_map fa fp (Inl (a ,p)) = Inl (fa a, fp p)"
-"pre_process_map fa fp (Inr (p1, p2)) = Inr (fp p1, fp p2)"
-unfolding pre_process_map_def by auto
-
lemma pre_process_pred[simp]:
"pre_process_pred (op =) \<phi> (Inl (a,p)) (Inl (a',p')) \<longleftrightarrow> a = a' \<and> \<phi> p p'"
"pre_process_pred (op =) \<phi> (Inr (p,q)) (Inr (p',q')) \<longleftrightarrow> \<phi> p p' \<and> \<phi> q q'"
@@ -119,116 +112,15 @@
qed
-subsection {* Coiteration and corecursion *}
-
-(* Preliminaries: *)
-definition
-"join22 isA pr co isC c1 c2 \<equiv>
- \<lambda> P. if isA P then Inl (pr P, co P)
- else if isC P then Inr (c1 P, c2 P)
- else undefined"
-
-declare process.unf_fld[simp]
-declare process.fld_unf[simp]
-
-lemma unf_Action[simp]:
-"process_unf (Action a p) = Inl (a,p)"
-unfolding Action_def process.unf_fld ..
-
-lemma unf_Choice[simp]:
-"process_unf (Choice p1 p2) = Inr (p1,p2)"
-unfolding Choice_def process.unf_fld ..
-
-lemma isAction_unf:
-assumes "isAction p"
-shows "process_unf p = Inl (prefOf p, contOf p)"
-using assms unfolding isAction_def by auto
-
-lemma isChoice_unf:
-assumes "isChoice p"
-shows "process_unf p = Inr (ch1Of p, ch2Of p)"
-using assms unfolding isChoice_def by auto
-
-lemma unf_join22:
-"process_unf p = join22 isAction prefOf contOf isChoice ch1Of ch2Of p"
-unfolding join22_def
-using isAction_unf isChoice_unf not_isAction_isChoice isAction_isChoice by auto
-
-lemma isA_join22:
-assumes "isA P"
-shows "join22 isA pr co isC c1 c2 P = Inl (pr P, co P)"
-using assms unfolding join22_def by auto
-
-lemma isC_join22:
-assumes "\<not> isA P" and "isC P"
-shows "join22 isA pr co isC c1 c2 P = Inr (c1 P, c2 P)"
-using assms unfolding join22_def by auto
-
-(* Coiteration *)
-definition pcoiter ::
-"('b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'b)
- \<Rightarrow>
- ('b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('b \<Rightarrow> 'b)
- \<Rightarrow>
- 'b \<Rightarrow> 'a process"
-where "pcoiter isA pr co isC c1 c2 \<equiv> process_unf_coiter (join22 isA pr co isC c1 c2)"
-
-lemma unf_prefOf:
-assumes "process_unf q = Inl (a,p)"
-shows "prefOf q = a"
-using assms by (cases rule: process_exhaust[of q]) auto
-
-lemma unf_contOf:
-assumes "process_unf q = Inl (a,p)"
-shows "contOf q = p"
-using assms by (cases rule: process_exhaust[of q]) auto
-
-lemma unf_ch1Of:
-assumes "process_unf q = Inr (p1,p2)"
-shows "ch1Of q = p1"
-using assms by (cases rule: process_exhaust[of q]) auto
-
-lemma unf_ch2Of:
-assumes "process_unf q = Inr (p1,p2)"
-shows "ch2Of q = p2"
-using assms by (cases rule: process_exhaust[of q]) auto
-
-theorem pcoiter:
-"\<And>P. isA P \<Longrightarrow>
- pcoiter isA pr co isC c1 c2 P =
- Action (pr P)
- (pcoiter isA pr co isC c1 c2 (co P))"
-"\<And>P. \<lbrakk>\<not> isA P; isC P\<rbrakk> \<Longrightarrow>
- pcoiter isA pr co isC c1 c2 P =
- Choice (pcoiter isA pr co isC c1 c2 (c1 P))
- (pcoiter isA pr co isC c1 c2 (c2 P))"
-proof-
- fix P
- let ?f = "pcoiter isA pr co isC c1 c2" let ?s = "join22 isA pr co isC c1 c2"
- assume isA: "isA P"
- have unf: "process_unf (process_unf_coiter ?s P) = Inl (pr P, ?f (co P))"
- using process.unf_coiters[of ?s P]
- unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA]
- pre_process_map id_apply pcoiter_def .
- thus "?f P = Action (pr P) (?f (co P))"
- unfolding pcoiter_def Action_def using process.fld_unf by metis
-next
- fix P
- let ?f = "pcoiter isA pr co isC c1 c2" let ?s = "join22 isA pr co isC c1 c2"
- assume isA: "\<not> isA P" and isC: "isC P"
- have unf: "process_unf (process_unf_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))"
- using process.unf_coiters[of ?s P]
- unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC]
- pre_process_map id_apply pcoiter_def .
- thus "?f P = Choice (?f (c1 P)) (?f (c2 P))"
- unfolding pcoiter_def Choice_def using process.fld_unf by metis
-qed
+subsection {* Coiteration *}
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
@@ -246,18 +138,17 @@
definition
"BX \<equiv>
- pcoiter
+ process_coiter
(\<lambda> P. True)
(\<lambda> P. ''a'')
(\<lambda> P. P)
undefined
undefined
- undefined
()"
lemma BX: "BX = Action ''a'' BX"
unfolding BX_def
-using pcoiter(1)[of "\<lambda> P. True" "()" "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
+using process.coiters(1)[of "\<lambda> P. True" "()" "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
@@ -269,19 +160,18 @@
definition "co \<equiv> \<lambda> K. case K of x \<Rightarrow> undefined |y \<Rightarrow> x |ax \<Rightarrow> x"
lemmas Action_defs = isA_def pr_def co_def
-definition "isC \<equiv> \<lambda> K. case K of x \<Rightarrow> True |y \<Rightarrow> False |ax \<Rightarrow> False"
definition "c1 \<equiv> \<lambda> K. case K of x \<Rightarrow> ax |y \<Rightarrow> undefined |ax \<Rightarrow> undefined"
definition "c2 \<equiv> \<lambda> K. case K of x \<Rightarrow> y |y \<Rightarrow> undefined |ax \<Rightarrow> undefined"
-lemmas Choice_defs = isC_def c1_def c2_def
+lemmas Choice_defs = c1_def c2_def
-definition "F \<equiv> pcoiter isA pr co isC c1 c2"
+definition "F \<equiv> process_coiter isA pr co c1 c2"
definition "X = F x" definition "Y = F y" definition "AX = F ax"
lemma X_Y_AX: "X = Choice AX Y" "Y = Action ''b'' X" "AX = Action ''a'' X"
unfolding X_def Y_def AX_def F_def
-using pcoiter(2)[of isA x isC "pr" co c1 c2]
- pcoiter(1)[of isA y "pr" co isC c1 c2]
- pcoiter(1)[of isA ax "pr" co isC c1 c2]
+using process.coiters(2)[of isA x "pr" co c1 c2]
+ process.coiters(1)[of isA y "pr" co c1 c2]
+ process.coiters(1)[of isA ax "pr" co c1 c2]
unfolding Action_defs Choice_defs by simp_all
(* end product: *)
@@ -329,16 +219,6 @@
|
"CONT sys (ACT a T) = T"
-fun isCH where
-"isCH sys (VAR X) =
- (case sys X of CH T1 T2 \<Rightarrow> True |PROC p \<Rightarrow> isChoice p |_ \<Rightarrow> False)"
-|
-"isCH sys (PROC p) = isChoice p"
-|
-"isCH sys (ACT a T) = False"
-|
-"isCH sys (CH T1 T2) = True"
-
fun CH1 where
"CH1 sys (VAR X) =
(case sys X of CH T1 T2 \<Rightarrow> T1 |PROC p \<Rightarrow> PROC (ch1Of p))"
@@ -357,22 +237,12 @@
definition "guarded sys \<equiv> \<forall> X Y. sys X \<noteq> VAR Y"
-lemma guarded_isACT_isCH:
-assumes g: "guarded sys"
-shows "isACT sys T \<or> isCH sys T"
-proof(induct T)
- case (VAR X)
- thus ?case
- using g isAction_isChoice unfolding guarded_def by (cases "sys X", auto)
-qed(insert isAction_isChoice assms, unfold guarded_def, auto)
-
definition
"solution sys \<equiv>
- pcoiter
+ process_coiter
(isACT sys)
(PREF sys)
(CONT sys)
- (isCH sys)
(CH1 sys)
(CH2 sys)"
@@ -380,26 +250,21 @@
assumes "isACT sys T"
shows "solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
unfolding solution_def
-using pcoiter(1)[of "isACT sys" T "PREF sys" "CONT sys"
- "isCH sys" "CH1 sys" "CH2 sys"] assms by simp
+using process.coiters(1)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
+ assms by simp
lemma solution_Choice:
-assumes "\<not> isACT sys T" "isCH sys T"
+assumes "\<not> isACT sys T"
shows "solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"
unfolding solution_def
-using pcoiter(2)[of "isACT sys" T "isCH sys" "PREF sys" "CONT sys"
- "CH1 sys" "CH2 sys"] assms by simp
+using process.coiters(2)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"]
+ assms by simp
lemma isACT_VAR:
assumes g: "guarded sys"
shows "isACT sys (VAR X) \<longleftrightarrow> isACT sys (sys X)"
using g unfolding guarded_def by (cases "sys X") auto
-lemma isCH_VAR:
-assumes g: "guarded sys"
-shows "isCH sys (VAR X) \<longleftrightarrow> isCH sys (sys X)"
-using g unfolding guarded_def by (cases "sys X") auto
-
lemma solution_VAR:
assumes g: "guarded sys"
shows "solution sys (VAR X) = solution sys (sys X)"
@@ -413,17 +278,8 @@
case False note FFalse = False
hence TT: "\<not> isACT sys (sys X)" unfolding isACT_VAR[OF g] .
show ?thesis
- proof(cases "isCH sys (VAR X)")
- case True
- hence T: "isCH sys (sys X)" unfolding isCH_VAR[OF g] .
- show ?thesis
- unfolding solution_Choice[OF TT T] using solution_Choice[of sys "VAR X"] FFalse True g
- unfolding guarded_def by (cases "sys X", auto)
- next
- case False
- hence False using FFalse guarded_isACT_isCH[OF g, of "VAR X"] by simp
- thus ?thesis by simp
- qed
+ unfolding solution_Choice[OF TT] using solution_Choice[of sys "VAR X"] FFalse g
+ unfolding guarded_def by (cases "sys X", auto)
qed
lemma solution_PROC[simp]:
@@ -441,11 +297,10 @@
unfolding solution_Action[OF 0] by auto
next
assume "isChoice p"
- hence 0: "isCH sys (PROC p)" and p: "\<not> isAction p"
+ hence 0: "\<not> isACT sys (PROC p)"
using not_isAction_isChoice by auto
- hence 1: "\<not> isACT sys (PROC p)" by simp
- show ?thesis using 0 iss not_isAction_isChoice
- unfolding solution_Choice[OF 1 0] by auto
+ thus ?thesis using iss isAction_isChoice
+ unfolding solution_Choice[OF 0] by auto
qed
next
case (Action a a' p p')
@@ -453,9 +308,8 @@
show ?case using Action unfolding solution_Action[OF 0] by simp
next
case (Choice p q p' q')
- hence 0: "isCH sys (PROC (Choice p q))" by simp
- hence 1: "\<not> isACT sys (PROC (Choice p q))" using not_isAction_isChoice by auto
- show ?case using Choice unfolding solution_Choice[OF 1 0] by simp
+ hence 0: "\<not> isACT sys (PROC (Choice p q))" using not_isAction_isChoice by auto
+ show ?case using Choice unfolding solution_Choice[OF 0] by simp
qed
}
thus ?thesis by metis
@@ -467,7 +321,7 @@
lemma solution_CH[simp]:
"solution sys (CH T1 T2) = Choice (solution sys T1) (solution sys T2)"
-by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) isCH.simps(4) solution_Choice)
+by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) solution_Choice)
(* Example: *)