equal
deleted
inserted
replaced
10 *) |
10 *) |
11 |
11 |
12 open Ntree; |
12 open Ntree; |
13 |
13 |
14 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))"; |
14 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))"; |
15 by (rtac (ntree.unfold RS trans) 1); |
15 let open ntree; val rew = rewrite_rule con_defs in |
16 bws ntree.con_defs; |
16 by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs) |
17 br equalityI 1; |
17 addEs [rew elim]) 1) |
18 by (fast_tac sum_cs 1); |
18 end; |
19 by (fast_tac (sum_cs addIs datatype_intrs |
|
20 addDs [ntree.dom_subset RS subsetD] |
|
21 addEs [nat_fun_into_univ]) 1); |
|
22 val ntree_unfold = result(); |
19 val ntree_unfold = result(); |
23 |
20 |
24 (*A nicer induction rule than the standard one*) |
21 (*A nicer induction rule than the standard one*) |
25 val major::prems = goal Ntree.thy |
22 val major::prems = goal Ntree.thy |
26 "[| t: ntree(A); \ |
23 "[| t: ntree(A); \ |