author | kuncar |
Tue, 13 Aug 2013 15:59:22 +0200 | |
changeset 53013 | 3fbcfa911863 |
parent 52350 | 7e352bb76009 |
child 54014 | 21dac9a60f0c |
permissions | -rw-r--r-- |
50530 | 1 |
(* Title: HOL/BNF/Examples/Derivation_Trees/DTree.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
5 |
Derivation trees with nonterminal internal nodes and terminal leaves. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
49508 | 8 |
header {* Trees with Nonterminal Internal Nodes and Terminal Leaves *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
10 |
theory DTree |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
imports Prelim |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
53013
3fbcfa911863
remove unnecessary dependencies on Library/Quotient_*
kuncar
parents:
52350
diff
changeset
|
14 |
hide_fact (open) Lifting_Product.prod_rel_def |
49463 | 15 |
|
49631 | 16 |
typedecl N |
17 |
typedecl T |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51410
diff
changeset
|
19 |
codatatype dtree = NNode (root: N) (ccont: "(T + dtree) fset") |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
|
49882 | 21 |
subsection{* Transporting the Characteristic Lemmas from @{text "fset"} to @{text "set"} *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
definition "Node n as \<equiv> NNode n (the_inv fset as)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
definition "cont \<equiv> fset o ccont" |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
25 |
definition "unfold rt ct \<equiv> dtree_unfold rt (the_inv fset o ct)" |
52350 | 26 |
definition "corec rt ct \<equiv> dtree_corec rt (the_inv fset o ct)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
lemma finite_cont[simp]: "finite (cont tr)" |
52350 | 29 |
unfolding cont_def o_apply by (cases tr, clarsimp) (transfer, simp) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
31 |
lemma Node_root_cont[simp]: |
51410
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
32 |
"Node (root tr) (cont tr) = tr" |
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
33 |
unfolding Node_def cont_def o_apply |
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
34 |
apply (rule trans[OF _ dtree.collapse]) |
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
35 |
apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]]) |
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
36 |
apply transfer apply simp_all |
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
37 |
done |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
39 |
lemma dtree_simps[simp]: |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
40 |
assumes "finite as" and "finite as'" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
shows "Node n as = Node n' as' \<longleftrightarrow> n = n' \<and> as = as'" |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
42 |
using assms dtree.inject unfolding Node_def |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
by (metis fset_to_fset) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
45 |
lemma dtree_cases[elim, case_names Node Choice]: |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
assumes Node: "\<And> n as. \<lbrakk>finite as; tr = Node n as\<rbrakk> \<Longrightarrow> phi" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
shows phi |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
48 |
apply(cases rule: dtree.exhaust[of tr]) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
49 |
using Node unfolding Node_def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
50 |
by (metis Node Node_root_cont finite_cont) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
51 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
52 |
lemma dtree_sel_ctor[simp]: |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49076
diff
changeset
|
53 |
"root (Node n as) = n" |
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49076
diff
changeset
|
54 |
"finite as \<Longrightarrow> cont (Node n as) = as" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
unfolding Node_def cont_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
57 |
lemmas root_Node = dtree_sel_ctor(1) |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
58 |
lemmas cont_Node = dtree_sel_ctor(2) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
59 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
60 |
lemma dtree_cong: |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
61 |
assumes "root tr = root tr'" and "cont tr = cont tr'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
62 |
shows "tr = tr'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
63 |
by (metis Node_root_cont assms) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
64 |
|
49879 | 65 |
lemma set_rel_cont: |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
66 |
"set_rel \<chi> (cont tr1) (cont tr2) = fset_rel \<chi> (ccont tr1) (ccont tr2)" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
67 |
unfolding cont_def comp_def fset_rel_fset .. |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
68 |
|
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
69 |
lemma dtree_coinduct[elim, consumes 1, case_names Lift, induct pred: "HOL.eq"]: |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49076
diff
changeset
|
70 |
assumes phi: "\<phi> tr1 tr2" and |
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49076
diff
changeset
|
71 |
Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
72 |
root tr1 = root tr2 \<and> set_rel (sum_rel op = \<phi>) (cont tr1) (cont tr2)" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
shows "tr1 = tr2" |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
74 |
using phi apply(elim dtree.coinduct) |
49879 | 75 |
apply(rule Lift[unfolded set_rel_cont]) . |
76 |
||
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
77 |
lemma unfold: |
49508 | 78 |
"root (unfold rt ct b) = rt b" |
79 |
"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)" |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
80 |
using dtree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
apply - apply metis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
unfolding cont_def comp_def |
51410
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
83 |
by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
85 |
lemma corec: |
52350 | 86 |
"root (corec rt ct b) = rt b" |
87 |
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)" |
|
88 |
using dtree.sel_corec[of rt "the_inv fset \<circ> ct" b] unfolding corec_def |
|
49631 | 89 |
apply - |
90 |
apply simp |
|
91 |
unfolding cont_def comp_def id_def |
|
51410
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
92 |
by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
end |