# HG changeset patch # User blanchet # Date 1348235609 -7200 # Node ID 1e205327f0592f6fcd5f071240fa6b979cfd7979 # Parent 8826d5a4332b56318ef34fc3c72e17438bc8de62 adapted examples to renamings diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/HFset.thy --- a/src/HOL/Codatatype/Examples/HFset.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/HFset.thy Fri Sep 21 15:53:29 2012 +0200 @@ -21,22 +21,22 @@ subsection{* Constructors *} -definition "Fold hs \ hfset_fld hs" +definition "Fold hs \ hfset_ctor hs" lemma hfset_simps[simp]: "\hs1 hs2. Fold hs1 = Fold hs2 \ hs1 = hs2" -unfolding Fold_def hfset.fld_inject by auto +unfolding Fold_def hfset.ctor_inject by auto theorem hfset_cases[elim, case_names Fold]: assumes Fold: "\ hs. h = Fold hs \ phi" shows phi using Fold unfolding Fold_def -by (cases rule: hfset.fld_exhaust[of h]) simp +by (cases rule: hfset.ctor_exhaust[of h]) simp lemma hfset_induct[case_names Fold, induct type: hfset]: assumes Fold: "\ hs. (\ h. h |\| hs \ phi h) \ phi (Fold hs)" shows "phi t" -apply (induct rule: hfset.fld_induct) +apply (induct rule: hfset.ctor_induct) using Fold unfolding Fold_def fset_fset_member mem_Collect_eq .. (* alternative induction principle, using fset: *) @@ -46,15 +46,15 @@ apply (induct rule: hfset_induct) using Fold by (metis notin_fset) -subsection{* Recursion and iteration *} +subsection{* Recursion and iteration (fold) *} -lemma hfset_fld_rec: -"hfset_fld_rec R (Fold hs) = R (map_fset hs)" -using hfset.fld_recs unfolding Fold_def . +lemma hfset_ctor_rec: +"hfset_ctor_rec R (Fold hs) = R (map_fset hs)" +using hfset.ctor_recs unfolding Fold_def . (* The iterator has a simpler form: *) -lemma hfset_fld_iter: -"hfset_fld_iter R (Fold hs) = R (map_fset (hfset_fld_iter R) hs)" -using hfset.fld_iters unfolding Fold_def . +lemma hfset_ctor_fold: +"hfset_ctor_fold R (Fold hs) = R (map_fset (hfset_ctor_fold R) hs)" +using hfset.ctor_folds unfolding Fold_def . end diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Gram_Lang.thy Fri Sep 21 15:53:29 2012 +0200 @@ -468,12 +468,12 @@ (* The default tree of a nonterminal *) definition deftr :: "N \ Tree" where -"deftr \ coit id S" +"deftr \ unfold id S" lemma deftr_simps[simp]: "root (deftr n) = n" "cont (deftr n) = image (id \ deftr) (S n)" -using coit(1)[of id S n] coit(2)[of S n id, OF finite_S] +using unfold(1)[of id S n] unfold(2)[of S n id, OF finite_S] unfolding deftr_def by simp_all lemmas root_deftr = deftr_simps(1) @@ -509,13 +509,13 @@ (* Hereditary substitution: *) definition hsubst :: "Tree \ Tree" where -"hsubst \ coit hsubst_r hsubst_c" +"hsubst \ unfold hsubst_r hsubst_c" lemma finite_hsubst_c: "finite (hsubst_c n)" unfolding hsubst_c_def by (metis finite_cont) lemma root_hsubst[simp]: "root (hsubst tr) = root tr" -using coit(1)[of hsubst_r hsubst_c tr] unfolding hsubst_def hsubst_r_def by simp +using unfold(1)[of hsubst_r hsubst_c tr] unfolding hsubst_def hsubst_r_def by simp lemma root_o_subst[simp]: "root o hsubst = root" unfolding comp_def root_hsubst .. @@ -524,7 +524,7 @@ assumes "root tr = root tr0" shows "cont (hsubst tr) = (id \ hsubst) ` (cont tr0)" apply(subst id_o[symmetric, of id]) unfolding id_o -using coit(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c] +using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c] unfolding hsubst_def hsubst_c_def using assms by simp lemma hsubst_eq: @@ -536,7 +536,7 @@ assumes "root tr \ root tr0" shows "cont (hsubst tr) = (id \ hsubst) ` (cont tr)" apply(subst id_o[symmetric, of id]) unfolding id_o -using coit(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c] +using unfold(2)[of hsubst_c tr hsubst_r, OF finite_hsubst_c] unfolding hsubst_def hsubst_c_def using assms by simp lemma Inl_cont_hsubst_eq[simp]: @@ -951,13 +951,13 @@ (* The regular tree of a function: *) definition regOf :: "N \ Tree" where -"regOf \ coit regOf_r regOf_c" +"regOf \ unfold regOf_r regOf_c" lemma finite_regOf_c: "finite (regOf_c n)" unfolding regOf_c_def by (metis finite_cont finite_imageI) lemma root_regOf_pick: "root (regOf n) = root (pick n)" -using coit(1)[of regOf_r regOf_c n] unfolding regOf_def regOf_r_def by simp +using unfold(1)[of regOf_r regOf_c n] unfolding regOf_def regOf_r_def by simp lemma root_regOf[simp]: assumes "inItr UNIV tr0 n" @@ -968,7 +968,7 @@ "cont (regOf n) = (id \ (regOf o root)) ` cont (pick n)" apply(subst id_o[symmetric, of id]) unfolding sum_map.comp[symmetric] unfolding image_compose unfolding regOf_c_def[symmetric] -using coit(2)[of regOf_c n regOf_r, OF finite_regOf_c] +using unfold(2)[of regOf_c n regOf_r, OF finite_regOf_c] unfolding regOf_def .. lemma Inl_cont_regOf[simp]: @@ -1010,7 +1010,7 @@ shows "(id \ (root \ regOf \ root)) t_tr = (id \ root) t_tr" using assms apply(cases t_tr) apply (metis (lifting) sum_map.simps(1)) - using pick regOf_def regOf_r_def coit(1) + using pick regOf_def regOf_r_def unfold(1) inItr.Base o_apply subtr_StepL subtr_inItr sum_map.simps(2) by (metis UNIV_I) diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Parallel.thy Fri Sep 21 15:53:29 2012 +0200 @@ -31,7 +31,7 @@ declare par_r.simps[simp del] declare par_c.simps[simp del] definition par :: "Tree \ Tree \ Tree" where -"par \ coit par_r par_c" +"par \ unfold par_r par_c" abbreviation par_abbr (infixr "\" 80) where "tr1 \ tr2 \ par (tr1, tr2)" @@ -42,11 +42,11 @@ using finite_cont by auto lemma root_par: "root (tr1 \ tr2) = root tr1 + root tr2" -using coit(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp +using unfold(1)[of par_r par_c "(tr1,tr2)"] unfolding par_def par_r.simps by simp lemma cont_par: "cont (tr1 \ tr2) = (id \ par) ` par_c (tr1,tr2)" -using coit(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c] +using unfold(2)[of par_c "(tr1,tr2)" par_r, OF finite_par_c] unfolding par_def .. lemma Inl_cont_par[simp]: diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy --- a/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Infinite_Derivation_Trees/Tree.thy Fri Sep 21 15:53:29 2012 +0200 @@ -2,16 +2,16 @@ Author: Andrei Popescu, TU Muenchen Copyright 2012 -Trees with nonterminal internal nodes and terminal leafs. +Trees with nonterminal internal nodes and terminal leaves. *) -header {* Trees with nonterminal internal nodes and terminal leafs *} +header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *} theory Tree imports Prelim begin -hide_fact (open) Quotient_Product.prod_pred_def +hide_fact (open) Quotient_Product.prod_rel_def typedecl N typedecl T @@ -20,7 +20,7 @@ section {* Sugar notations for Tree *} -subsection{* Setup for map, set, pred *} +subsection{* Setup for map, set, rel *} (* These should be eventually inferred from compositionality *) @@ -40,8 +40,8 @@ (\ 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 pre_Tree_pred: "pre_Tree_pred \ (n1,as1) (n2,as2) \ n1 = n2 \ llift2 \ as1 as2" -unfolding llift2_def pre_Tree_pred_def sum_pred_def[abs_def] prod_pred_def fset_pred_def split_conv +lemma pre_Tree_rel: "pre_Tree_rel \ (n1,as1) (n2,as2) \ n1 = n2 \ llift2 \ as1 as2" +unfolding llift2_def pre_Tree_rel_def sum_rel_def[abs_def] prod_rel_def fset_rel_def split_conv apply (auto split: sum.splits) apply (metis sumE) apply (metis sumE) @@ -55,7 +55,7 @@ subsection{* Constructors *} definition NNode :: "N \ (T + Tree)fset \ Tree" -where "NNode n as \ Tree_fld (n,as)" +where "NNode n as \ Tree_ctor (n,as)" lemmas ctor_defs = NNode_def @@ -84,7 +84,7 @@ (* 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.ctor_dtor pair_collapse) lemma NNode_asNNode: "NNode (fst (asNNode tr)) (snd (asNNode tr)) = tr" @@ -101,13 +101,13 @@ (* Constructors *) theorem TTree_simps[simp]: "NNode n as = NNode n' as' \ n = n' \ as = as'" -unfolding ctor_defs Tree.fld_inject by auto +unfolding ctor_defs Tree.ctor_inject by auto theorem TTree_cases[elim, case_names NNode Choice]: assumes NNode: "\ n as. tr = NNode n as \ phi" shows phi -proof(cases rule: Tree.fld_exhaust[of tr]) - fix x assume "tr = Tree_fld x" +proof(cases rule: Tree.ctor_exhaust[of tr]) + fix x assume "tr = Tree_ctor x" thus ?thesis apply(cases x) using NNode unfolding ctor_defs apply blast @@ -130,13 +130,13 @@ \\ (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 +apply(rule mp[OF Tree.rel_coinduct[of \ tr1 tr2] phi]) proof clarify fix tr1 tr2 assume \: "\ tr1 tr2" - show "pre_Tree_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) + show "pre_Tree_rel \ (Tree_dtor tr1) (Tree_dtor tr2)" + apply(cases rule: Tree.ctor_exhaust[of tr1], cases rule: Tree.ctor_exhaust[of tr2]) + apply (simp add: Tree.dtor_ctor) apply(case_tac x, case_tac xa, simp) - unfolding pre_Tree_pred apply(rule NNode) using \ unfolding NNode_def by simp + unfolding pre_Tree_rel apply(rule NNode) using \ unfolding NNode_def by simp qed theorem TTree_coind[elim, consumes 1, case_names LLift]: @@ -152,58 +152,58 @@ subsection {* Coiteration *} (* Preliminaries: *) -declare Tree.unf_fld[simp] -declare Tree.fld_unf[simp] +declare Tree.dtor_ctor[simp] +declare Tree.ctor_dtor[simp] -lemma Tree_unf_NNode[simp]: -"Tree_unf (NNode n as) = (n,as)" -unfolding NNode_def Tree.unf_fld .. +lemma Tree_dtor_NNode[simp]: +"Tree_dtor (NNode n as) = (n,as)" +unfolding NNode_def Tree.dtor_ctor .. -lemma Tree_unf_root_ccont: -"Tree_unf tr = (root tr, ccont tr)" +lemma Tree_dtor_root_ccont: +"Tree_dtor tr = (root tr, ccont tr)" unfolding root_def ccont_def -by (metis (lifting) NNode_asNNode Tree_unf_NNode) +by (metis (lifting) NNode_asNNode Tree_dtor_NNode) (* Coiteration *) -definition TTree_coit :: +definition TTree_unfold :: "('b \ N) \ ('b \ (T + 'b) fset) \ 'b \ Tree" -where "TTree_coit rt ct \ Tree_unf_coiter " +where "TTree_unfold rt ct \ Tree_dtor_unfold " -lemma Tree_coit_coit: -"Tree_unf_coiter s = TTree_coit (fst o s) (snd o s)" +lemma Tree_unfold_unfold: +"Tree_dtor_unfold s = TTree_unfold (fst o s) (snd o s)" apply(rule ext) -unfolding TTree_coit_def by simp +unfolding TTree_unfold_def by simp -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.unf_coiters[of "" b] unfolding Tree_coit_coit fst_convol snd_convol +theorem TTree_unfold: +"root (TTree_unfold rt ct b) = rt b" +"ccont (TTree_unfold rt ct b) = map_fset (id \ TTree_unfold rt ct) (ct b)" +using Tree.dtor_unfolds[of "" b] unfolding Tree_unfold_unfold fst_convol snd_convol unfolding pre_Tree_map' fst_convol' snd_convol' -unfolding Tree_unf_root_ccont by simp_all +unfolding Tree_dtor_root_ccont by simp_all -(* Corecursion, stronger than coiteration *) +(* Corecursion, stronger than coiteration (unfold) *) definition TTree_corec :: "('b \ N) \ ('b \ (T + (Tree + 'b)) fset) \ 'b \ Tree" -where "TTree_corec rt ct \ Tree_unf_corec " +where "TTree_corec rt ct \ Tree_dtor_corec " -lemma Tree_unf_corec_corec: -"Tree_unf_corec s = TTree_corec (fst o s) (snd o s)" +lemma Tree_dtor_corec_corec: +"Tree_dtor_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" "ccont (TTree_corec rt ct b) = map_fset (id \ ([[id, TTree_corec rt ct]]) ) (ct b)" -using Tree.unf_corecs[of "" b] unfolding Tree_unf_corec_corec fst_convol snd_convol +using Tree.dtor_corecs[of "" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol unfolding pre_Tree_map' fst_convol' snd_convol' -unfolding Tree_unf_root_ccont by simp_all +unfolding Tree_dtor_root_ccont by simp_all subsection{* The characteristic theorems transported from fset to set *} definition "Node n as \ NNode n (the_inv fset as)" definition "cont \ fset o ccont" -definition "coit rt ct \ TTree_coit rt (the_inv fset o ct)" +definition "unfold rt ct \ TTree_unfold rt (the_inv fset o ct)" definition "corec rt ct \ TTree_corec rt (the_inv fset o ct)" definition lift ("_ ^#" 200) where @@ -305,10 +305,10 @@ 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" -"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 +theorem unfold: +"root (unfold rt ct b) = rt b" +"finite (ct b) \ cont (unfold rt ct b) = image (id \ unfold rt ct) (ct b)" +using TTree_unfold[of rt "the_inv fset \ ct" b] unfolding unfold_def apply - apply metis unfolding cont_def comp_def by (metis (no_types) fset_to_fset map_fset_image) diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/Lambda_Term.thy --- a/src/HOL/Codatatype/Examples/Lambda_Term.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Lambda_Term.thy Fri Sep 21 15:53:29 2012 +0200 @@ -46,10 +46,10 @@ subsection{* Constructors *} -definition "Var x \ trm_fld (Inl x)" -definition "App t1 t2 \ trm_fld (Inr (Inl (t1,t2)))" -definition "Lam x t \ trm_fld (Inr (Inr (Inl (x,t))))" -definition "Lt xts t \ trm_fld (Inr (Inr (Inr (xts,t))))" +definition "Var x \ trm_ctor (Inl x)" +definition "App t1 t2 \ trm_ctor (Inr (Inl (t1,t2)))" +definition "Lam x t \ trm_ctor (Inr (Inr (Inl (x,t))))" +definition "Lt xts t \ trm_ctor (Inr (Inr (Inr (xts,t))))" lemmas ctor_defs = Var_def App_def Lam_def Lt_def @@ -62,7 +62,7 @@ "\ x t1 t2. Var x \ App t1 t2" "\x y t. Var x \ Lam y t" "\ x xts t. Var x \ Lt xts t" "\ t1 t2 x t. App t1 t2 \ Lam x t" "\ t1 t2 xts t. App t1 t2 \ Lt xts t" "\x t xts t1. Lam x t \ Lt xts t1" -unfolding ctor_defs trm.fld_inject by auto +unfolding ctor_defs trm.ctor_inject by auto theorem trm_cases[elim, case_names Var App Lam Lt]: assumes Var: "\ x. t = Var x \ phi" @@ -70,8 +70,8 @@ and Lam: "\ x t1. t = Lam x t1 \ phi" and Lt: "\ xts t1. t = Lt xts t1 \ phi" shows phi -proof(cases rule: trm.fld_exhaust[of t]) - fix x assume "t = trm_fld x" +proof(cases rule: trm.ctor_exhaust[of t]) + fix x assume "t = trm_ctor x" thus ?thesis apply(cases x) using Var unfolding ctor_defs apply blast apply(case_tac b) using App unfolding ctor_defs apply(case_tac a, blast) @@ -85,10 +85,10 @@ and Lam: "\ x t. phi t \ phi (Lam x t)" and Lt: "\ xts t. \\ x1 t1. (x1,t1) |\| xts \ phi t1; phi t\ \ phi (Lt xts t)" shows "phi t" -proof(induct rule: trm.fld_induct) +proof(induct rule: trm.ctor_induct) fix u :: "'a + 'a trm \ 'a trm + 'a \ 'a trm + ('a \ 'a trm) fset \ 'a trm" assume IH: "\t. t \ pre_trm_set2 u \ phi t" - show "phi (trm_fld u)" + show "phi (trm_ctor u)" proof(cases u) case (Inl x) show ?thesis using Var unfolding Var_def Inl . @@ -119,7 +119,7 @@ qed -subsection{* Recursion and iteration *} +subsection{* Recursion and iteration (fold) *} definition "sumJoin4 f1 f2 f3 f4 \ @@ -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_fld_rec (sumJoin4 var app lam lt)" +definition "trmrec var app lam lt \ trm_ctor_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.fld_recs pre_trm_map(1) by simp +unfolding trmrec_def Var_def trm.ctor_recs pre_trm_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.fld_recs pre_trm_map(2) convol_def by simp +unfolding trmrec_def App_def trm.ctor_recs pre_trm_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.fld_recs pre_trm_map(3) convol_def by simp +unfolding trmrec_def Lam_def trm.ctor_recs pre_trm_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.fld_recs pre_trm_map(4) convol_def by simp +unfolding trmrec_def Lt_def trm.ctor_recs pre_trm_map(4) convol_def by simp definition "sumJoinI4 f1 f2 f3 f4 \ @@ -174,30 +174,30 @@ unfolding sumJoinI4_def by auto (* The iterator has a simpler, hence more manageable type. *) -definition "trmiter var app lam lt \ trm_fld_iter (sumJoinI4 var app lam lt)" +definition "trmfold var app lam lt \ trm_ctor_fold (sumJoinI4 var app lam lt)" -lemma trmiter_Var[simp]: -"trmiter var app lam lt (Var x) = var x" -unfolding trmiter_def Var_def trm.fld_iters pre_trm_map(1) by simp +lemma trmfold_Var[simp]: +"trmfold var app lam lt (Var x) = var x" +unfolding trmfold_def Var_def trm.ctor_folds pre_trm_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.fld_iters pre_trm_map(2) by simp +lemma trmfold_App[simp]: +"trmfold var app lam lt (App t1 t2) = + app (trmfold var app lam lt t1) (trmfold var app lam lt t2)" +unfolding trmfold_def App_def trm.ctor_folds pre_trm_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.fld_iters pre_trm_map(3) by simp +lemma trmfold_Lam[simp]: +"trmfold var app lam lt (Lam x t) = lam x (trmfold var app lam lt t)" +unfolding trmfold_def Lam_def trm.ctor_folds pre_trm_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.fld_iters pre_trm_map(4) by simp +lemma trmfold_Lt[simp]: +"trmfold var app lam lt (Lt xts t) = + lt (map_fset (\ (x,t). (x,trmfold var app lam lt t)) xts) (trmfold var app lam lt t)" +unfolding trmfold_def Lt_def trm.ctor_folds pre_trm_map(4) by simp subsection{* Example: The set of all variables varsOf and free variables fvarsOf of a term: *} -definition "varsOf = trmiter +definition "varsOf = trmfold (\ x. {x}) (\ X1 X2. X1 \ X2) (\ x X. X \ {x}) @@ -211,7 +211,7 @@ varsOf t \ (\ { {x} \ X | x X. (x,X) |\| map_fset (\ (x,t1). (x,varsOf t1)) xts})" unfolding varsOf_def by simp_all -definition "fvarsOf = trmiter +definition "fvarsOf = trmfold (\ x. {x}) (\ X1 X2. X1 \ X2) (\ x X. X - {x}) diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/ListF.thy --- a/src/HOL/Codatatype/Examples/ListF.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/ListF.thy Fri Sep 21 15:53:29 2012 +0200 @@ -14,49 +14,49 @@ data_raw listF: 'list = "unit + 'a \ 'list" -definition "NilF = listF_fld (Inl ())" -definition "Conss a as \ listF_fld (Inr (a, as))" +definition "NilF = listF_ctor (Inl ())" +definition "Conss a as \ listF_ctor (Inr (a, as))" lemma listF_map_NilF[simp]: "listF_map f NilF = NilF" -unfolding listF_map_def pre_listF_map_def NilF_def listF.fld_iters by simp +unfolding listF_map_def pre_listF_map_def NilF_def listF.ctor_folds by simp lemma listF_map_Conss[simp]: "listF_map f (Conss x xs) = Conss (f x) (listF_map f xs)" -unfolding listF_map_def pre_listF_map_def Conss_def listF.fld_iters by simp +unfolding listF_map_def pre_listF_map_def Conss_def listF.ctor_folds by simp lemma listF_set_NilF[simp]: "listF_set NilF = {}" -unfolding listF_set_def NilF_def listF.fld_iters pre_listF_set1_def pre_listF_set2_def +unfolding listF_set_def NilF_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def sum_set_defs pre_listF_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.fld_iters pre_listF_set1_def pre_listF_set2_def +unfolding listF_set_def Conss_def listF.ctor_folds pre_listF_set1_def pre_listF_set2_def sum_set_defs prod_set_defs pre_listF_map_def collect_def[abs_def] by simp -lemma iter_sum_case_NilF: "listF_fld_iter (sum_case f g) NilF = f ()" -unfolding NilF_def listF.fld_iters pre_listF_map_def by simp +lemma fold_sum_case_NilF: "listF_ctor_fold (sum_case f g) NilF = f ()" +unfolding NilF_def listF.ctor_folds pre_listF_map_def by simp -lemma iter_sum_case_Conss: - "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_iters pre_listF_map_def by simp +lemma fold_sum_case_Conss: + "listF_ctor_fold (sum_case f g) (Conss y ys) = g (y, listF_ctor_fold (sum_case f g) ys)" +unfolding Conss_def listF.ctor_folds pre_listF_map_def by simp (* familiar induction principle *) lemma listF_induct: fixes xs :: "'a listF" assumes IB: "P NilF" and IH: "\x xs. P xs \ P (Conss x xs)" shows "P xs" -proof (rule listF.fld_induct) +proof (rule listF.ctor_induct) fix xs :: "unit + 'a \ 'a listF" assume raw_IH: "\a. a \ pre_listF_set2 xs \ P a" - show "P (listF_fld xs)" + show "P (listF_ctor xs)" proof (cases xs) case (Inl a) with IB show ?thesis unfolding NilF_def by simp next case (Inr b) - then obtain y ys where yys: "listF_fld xs = Conss y ys" - unfolding Conss_def listF.fld_inject by (blast intro: prod.exhaust) + then obtain y ys where yys: "listF_ctor xs = Conss y ys" + unfolding Conss_def listF.ctor_inject by (blast intro: prod.exhaust) hence "ys \ pre_listF_set2 xs" - unfolding pre_listF_set2_def Conss_def listF.fld_inject sum_set_defs prod_set_defs + unfolding pre_listF_set2_def Conss_def listF.ctor_inject sum_set_defs prod_set_defs collect_def[abs_def] by simp with raw_IH have "P ys" by blast with IH have "P (Conss y ys)" by blast @@ -65,27 +65,27 @@ qed rep_datatype NilF Conss -by (blast intro: listF_induct) (auto simp add: NilF_def Conss_def listF.fld_inject) +by (blast intro: listF_induct) (auto simp add: NilF_def Conss_def listF.ctor_inject) definition Singll ("[[_]]") where [simp]: "Singll a \ Conss a NilF" definition appendd (infixr "@@" 65) where - "appendd \ listF_fld_iter (sum_case (\ _. id) (\ (a,f) bs. Conss a (f bs)))" + "appendd \ listF_ctor_fold (sum_case (\ _. id) (\ (a,f) bs. Conss a (f bs)))" -definition "lrev \ listF_fld_iter (sum_case (\ _. NilF) (\ (b,bs). bs @@ [[b]]))" +definition "lrev \ listF_ctor_fold (sum_case (\ _. NilF) (\ (b,bs). bs @@ [[b]]))" lemma lrev_NilF[simp]: "lrev NilF = NilF" -unfolding lrev_def by (simp add: iter_sum_case_NilF) +unfolding lrev_def by (simp add: fold_sum_case_NilF) lemma lrev_Conss[simp]: "lrev (Conss y ys) = lrev ys @@ [[y]]" -unfolding lrev_def by (simp add: iter_sum_case_Conss) +unfolding lrev_def by (simp add: fold_sum_case_Conss) lemma NilF_appendd[simp]: "NilF @@ ys = ys" -unfolding appendd_def by (simp add: iter_sum_case_NilF) +unfolding appendd_def by (simp add: fold_sum_case_NilF) lemma Conss_append[simp]: "Conss x xs @@ ys = Conss x (xs @@ ys)" -unfolding appendd_def by (simp add: iter_sum_case_Conss) +unfolding appendd_def by (simp add: fold_sum_case_Conss) lemma appendd_NilF[simp]: "xs @@ NilF = xs" by (rule listF_induct) auto diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/Process.thy --- a/src/HOL/Codatatype/Examples/Process.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Process.thy Fri Sep 21 15:53:29 2012 +0200 @@ -11,7 +11,7 @@ imports "../Codatatype" begin -hide_fact (open) Quotient_Product.prod_pred_def +hide_fact (open) Quotient_Product.prod_rel_def codata 'a process = isAction: Action (prefOf: 'a) (contOf: "'a process") | @@ -24,9 +24,9 @@ subsection {* Basic properties *} declare - pre_process_pred_def[simp] - sum_pred_def[simp] - prod_pred_def[simp] + pre_process_rel_def[simp] + sum_rel_def[simp] + prod_rel_def[simp] (* Constructors versus discriminators *) theorem isAction_isChoice: @@ -45,61 +45,61 @@ Act: "\ a a' p p'. \ (Action a p) (Action a' p') \ a = a' \ \ p p'" and Ch: "\ p q p' q'. \ (Choice p q) (Choice p' q') \ \ p p' \ \ q q'" shows "p = p'" -proof(intro mp[OF process.pred_coinduct, of \, OF _ phi], clarify) +proof(intro mp[OF process.rel_coinduct, of \, OF _ phi], clarify) fix p p' assume \: "\ p p'" - show "pre_process_pred (op =) \ (process_unf p) (process_unf p')" + show "pre_process_rel (op =) \ (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 \] 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' \ \ q q'" using Act[OF \[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 + 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 \] 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: "\ p1 p1' \ \ p2 p2'" using Ch[OF \[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 - show ?thesis using 0 unfolding unf by simp + 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 (* Stronger coinduction, up to equality: *) -theorem process_coind_upto[elim, consumes 1, case_names iss Action Choice]: +theorem process_strong_coind[elim, consumes 1, case_names iss Action Choice]: assumes phi: "\ p p'" and iss: "\p p'. \ p p' \ (isAction p \ isAction p') \ (isChoice p \ isChoice p')" and Act: "\ a a' p p'. \ (Action a p) (Action a' p') \ a = a' \ (\ p p' \ p = p')" and Ch: "\ p q p' q'. \ (Choice p q) (Choice p' q') \ (\ p p' \ p = p') \ (\ q q' \ q = q')" shows "p = p'" -proof(intro mp[OF process.pred_coinduct_upto, of \, OF _ phi], clarify) +proof(intro mp[OF process.rel_strong_coinduct, of \, OF _ phi], clarify) fix p p' assume \: "\ p p'" - show "pre_process_pred (op =) (\a b. \ a b \ a = b) (process_unf p) (process_unf p')" + show "pre_process_rel (op =) (\a b. \ a b \ 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 \] 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' \ (\ q q' \ q = q')" using Act[OF \[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 + 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 \] 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: "(\ p1 p1' \ p1 = p1') \ (\ p2 p2' \ p2 = p2')" using Ch[OF \[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 - show ?thesis using 0 unfolding unf by simp + 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 -subsection {* Coiteration *} +subsection {* Coiteration (unfold) *} section{* Coinductive definition of the notion of trace *} @@ -125,7 +125,7 @@ definition "BX \ - process_coiter + process_unfold (\ P. True) (\ P. ''a'') (\ P. P) @@ -135,7 +135,7 @@ lemma BX: "BX = Action ''a'' BX" unfolding BX_def -using process.coiters(1)[of "\ P. True" "()" "\ P. ''a''" "\ P. P"] by simp +using process.unfolds(1)[of "\ P. True" "()" "\ P. ''a''" "\ P. P"] by simp subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *} @@ -151,14 +151,14 @@ definition "c2 \ \ K. case K of x \ y |y \ undefined |ax \ undefined" lemmas Choice_defs = c1_def c2_def -definition "F \ process_coiter isA pr co c1 c2" +definition "F \ process_unfold 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 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] +using process.unfolds(2)[of isA x "pr" co c1 c2] + process.unfolds(1)[of isA y "pr" co c1 c2] + process.unfolds(1)[of isA ax "pr" co c1 c2] unfolding Action_defs Choice_defs by simp_all (* end product: *) @@ -226,7 +226,7 @@ definition "solution sys \ - process_coiter + process_unfold (isACT sys) (PREF sys) (CONT sys) @@ -237,14 +237,14 @@ assumes "isACT sys T" shows "solution sys T = Action (PREF sys T) (solution sys (CONT sys T))" unfolding solution_def -using process.coiters(1)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"] +using process.unfolds(1)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"] assms by simp lemma solution_Choice: assumes "\ isACT sys T" shows "solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))" unfolding solution_def -using process.coiters(2)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"] +using process.unfolds(2)[of "isACT sys" T "PREF sys" "CONT sys" "CH1 sys" "CH2 sys"] assms by simp lemma isACT_VAR: diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/Stream.thy --- a/src/HOL/Codatatype/Examples/Stream.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/Stream.thy Fri Sep 21 15:53:29 2012 +0200 @@ -12,27 +12,27 @@ imports TreeFI begin -hide_const (open) Quotient_Product.prod_pred -hide_fact (open) Quotient_Product.prod_pred_def +hide_const (open) Quotient_Product.prod_rel +hide_fact (open) Quotient_Product.prod_rel_def codata_raw stream: 's = "'a \ 's" (* selectors for streams *) -definition "hdd as \ fst (stream_unf as)" -definition "tll as \ snd (stream_unf as)" +definition "hdd as \ fst (stream_dtor as)" +definition "tll as \ snd (stream_dtor as)" -lemma coiter_pair_fun_hdd[simp]: "hdd (stream_unf_coiter (f \ g) t) = f t" -unfolding hdd_def pair_fun_def stream.unf_coiters by simp +lemma unfold_pair_fun_hdd[simp]: "hdd (stream_dtor_unfold (f \ g) t) = f t" +unfolding hdd_def pair_fun_def stream.dtor_unfolds 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_coiters by simp +lemma unfold_pair_fun_tll[simp]: "tll (stream_dtor_unfold (f \ g) t) = + stream_dtor_unfold (f \ g) (g t)" +unfolding tll_def pair_fun_def stream.dtor_unfolds by simp (* infinite trees: *) coinductive infiniteTr where "\tr' \ listF_set (sub tr); infiniteTr tr'\ \ infiniteTr tr" -lemma infiniteTr_coind_upto[consumes 1, case_names sub]: +lemma infiniteTr_strong_coind[consumes 1, case_names sub]: assumes *: "phi tr" and **: "\ tr. phi tr \ \ tr' \ listF_set (sub tr). phi tr' \ infiniteTr tr'" shows "infiniteTr tr" @@ -48,7 +48,7 @@ "infiniteTr tr \ (\ tr' \ listF_set (sub tr). infiniteTr tr')" by (erule infiniteTr.cases) blast -definition "konigPath \ stream_unf_coiter +definition "konigPath \ stream_dtor_unfold (lab \ (\tr. SOME tr'. tr' \ listF_set (sub tr) \ infiniteTr tr'))" lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t" @@ -63,7 +63,7 @@ "\hdd as = lab tr; tr' \ listF_set (sub tr); properPath (tll as) tr'\ \ properPath as tr" -lemma properPath_coind_upto[consumes 1, case_names hdd_lab sub]: +lemma properPath_strong_coind[consumes 1, case_names hdd_lab sub]: assumes *: "phi as tr" and **: "\ as tr. phi as tr \ hdd as = lab tr" and ***: "\ as tr. @@ -79,7 +79,7 @@ phi as tr \ \ tr' \ listF_set (sub tr). phi (tll as) tr'" shows "properPath as tr" -using properPath_coind_upto[of phi, OF * **] *** by blast +using properPath_strong_coind[of phi, OF * **] *** by blast lemma properPath_hdd_lab: "properPath as tr \ hdd as = lab tr" @@ -114,25 +114,25 @@ (* some more stream theorems *) -lemma stream_map[simp]: "stream_map f = stream_unf_coiter (f o hdd \ tll)" +lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (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 -lemma prod_pred[simp]: "prod_pred \1 \2 a b = (\1 (fst a) (fst b) \ \2 (snd a) (snd b))" -unfolding prod_pred_def by auto +lemma prod_rel[simp]: "prod_rel \1 \2 a b = (\1 (fst a) (fst b) \ \2 (snd a) (snd b))" +unfolding prod_rel_def by auto -lemmas stream_coind = mp[OF stream.pred_coinduct, unfolded prod_pred[abs_def], - folded hdd_def tll_def] +lemmas stream_coind = + mp[OF stream.rel_coinduct, unfolded prod_rel[abs_def], folded hdd_def tll_def] definition plus :: "nat stream \ nat stream \ nat stream" (infixr "\" 66) where [simp]: "plus xs ys = - stream_unf_coiter ((%(xs, ys). hdd xs + hdd ys) \ (%(xs, ys). (tll xs, tll ys))) (xs, ys)" + stream_dtor_unfold ((%(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_unf_coiter ((%x. 1) \ id) ()" -definition twos :: "nat stream" where [simp]: "twos = stream_unf_coiter ((%x. 2) \ id) ()" +definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \ id) ()" +definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \ id) ()" definition ns :: "nat \ nat stream" where [simp]: "ns n = scalar n ones" lemma "ones \ ones = twos" diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/TreeFI.thy --- a/src/HOL/Codatatype/Examples/TreeFI.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFI.thy Fri Sep 21 15:53:29 2012 +0200 @@ -21,29 +21,29 @@ by (auto simp add: listF.set_natural') (* selectors for trees *) -definition "lab tr \ fst (treeFI_unf tr)" -definition "sub tr \ snd (treeFI_unf tr)" +definition "lab tr \ fst (treeFI_dtor tr)" +definition "sub tr \ snd (treeFI_dtor tr)" -lemma unf[simp]: "treeFI_unf tr = (lab tr, sub tr)" +lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)" unfolding lab_def sub_def by simp definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" -lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \ g) t) = f t" -unfolding lab_def pair_fun_def treeFI.unf_coiters pre_treeFI_map_def by simp +lemma unfold_pair_fun_lab: "lab (treeFI_dtor_unfold (f \ g) t) = f t" +unfolding lab_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_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_coiters pre_treeFI_map_def by simp +lemma unfold_pair_fun_sub: "sub (treeFI_dtor_unfold (f \ g) t) = listF_map (treeFI_dtor_unfold (f \ g)) (g t)" +unfolding sub_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_map_def by simp (* Tree reverse:*) -definition "trev \ treeFI_unf_coiter (lab \ lrev o sub)" +definition "trev \ treeFI_dtor_unfold (lab \ lrev o sub)" lemma trev_simps1[simp]: "lab (trev t) = lab t" -unfolding trev_def by (simp add: coiter_pair_fun_lab) +unfolding trev_def by (simp add: unfold_pair_fun_lab) lemma trev_simps2[simp]: "sub (trev t) = listF_map trev (lrev (sub t))" -unfolding trev_def by (simp add: coiter_pair_fun_sub) +unfolding trev_def by (simp add: unfold_pair_fun_sub) lemma treeFI_coinduct: assumes *: "phi x y" @@ -52,14 +52,14 @@ lengthh (sub a) = lengthh (sub b) \ (\i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i))" shows "x = y" -proof (rule mp[OF treeFI.unf_coinduct, of phi, OF _ *]) +proof (rule mp[OF treeFI.dtor_coinduct, of phi, OF _ *]) fix a b :: "'a treeFI" let ?zs = "zipp (sub a) (sub b)" let ?z = "(lab a, ?zs)" assume "phi a b" with step have step': "lab a = lab b" "lengthh (sub a) = lengthh (sub b)" "\i < lengthh (sub a). phi (nthh (sub a) i) (nthh (sub b) i)" by auto - hence "pre_treeFI_map id fst ?z = treeFI_unf a" "pre_treeFI_map id snd ?z = treeFI_unf b" + hence "pre_treeFI_map id fst ?z = treeFI_dtor a" "pre_treeFI_map id snd ?z = treeFI_dtor b" unfolding pre_treeFI_map_def by auto moreover have "\(x, y) \ pre_treeFI_set2 ?z. phi x y" proof safe @@ -72,8 +72,8 @@ with step'(3) show "phi z1 z2" by auto qed ultimately show "\z. - (pre_treeFI_map id fst z = treeFI_unf a \ - pre_treeFI_map id snd z = treeFI_unf b) \ + (pre_treeFI_map id fst z = treeFI_dtor a \ + pre_treeFI_map id snd z = treeFI_dtor b) \ (\x y. (x, y) \ pre_treeFI_set2 z \ phi x y)" by blast qed diff -r 8826d5a4332b -r 1e205327f059 src/HOL/Codatatype/Examples/TreeFsetI.thy --- a/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 21 15:53:29 2012 +0200 +++ b/src/HOL/Codatatype/Examples/TreeFsetI.thy Fri Sep 21 15:53:29 2012 +0200 @@ -13,7 +13,7 @@ begin hide_const (open) Sublist.sub -hide_fact (open) Quotient_Product.prod_pred_def +hide_fact (open) Quotient_Product.prod_rel_def definition pair_fun (infixr "\" 50) where "f \ g \ \x. (f x, g x)" @@ -21,36 +21,36 @@ codata_raw treeFsetI: 't = "'a \ 't fset" (* selectors for trees *) -definition "lab t \ fst (treeFsetI_unf t)" -definition "sub t \ snd (treeFsetI_unf t)" +definition "lab t \ fst (treeFsetI_dtor t)" +definition "sub t \ snd (treeFsetI_dtor t)" -lemma unf[simp]: "treeFsetI_unf t = (lab t, sub t)" +lemma dtor[simp]: "treeFsetI_dtor t = (lab t, sub t)" unfolding lab_def sub_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_coiters pre_treeFsetI_map_def by simp +lemma unfold_pair_fun_lab: "lab (treeFsetI_dtor_unfold (f \ g) t) = f t" +unfolding lab_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_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_coiters pre_treeFsetI_map_def by simp +lemma unfold_pair_fun_sub: "sub (treeFsetI_dtor_unfold (f \ g) t) = map_fset (treeFsetI_dtor_unfold (f \ g)) (g t)" +unfolding sub_def pair_fun_def treeFsetI.dtor_unfolds pre_treeFsetI_map_def by simp (* tree map (contrived example): *) -definition "tmap f \ treeFsetI_unf_coiter (f o lab \ sub)" +definition "tmap f \ treeFsetI_dtor_unfold (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) +unfolding tmap_def by (simp add: unfold_pair_fun_lab) lemma trev_simps2[simp]: "sub (tmap f t) = map_fset (tmap f) (sub t)" -unfolding tmap_def by (simp add: coiter_pair_fun_sub) +unfolding tmap_def by (simp add: unfold_pair_fun_sub) -lemma pre_treeFsetI_pred[simp]: "pre_treeFsetI_pred R1 R2 a b = (R1 (fst a) (fst b) \ +lemma pre_treeFsetI_rel[simp]: "pre_treeFsetI_rel R1 R2 a b = (R1 (fst a) (fst b) \ (\t \ fset (snd a). (\u \ fset (snd b). R2 t u)) \ (\t \ fset (snd b). (\u \ fset (snd a). R2 u t)))" apply (cases a) apply (cases b) -apply (simp add: pre_treeFsetI_pred_def prod_pred_def fset_pred_def) +apply (simp add: pre_treeFsetI_rel_def prod_rel_def fset_rel_def) done -lemmas treeFsetI_coind = mp[OF treeFsetI.pred_coinduct] +lemmas treeFsetI_coind = mp[OF treeFsetI.rel_coinduct] lemma "tmap (f o g) x = tmap f (tmap g x)" by (intro treeFsetI_coind[where P="%x1 x2. \x. x1 = tmap (f o g) x \ x2 = tmap f (tmap g x)"])