# HG changeset patch # User blanchet # Date 1347218551 -7200 # Node ID 2267901ae9110de9a989e2b2ea535966decc5580 # Parent fe22b6a5740b802b3a2f7a5a3eaf5da637dd4d3e simplify "Process" example further diff -r fe22b6a5740b -r 2267901ae911 src/HOL/Codatatype/Examples/Process.thy --- 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 =) \ (Inl (a,p)) (Inl (a',p')) \ a = a' \ \ p p'" "pre_process_pred (op =) \ (Inr (p,q)) (Inr (p',q')) \ \ p p' \ \ q q'" @@ -119,116 +112,15 @@ qed -subsection {* Coiteration and corecursion *} - -(* Preliminaries: *) -definition -"join22 isA pr co isC c1 c2 \ - \ 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 "\ 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 \ bool) \ ('b \ 'a) \ ('b \ 'b) - \ - ('b \ bool) \ ('b \ 'b) \ ('b \ 'b) - \ - 'b \ 'a process" -where "pcoiter isA pr co isC c1 c2 \ 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: -"\P. isA P \ - pcoiter isA pr co isC c1 c2 P = - Action (pr P) - (pcoiter isA pr co isC c1 c2 (co P))" -"\P. \\ isA P; isC P\ \ - 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: "\ 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 \ 'a stream \ 'a stream" (* Use the existing coinductive package (distinct from our @@ -246,18 +138,17 @@ definition "BX \ - pcoiter + process_coiter (\ P. True) (\ P. ''a'') (\ P. P) undefined undefined - undefined ()" lemma BX: "BX = Action ''a'' BX" unfolding BX_def -using pcoiter(1)[of "\ P. True" "()" "\ P. ''a''" "\ P. P"] by simp +using process.coiters(1)[of "\ P. True" "()" "\ P. ''a''" "\ P. P"] by simp subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *} @@ -269,19 +160,18 @@ definition "co \ \ K. case K of x \ undefined |y \ x |ax \ x" lemmas Action_defs = isA_def pr_def co_def -definition "isC \ \ K. case K of x \ True |y \ False |ax \ False" definition "c1 \ \ K. case K of x \ ax |y \ undefined |ax \ undefined" definition "c2 \ \ K. case K of x \ y |y \ undefined |ax \ undefined" -lemmas Choice_defs = isC_def c1_def c2_def +lemmas Choice_defs = c1_def c2_def -definition "F \ pcoiter isA pr co isC c1 c2" +definition "F \ 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 \ True |PROC p \ isChoice p |_ \ 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 \ T1 |PROC p \ PROC (ch1Of p))" @@ -357,22 +237,12 @@ definition "guarded sys \ \ X Y. sys X \ VAR Y" -lemma guarded_isACT_isCH: -assumes g: "guarded sys" -shows "isACT sys T \ 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 \ - 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 "\ isACT sys T" "isCH sys T" +assumes "\ 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) \ 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) \ 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: "\ 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: "\ isAction p" + hence 0: "\ isACT sys (PROC p)" using not_isAction_isChoice by auto - hence 1: "\ 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: "\ 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: "\ 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: *)