author | wenzelm |
Tue, 29 Nov 2005 18:09:12 +0100 | |
changeset 18283 | f8a49f09a202 |
parent 18265 | f3f81becc1f1 |
child 18288 | feb79a6b274b |
permissions | -rw-r--r-- |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
1 |
(* ID: $Id$ |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
2 |
Author: Christian Urban |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
3 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
4 |
The nominal induct proof method (cf. ~~/src/Provers/induct_method.ML). |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
5 |
*) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
6 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
7 |
structure NominalInduct: |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
8 |
sig |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
9 |
val nominal_induct_tac: Proof.context -> (string option * term) option list -> |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
10 |
term list -> (string * typ) list list -> thm -> thm list -> int -> RuleCases.cases_tactic |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
11 |
val nominal_induct_method: Method.src -> Proof.context -> Method.method |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
12 |
end = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
13 |
struct |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
14 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
15 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
16 |
(** misc tools **) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
17 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
18 |
fun nth_list xss i = nth xss i handle Subscript => []; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
19 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
20 |
fun align_right msg xs ys = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
21 |
let val m = length xs and n = length ys |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
22 |
in if m < n then raise ERROR_MESSAGE msg else (Library.drop (m - n, xs) ~~ ys) end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
23 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
24 |
fun prep_inst thy tune (tm, ts) = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
25 |
let |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
26 |
val cert = Thm.cterm_of thy; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
27 |
fun prep_var (x, SOME t) = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
28 |
let |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
29 |
val cx = cert x; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
30 |
val {T = xT, thy, ...} = Thm.rep_cterm cx; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
31 |
val ct = cert (tune t); |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
32 |
in |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
33 |
if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
34 |
else raise ERROR_MESSAGE (Pretty.string_of (Pretty.block |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
35 |
[Pretty.str "Ill-typed instantiation:", Pretty.fbrk, |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
36 |
Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1, |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
37 |
Display.pretty_ctyp (#T (Thm.crep_cterm ct))])) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
38 |
end |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
39 |
| prep_var (_, NONE) = NONE; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
40 |
val xs = InductAttrib.vars_of tm; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
41 |
in |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
42 |
align_right "Rule has fewer variables than instantiations given" xs ts |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
43 |
|> List.mapPartial prep_var |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
44 |
end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
45 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
46 |
fun add_defs def_insts = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
47 |
let |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
48 |
fun add (SOME (SOME x, t)) ctxt = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
49 |
let val ((lhs, def), ctxt') = ProofContext.add_def (x, t) ctxt |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
50 |
in ((SOME (Free lhs), [def]), ctxt') end |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
51 |
| add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
52 |
| add NONE ctxt = ((NONE, []), ctxt); |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
53 |
in fold_map add def_insts #> apfst (split_list #> apsnd List.concat) end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
54 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
55 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
56 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
57 |
(** nominal_induct_tac **) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
58 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
59 |
fun make_fresh [] = HOLogic.unit |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
60 |
| make_fresh [t] = t |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
61 |
| make_fresh ts = foldr1 HOLogic.mk_prod ts; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
62 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
63 |
val split_fresh = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
64 |
Simplifier.full_simplify (HOL_basic_ss addsimps [split_paired_all, unit_all_eq1]); |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
65 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
66 |
fun nominal_induct_tac ctxt def_insts fresh fixing rule facts = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
67 |
let |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
68 |
val thy = ProofContext.theory_of ctxt; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
69 |
val cert = Thm.cterm_of thy; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
70 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
71 |
val ((insts, defs), defs_ctxt) = add_defs def_insts ctxt; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
72 |
val atomized_defs = map ObjectLogic.atomize_thm defs; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
73 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
74 |
fun inst_rule r = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
75 |
Drule.cterm_instantiate |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
76 |
(prep_inst thy (InductMethod.atomize_term thy) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
77 |
(Thm.concl_of r, insts @ [SOME (make_fresh fresh)])) r; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
78 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
79 |
fun rule_cases r = RuleCases.make false (SOME (Thm.prop_of r)) (InductMethod.rulified_term r); |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
80 |
in |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
81 |
SUBGOAL_CASES (fn (goal, i) => fn st => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
82 |
rule |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
83 |
|> inst_rule |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
84 |
|> `RuleCases.get |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
85 |
|> RuleCases.consume defs facts |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
86 |
|> Seq.maps (fn ((cases, (k, more_facts)), r) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
87 |
(CONJUNCTS (ALLGOALS (fn j => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
88 |
Method.insert_tac (more_facts @ atomized_defs) j |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
89 |
THEN InductMethod.fix_tac defs_ctxt k (nth_list fixing (j - 1)) j)) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
90 |
THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
91 |
InductMethod.guess_instance (split_fresh r) i st' |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
92 |
|> Seq.maps (fn r' => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
93 |
CASES (rule_cases r' cases) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
94 |
(Tactic.rtac r' i THEN |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
95 |
PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st')))) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
96 |
THEN_ALL_NEW_CASES InductMethod.rulify_tac |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
97 |
end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
98 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
99 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
100 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
101 |
(** concrete syntax **) |
17870 | 102 |
|
103 |
local |
|
104 |
||
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
105 |
val freshN = "fresh"; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
106 |
val fixingN = "fixing"; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
107 |
val ruleN = "rule"; |
17870 | 108 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
109 |
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME; |
17870 | 110 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
111 |
val def_inst = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
112 |
((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
113 |
-- Args.local_term) >> SOME || |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
114 |
inst >> Option.map (pair NONE); |
18099 | 115 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
116 |
val free = Scan.state -- Args.local_term >> (fn (_, Free v) => v | (ctxt, t) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
117 |
error ("Bad free variable: " ^ ProofContext.string_of_term ctxt t)); |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
118 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
119 |
fun unless_more_args scan = Scan.unless (Scan.lift |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
120 |
((Args.$$$ freshN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
121 |
|
17870 | 122 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
123 |
val def_insts = Scan.repeat (unless_more_args def_inst); |
17870 | 124 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
125 |
val fresh = Scan.optional (Scan.lift (Args.$$$ freshN -- Args.colon) |-- |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
126 |
Scan.repeat (unless_more_args Args.local_term)) []; |
17870 | 127 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
128 |
val fixing = Scan.optional (Scan.lift (Args.$$$ fixingN -- Args.colon) |-- |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
129 |
Args.and_list1 (Scan.repeat (unless_more_args free))) []; |
17870 | 130 |
|
131 |
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm; |
|
132 |
||
133 |
in |
|
134 |
||
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
135 |
fun nominal_induct_method src = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
136 |
Method.syntax (def_insts -- fresh -- fixing -- rule_spec) src |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
137 |
#> (fn (ctxt, (((x, y), z), w)) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
138 |
Method.RAW_METHOD_CASES (fn facts => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
139 |
HEADGOAL (nominal_induct_tac ctxt x y z w facts))); |
17870 | 140 |
|
141 |
end; |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
142 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
143 |
end; |