--- 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 \<equiv> hfset_fld hs"
+definition "Fold hs \<equiv> hfset_ctor hs"
lemma hfset_simps[simp]:
"\<And>hs1 hs2. Fold hs1 = Fold hs2 \<longrightarrow> 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: "\<And> hs. h = Fold hs \<Longrightarrow> 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: "\<And> hs. (\<And> h. h |\<in>| hs \<Longrightarrow> phi h) \<Longrightarrow> 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 <id, hfset_fld_rec R> hs)"
-using hfset.fld_recs unfolding Fold_def .
+lemma hfset_ctor_rec:
+"hfset_ctor_rec R (Fold hs) = R (map_fset <id, hfset_ctor_rec R> 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
--- 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 \<Rightarrow> Tree" where
-"deftr \<equiv> coit id S"
+"deftr \<equiv> unfold id S"
lemma deftr_simps[simp]:
"root (deftr n) = n"
"cont (deftr n) = image (id \<oplus> 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 \<Rightarrow> Tree" where
-"hsubst \<equiv> coit hsubst_r hsubst_c"
+"hsubst \<equiv> 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 \<oplus> 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 \<noteq> root tr0"
shows "cont (hsubst tr) = (id \<oplus> 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 \<Rightarrow> Tree" where
-"regOf \<equiv> coit regOf_r regOf_c"
+"regOf \<equiv> 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 \<oplus> (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 \<oplus> (root \<circ> regOf \<circ> root)) t_tr = (id \<oplus> 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)
--- 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 \<times> Tree \<Rightarrow> Tree" where
-"par \<equiv> coit par_r par_c"
+"par \<equiv> unfold par_r par_c"
abbreviation par_abbr (infixr "\<parallel>" 80) where "tr1 \<parallel> tr2 \<equiv> par (tr1, tr2)"
@@ -42,11 +42,11 @@
using finite_cont by auto
lemma root_par: "root (tr1 \<parallel> 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 \<parallel> tr2) = (id \<oplus> 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]:
--- 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 @@
(\<forall> tr1. Inr tr1 \<in> fset as1 \<longrightarrow> (\<exists> tr2. Inr tr2 \<in> fset as2 \<and> \<phi> tr1 tr2)) \<and>
(\<forall> tr2. Inr tr2 \<in> fset as2 \<longrightarrow> (\<exists> tr1. Inr tr1 \<in> fset as1 \<and> \<phi> tr1 tr2))"
-lemma pre_Tree_pred: "pre_Tree_pred \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> 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 \<phi> (n1,as1) (n2,as2) \<longleftrightarrow> n1 = n2 \<and> llift2 \<phi> 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 \<Rightarrow> (T + Tree)fset \<Rightarrow> Tree"
-where "NNode n as \<equiv> Tree_fld (n,as)"
+where "NNode n as \<equiv> Tree_ctor (n,as)"
lemmas ctor_defs = NNode_def
@@ -84,7 +84,7 @@
(* Constructors versus selectors *)
lemma NNode_surj: "\<exists> 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' \<longleftrightarrow> n = n' \<and> 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: "\<And> n as. tr = NNode n as \<Longrightarrow> 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 @@
\<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow>
n1 = n2 \<and> llift2 \<phi> as1 as2"
shows "tr1 = tr2"
-apply(rule mp[OF Tree.pred_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
+apply(rule mp[OF Tree.rel_coinduct[of \<phi> tr1 tr2] phi]) proof clarify
fix tr1 tr2 assume \<phi>: "\<phi> tr1 tr2"
- show "pre_Tree_pred \<phi> (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 \<phi> (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 \<phi> unfolding NNode_def by simp
+ unfolding pre_Tree_rel apply(rule NNode) using \<phi> 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 \<Rightarrow> N) \<Rightarrow> ('b \<Rightarrow> (T + 'b) fset) \<Rightarrow> 'b \<Rightarrow> Tree"
-where "TTree_coit rt ct \<equiv> Tree_unf_coiter <rt,ct>"
+where "TTree_unfold rt ct \<equiv> Tree_dtor_unfold <rt,ct>"
-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 \<oplus> TTree_coit rt ct) (ct b)"
-using Tree.unf_coiters[of "<rt,ct>" 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 \<oplus> TTree_unfold rt ct) (ct b)"
+using Tree.dtor_unfolds[of "<rt,ct>" 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 \<Rightarrow> N) \<Rightarrow> ('b \<Rightarrow> (T + (Tree + 'b)) fset) \<Rightarrow> 'b \<Rightarrow> Tree"
-where "TTree_corec rt ct \<equiv> Tree_unf_corec <rt,ct>"
+where "TTree_corec rt ct \<equiv> Tree_dtor_corec <rt,ct>"
-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 \<oplus> ([[id, TTree_corec rt ct]]) ) (ct b)"
-using Tree.unf_corecs[of "<rt,ct>" b] unfolding Tree_unf_corec_corec fst_convol snd_convol
+using Tree.dtor_corecs[of "<rt,ct>" 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 \<equiv> NNode n (the_inv fset as)"
definition "cont \<equiv> fset o ccont"
-definition "coit rt ct \<equiv> TTree_coit rt (the_inv fset o ct)"
+definition "unfold rt ct \<equiv> TTree_unfold rt (the_inv fset o ct)"
definition "corec rt ct \<equiv> 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) \<Longrightarrow> cont (coit rt ct b) = image (id \<oplus> coit rt ct) (ct b)"
-using TTree_coit[of rt "the_inv fset \<circ> ct" b] unfolding coit_def
+theorem unfold:
+"root (unfold rt ct b) = rt b"
+"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)"
+using TTree_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def
apply - apply metis
unfolding cont_def comp_def
by (metis (no_types) fset_to_fset map_fset_image)
--- 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 \<equiv> trm_fld (Inl x)"
-definition "App t1 t2 \<equiv> trm_fld (Inr (Inl (t1,t2)))"
-definition "Lam x t \<equiv> trm_fld (Inr (Inr (Inl (x,t))))"
-definition "Lt xts t \<equiv> trm_fld (Inr (Inr (Inr (xts,t))))"
+definition "Var x \<equiv> trm_ctor (Inl x)"
+definition "App t1 t2 \<equiv> trm_ctor (Inr (Inl (t1,t2)))"
+definition "Lam x t \<equiv> trm_ctor (Inr (Inr (Inl (x,t))))"
+definition "Lt xts t \<equiv> trm_ctor (Inr (Inr (Inr (xts,t))))"
lemmas ctor_defs = Var_def App_def Lam_def Lt_def
@@ -62,7 +62,7 @@
"\<And> x t1 t2. Var x \<noteq> App t1 t2" "\<And>x y t. Var x \<noteq> Lam y t" "\<And> x xts t. Var x \<noteq> Lt xts t"
"\<And> t1 t2 x t. App t1 t2 \<noteq> Lam x t" "\<And> t1 t2 xts t. App t1 t2 \<noteq> Lt xts t"
"\<And>x t xts t1. Lam x t \<noteq> 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: "\<And> x. t = Var x \<Longrightarrow> phi"
@@ -70,8 +70,8 @@
and Lam: "\<And> x t1. t = Lam x t1 \<Longrightarrow> phi"
and Lt: "\<And> xts t1. t = Lt xts t1 \<Longrightarrow> 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: "\<And> x t. phi t \<Longrightarrow> phi (Lam x t)"
and Lt: "\<And> xts t. \<lbrakk>\<And> x1 t1. (x1,t1) |\<in>| xts \<Longrightarrow> phi t1; phi t\<rbrakk> \<Longrightarrow> phi (Lt xts t)"
shows "phi t"
-proof(induct rule: trm.fld_induct)
+proof(induct rule: trm.ctor_induct)
fix u :: "'a + 'a trm \<times> 'a trm + 'a \<times> 'a trm + ('a \<times> 'a trm) fset \<times> 'a trm"
assume IH: "\<And>t. t \<in> pre_trm_set2 u \<Longrightarrow> 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 \<equiv>
@@ -137,25 +137,25 @@
"\<And> 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 \<equiv> trm_fld_rec (sumJoin4 var app lam lt)"
+definition "trmrec var app lam lt \<equiv> 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 (\<lambda> (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 \<equiv>
@@ -174,30 +174,30 @@
unfolding sumJoinI4_def by auto
(* The iterator has a simpler, hence more manageable type. *)
-definition "trmiter var app lam lt \<equiv> trm_fld_iter (sumJoinI4 var app lam lt)"
+definition "trmfold var app lam lt \<equiv> 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 (\<lambda> (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 (\<lambda> (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
(\<lambda> x. {x})
(\<lambda> X1 X2. X1 \<union> X2)
(\<lambda> x X. X \<union> {x})
@@ -211,7 +211,7 @@
varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,varsOf t1)) xts})"
unfolding varsOf_def by simp_all
-definition "fvarsOf = trmiter
+definition "fvarsOf = trmfold
(\<lambda> x. {x})
(\<lambda> X1 X2. X1 \<union> X2)
(\<lambda> x X. X - {x})
--- 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 \<times> 'list"
-definition "NilF = listF_fld (Inl ())"
-definition "Conss a as \<equiv> listF_fld (Inr (a, as))"
+definition "NilF = listF_ctor (Inl ())"
+definition "Conss a as \<equiv> 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} \<union> 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: "\<And>x xs. P xs \<Longrightarrow> P (Conss x xs)"
shows "P xs"
-proof (rule listF.fld_induct)
+proof (rule listF.ctor_induct)
fix xs :: "unit + 'a \<times> 'a listF"
assume raw_IH: "\<And>a. a \<in> pre_listF_set2 xs \<Longrightarrow> 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 \<in> 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 \<equiv> Conss a NilF"
definition appendd (infixr "@@" 65) where
- "appendd \<equiv> listF_fld_iter (sum_case (\<lambda> _. id) (\<lambda> (a,f) bs. Conss a (f bs)))"
+ "appendd \<equiv> listF_ctor_fold (sum_case (\<lambda> _. id) (\<lambda> (a,f) bs. Conss a (f bs)))"
-definition "lrev \<equiv> listF_fld_iter (sum_case (\<lambda> _. NilF) (\<lambda> (b,bs). bs @@ [[b]]))"
+definition "lrev \<equiv> listF_ctor_fold (sum_case (\<lambda> _. NilF) (\<lambda> (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
--- 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: "\<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.pred_coinduct, of \<phi>, OF _ phi], clarify)
+proof(intro mp[OF process.rel_coinduct, of \<phi>, OF _ phi], clarify)
fix p p' assume \<phi>: "\<phi> p p'"
- show "pre_process_pred (op =) \<phi> (process_unf p) (process_unf 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 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 \<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 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: "\<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.pred_coinduct_upto, of \<phi>, OF _ phi], clarify)
+proof(intro mp[OF process.rel_strong_coinduct, of \<phi>, OF _ phi], clarify)
fix p p' assume \<phi>: "\<phi> p p'"
- show "pre_process_pred (op =) (\<lambda>a b. \<phi> a b \<or> a = b) (process_unf p) (process_unf 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 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 \<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 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 \<equiv>
- process_coiter
+ process_unfold
(\<lambda> P. True)
(\<lambda> P. ''a'')
(\<lambda> P. P)
@@ -135,7 +135,7 @@
lemma BX: "BX = Action ''a'' BX"
unfolding BX_def
-using process.coiters(1)[of "\<lambda> P. True" "()" "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
+using process.unfolds(1)[of "\<lambda> P. True" "()" "\<lambda> P. ''a''" "\<lambda> P. P"] by simp
subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
@@ -151,14 +151,14 @@
definition "c2 \<equiv> \<lambda> K. case K of x \<Rightarrow> y |y \<Rightarrow> undefined |ax \<Rightarrow> undefined"
lemmas Choice_defs = c1_def c2_def
-definition "F \<equiv> process_coiter isA pr co c1 c2"
+definition "F \<equiv> 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 \<equiv>
- 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 "\<not> 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:
--- 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 \<times> 's"
(* selectors for streams *)
-definition "hdd as \<equiv> fst (stream_unf as)"
-definition "tll as \<equiv> snd (stream_unf as)"
+definition "hdd as \<equiv> fst (stream_dtor as)"
+definition "tll as \<equiv> snd (stream_dtor as)"
-lemma coiter_pair_fun_hdd[simp]: "hdd (stream_unf_coiter (f \<odot> 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 \<odot> 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 \<odot> g) t) =
- stream_unf_coiter (f \<odot> 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 \<odot> g) t) =
+ stream_dtor_unfold (f \<odot> g) (g t)"
+unfolding tll_def pair_fun_def stream.dtor_unfolds by simp
(* infinite trees: *)
coinductive infiniteTr where
"\<lbrakk>tr' \<in> listF_set (sub tr); infiniteTr tr'\<rbrakk> \<Longrightarrow> infiniteTr tr"
-lemma infiniteTr_coind_upto[consumes 1, case_names sub]:
+lemma infiniteTr_strong_coind[consumes 1, case_names sub]:
assumes *: "phi tr" and
**: "\<And> tr. phi tr \<Longrightarrow> \<exists> tr' \<in> listF_set (sub tr). phi tr' \<or> infiniteTr tr'"
shows "infiniteTr tr"
@@ -48,7 +48,7 @@
"infiniteTr tr \<Longrightarrow> (\<exists> tr' \<in> listF_set (sub tr). infiniteTr tr')"
by (erule infiniteTr.cases) blast
-definition "konigPath \<equiv> stream_unf_coiter
+definition "konigPath \<equiv> stream_dtor_unfold
(lab \<odot> (\<lambda>tr. SOME tr'. tr' \<in> listF_set (sub tr) \<and> infiniteTr tr'))"
lemma hdd_simps1[simp]: "hdd (konigPath t) = lab t"
@@ -63,7 +63,7 @@
"\<lbrakk>hdd as = lab tr; tr' \<in> listF_set (sub tr); properPath (tll as) tr'\<rbrakk> \<Longrightarrow>
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
**: "\<And> as tr. phi as tr \<Longrightarrow> hdd as = lab tr" and
***: "\<And> as tr.
@@ -79,7 +79,7 @@
phi as tr \<Longrightarrow>
\<exists> tr' \<in> 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 \<Longrightarrow> 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 \<odot> tll)"
+lemma stream_map[simp]: "stream_map f = stream_dtor_unfold (f o hdd \<odot> 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 \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>2 (snd a) (snd b))"
-unfolding prod_pred_def by auto
+lemma prod_rel[simp]: "prod_rel \<phi>1 \<phi>2 a b = (\<phi>1 (fst a) (fst b) \<and> \<phi>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 \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<oplus>" 66) where
[simp]: "plus xs ys =
- stream_unf_coiter ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
+ stream_dtor_unfold ((%(xs, ys). hdd xs + hdd ys) \<odot> (%(xs, ys). (tll xs, tll ys))) (xs, ys)"
definition scalar :: "nat \<Rightarrow> nat stream \<Rightarrow> nat stream" (infixr "\<cdot>" 68) where
[simp]: "scalar n = stream_map (\<lambda>x. n * x)"
-definition ones :: "nat stream" where [simp]: "ones = stream_unf_coiter ((%x. 1) \<odot> id) ()"
-definition twos :: "nat stream" where [simp]: "twos = stream_unf_coiter ((%x. 2) \<odot> id) ()"
+definition ones :: "nat stream" where [simp]: "ones = stream_dtor_unfold ((%x. 1) \<odot> id) ()"
+definition twos :: "nat stream" where [simp]: "twos = stream_dtor_unfold ((%x. 2) \<odot> id) ()"
definition ns :: "nat \<Rightarrow> nat stream" where [simp]: "ns n = scalar n ones"
lemma "ones \<oplus> ones = twos"
--- 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 \<equiv> fst (treeFI_unf tr)"
-definition "sub tr \<equiv> snd (treeFI_unf tr)"
+definition "lab tr \<equiv> fst (treeFI_dtor tr)"
+definition "sub tr \<equiv> 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 "\<odot>" 50) where
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-lemma coiter_pair_fun_lab: "lab (treeFI_unf_coiter (f \<odot> 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 \<odot> 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 \<odot> g) t) = listF_map (treeFI_unf_coiter (f \<odot> 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 \<odot> g) t) = listF_map (treeFI_dtor_unfold (f \<odot> g)) (g t)"
+unfolding sub_def pair_fun_def treeFI.dtor_unfolds pre_treeFI_map_def by simp
(* Tree reverse:*)
-definition "trev \<equiv> treeFI_unf_coiter (lab \<odot> lrev o sub)"
+definition "trev \<equiv> treeFI_dtor_unfold (lab \<odot> 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) \<and>
(\<forall>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)"
"\<forall>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 "\<forall>(x, y) \<in> 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 "\<exists>z.
- (pre_treeFI_map id fst z = treeFI_unf a \<and>
- pre_treeFI_map id snd z = treeFI_unf b) \<and>
+ (pre_treeFI_map id fst z = treeFI_dtor a \<and>
+ pre_treeFI_map id snd z = treeFI_dtor b) \<and>
(\<forall>x y. (x, y) \<in> pre_treeFI_set2 z \<longrightarrow> phi x y)" by blast
qed
--- 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 "\<odot>" 50) where
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
@@ -21,36 +21,36 @@
codata_raw treeFsetI: 't = "'a \<times> 't fset"
(* selectors for trees *)
-definition "lab t \<equiv> fst (treeFsetI_unf t)"
-definition "sub t \<equiv> snd (treeFsetI_unf t)"
+definition "lab t \<equiv> fst (treeFsetI_dtor t)"
+definition "sub t \<equiv> 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 \<odot> 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 \<odot> 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 \<odot> g) t) = map_fset (treeFsetI_unf_coiter (f \<odot> 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 \<odot> g) t) = map_fset (treeFsetI_dtor_unfold (f \<odot> 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 \<equiv> treeFsetI_unf_coiter (f o lab \<odot> sub)"
+definition "tmap f \<equiv> treeFsetI_dtor_unfold (f o lab \<odot> 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) \<and>
+lemma pre_treeFsetI_rel[simp]: "pre_treeFsetI_rel R1 R2 a b = (R1 (fst a) (fst b) \<and>
(\<forall>t \<in> fset (snd a). (\<exists>u \<in> fset (snd b). R2 t u)) \<and>
(\<forall>t \<in> fset (snd b). (\<exists>u \<in> 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. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])