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 \<equiv> NNode n (the_inv fset as)"
blanchet@48975
    22
definition "cont \<equiv> fset o ccont"
blanchet@55931
    23
definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (map_sum id Inr) o ct)"
blanchet@54536
    24
definition "corec rt ct \<equiv> 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' \<longleftrightarrow> n = n' \<and> 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: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> 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 \<Longrightarrow> 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 \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (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: "\<phi> tr1 tr2" and
blanchet@49128
    69
Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow>
blanchet@55938
    70
                  root tr1 = root tr2 \<and> rel_set (sum_rel op = \<phi>) (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) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> 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) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)"
blanchet@52350
    86
using dtree.sel_corec[of rt "the_inv fset \<circ> 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