src/HOL/BNF_Examples/Derivation_Trees/DTree.thy
 author blanchet Thu Mar 06 14:57:14 2014 +0100 (2014-03-06) changeset 55938 f20d1db5aa3c parent 55933 12ee2c407dad child 55943 5c2df04e97d1 permissions -rw-r--r--
renamed 'set_rel' to 'rel_set'
 blanchet@55075 ` 1` ```(* Title: HOL/BNF_Examples/Derivation_Trees/DTree.thy ``` blanchet@48975 ` 2` ``` Author: Andrei Popescu, TU Muenchen ``` blanchet@48975 ` 3` ``` Copyright 2012 ``` blanchet@48975 ` 4` popescua@49877 ` 5` ```Derivation trees with nonterminal internal nodes and terminal leaves. ``` blanchet@48975 ` 6` ```*) ``` blanchet@48975 ` 7` blanchet@49508 ` 8` ```header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *} ``` blanchet@48975 ` 9` popescua@49877 ` 10` ```theory DTree ``` blanchet@48975 ` 11` ```imports Prelim ``` blanchet@48975 ` 12` ```begin ``` blanchet@48975 ` 13` blanchet@49631 ` 14` ```typedecl N ``` blanchet@49631 ` 15` ```typedecl T ``` blanchet@48975 ` 16` blanchet@51804 ` 17` ```codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset") ``` blanchet@48975 ` 18` traytel@49882 ` 19` ```subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *} ``` blanchet@48975 ` 20` blanchet@48975 ` 21` ```definition "Node n as \ NNode n (the_inv fset as)" ``` blanchet@48975 ` 22` ```definition "cont \ fset o ccont" ``` blanchet@55931 ` 23` ```definition "unfold rt ct \ corec_dtree rt (the_inv fset o image (map_sum id Inr) o ct)" ``` blanchet@54536 ` 24` ```definition "corec rt ct \ corec_dtree rt (the_inv fset o ct)" ``` blanchet@48975 ` 25` blanchet@48975 ` 26` ```lemma finite_cont[simp]: "finite (cont tr)" ``` blanchet@55066 ` 27` ``` unfolding cont_def comp_apply by (cases tr, clarsimp) ``` blanchet@48975 ` 28` popescua@49877 ` 29` ```lemma Node_root_cont[simp]: ``` traytel@51410 ` 30` ``` "Node (root tr) (cont tr) = tr" ``` blanchet@55066 ` 31` ``` unfolding Node_def cont_def comp_apply ``` traytel@51410 ` 32` ``` apply (rule trans[OF _ dtree.collapse]) ``` traytel@51410 ` 33` ``` apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]]) ``` traytel@54014 ` 34` ``` apply (simp_all add: fset_inject) ``` traytel@51410 ` 35` ``` done ``` blanchet@48975 ` 36` popescua@49877 ` 37` ```lemma dtree_simps[simp]: ``` blanchet@48975 ` 38` ```assumes "finite as" and "finite as'" ``` blanchet@48975 ` 39` ```shows "Node n as = Node n' as' \ n = n' \ as = as'" ``` popescua@49877 ` 40` ```using assms dtree.inject unfolding Node_def ``` blanchet@48975 ` 41` ```by (metis fset_to_fset) ``` blanchet@48975 ` 42` popescua@49877 ` 43` ```lemma dtree_cases[elim, case_names Node Choice]: ``` blanchet@48975 ` 44` ```assumes Node: "\ n as. \finite as; tr = Node n as\ \ phi" ``` blanchet@48975 ` 45` ```shows phi ``` popescua@49877 ` 46` ```apply(cases rule: dtree.exhaust[of tr]) ``` blanchet@48975 ` 47` ```using Node unfolding Node_def ``` blanchet@48975 ` 48` ```by (metis Node Node_root_cont finite_cont) ``` blanchet@48975 ` 49` popescua@49877 ` 50` ```lemma dtree_sel_ctor[simp]: ``` blanchet@49128 ` 51` ```"root (Node n as) = n" ``` blanchet@49128 ` 52` ```"finite as \ cont (Node n as) = as" ``` blanchet@48975 ` 53` ```unfolding Node_def cont_def by auto ``` blanchet@48975 ` 54` popescua@49877 ` 55` ```lemmas root_Node = dtree_sel_ctor(1) ``` popescua@49877 ` 56` ```lemmas cont_Node = dtree_sel_ctor(2) ``` blanchet@48975 ` 57` popescua@49877 ` 58` ```lemma dtree_cong: ``` popescua@49877 ` 59` ```assumes "root tr = root tr'" and "cont tr = cont tr'" ``` popescua@49877 ` 60` ```shows "tr = tr'" ``` popescua@49877 ` 61` ```by (metis Node_root_cont assms) ``` blanchet@48975 ` 62` blanchet@55938 ` 63` ```lemma rel_set_cont: ``` blanchet@55938 ` 64` ```"rel_set \ (cont tr1) (cont tr2) = rel_fset \ (ccont tr1) (ccont tr2)" ``` blanchet@55933 ` 65` ```unfolding cont_def comp_def rel_fset_fset .. ``` popescua@49877 ` 66` popescua@49877 ` 67` ```lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]: ``` blanchet@49128 ` 68` ```assumes phi: "\ tr1 tr2" and ``` blanchet@49128 ` 69` ```Lift: "\ tr1 tr2. \ tr1 tr2 \ ``` blanchet@55938 ` 70` ``` root tr1 = root tr2 \ rel_set (sum_rel op = \) (cont tr1) (cont tr2)" ``` blanchet@48975 ` 71` ```shows "tr1 = tr2" ``` popescua@49877 ` 72` ```using phi apply(elim dtree.coinduct) ``` blanchet@55938 ` 73` ```apply(rule Lift[unfolded rel_set_cont]) . ``` traytel@49879 ` 74` popescua@49877 ` 75` ```lemma unfold: ``` blanchet@49508 ` 76` ```"root (unfold rt ct b) = rt b" ``` blanchet@49508 ` 77` ```"finite (ct b) \ cont (unfold rt ct b) = image (id \ unfold rt ct) (ct b)" ``` blanchet@55931 ` 78` ```using dtree.sel_corec[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def ``` blanchet@55857 ` 79` ```apply blast ``` blanchet@48975 ` 80` ```unfolding cont_def comp_def ``` blanchet@55931 ` 81` ```by (simp add: case_sum_o_inj map_sum.compositionality image_image) ``` blanchet@48975 ` 82` popescua@49877 ` 83` ```lemma corec: ``` blanchet@52350 ` 84` ```"root (corec rt ct b) = rt b" ``` blanchet@52350 ` 85` ```"finite (ct b) \ cont (corec rt ct b) = image (id \ ([[id, corec rt ct]])) (ct b)" ``` blanchet@52350 ` 86` ```using dtree.sel_corec[of rt "the_inv fset \ ct" b] unfolding corec_def ``` blanchet@49631 ` 87` ```unfolding cont_def comp_def id_def ``` blanchet@55857 ` 88` ```by simp_all ``` blanchet@48975 ` 89` blanchet@48975 ` 90` ```end ```