21 fun check_type ctxt (t, pos) = |
21 fun check_type ctxt (t, pos) = |
22 let |
22 let |
23 val u = singleton (Variable.polymorphic ctxt) t; |
23 val u = singleton (Variable.polymorphic ctxt) t; |
24 val U = Term.fastype_of u; |
24 val U = Term.fastype_of u; |
25 val _ = Term.is_TVar U andalso |
25 val _ = Term.is_TVar U andalso |
26 error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.str_of pos); |
26 error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u ^ Position.here pos); |
27 in (u, U) end; |
27 in (u, U) end; |
28 |
28 |
29 fun gen_case_tac ctxt0 s opt_rule i st = |
29 fun gen_case_tac ctxt0 s opt_rule i st = |
30 let |
30 let |
31 val (_, ctxt) = Variable.focus_subgoal i st ctxt0; |
31 val (_, ctxt) = Variable.focus_subgoal i st ctxt0; |
73 let |
73 let |
74 val t = Syntax.read_term ctxt name; |
74 val t = Syntax.read_term ctxt name; |
75 val pos = Syntax.read_token_pos name; |
75 val pos = Syntax.read_token_pos name; |
76 val (x, _) = Term.dest_Free t handle TERM _ => |
76 val (x, _) = Term.dest_Free t handle TERM _ => |
77 error ("Induction argument not a variable: " ^ |
77 error ("Induction argument not a variable: " ^ |
78 Syntax.string_of_term ctxt t ^ Position.str_of pos); |
78 Syntax.string_of_term ctxt t ^ Position.here pos); |
79 val eq_x = fn Free (y, _) => x = y | _ => false; |
79 val eq_x = fn Free (y, _) => x = y | _ => false; |
80 val _ = |
80 val _ = |
81 if Term.exists_subterm eq_x concl then () |
81 if Term.exists_subterm eq_x concl then () |
82 else |
82 else |
83 error ("No such variable in subgoal: " ^ |
83 error ("No such variable in subgoal: " ^ |
84 Syntax.string_of_term ctxt t ^ Position.str_of pos); |
84 Syntax.string_of_term ctxt t ^ Position.here pos); |
85 val _ = |
85 val _ = |
86 if (exists o Term.exists_subterm) eq_x prems then |
86 if (exists o Term.exists_subterm) eq_x prems then |
87 warning ("Induction variable occurs also among premises: " ^ |
87 warning ("Induction variable occurs also among premises: " ^ |
88 Syntax.string_of_term ctxt t ^ Position.str_of pos) |
88 Syntax.string_of_term ctxt t ^ Position.here pos) |
89 else (); |
89 else (); |
90 in #1 (check_type ctxt (t, pos)) end; |
90 in #1 (check_type ctxt (t, pos)) end; |
91 |
91 |
92 val argss = map (map (Option.map induct_var)) varss; |
92 val argss = map (map (Option.map induct_var)) varss; |
93 val rule = |
93 val rule = |