author | paulson |
Thu, 13 Jan 2000 17:34:59 +0100 | |
changeset 8125 | df502e820d07 |
parent 6112 | 5e4871c5136b |
child 11316 | b4e71bd751e4 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/ex/Ntree.ML |
486 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
486 | 4 |
Copyright 1994 University of Cambridge |
5 |
||
6 |
Datatype definition n-ary branching trees |
|
7 |
Demonstrates a simple use of function space in a datatype definition |
|
8 |
||
9 |
Based upon ex/Term.ML |
|
10 |
*) |
|
11 |
||
539 | 12 |
(** ntree **) |
13 |
||
5068 | 14 |
Goal "ntree(A) = A * (UN n: nat. n -> ntree(A))"; |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
15 |
let open ntree; val rew = rewrite_rule con_defs in |
4091 | 16 |
by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) |
529
f0d16216e394
ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
lcp
parents:
515
diff
changeset
|
17 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
18 |
qed "ntree_unfold"; |
486 | 19 |
|
20 |
(*A nicer induction rule than the standard one*) |
|
21 |
val major::prems = goal Ntree.thy |
|
1461 | 22 |
"[| t: ntree(A); \ |
486 | 23 |
\ !!x n h. [| x: A; n: nat; h: n -> ntree(A); ALL i:n. P(h`i) \ |
1461 | 24 |
\ |] ==> P(Branch(x,h)) \ |
486 | 25 |
\ |] ==> P(t)"; |
515 | 26 |
by (rtac (major RS ntree.induct) 1); |
27 |
by (etac UN_E 1); |
|
486 | 28 |
by (REPEAT_SOME (ares_tac prems)); |
4091 | 29 |
by (fast_tac (claset() addEs [fun_weaken_type]) 1); |
30 |
by (fast_tac (claset() addDs [apply_type]) 1); |
|
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
31 |
qed "ntree_induct"; |
486 | 32 |
|
33 |
(*Induction on ntree(A) to prove an equation*) |
|
34 |
val major::prems = goal Ntree.thy |
|
1461 | 35 |
"[| t: ntree(A); f: ntree(A)->B; g: ntree(A)->B; \ |
486 | 36 |
\ !!x n h. [| x: A; n: nat; h: n -> ntree(A); f O h = g O h |] ==> \ |
1461 | 37 |
\ f ` Branch(x,h) = g ` Branch(x,h) \ |
486 | 38 |
\ |] ==> f`t=g`t"; |
539 | 39 |
by (rtac (major RS ntree_induct) 1); |
486 | 40 |
by (REPEAT_SOME (ares_tac prems)); |
41 |
by (cut_facts_tac prems 1); |
|
1461 | 42 |
by (rtac fun_extension 1); |
486 | 43 |
by (REPEAT_SOME (ares_tac [comp_fun])); |
4091 | 44 |
by (asm_simp_tac (simpset() addsimps [comp_fun_apply]) 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
45 |
qed "ntree_induct_eqn"; |
486 | 46 |
|
47 |
(** Lemmas to justify using "Ntree" in other recursive type definitions **) |
|
48 |
||
5137 | 49 |
Goalw ntree.defs "A<=B ==> ntree(A) <= ntree(B)"; |
486 | 50 |
by (rtac lfp_mono 1); |
515 | 51 |
by (REPEAT (rtac ntree.bnd_mono 1)); |
486 | 52 |
by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
53 |
qed "ntree_mono"; |
486 | 54 |
|
55 |
(*Easily provable by induction also*) |
|
5068 | 56 |
Goalw (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)"; |
486 | 57 |
by (rtac lfp_lowerbound 1); |
58 |
by (rtac (A_subset_univ RS univ_mono) 2); |
|
4152 | 59 |
by Safe_tac; |
486 | 60 |
by (REPEAT (ares_tac [Pair_in_univ, nat_fun_univ RS subsetD] 1)); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
61 |
qed "ntree_univ"; |
486 | 62 |
|
539 | 63 |
val ntree_subset_univ = [ntree_mono, ntree_univ] MRS subset_trans |> standard; |
64 |
||
65 |
||
8125 | 66 |
(** ntree recursion **) |
67 |
||
68 |
Goal "ntree_rec(b, Branch(x,h)) \ |
|
69 |
\ = b(x, h, lam i: domain(h). ntree_rec(b, h`i))"; |
|
70 |
by (rtac (ntree_rec_def RS def_Vrecursor RS trans) 1); |
|
71 |
by (Simp_tac 1); |
|
72 |
by (rewrite_goals_tac ntree.con_defs); |
|
73 |
by (asm_simp_tac (simpset() addsimps [rank_pair2 RSN (2, lt_trans), |
|
74 |
rank_apply]) 1);; |
|
75 |
qed "ntree_rec_Branch"; |
|
76 |
||
77 |
Goalw [ntree_copy_def] |
|
78 |
"ntree_copy (Branch(x, h)) = Branch(x, lam i : domain(h). ntree_copy (h`i))"; |
|
79 |
by (rtac ntree_rec_Branch 1); |
|
80 |
qed "ntree_copy_Branch"; |
|
81 |
||
82 |
Addsimps [ntree_copy_Branch]; |
|
83 |
||
84 |
Goal "z : ntree(A) ==> ntree_copy(z) = z"; |
|
85 |
by (induct_tac "z" 1); |
|
86 |
by (auto_tac (claset(), simpset() addsimps [domain_of_fun, Pi_Collect_iff])); |
|
87 |
qed "ntree_copy_is_ident"; |
|
88 |
||
89 |
||
90 |
||
539 | 91 |
(** maptree **) |
92 |
||
5068 | 93 |
Goal "maptree(A) = A * (maptree(A) -||> maptree(A))"; |
539 | 94 |
let open maptree; val rew = rewrite_rule con_defs in |
4091 | 95 |
by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) |
539 | 96 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
97 |
qed "maptree_unfold"; |
486 | 98 |
|
539 | 99 |
(*A nicer induction rule than the standard one*) |
100 |
val major::prems = goal Ntree.thy |
|
1461 | 101 |
"[| t: maptree(A); \ |
102 |
\ !!x n h. [| x: A; h: maptree(A) -||> maptree(A); \ |
|
103 |
\ ALL y: field(h). P(y) \ |
|
104 |
\ |] ==> P(Sons(x,h)) \ |
|
539 | 105 |
\ |] ==> P(t)"; |
106 |
by (rtac (major RS maptree.induct) 1); |
|
107 |
by (REPEAT_SOME (ares_tac prems)); |
|
108 |
by (eresolve_tac [Collect_subset RS FiniteFun_mono1 RS subsetD] 1); |
|
109 |
by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1); |
|
110 |
by (dresolve_tac [Fin.dom_subset RS subsetD] 1); |
|
2469 | 111 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
112 |
qed "maptree_induct"; |
539 | 113 |
|
114 |
||
115 |
(** maptree2 **) |
|
116 |
||
5068 | 117 |
Goal "maptree2(A,B) = A * (B -||> maptree2(A,B))"; |
539 | 118 |
let open maptree2; val rew = rewrite_rule con_defs in |
4091 | 119 |
by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1) |
539 | 120 |
end; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
121 |
qed "maptree2_unfold"; |
539 | 122 |
|
123 |
(*A nicer induction rule than the standard one*) |
|
124 |
val major::prems = goal Ntree.thy |
|
1461 | 125 |
"[| t: maptree2(A,B); \ |
539 | 126 |
\ !!x n h. [| x: A; h: B -||> maptree2(A,B); ALL y:range(h). P(y) \ |
1461 | 127 |
\ |] ==> P(Sons2(x,h)) \ |
539 | 128 |
\ |] ==> P(t)"; |
129 |
by (rtac (major RS maptree2.induct) 1); |
|
130 |
by (REPEAT_SOME (ares_tac prems)); |
|
131 |
by (eresolve_tac [[subset_refl, Collect_subset] MRS |
|
1461 | 132 |
FiniteFun_mono RS subsetD] 1); |
539 | 133 |
by (dresolve_tac [FiniteFun.dom_subset RS subsetD] 1); |
134 |
by (dresolve_tac [Fin.dom_subset RS subsetD] 1); |
|
2469 | 135 |
by (Fast_tac 1); |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
539
diff
changeset
|
136 |
qed "maptree2_induct"; |
539 | 137 |