# HG changeset patch # User blanchet # Date 1348816369 -7200 # Node ID 9ce0c2cbadb8afe34db941d8bf2fc9a343c984d1 # Parent 99700c4e0b33a4bcefd91ee9cec7011395dd2326 modernized example diff -r 99700c4e0b33 -r 9ce0c2cbadb8 src/HOL/BNF/Examples/Infinite_Derivation_Trees/Tree.thy --- 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 \ (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 \ 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 \ f) (snd n_as))" -using pre_Tree_map by(cases n_as, simp) - - definition "llift2 \ as1 as2 \ (\ n. Inl n \ fset as1 \ Inl n \ fset as2) \ @@ -52,79 +39,9 @@ done -subsection{* Constructors *} - -definition NNode :: "N \ (T + Tree)fset \ Tree" -where "NNode n as \ Tree_ctor (n,as)" - -lemmas ctor_defs = NNode_def - - -subsection {* Pre-selectors *} - -(* These are mere auxiliaries *) - -definition "asNNode tr \ 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 \ N" where "root tr = fst (asNNode tr)" -definition ccont :: "Tree \ (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: "\ 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' \ n = n' \ as = as'" -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.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: "\ tr1 tr2" and NNode: "\ n1 n2 as1 as2. \\ (NNode n1 as1) (NNode n2 as2)\ \ @@ -141,70 +58,18 @@ theorem TTree_coind[elim, consumes 1, case_names LLift]: assumes phi: "\ tr1 tr2" and -LLift: "\ tr1 tr2. \ tr1 tr2 \ - root tr1 = root tr2 \ llift2 \ (ccont tr1) (ccont tr2)" +LLift: "\ tr1 tr2. \ tr1 tr2 \ root tr1 = root tr2 \ llift2 \ (ccont tr1) (ccont tr2)" shows "tr1 = tr2" -using phi apply(induct rule: TTree_coind_Node) -using LLift by (metis TTree_sel_ctor) - - - -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 \ N) \ ('b \ (T + 'b) fset) \ 'b \ Tree" -where "TTree_unfold rt ct \ Tree_dtor_unfold " - -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 \ TTree_unfold rt ct) (ct b)" -using Tree.dtor_unfold[of "" 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 \ N) \ ('b \ (T + (Tree + 'b)) fset) \ 'b \ Tree" -where "TTree_corec rt ct \ Tree_dtor_corec " - -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.dtor_corec[of "" 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 \ NNode n (the_inv fset as)" definition "cont \ fset o ccont" -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 "unfold rt ct \ Tree_unfold rt (the_inv fset o ct)" +definition "corec rt ct \ Tree_corec rt (the_inv fset o ct)" definition lift ("_ ^#" 200) where "lift \ as \ (\ tr. Inr tr \ as \ \ 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' \ n = n' \ 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: "\ n as. \finite as; tr = Node n as\ \ 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 @@ \finite as1; finite as2; \ (Node n1 as1) (Node n2 as2)\ \ n1 = n2 \ (\^#2) as1 as2" shows "tr1 = tr2" -using phi apply(induct rule: TTree_coind_Node) +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) \ 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 +using Tree.sel_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) - theorem corec: "root (corec rt ct b) = rt b" "finite (ct b) \ cont (corec rt ct b) = image (id \ ([[id, corec rt ct]])) (ct b)" -using TTree_corec[of rt "the_inv fset \ ct" b] unfolding corec_def -apply - apply metis -unfolding cont_def comp_def +using Tree.sel_corec[of rt "the_inv fset \ 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 diff -r 99700c4e0b33 -r 9ce0c2cbadb8 src/HOL/BNF/Examples/TreeFsetI.thy --- 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 "\" 50) where "f \ g \ \x. (f x, g x)" -codata_raw treeFsetI: 't = "'a \ 't fset" - -(* selectors for trees *) -definition "lab t \ fst (treeFsetI_dtor t)" -definition "sub t \ 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 \ 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 \ g) t) = map_fset (treeFsetI_dtor_unfold (f \ 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 \ treeFsetI_dtor_unfold (f o lab \ 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) \ - (\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_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. \x. x1 = tmap (f o g) x \ x2 = tmap f (tmap g x)"]) - force+ +apply (rule treeFsetI.coinduct[of "%x1 x2. \x. x1 = tmap (f o g) x \ x2 = tmap f (tmap g x)"]) +apply auto +apply (unfold fset_rel_def) +by auto end diff -r 99700c4e0b33 -r 9ce0c2cbadb8 src/HOL/BNF/Tools/bnf_def.ML --- 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;