83 end; |
83 end; |
84 |
84 |
85 in |
85 in |
86 |
86 |
87 (* generic induction tactic for datatypes *) |
87 (* generic induction tactic for datatypes *) |
88 fun induct_tac var i = |
88 fun induct_tac var i state = state |> |
89 let fun induct state = |
|
90 let val (_, _, Bi, _) = dest_state (state, i) |
89 let val (_, _, Bi, _) = dest_state (state, i) |
91 val sign = #sign(rep_thm state) |
90 val sign = #sign(rep_thm state) |
92 val tn = find_tname var Bi |
91 val tn = find_tname var Bi |
93 val ind_tac = #induct_tac(get_dt_info sign tn) |
92 val ind_tac = #induct_tac(get_dt_info sign tn) |
94 in ind_tac var i end |
93 in ind_tac var i end; |
95 in STATE induct end; |
|
96 |
94 |
97 (* generic exhaustion tactic for datatypes *) |
95 (* generic exhaustion tactic for datatypes *) |
98 fun exhaust_tac aterm i = |
96 fun exhaust_tac aterm i state = state |> |
99 let fun exhaust state = |
|
100 let val sign = #sign(rep_thm state) |
97 let val sign = #sign(rep_thm state) |
101 val tn = infer_tname state sign i aterm |
98 val tn = infer_tname state sign i aterm |
102 val exh_tac = #exhaust_tac(get_dt_info sign tn) |
99 val exh_tac = #exhaust_tac(get_dt_info sign tn) |
103 in exh_tac aterm i end |
100 in exh_tac aterm i end; |
104 in STATE exhaust end; |
|
105 |
101 |
106 end; |
102 end; |
107 |
103 |
108 (*Must be redefined in order to refer to the new instance of bind_thm |
104 (*Must be redefined in order to refer to the new instance of bind_thm |
109 created by init_thy_reader.*) (* FIXME: move *) |
105 created by init_thy_reader.*) (* FIXME: move *) |