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