equal
deleted
inserted
replaced
13 |
13 |
14 (** ntree **) |
14 (** ntree **) |
15 |
15 |
16 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))"; |
16 goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))"; |
17 let open ntree; val rew = rewrite_rule con_defs in |
17 let open ntree; val rew = rewrite_rule con_defs in |
18 by (fast_tac (!claset addSIs (equalityI :: map rew intrs) |
18 by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1) |
19 addEs [rew elim]) 1) |
|
20 end; |
19 end; |
21 qed "ntree_unfold"; |
20 qed "ntree_unfold"; |
22 |
21 |
23 (*A nicer induction rule than the standard one*) |
22 (*A nicer induction rule than the standard one*) |
24 val major::prems = goal Ntree.thy |
23 val major::prems = goal Ntree.thy |
68 |
67 |
69 (** maptree **) |
68 (** maptree **) |
70 |
69 |
71 goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))"; |
70 goal Ntree.thy "maptree(A) = A * (maptree(A) -||> maptree(A))"; |
72 let open maptree; val rew = rewrite_rule con_defs in |
71 let open maptree; val rew = rewrite_rule con_defs in |
73 by (fast_tac (!claset addSIs (equalityI :: map rew intrs) |
72 by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1) |
74 addEs [rew elim]) 1) |
|
75 end; |
73 end; |
76 qed "maptree_unfold"; |
74 qed "maptree_unfold"; |
77 |
75 |
78 (*A nicer induction rule than the standard one*) |
76 (*A nicer induction rule than the standard one*) |
79 val major::prems = goal Ntree.thy |
77 val major::prems = goal Ntree.thy |
93 |
91 |
94 (** maptree2 **) |
92 (** maptree2 **) |
95 |
93 |
96 goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))"; |
94 goal Ntree.thy "maptree2(A,B) = A * (B -||> maptree2(A,B))"; |
97 let open maptree2; val rew = rewrite_rule con_defs in |
95 let open maptree2; val rew = rewrite_rule con_defs in |
98 by (fast_tac (!claset addSIs (equalityI :: map rew intrs) |
96 by (fast_tac (!claset addSIs (map rew intrs) addEs [rew elim]) 1) |
99 addEs [rew elim]) 1) |
|
100 end; |
97 end; |
101 qed "maptree2_unfold"; |
98 qed "maptree2_unfold"; |
102 |
99 |
103 (*A nicer induction rule than the standard one*) |
100 (*A nicer induction rule than the standard one*) |
104 val major::prems = goal Ntree.thy |
101 val major::prems = goal Ntree.thy |