# HG changeset patch # User blanchet # Date 1346772188 -7200 # Node ID 1a86ef0a02105a3518aefc29885f46b8ba0588ee # Parent f7326a0d7f194a4c7f739170dd7772c85065d2ff renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/HFset.thy --- a/src/HOL/Codatatype/Examples/HFset.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/HFset.thy Tue Sep 04 17:23:08 2012 +0200 @@ -48,13 +48,13 @@ subsection{* Recursion and iteration *} -lemma hfset_rec: -"hfset_rec R (Fold hs) = R (map_fset hs)" -using hfset.rec unfolding Fold_def . +lemma hfset_fld_rec: +"hfset_fld_rec R (Fold hs) = R (map_fset hs)" +using hfset.fld_rec unfolding Fold_def . (* The iterator has a simpler form: *) -lemma hfset_iter: -"hfset_iter R (Fold hs) = R (map_fset (hfset_iter R) hs)" -using hfset.iter unfolding Fold_def . +lemma hfset_fld_iter: +"hfset_fld_iter R (Fold hs) = R (map_fset (hfset_fld_iter R) hs)" +using hfset.fld_iter unfolding Fold_def . end diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Tue Sep 04 17:23:08 2012 +0200 @@ -24,20 +24,20 @@ (* These should be eventually inferred from compositionality *) -lemma TreeBNF_map: -"TreeBNF_map f (n,as) = (n, map_fset (id \ f) as)" -unfolding TreeBNF_map_def id_apply -sum_map_def by simp +lemma TreeBNF_map: +"TreeBNF_map f (n, as) = (n, map_fset (id \ f) as)" +unfolding TreeBNF_map_def id_apply +sum_map_def by simp lemma TreeBNF_map': "TreeBNF_map f n_as = (fst n_as, map_fset (id \ f) (snd n_as))" using TreeBNF_map by(cases n_as, simp) -definition -"llift2 \ as1 as2 \ - (\ n. Inl n \ fset as1 \ Inl n \ fset as2) \ - (\ tr1. Inr tr1 \ fset as1 \ (\ tr2. Inr tr2 \ fset as2 \ \ tr1 tr2)) \ +definition +"llift2 \ as1 as2 \ + (\ n. Inl n \ fset as1 \ Inl n \ fset as2) \ + (\ tr1. Inr tr1 \ fset as1 \ (\ tr2. Inr tr2 \ fset as2 \ \ tr1 tr2)) \ (\ tr2. Inr tr2 \ fset as2 \ (\ tr1. Inr tr1 \ fset as1 \ \ tr1 tr2))" lemma TreeBNF_pred: "TreeBNF_pred \ (n1,as1) (n2,as2) \ n1 = n2 \ llift2 \ as1 as2" @@ -65,7 +65,7 @@ (* These are mere auxiliaries *) definition "asNNode tr \ SOME n_as. NNode (fst n_as) (snd n_as) = tr" -lemmas pre_sel_defs = asNNode_def +lemmas pre_sel_defs = asNNode_def subsection {* Selectors *} @@ -84,9 +84,9 @@ (* Constructors versus selectors *) lemma NNode_surj: "\ n as. NNode n as = tr" unfolding NNode_def -by (metis Tree.fld_unf pair_collapse) +by (metis Tree.fld_unf pair_collapse) -lemma NNode_asNNode: +lemma NNode_asNNode: "NNode (fst (asNNode tr)) (snd (asNNode tr)) = tr" proof- obtain n as where "NNode n as = tr" using NNode_surj[of tr] by blast @@ -94,12 +94,12 @@ thus ?thesis unfolding asNNode_def by(rule someI) qed -theorem NNode_root_ccont[simp]: +theorem NNode_root_ccont[simp]: "NNode (root tr) (ccont tr) = tr" using NNode_asNNode unfolding root_def ccont_def . (* Constructors *) -theorem TTree_simps[simp]: +theorem TTree_simps[simp]: "NNode n as = NNode n' as' \ n = n' \ as = as'" unfolding ctor_defs Tree.fld_inject by auto @@ -109,7 +109,7 @@ proof(cases rule: Tree.fld_exhaust[of tr]) fix x assume "tr = Tree_fld x" thus ?thesis - apply(cases x) + apply(cases x) using NNode unfolding ctor_defs apply blast done qed @@ -125,33 +125,33 @@ subsection{* Coinduction *} theorem TTree_coind_Node[elim, consumes 1, case_names NNode, induct pred: "HOL.eq"]: -assumes phi: "\ tr1 tr2" and -NNode: "\ n1 n2 as1 as2. - \\ (NNode n1 as1) (NNode n2 as2)\ \ +assumes phi: "\ tr1 tr2" and +NNode: "\ n1 n2 as1 as2. + \\ (NNode n1 as1) (NNode n2 as2)\ \ n1 = n2 \ llift2 \ as1 as2" shows "tr1 = tr2" apply(rule mp[OF Tree.pred_coinduct[of \ tr1 tr2] phi]) proof clarify fix tr1 tr2 assume \: "\ tr1 tr2" - show "TreeBNF_pred \ (Tree_unf tr1) (Tree_unf tr2)" + show "TreeBNF_pred \ (Tree_unf tr1) (Tree_unf tr2)" apply(cases rule: Tree.fld_exhaust[of tr1], cases rule: Tree.fld_exhaust[of tr2]) - apply (simp add: Tree.unf_fld) + apply (simp add: Tree.unf_fld) apply(case_tac x, case_tac xa, simp) unfolding TreeBNF_pred apply(rule NNode) using \ unfolding NNode_def by simp qed theorem TTree_coind[elim, consumes 1, case_names LLift]: -assumes phi: "\ tr1 tr2" and -LLift: "\ tr1 tr2. \ tr1 tr2 \ +assumes phi: "\ tr1 tr2" and +LLift: "\ tr1 tr2. \ tr1 tr2 \ root tr1 = root tr2 \ llift2 \ (ccont tr1) (ccont tr2)" shows "tr1 = tr2" using phi apply(induct rule: TTree_coind_Node) -using LLift by (metis TTree_sel_ctor) +using LLift by (metis TTree_sel_ctor) subsection {* Coiteration *} - -(* Preliminaries: *) + +(* Preliminaries: *) declare Tree.unf_fld[simp] declare Tree.fld_unf[simp] @@ -162,40 +162,40 @@ lemma Tree_unf_root_ccont: "Tree_unf tr = (root tr, ccont tr)" unfolding root_def ccont_def -by (metis (lifting) NNode_asNNode Tree_unf_NNode) +by (metis (lifting) NNode_asNNode Tree_unf_NNode) (* Coiteration *) -definition TTree_coit :: +definition TTree_coit :: "('b \ N) \ ('b \ (T + 'b) fset) \ 'b \ Tree" -where "TTree_coit rt ct \ Tree_coiter " +where "TTree_coit rt ct \ Tree_unf_coiter " -lemma Tree_coit_coit: -"Tree_coiter s = TTree_coit (fst o s) (snd o s)" +lemma Tree_coit_coit: +"Tree_unf_coiter s = TTree_coit (fst o s) (snd o s)" apply(rule ext) unfolding TTree_coit_def by simp -theorem TTree_coit: -"root (TTree_coit rt ct b) = rt b" +theorem TTree_coit: +"root (TTree_coit rt ct b) = rt b" "ccont (TTree_coit rt ct b) = map_fset (id \ TTree_coit rt ct) (ct b)" -using Tree.coiter[of "" b] unfolding Tree_coit_coit fst_convol snd_convol -unfolding TreeBNF_map' fst_convol' snd_convol' -unfolding Tree_unf_root_ccont by simp_all +using Tree.unf_coiter[of "" b] unfolding Tree_coit_coit fst_convol snd_convol +unfolding TreeBNF_map' fst_convol' snd_convol' +unfolding Tree_unf_root_ccont by simp_all -(* Corecursion, stronger than coitation *) -definition TTree_corec :: +(* Corecursion, stronger than coiteration *) +definition TTree_corec :: "('b \ N) \ ('b \ (T + (Tree + 'b)) fset) \ 'b \ Tree" -where "TTree_corec rt ct \ Tree_corec " +where "TTree_corec rt ct \ Tree_unf_corec " -lemma Tree_corec_corec: -"Tree_corec s = TTree_corec (fst o s) (snd o s)" +lemma Tree_unf_corec_corec: +"Tree_unf_corec s = TTree_corec (fst o s) (snd o s)" apply(rule ext) unfolding TTree_corec_def by simp -theorem TTree_corec: -"root (TTree_corec rt ct b) = rt b" +theorem TTree_corec: +"root (TTree_corec rt ct b) = rt b" "ccont (TTree_corec rt ct b) = map_fset (id \ ([[id, TTree_corec rt ct]]) ) (ct b)" -using Tree.corec[of "" b] unfolding Tree_corec_corec fst_convol snd_convol -unfolding TreeBNF_map' fst_convol' snd_convol' +using Tree.unf_corec[of "" b] unfolding Tree_unf_corec_corec fst_convol snd_convol +unfolding TreeBNF_map' fst_convol' snd_convol' unfolding Tree_unf_root_ccont by simp_all @@ -206,39 +206,39 @@ definition "coit rt ct \ TTree_coit rt (the_inv fset o ct)" definition "corec rt ct \ TTree_corec rt (the_inv fset o ct)" -definition lift ("_ ^#" 200) where +definition lift ("_ ^#" 200) where "lift \ as \ (\ tr. Inr tr \ as \ \ tr)" -definition lift2 ("_ ^#2" 200) where -"lift2 \ as1 as2 \ - (\ n. Inl n \ as1 \ Inl n \ as2) \ - (\ tr1. Inr tr1 \ as1 \ (\ tr2. Inr tr2 \ as2 \ \ tr1 tr2)) \ +definition lift2 ("_ ^#2" 200) where +"lift2 \ as1 as2 \ + (\ n. Inl n \ as1 \ Inl n \ as2) \ + (\ tr1. Inr tr1 \ as1 \ (\ tr2. Inr tr2 \ as2 \ \ tr1 tr2)) \ (\ tr2. Inr tr2 \ as2 \ (\ tr1. Inr tr1 \ as1 \ \ tr1 tr2))" -definition liftS ("_ ^#s" 200) where +definition liftS ("_ ^#s" 200) where "liftS trs = {as. Inr -` as \ trs}" -lemma lift2_llift2: -"\finite as1; finite as2\ \ +lemma lift2_llift2: +"\finite as1; finite as2\ \ lift2 \ as1 as2 \ llift2 \ (the_inv fset as1) (the_inv fset as2)" unfolding lift2_def llift2_def by auto -lemma llift2_lift2: +lemma llift2_lift2: "llift2 \ as1 as2 \ lift2 \ (fset as1) (fset as2)" using lift2_llift2 by (metis finite_fset fset_cong fset_to_fset) lemma mono_lift: -assumes "(\^#) as" +assumes "(\^#) as" and "\ tr. \ tr \ \' tr" shows "(\'^#) as" using assms unfolding lift_def[abs_def] by blast lemma mono_liftS: assumes "trs1 \ trs2 " -shows "(trs1 ^#s) \ (trs2 ^#s)" +shows "(trs1 ^#s) \ (trs2 ^#s)" using assms unfolding liftS_def[abs_def] by blast -lemma lift_mono: +lemma lift_mono: assumes "\ \ \'" shows "(\^#) \ (\'^#)" using assms unfolding lift_def[abs_def] by blast @@ -249,20 +249,20 @@ shows "(\'^#2) as1 as2" using assms unfolding lift2_def[abs_def] by blast -lemma lift2_mono: +lemma lift2_mono: assumes "\ \ \'" shows "(\^#2) \ (\'^#2)" -using assms unfolding lift2_def[abs_def] by blast +using assms unfolding lift2_def[abs_def] by blast lemma finite_cont[simp]: "finite (cont tr)" unfolding cont_def by auto -theorem Node_root_cont[simp]: +theorem Node_root_cont[simp]: "Node (root tr) (cont tr) = tr" using NNode_root_ccont unfolding Node_def cont_def by (metis cont_def finite_cont fset_cong fset_to_fset o_def) -theorem Tree_simps[simp]: +theorem Tree_simps[simp]: assumes "finite as" and "finite as'" shows "Node n as = Node n' as' \ n = n' \ as = as'" using assms TTree_simps unfolding Node_def @@ -276,18 +276,18 @@ by (metis Node Node_root_cont finite_cont) theorem Tree_sel_ctor[simp]: -"root (Node n as) = n" -"finite as \ cont (Node n as) = as" +"root (Node n as) = n" +"finite as \ cont (Node n as) = as" unfolding Node_def cont_def by auto theorems root_Node = Tree_sel_ctor(1) theorems cont_Node = Tree_sel_ctor(2) theorem Tree_coind_Node[elim, consumes 1, case_names Node]: -assumes phi: "\ tr1 tr2" and -Node: -"\ n1 n2 as1 as2. - \finite as1; finite as2; \ (Node n1 as1) (Node n2 as2)\ +assumes phi: "\ tr1 tr2" and +Node: +"\ n1 n2 as1 as2. + \finite as1; finite as2; \ (Node n1 as1) (Node n2 as2)\ \ n1 = n2 \ (\^#2) as1 as2" shows "tr1 = tr2" using phi apply(induct rule: TTree_coind_Node) @@ -298,15 +298,15 @@ by (metis finite_fset fset_cong fset_to_fset) theorem Tree_coind[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]: -assumes phi: "\ tr1 tr2" and -Lift: "\ tr1 tr2. \ tr1 tr2 \ +assumes phi: "\ tr1 tr2" and +Lift: "\ tr1 tr2. \ tr1 tr2 \ root tr1 = root tr2 \ (\^#2) (cont tr1) (cont tr2)" shows "tr1 = tr2" using phi apply(induct rule: TTree_coind) unfolding llift2_lift2 apply(rule Lift[unfolded cont_def comp_def]) . -theorem coit: -"root (coit rt ct b) = rt b" +theorem coit: +"root (coit rt ct b) = rt b" "finite (ct b) \ cont (coit rt ct b) = image (id \ coit rt ct) (ct b)" using TTree_coit[of rt "the_inv fset \ ct" b] unfolding coit_def apply - apply metis @@ -314,8 +314,8 @@ by (metis (no_types) fset_to_fset map_fset_image) -theorem corec: -"root (corec rt ct b) = rt b" +theorem corec: +"root (corec rt ct b) = rt b" "finite (ct b) \ cont (corec rt ct b) = image (id \ ([[id, corec rt ct]])) (ct b)" using TTree_corec[of rt "the_inv fset \ ct" b] unfolding corec_def apply - apply metis diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/Lambda_Term.thy --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Tue Sep 04 17:23:08 2012 +0200 @@ -137,25 +137,25 @@ "\ xtas t a. sumJoin4 var app lam lt (Inr (Inr (Inr (xtas,(t,a))))) = lt xtas t a" unfolding sumJoin4_def by auto -definition "trmrec var app lam lt \ trm_rec (sumJoin4 var app lam lt)" +definition "trmrec var app lam lt \ trm_fld_rec (sumJoin4 var app lam lt)" lemma trmrec_Var[simp]: "trmrec var app lam lt (Var x) = var x" -unfolding trmrec_def Var_def trm.rec trmBNF_map(1) by simp +unfolding trmrec_def Var_def trm.fld_rec trmBNF_map(1) by simp lemma trmrec_App[simp]: "trmrec var app lam lt (App t1 t2) = app t1 (trmrec var app lam lt t1) t2 (trmrec var app lam lt t2)" -unfolding trmrec_def App_def trm.rec trmBNF_map(2) convol_def by simp +unfolding trmrec_def App_def trm.fld_rec trmBNF_map(2) convol_def by simp lemma trmrec_Lam[simp]: "trmrec var app lam lt (Lam x t) = lam x t (trmrec var app lam lt t)" -unfolding trmrec_def Lam_def trm.rec trmBNF_map(3) convol_def by simp +unfolding trmrec_def Lam_def trm.fld_rec trmBNF_map(3) convol_def by simp lemma trmrec_Lt[simp]: "trmrec var app lam lt (Lt xts t) = lt (map_fset (\ (x,t). (x,t,trmrec var app lam lt t)) xts) t (trmrec var app lam lt t)" -unfolding trmrec_def Lt_def trm.rec trmBNF_map(4) convol_def by simp +unfolding trmrec_def Lt_def trm.fld_rec trmBNF_map(4) convol_def by simp definition "sumJoinI4 f1 f2 f3 f4 \ @@ -174,25 +174,25 @@ unfolding sumJoinI4_def by auto (* The iterator has a simpler, hence more manageable type. *) -definition "trmiter var app lam lt \ trm_iter (sumJoinI4 var app lam lt)" +definition "trmiter var app lam lt \ trm_fld_iter (sumJoinI4 var app lam lt)" lemma trmiter_Var[simp]: "trmiter var app lam lt (Var x) = var x" -unfolding trmiter_def Var_def trm.iter trmBNF_map(1) by simp +unfolding trmiter_def Var_def trm.fld_iter trmBNF_map(1) by simp lemma trmiter_App[simp]: "trmiter var app lam lt (App t1 t2) = app (trmiter var app lam lt t1) (trmiter var app lam lt t2)" -unfolding trmiter_def App_def trm.iter trmBNF_map(2) by simp +unfolding trmiter_def App_def trm.fld_iter trmBNF_map(2) by simp lemma trmiter_Lam[simp]: "trmiter var app lam lt (Lam x t) = lam x (trmiter var app lam lt t)" -unfolding trmiter_def Lam_def trm.iter trmBNF_map(3) by simp +unfolding trmiter_def Lam_def trm.fld_iter trmBNF_map(3) by simp lemma trmiter_Lt[simp]: "trmiter var app lam lt (Lt xts t) = lt (map_fset (\ (x,t). (x,trmiter var app lam lt t)) xts) (trmiter var app lam lt t)" -unfolding trmiter_def Lt_def trm.iter trmBNF_map(4) by simp +unfolding trmiter_def Lt_def trm.fld_iter trmBNF_map(4) by simp subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *} diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/ListF.thy --- a/src/HOL/Codatatype/Examples/ListF.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/ListF.thy Tue Sep 04 17:23:08 2012 +0200 @@ -18,27 +18,27 @@ definition "Conss a as \ listF_fld (Inr (a, as))" lemma listF_map_NilF[simp]: "listF_map f NilF = NilF" -unfolding listF_map_def listFBNF_map_def NilF_def listF.iter by simp +unfolding listF_map_def listFBNF_map_def NilF_def listF.fld_iter by simp lemma listF_map_Conss[simp]: "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)" -unfolding listF_map_def listFBNF_map_def Conss_def listF.iter by simp +unfolding listF_map_def listFBNF_map_def Conss_def listF.fld_iter by simp lemma listF_set_NilF[simp]: "listF_set NilF = {}" -unfolding listF_set_def NilF_def listF.iter listFBNF_set1_def listFBNF_set2_def +unfolding listF_set_def NilF_def listF.fld_iter listFBNF_set1_def listFBNF_set2_def sum_set_defs listFBNF_map_def collect_def[abs_def] by simp lemma listF_set_Conss[simp]: "listF_set (Conss x xs) = {x} \ listF_set xs" -unfolding listF_set_def Conss_def listF.iter listFBNF_set1_def listFBNF_set2_def +unfolding listF_set_def Conss_def listF.fld_iter listFBNF_set1_def listFBNF_set2_def sum_set_defs prod_set_defs listFBNF_map_def collect_def[abs_def] by simp -lemma iter_sum_case_NilF: "listF_iter (sum_case f g) NilF = f ()" -unfolding NilF_def listF.iter listFBNF_map_def by simp +lemma iter_sum_case_NilF: "listF_fld_iter (sum_case f g) NilF = f ()" +unfolding NilF_def listF.fld_iter listFBNF_map_def by simp lemma iter_sum_case_Conss: - "listF_iter (sum_case f g) (Conss y ys) = g (y, listF_iter (sum_case f g) ys)" -unfolding Conss_def listF.iter listFBNF_map_def by simp + "listF_fld_iter (sum_case f g) (Conss y ys) = g (y, listF_fld_iter (sum_case f g) ys)" +unfolding Conss_def listF.fld_iter listFBNF_map_def by simp (* familiar induction principle *) lemma listF_induct: @@ -71,9 +71,9 @@ [simp]: "Singll a \ Conss a NilF" definition appendd (infixr "@@" 65) where - "appendd \ listF_iter (sum_case (\ _. id) (\ (a,f) bs. Conss a (f bs)))" + "appendd \ listF_fld_iter (sum_case (\ _. id) (\ (a,f) bs. Conss a (f bs)))" -definition "lrev \ listF_iter (sum_case (\ _. NilF) (\ (b,bs). bs @@ [[b]]))" +definition "lrev \ listF_fld_iter (sum_case (\ _. NilF) (\ (b,bs). bs @@ [[b]]))" lemma lrev_NilF[simp]: "lrev NilF = NilF" unfolding lrev_def by (simp add: iter_sum_case_NilF) diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/Process.thy --- a/src/HOL/Codatatype/Examples/Process.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Process.thy Tue Sep 04 17:23:08 2012 +0200 @@ -290,7 +290,7 @@ ('b \ bool) \ ('b \ 'b) \ ('b \ 'b) \ 'b \ 'a process" -where "pcoiter isA pr co isC c1 c2 \ process_coiter (join22 isA pr co isC c1 c2)" +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)" @@ -325,8 +325,8 @@ 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_coiter ?s P) = Inl (pr P, ?f (co P))" - using process.coiter[of ?s P] + have unf: "process_unf (process_unf_coiter ?s P) = Inl (pr P, ?f (co P))" + using process.unf_coiter[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] processBNF_map id_apply pcoiter_def . thus "?f P = Action (pr P) (?f (co P))" @@ -335,8 +335,8 @@ 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_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))" - using process.coiter[of ?s P] + have unf: "process_unf (process_unf_coiter ?s P) = Inr (?f (c1 P), ?f (c2 P))" + using process.unf_coiter[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] processBNF_map id_apply pcoiter_def . thus "?f P = Choice (?f (c1 P)) (?f (c2 P))" @@ -351,7 +351,7 @@ \ 'b \ 'a process" where -"pcorec isA pr co isC c1 c2 \ process_corec (join22 isA pr co isC c1 c2)" +"pcorec isA pr co isC c1 c2 \ process_unf_corec (join22 isA pr co isC c1 c2)" theorem pcorec_Action: assumes isA: "isA P" @@ -366,15 +366,15 @@ show ?thesis proof(cases "co P") case (Inl p) - have "process_unf (process_corec ?s P) = Inl (pr P, p)" - using process.corec[of ?s P] + have "process_unf (process_unf_corec ?s P) = Inl (pr P, p)" + using process.unf_corec[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] processBNF_map id_apply pcorec_def Inl by simp thus ?thesis unfolding Inl pcorec_def Action_def using process.fld_unf by (simp, metis) next case (Inr Q) - have "process_unf (process_corec ?s P) = Inl (pr P, ?f Q)" - using process.corec[of ?s P] + have "process_unf (process_unf_corec ?s P) = Inl (pr P, ?f Q)" + using process.unf_corec[of ?s P] unfolding isA_join22[of isA P "pr" co isC c1 c2, OF isA] processBNF_map id_apply pcorec_def Inr by simp thus ?thesis unfolding Inr pcorec_def Action_def using process.fld_unf by (simp, metis) @@ -404,15 +404,15 @@ show ?thesis proof(cases "c2 P") case (Inl p2) note c2 = Inl - have "process_unf (process_corec ?s P) = Inr (p1, p2)" - using process.corec[of ?s P] + have "process_unf (process_unf_corec ?s P) = Inr (p1, p2)" + using process.unf_corec[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] processBNF_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) next case (Inr Q2) note c2 = Inr - have "process_unf (process_corec ?s P) = Inr (p1, ?f Q2)" - using process.corec[of ?s P] + have "process_unf (process_unf_corec ?s P) = Inr (p1, ?f Q2)" + using process.unf_corec[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] processBNF_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) @@ -422,15 +422,15 @@ show ?thesis proof(cases "c2 P") case (Inl p2) note c2 = Inl - have "process_unf (process_corec ?s P) = Inr (?f Q1, p2)" - using process.corec[of ?s P] + have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, p2)" + using process.unf_corec[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] processBNF_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) next case (Inr Q2) note c2 = Inr - have "process_unf (process_corec ?s P) = Inr (?f Q1, ?f Q2)" - using process.corec[of ?s P] + have "process_unf (process_unf_corec ?s P) = Inr (?f Q1, ?f Q2)" + using process.unf_corec[of ?s P] unfolding isC_join22[of isA P isC "pr" co c1 c2, OF isA isC] processBNF_map id_apply pcorec_def c1 c2 by simp thus ?thesis unfolding c1 c2 pcorec_def Choice_def using process.fld_unf by (simp, metis) diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/Stream.thy --- a/src/HOL/Codatatype/Examples/Stream.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Stream.thy Tue Sep 04 17:23:08 2012 +0200 @@ -18,12 +18,12 @@ definition "hdd as \ fst (stream_unf as)" definition "tll as \ snd (stream_unf as)" -lemma coiter_pair_fun_hdd[simp]: "hdd (stream_coiter (f \ g) t) = f t" -unfolding hdd_def pair_fun_def stream.coiter by simp +lemma coiter_pair_fun_hdd[simp]: "hdd (stream_unf_coiter (f \ g) t) = f t" +unfolding hdd_def pair_fun_def stream.unf_coiter by simp -lemma coiter_pair_fun_tll[simp]: "tll (stream_coiter (f \ g) t) = - stream_coiter (f \ g) (g t)" -unfolding tll_def pair_fun_def stream.coiter by simp +lemma coiter_pair_fun_tll[simp]: "tll (stream_unf_coiter (f \ g) t) = + stream_unf_coiter (f \ g) (g t)" +unfolding tll_def pair_fun_def stream.unf_coiter by simp (* infinite trees: *) coinductive infiniteTr where @@ -45,7 +45,7 @@ "infiniteTr tr \ (\ tr' \ listF_set (sub tr). infiniteTr tr')" by (erule infiniteTr.cases) blast -definition "konigPath \ stream_coiter +definition "konigPath \ stream_unf_coiter (lab \ (\tr. SOME tr'. tr' \ listF_set (sub tr) \ infiniteTr tr'))" lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t" @@ -111,7 +111,7 @@ (* some more stream theorems *) -lemma stream_map[simp]: "stream_map f = stream_coiter (f o hdd \ tll)" +lemma stream_map[simp]: "stream_map f = stream_unf_coiter (f o hdd \ tll)" unfolding stream_map_def pair_fun_def hdd_def[abs_def] tll_def[abs_def] map_pair_def o_def prod_case_beta by simp @@ -123,13 +123,13 @@ definition plus :: "nat stream \ nat stream \ nat stream" (infixr "\" 66) where [simp]: "plus xs ys = - stream_coiter ((%(xs, ys). hdd xs + hdd ys) \ (%(xs, ys). (tll xs, tll ys))) (xs, ys)" + stream_unf_coiter ((%(xs, ys). hdd xs + hdd ys) \ (%(xs, ys). (tll xs, tll ys))) (xs, ys)" definition scalar :: "nat \ nat stream \ nat stream" (infixr "\" 68) where [simp]: "scalar n = stream_map (\x. n * x)" -definition ones :: "nat stream" where [simp]: "ones = stream_coiter ((%x. 1) \ id) ()" -definition twos :: "nat stream" where [simp]: "twos = stream_coiter ((%x. 2) \ id) ()" +definition ones :: "nat stream" where [simp]: "ones = stream_unf_coiter ((%x. 1) \ id) ()" +definition twos :: "nat stream" where [simp]: "twos = stream_unf_coiter ((%x. 2) \ id) ()" definition ns :: "nat \ nat stream" where [simp]: "ns n = scalar n ones" lemma "ones \ ones = twos" diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Tue Sep 04 17:23:08 2012 +0200 @@ -30,14 +30,14 @@ definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" -lemma coiter_pair_fun_lab: "lab (treeFI_coiter (f \ g) t) = f t" -unfolding lab_def pair_fun_def treeFI.coiter treeFIBNF_map_def by simp +lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \ g) t) = f t" +unfolding lab_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp -lemma coiter_pair_fun_sub: "sub (treeFI_coiter (f \ g) t) = listF_map (treeFI_coiter (f \ g)) (g t)" -unfolding sub_def pair_fun_def treeFI.coiter treeFIBNF_map_def by simp +lemma coiter_pair_fun_sub: "sub (treeFI_unf_coiter (f \ g) t) = listF_map (treeFI_unf_coiter (f \ g)) (g t)" +unfolding sub_def pair_fun_def treeFI.unf_coiter treeFIBNF_map_def by simp (* Tree reverse:*) -definition "trev \ treeFI_coiter (lab \ lrev o sub)" +definition "trev \ treeFI_unf_coiter (lab \ lrev o sub)" lemma trev_simps1[simp]: "lab (trev t) = lab t" unfolding trev_def by (simp add: coiter_pair_fun_lab) diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Tue Sep 04 17:23:08 2012 +0200 @@ -26,14 +26,14 @@ lemma unf[simp]: "treeFsetI_unf t = (lab t, sub t)" unfolding lab_def sub_def by simp -lemma coiter_pair_fun_lab: "lab (treeFsetI_coiter (f \ g) t) = f t" -unfolding lab_def pair_fun_def treeFsetI.coiter treeFsetIBNF_map_def by simp +lemma coiter_pair_fun_lab: "lab (treeFsetI_unf_coiter (f \ g) t) = f t" +unfolding lab_def pair_fun_def treeFsetI.unf_coiter treeFsetIBNF_map_def by simp -lemma coiter_pair_fun_sub: "sub (treeFsetI_coiter (f \ g) t) = map_fset (treeFsetI_coiter (f \ g)) (g t)" -unfolding sub_def pair_fun_def treeFsetI.coiter treeFsetIBNF_map_def by simp +lemma coiter_pair_fun_sub: "sub (treeFsetI_unf_coiter (f \ g) t) = map_fset (treeFsetI_unf_coiter (f \ g)) (g t)" +unfolding sub_def pair_fun_def treeFsetI.unf_coiter treeFsetIBNF_map_def by simp (* tree map (contrived example): *) -definition "tmap f \ treeFsetI_coiter (f o lab \ sub)" +definition "tmap f \ treeFsetI_unf_coiter (f o lab \ sub)" lemma tmap_simps1[simp]: "lab (tmap f t) = f (lab t)" unfolding tmap_def by (simp add: coiter_pair_fun_lab) diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Tools/bnf_fp_util.ML --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 04 17:23:08 2012 +0200 @@ -18,15 +18,17 @@ val coN: string val coinductN: string val coiterN: string - val coiter_uniqueN: string + val unf_coiter_uniqueN: string val corecN: string val exhaustN: string val fldN: string - val fld_coiterN: string + val fld_unf_coiterN: string val fld_exhaustN: string val fld_induct2N: string val fld_inductN: string val fld_injectN: string + val fld_iterN: string + val fld_recN: string val fld_unfN: string val hsetN: string val hset_recN: string @@ -34,7 +36,7 @@ val injectN: string val isNodeN: string val iterN: string - val iter_uniqueN: string + val fld_iter_uniqueN: string val lsbisN: string val map_simpsN: string val map_uniqueN: string @@ -56,6 +58,8 @@ val unfN: string val unf_coinductN: string val unf_coinduct_uptoN: string + val unf_coiterN: string + val unf_corecN: string val unf_exhaustN: string val unf_fldN: string val unf_injectN: string @@ -127,11 +131,13 @@ val iterN = "iter" val coiterN = coN ^ iterN val uniqueN = "_unique" -val iter_uniqueN = iterN ^ uniqueN -val coiter_uniqueN = coiterN ^ uniqueN val fldN = "fld" val unfN = "unf" -val fld_coiterN = fldN ^ "_" ^ coiterN +val fld_iterN = fldN ^ "_" ^ iterN +val unf_coiterN = unfN ^ "_" ^ coiterN +val fld_iter_uniqueN = fld_iterN ^ uniqueN +val unf_coiter_uniqueN = unf_coiterN ^ uniqueN +val fld_unf_coiterN = fldN ^ "_" ^ unf_coiterN val map_simpsN = mapN ^ "_simps" val map_uniqueN = mapN ^ uniqueN val min_algN = "min_alg" @@ -153,6 +159,8 @@ val str_initN = "str_init" val recN = "rec" val corecN = coN ^ recN +val fld_recN = fldN ^ "_" ^ recN +val unf_corecN = unfN ^ "_" ^ corecN val fld_unfN = fldN ^ "_" ^ unfN val unf_fldN = unfN ^ "_" ^ fldN diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Tools/bnf_gfp.ML --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 04 17:23:08 2012 +0200 @@ -1938,7 +1938,7 @@ val timer = time (timer "unf definitions & thms"); - fun coiter_bind i = Binding.suffix_name ("_" ^ coN ^ iterN) (nth bs (i - 1)); + fun coiter_bind i = Binding.suffix_name ("_" ^ unf_coiterN) (nth bs (i - 1)); val coiter_name = Binding.name_of o coiter_bind; val coiter_def_bind = rpair [] o Thm.def_binding o coiter_bind; @@ -2129,7 +2129,7 @@ trans OF [mor RS unique, coiter_unf]) coiter_unique_mor_thms coiter_unf_thms end; - fun corec_bind i = Binding.suffix_name ("_" ^ coN ^ recN) (nth bs (i - 1)); + fun corec_bind i = Binding.suffix_name ("_" ^ unf_corecN) (nth bs (i - 1)); val corec_name = Binding.name_of o corec_bind; val corec_def_bind = rpair [] o Thm.def_binding o corec_bind; @@ -2973,16 +2973,16 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = - [(coiterN, coiter_thms), - (coiter_uniqueN, coiter_unique_thms), - (corecN, corec_thms), + [(unf_coiterN, coiter_thms), + (unf_coiter_uniqueN, coiter_unique_thms), + (unf_corecN, corec_thms), (unf_fldN, unf_fld_thms), (fld_unfN, fld_unf_thms), (unf_injectN, unf_inject_thms), (unf_exhaustN, unf_exhaust_thms), (fld_injectN, fld_inject_thms), (fld_exhaustN, fld_exhaust_thms), - (fld_coiterN, fld_coiter_thms)] + (fld_unf_coiterN, fld_coiter_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => diff -r f7326a0d7f19 -r 1a86ef0a0210 src/HOL/Codatatype/Tools/bnf_lfp.ML --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 16:27:27 2012 +0200 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 04 17:23:08 2012 +0200 @@ -1052,7 +1052,7 @@ (mk_mor UNIVs flds active_UNIVs ss (map (mk_nthN n iter_f) ks)); val iter = HOLogic.choice_const iterT $ iter_fun; - fun iter_bind i = Binding.suffix_name ("_" ^ iterN) (nth bs (i - 1)); + fun iter_bind i = Binding.suffix_name ("_" ^ fld_iterN) (nth bs (i - 1)); val iter_name = Binding.name_of o iter_bind; val iter_def_bind = rpair [] o Thm.def_binding o iter_bind; @@ -1210,7 +1210,7 @@ trans OF [mor RS unique, iter_fld]) iter_unique_mor_thms iter_fld_thms end; - fun rec_bind i = Binding.suffix_name ("_" ^ recN) (nth bs (i - 1)); + fun rec_bind i = Binding.suffix_name ("_" ^ fld_recN) (nth bs (i - 1)); val rec_name = Binding.name_of o rec_bind; val rec_def_bind = rpair [] o Thm.def_binding o rec_bind; @@ -1797,9 +1797,9 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); val notes = - [(iterN, iter_thms), - (iter_uniqueN, iter_unique_thms), - (recN, rec_thms), + [(fld_iterN, iter_thms), + (fld_iter_uniqueN, iter_unique_thms), + (fld_recN, rec_thms), (unf_fldN, unf_fld_thms), (fld_unfN, fld_unf_thms), (unf_injectN, unf_inject_thms),