author | blanchet |
Thu, 11 Sep 2014 19:26:59 +0200 | |
changeset 58309 | a09ec6daaa19 |
parent 57991 | src/HOL/BNF_Examples/Derivation_Trees/DTree.thy@f50b3726266f |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
57991
diff
changeset
|
1 |
(* Title: HOL/Datatype_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 |
|
49631 | 14 |
typedecl N |
15 |
typedecl T |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51410
diff
changeset
|
17 |
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
|
18 |
|
49882 | 19 |
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
|
20 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
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
|
22 |
definition "cont \<equiv> fset o ccont" |
55931 | 23 |
definition "unfold rt ct \<equiv> corec_dtree rt (the_inv fset o image (map_sum id Inr) o ct)" |
54536 | 24 |
definition "corec rt ct \<equiv> corec_dtree 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
|
25 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
lemma finite_cont[simp]: "finite (cont tr)" |
55066 | 27 |
unfolding cont_def comp_apply by (cases tr, clarsimp) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
29 |
lemma Node_root_cont[simp]: |
51410
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
30 |
"Node (root tr) (cont tr) = tr" |
55066 | 31 |
unfolding Node_def cont_def comp_apply |
51410
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
32 |
apply (rule trans[OF _ dtree.collapse]) |
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
33 |
apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]]) |
54014 | 34 |
apply (simp_all add: fset_inject) |
51410
f0865a641e76
BNF uses fset defined via Lifting/Transfer rather than Quotient
traytel
parents:
50530
diff
changeset
|
35 |
done |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
36 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
37 |
lemma dtree_simps[simp]: |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
by (metis fset_to_fset) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
43 |
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
|
44 |
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
|
45 |
shows phi |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
46 |
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
|
47 |
using Node unfolding Node_def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
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
|
49 |
|
57991
f50b3726266f
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents:
57983
diff
changeset
|
50 |
lemma dtree_sel_ctr[simp]: |
49128
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49076
diff
changeset
|
51 |
"root (Node n as) = n" |
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49076
diff
changeset
|
52 |
"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
|
53 |
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
|
54 |
|
57991
f50b3726266f
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents:
57983
diff
changeset
|
55 |
lemmas root_Node = dtree_sel_ctr(1) |
f50b3726266f
don't note low-level (co)datatype theorems, unless 'bnf_note_all' is set
blanchet
parents:
57983
diff
changeset
|
56 |
lemmas cont_Node = dtree_sel_ctr(2) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
58 |
lemma dtree_cong: |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
59 |
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
|
60 |
shows "tr = tr'" |
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
61 |
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
|
62 |
|
55938 | 63 |
lemma rel_set_cont: |
64 |
"rel_set \<chi> (cont tr1) (cont tr2) = rel_fset \<chi> (ccont tr1) (ccont tr2)" |
|
55933 | 65 |
unfolding cont_def comp_def rel_fset_fset .. |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
66 |
|
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
67 |
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
|
68 |
assumes phi: "\<phi> tr1 tr2" and |
1a86ef0a0210
renamed low-level (co)iterators and (co)recursors with "fld_"/"unf_" prefix
blanchet
parents:
49076
diff
changeset
|
69 |
Lift: "\<And> tr1 tr2. \<phi> tr1 tr2 \<Longrightarrow> |
55943 | 70 |
root tr1 = root tr2 \<and> rel_set (rel_sum 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
|
71 |
shows "tr1 = tr2" |
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
72 |
using phi apply(elim dtree.coinduct) |
55938 | 73 |
apply(rule Lift[unfolded rel_set_cont]) . |
49879 | 74 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
75 |
lemma unfold: |
49508 | 76 |
"root (unfold rt ct b) = rt b" |
77 |
"finite (ct b) \<Longrightarrow> cont (unfold rt ct b) = image (id \<oplus> unfold rt ct) (ct b)" |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
55943
diff
changeset
|
78 |
using dtree.corec_sel[of rt "the_inv fset o image (map_sum id Inr) o ct" b] unfolding unfold_def |
55857 | 79 |
apply blast |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
unfolding cont_def comp_def |
55931 | 81 |
by (simp add: case_sum_o_inj map_sum.compositionality image_image) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
|
49877
b75555ec30a4
ported HOL/BNF/Examples/Derivation_Trees to the latest status of the codatatype package
popescua
parents:
49871
diff
changeset
|
83 |
lemma corec: |
52350 | 84 |
"root (corec rt ct b) = rt b" |
85 |
"finite (ct b) \<Longrightarrow> cont (corec rt ct b) = image (id \<oplus> ([[id, corec rt ct]])) (ct b)" |
|
57983
6edc3529bb4e
reordered some (co)datatype property names for more consistency
blanchet
parents:
55943
diff
changeset
|
86 |
using dtree.corec_sel[of rt "the_inv fset \<circ> ct" b] unfolding corec_def |
49631 | 87 |
unfolding cont_def comp_def id_def |
55857 | 88 |
by simp_all |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
end |