author | blanchet |
Thu, 11 Sep 2014 19:26:59 +0200 | |
changeset 58309 | a09ec6daaa19 |
parent 57207 | src/HOL/BNF_Examples/TreeFI.thy@df0f8ad7cc30 |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
57207
diff
changeset
|
1 |
(* Title: HOL/Datatype_Examples/TreeFI.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Author: Andrei Popescu, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
Finitely branching possibly infinite trees. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
header {* Finitely Branching Possibly Infinite Trees *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
theory TreeFI |
57207
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
12 |
imports Main |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
|
57207
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
15 |
codatatype 'a treeFI = Tree (lab: 'a) (sub: "'a treeFI list") |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
(* Tree reverse:*) |
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53470
diff
changeset
|
18 |
primcorec trev where |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53470
diff
changeset
|
19 |
"lab (trev t) = lab t" |
57207
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
20 |
| "sub (trev t) = map trev (rev (sub t))" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
lemma treeFI_coinduct: |
53470 | 23 |
assumes *: "phi x y" |
24 |
and step: "\<And>a b. phi a b \<Longrightarrow> |
|
25 |
lab a = lab b \<and> |
|
57207
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
26 |
length (sub a) = length (sub b) \<and> |
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
27 |
(\<forall>i < length (sub a). phi (nth (sub a) i) (nth (sub b) i))" |
53470 | 28 |
shows "x = y" |
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53470
diff
changeset
|
29 |
using * proof (coinduction arbitrary: x y) |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53470
diff
changeset
|
30 |
case (Eq_treeFI t1 t2) |
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53470
diff
changeset
|
31 |
from conjunct1[OF conjunct2[OF step[OF Eq_treeFI]]] conjunct2[OF conjunct2[OF step[OF Eq_treeFI]]] |
57207
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
32 |
have "list_all2 phi (sub t1) (sub t2)" |
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
33 |
proof (induction "sub t1" "sub t2" arbitrary: t1 t2 rule: list_induct2) |
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
34 |
case (Cons x xs y ys) |
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
35 |
note sub = Cons(3,4)[symmetric] and phi = mp[OF spec[OF Cons(5)], unfolded sub] |
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
36 |
and IH = Cons(2)[of "Tree (lab t1) (tl (sub t1))" "Tree (lab t2) (tl (sub t2))", |
53355 | 37 |
unfolded sub, simplified] |
38 |
from phi[of 0] show ?case unfolding sub by (auto intro!: IH dest: phi[simplified, OF Suc_mono]) |
|
39 |
qed simp |
|
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53470
diff
changeset
|
40 |
with conjunct1[OF step[OF Eq_treeFI]] show ?case by simp |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
41 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
42 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
lemma trev_trev: "trev (trev tr) = tr" |
57207
df0f8ad7cc30
got rid of 'listF' example, which is now subsumed by the real 'list' type
blanchet
parents:
55075
diff
changeset
|
44 |
by (coinduction arbitrary: tr rule: treeFI_coinduct) (auto simp add: rev_map) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
end |