--- a/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy Fri Sep 28 09:12:49 2012 +0200
@@ -13,27 +13,14 @@
hide_fact (open) Quotient_Product.prod_rel_def
-typedecl N typedecl T
+typedecl N
+typedecl T
-codata_raw Tree: 'Tree = "N \<times> (T + 'Tree) fset"
+codata Tree = NNode (root: N) (ccont: "(T + Tree) fset")
section {* Sugar notations for Tree *}
-subsection{* Setup for map, set, rel *}
-
-(* These should be eventually inferred from compositionality *)
-
-lemma pre_Tree_map:
-"pre_Tree_map f (n, as) = (n, map_fset (id \<oplus> f) as)"
-unfolding pre_Tree_map_def id_apply
-sum_map_def by simp
-
-lemma pre_Tree_map':
-"pre_Tree_map f n_as = (fst n_as, map_fset (id \<oplus> f) (snd n_as))"
-using pre_Tree_map by(cases n_as, simp)
-
-
definition
"llift2 \<phi> as1 as2 \<longleftrightarrow>
(\<forall> n. Inl n \<in> fset as1 \<longleftrightarrow> Inl n \<in> fset as2) \<and>
@@ -52,79 +39,9 @@
done
-subsection{* Constructors *}
-
-definition NNode :: "N \<Rightarrow> (T + Tree)fset \<Rightarrow> Tree"
-where "NNode n as \<equiv> Tree_ctor (n,as)"
-
-lemmas ctor_defs = NNode_def
-
-
-subsection {* Pre-selectors *}
-
-(* These are mere auxiliaries *)
-
-definition "asNNode tr \<equiv> SOME n_as. NNode (fst n_as) (snd n_as) = tr"
-lemmas pre_sel_defs = asNNode_def
-
-
-subsection {* Selectors *}
-
-(* One for each pair (constructor, constructor argument) *)
-
-(* For NNode: *)
-definition root :: "Tree \<Rightarrow> N" where "root tr = fst (asNNode tr)"
-definition ccont :: "Tree \<Rightarrow> (T + Tree)fset" where "ccont tr = snd (asNNode tr)"
-
-lemmas sel_defs = root_def ccont_def
-
-
-subsection {* Basic properties *}
-
-(* Constructors versus selectors *)
-lemma NNode_surj: "\<exists> n as. NNode n as = tr"
-unfolding NNode_def
-by (metis Tree.ctor_dtor pair_collapse)
-
-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
- hence "NNode (fst (n,as)) (snd (n,as)) = tr" by simp
- thus ?thesis unfolding asNNode_def by(rule someI)
-qed
-
-theorem NNode_root_ccont[simp]:
-"NNode (root tr) (ccont tr) = tr"
-using NNode_asNNode unfolding root_def ccont_def .
-
-(* Constructors *)
-theorem TTree_simps[simp]:
-"NNode n as = NNode n' as' \<longleftrightarrow> n = n' \<and> as = as'"
-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.ctor_exhaust[of tr])
- fix x assume "tr = Tree_ctor x"
- thus ?thesis
- apply(cases x)
- using NNode unfolding ctor_defs apply blast
- done
-qed
-
-(* Constructors versus selectors *)
-theorem TTree_sel_ctor[simp]:
-"root (NNode n as) = n"
-"ccont (NNode n as) = as"
-unfolding root_def ccont_def
-by (metis (no_types) NNode_asNNode TTree_simps)+
-
-
subsection{* Coinduction *}
-theorem TTree_coind_Node[elim, consumes 1, case_names NNode, induct pred: "HOL.eq"]:
+theorem Tree_coind_NNode[elim, consumes 1, case_names NNode, induct pred: "HOL.eq"]:
assumes phi: "\<phi> tr1 tr2" and
NNode: "\<And> n1 n2 as1 as2.
\<lbrakk>\<phi> (NNode n1 as1) (NNode n2 as2)\<rbrakk> \<Longrightarrow>
@@ -141,70 +58,18 @@
theorem TTree_coind[elim, consumes 1, case_names LLift]:
assumes phi: "\<phi> tr1 tr2" and
-LLift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
- root tr1 = root tr2 \<and> llift2 \<phi> (ccont tr1) (ccont tr2)"
+LLift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> root tr1 = root tr2 \<and> llift2 \<phi> (ccont tr1) (ccont tr2)"
shows "tr1 = tr2"
-using phi apply(induct rule: TTree_coind_Node)
-using LLift by (metis TTree_sel_ctor)
-
-
-
-subsection {* Coiteration *}
-
-(* Preliminaries: *)
-declare Tree.dtor_ctor[simp]
-declare Tree.ctor_dtor[simp]
-
-lemma Tree_dtor_NNode[simp]:
-"Tree_dtor (NNode n as) = (n,as)"
-unfolding NNode_def Tree.dtor_ctor ..
-
-lemma Tree_dtor_root_ccont:
-"Tree_dtor tr = (root tr, ccont tr)"
-unfolding root_def ccont_def
-by (metis (lifting) NNode_asNNode Tree_dtor_NNode)
-
-(* Coiteration *)
-definition TTree_unfold ::
-"('b \<Rightarrow> N) \<Rightarrow> ('b \<Rightarrow> (T + 'b) fset) \<Rightarrow> 'b \<Rightarrow> Tree"
-where "TTree_unfold rt ct \<equiv> Tree_dtor_unfold <rt,ct>"
-
-lemma Tree_unfold_unfold:
-"Tree_dtor_unfold s = TTree_unfold (fst o s) (snd o s)"
-apply(rule ext)
-unfolding TTree_unfold_def by simp
-
-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_unfold[of "<rt,ct>" b] unfolding Tree_unfold_unfold fst_convol snd_convol
-unfolding pre_Tree_map' fst_convol' snd_convol'
-unfolding Tree_dtor_root_ccont by simp_all
-
-(* 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_dtor_corec <rt,ct>"
-
-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.dtor_corec[of "<rt,ct>" b] unfolding Tree_dtor_corec_corec fst_convol snd_convol
-unfolding pre_Tree_map' fst_convol' snd_convol'
-unfolding Tree_dtor_root_ccont by simp_all
+using phi apply(induct rule: Tree_coind_NNode)
+using LLift by (metis Tree.sels)
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 "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 "unfold rt ct \<equiv> Tree_unfold rt (the_inv fset o ct)"
+definition "corec rt ct \<equiv> Tree_corec rt (the_inv fset o ct)"
definition lift ("_ ^#" 200) where
"lift \<phi> as \<longleftrightarrow> (\<forall> tr. Inr tr \<in> as \<longrightarrow> \<phi> tr)"
@@ -259,19 +124,19 @@
theorem Node_root_cont[simp]:
"Node (root tr) (cont tr) = tr"
-using NNode_root_ccont unfolding Node_def cont_def
+using Tree.collapse unfolding Node_def cont_def
by (metis cont_def finite_cont fset_cong fset_to_fset o_def)
theorem Tree_simps[simp]:
assumes "finite as" and "finite as'"
shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'"
-using assms TTree_simps unfolding Node_def
+using assms Tree.inject unfolding Node_def
by (metis fset_to_fset)
theorem Tree_cases[elim, case_names Node Choice]:
assumes Node: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> phi"
shows phi
-apply(cases rule: TTree_cases[of tr])
+apply(cases rule: Tree.exhaust[of tr])
using Node unfolding Node_def
by (metis Node Node_root_cont finite_cont)
@@ -290,7 +155,7 @@
\<lbrakk>finite as1; finite as2; \<phi> (Node n1 as1) (Node n2 as2)\<rbrakk>
\<Longrightarrow> n1 = n2 \<and> (\<phi>^#2) as1 as2"
shows "tr1 = tr2"
-using phi apply(induct rule: TTree_coind_Node)
+using phi apply(induct rule: Tree_coind_NNode)
unfolding llift2_lift2 apply(rule Node)
unfolding Node_def
apply (metis finite_fset)
@@ -308,19 +173,18 @@
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
+using Tree.sel_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)
-
theorem corec:
"root (corec rt ct b) = rt b"
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
-using TTree_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
-apply - apply metis
-unfolding cont_def comp_def
+using Tree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def
+apply -
+apply simp
+unfolding cont_def comp_def id_def
by (metis (no_types) fset_to_fset map_fset_image)
-
end
--- a/src/HOL/BNF/Examples/TreeFsetI.thy Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy Fri Sep 28 09:12:49 2012 +0200
@@ -15,45 +15,24 @@
hide_const (open) Sublist.sub
hide_fact (open) Quotient_Product.prod_rel_def
+codata 'a treeFsetI = Tree (lab: 'a) (sub: "'a treeFsetI fset")
+
definition pair_fun (infixr "\<odot>" 50) where
"f \<odot> g \<equiv> \<lambda>x. (f x, g x)"
-codata_raw treeFsetI: 't = "'a \<times> 't fset"
-
-(* selectors for trees *)
-definition "lab t \<equiv> fst (treeFsetI_dtor t)"
-definition "sub t \<equiv> snd (treeFsetI_dtor t)"
-
-lemma dtor[simp]: "treeFsetI_dtor t = (lab t, sub t)"
-unfolding lab_def sub_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_unfold 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_unfold pre_treeFsetI_map_def by simp
+(* tree map (contrived example): *)
+definition tmap where
+"tmap f = treeFsetI_unfold (f o lab) sub"
-(* tree map (contrived example): *)
-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: unfold_pair_fun_lab)
-
-lemma trev_simps2[simp]: "sub (tmap f t) = map_fset (tmap f) (sub t)"
-unfolding tmap_def by (simp add: unfold_pair_fun_sub)
-
-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_rel_def prod_rel_def fset_rel_def)
-done
-
-lemmas treeFsetI_coind = mp[OF treeFsetI.dtor_coinduct]
+lemma tmap_simps[simp]:
+"lab (tmap f t) = f (lab t)"
+"sub (tmap f t) = map_fset (tmap f) (sub t)"
+unfolding tmap_def treeFsetI.sel_unfold by simp+
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)"])
- force+
+apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
+apply auto
+apply (unfold fset_rel_def)
+by auto
end
--- a/src/HOL/BNF/Tools/bnf_def.ML Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Fri Sep 28 09:12:49 2012 +0200
@@ -1125,7 +1125,8 @@
fun mk_rel_eq () =
unfold_thms lthy (bnf_srel_def :: mem_Collect_etc')
- (Lazy.force srel_Id RS @{thm arg_cong[of _ _ "%A x y. (x, y) : A"]});
+ (Lazy.force srel_Id RS @{thm arg_cong[of _ _ "%A x y. (x, y) : A"]})
+ |> Drule.eta_contraction_rule;
val rel_eq = Lazy.lazy mk_rel_eq;