66 | Some (DT_DATA ds) => |
66 | Some (DT_DATA ds) => |
67 case assoc (ds, tn) of |
67 case assoc (ds, tn) of |
68 Some info => info |
68 Some info => info |
69 | None => error ("Not a datatype: " ^ quote tn) |
69 | None => error ("Not a datatype: " ^ quote tn) |
70 |
70 |
|
71 fun infer_tname state sign i aterm = |
|
72 let val (_, _, Bi, _) = dest_state (state, i) |
|
73 val params = Logic.strip_params Bi (*params of subgoal i*) |
|
74 val params = rev(rename_wrt_term Bi params) (*as they are printed*) |
|
75 val (types,sorts) = types_sorts state |
|
76 fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) |
|
77 | types'(ixn) = types ixn; |
|
78 val (ct,_) = read_def_cterm (sign,types',sorts) [] false |
|
79 (aterm,TVar(("",0),[])); |
|
80 in case #T(rep_cterm ct) of |
|
81 Type(tn,_) => tn |
|
82 | _ => error("Cannot induct on type of " ^ quote aterm) |
|
83 end; |
|
84 |
71 in |
85 in |
72 |
86 |
73 (* generic induction tactic for datatypes *) |
87 (* generic induction tactic for datatypes *) |
74 fun induct_tac var i = |
88 fun induct_tac var i = |
75 let fun induct state = |
89 let fun induct state = |
79 val ind_tac = #induct_tac(get_dt_info sign tn) |
93 val ind_tac = #induct_tac(get_dt_info sign tn) |
80 in ind_tac var i end |
94 in ind_tac var i end |
81 in STATE induct end; |
95 in STATE induct end; |
82 |
96 |
83 (* generic exhaustion tactic for datatypes *) |
97 (* generic exhaustion tactic for datatypes *) |
84 fun exhaust_tac var i = |
98 fun exhaust_tac aterm i = |
85 let fun exhaust state = |
99 let fun exhaust state = |
86 let val (_, _, Bi, _) = dest_state (state, i) |
100 let val sign = #sign(rep_thm state) |
87 val sign = #sign(rep_thm state) |
101 val tn = infer_tname state sign i aterm |
88 val tn = find_tname var Bi |
|
89 val exh_tac = #exhaust_tac(get_dt_info sign tn) |
102 val exh_tac = #exhaust_tac(get_dt_info sign tn) |
90 in exh_tac var i end |
103 in exh_tac aterm i end |
91 in STATE exhaust end; |
104 in STATE exhaust end; |
92 |
105 |
93 end; |
106 end; |
94 |
107 |
95 (*Must be redefined in order to refer to the new instance of bind_thm |
108 (*Must be redefined in order to refer to the new instance of bind_thm |