|
1 (* Title: HOL/Tools/induct_tacs.ML |
|
2 ID: $Id$ |
|
3 Author: Makarius |
|
4 |
|
5 Unstructured induction and cases analysis. |
|
6 *) |
|
7 |
|
8 signature INDUCT_TACS = |
|
9 sig |
|
10 val case_tac: Proof.context -> string -> int -> tactic |
|
11 val case_rule_tac: Proof.context -> string -> thm -> int -> tactic |
|
12 val induct_tac: Proof.context -> string option list list -> int -> tactic |
|
13 val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic |
|
14 val setup: theory -> theory |
|
15 end |
|
16 |
|
17 structure InductTacs: INDUCT_TACS = |
|
18 struct |
|
19 |
|
20 (* case analysis *) |
|
21 |
|
22 fun check_type ctxt t = |
|
23 let |
|
24 val u = singleton (Variable.polymorphic ctxt) t; |
|
25 val U = Term.fastype_of u; |
|
26 val _ = Term.is_TVar U andalso |
|
27 error ("Cannot determine type of " ^ Syntax.string_of_term ctxt u); |
|
28 in (u, U) end; |
|
29 |
|
30 fun gen_case_tac ctxt0 (s, opt_rule) i st = |
|
31 let |
|
32 val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0; |
|
33 val rule = |
|
34 (case opt_rule of |
|
35 SOME rule => rule |
|
36 | NONE => |
|
37 (case Induct.find_casesT ctxt |
|
38 (#2 (check_type ctxt (ProofContext.read_term_schematic ctxt s))) of |
|
39 rule :: _ => rule |
|
40 | [] => @{thm case_split})); |
|
41 val _ = Method.trace ctxt [rule]; |
|
42 |
|
43 val xi = |
|
44 (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of |
|
45 Var (xi, _) :: _ => xi |
|
46 | _ => raise THM ("Malformed cases rule", 0, [rule])); |
|
47 in res_inst_tac ctxt [(xi, s)] rule i st end |
|
48 handle THM _ => Seq.empty; |
|
49 |
|
50 fun case_tac ctxt s = gen_case_tac ctxt (s, NONE); |
|
51 fun case_rule_tac ctxt s rule = gen_case_tac ctxt (s, SOME rule); |
|
52 |
|
53 |
|
54 (* induction *) |
|
55 |
|
56 local |
|
57 |
|
58 fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x) |
|
59 | prep_var _ = NONE; |
|
60 |
|
61 fun prep_inst (concl, xs) = |
|
62 let val vs = Induct.vars_of concl |
|
63 in map_filter prep_var (Library.drop (length vs - length xs, vs) ~~ xs) end; |
|
64 |
|
65 in |
|
66 |
|
67 fun gen_induct_tac ctxt0 (varss, opt_rules) i st = |
|
68 let |
|
69 val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0; |
|
70 val (prems, concl) = Logic.strip_horn (Thm.term_of goal); |
|
71 |
|
72 fun induct_var name = |
|
73 let |
|
74 val t = Syntax.read_term ctxt name; |
|
75 val (x, _) = Term.dest_Free t handle TERM _ => |
|
76 error ("Induction argument not a variable: " ^ Syntax.string_of_term ctxt t); |
|
77 val eq_x = fn Free (y, _) => x = y | _ => false; |
|
78 val _ = |
|
79 if Term.exists_subterm eq_x concl then () |
|
80 else error ("No such variable in subgoal: " ^ Syntax.string_of_term ctxt t); |
|
81 val _ = |
|
82 if (exists o Term.exists_subterm) eq_x prems then |
|
83 warning ("Induction variable occurs also among premises: " ^ Syntax.string_of_term ctxt t) |
|
84 else (); |
|
85 in #1 (check_type ctxt t) end; |
|
86 |
|
87 val argss = map (map (Option.map induct_var)) varss; |
|
88 val _ = forall null argss andalso raise THM ("No induction arguments", 0, []); |
|
89 |
|
90 val rule = |
|
91 (case opt_rules of |
|
92 SOME rules => #2 (RuleCases.strict_mutual_rule ctxt rules) |
|
93 | NONE => |
|
94 (case map_filter (RuleCases.mutual_rule ctxt) (Induct.get_inductT ctxt argss) of |
|
95 (_, rule) :: _ => rule |
|
96 | [] => raise THM ("No induction rules", 0, []))); |
|
97 |
|
98 val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize); |
|
99 val _ = Method.trace ctxt [rule']; |
|
100 |
|
101 val concls = Logic.dest_conjunctions (Thm.concl_of rule); |
|
102 val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths => |
|
103 error "Induction rule has different numbers of variables"; |
|
104 in res_inst_tac ctxt insts rule' i st end |
|
105 handle THM _ => Seq.empty; |
|
106 |
|
107 end; |
|
108 |
|
109 fun induct_tac ctxt args = gen_induct_tac ctxt (args, NONE); |
|
110 fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt (args, SOME rules); |
|
111 |
|
112 |
|
113 (* method syntax *) |
|
114 |
|
115 local |
|
116 |
|
117 val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.$$$ ":"); |
|
118 val opt_rule = Scan.option (rule_spec |-- Attrib.thm); |
|
119 val opt_rules = Scan.option (rule_spec |-- Attrib.thms); |
|
120 |
|
121 val varss = |
|
122 Args.and_list (Scan.repeat (Scan.unless rule_spec (Scan.lift (Args.maybe Args.name)))); |
|
123 |
|
124 in |
|
125 |
|
126 val setup = |
|
127 Method.add_methods |
|
128 [("case_tac", Method.goal_args_ctxt' (Scan.lift Args.name -- opt_rule) gen_case_tac, |
|
129 "unstructured case analysis on types"), |
|
130 ("induct_tac", Method.goal_args_ctxt' (varss -- opt_rules) gen_induct_tac, |
|
131 "unstructured induction on types")]; |
|
132 |
|
133 end; |
|
134 |
|
135 end; |
|
136 |