author | wenzelm |
Wed, 30 Nov 2005 00:46:08 +0100 | |
changeset 18288 | feb79a6b274b |
parent 18283 | f8a49f09a202 |
child 18297 | 116fe71fad51 |
permissions | -rw-r--r-- |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
1 |
(* ID: $Id$ |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
2 |
Author: Christian Urban and Makarius |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
3 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
4 |
The nominal induct proof method. |
18283
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 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
16 |
(* proper tuples -- nested left *) |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
17 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
18 |
fun tupleT Ts = HOLogic.unitT |> fold (fn T => fn U => HOLogic.mk_prodT (U, T)) Ts; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
19 |
fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
20 |
|
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
21 |
fun tuple_fun Ts (xi, T) = |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
22 |
Library.funpow (length Ts) HOLogic.mk_split |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
23 |
(Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T)); |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
24 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
25 |
val split_all_tuples = |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
26 |
Simplifier.full_simplify (HOL_basic_ss addsimps |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
27 |
[split_conv, split_paired_all, unit_all_eq1, thm "fresh_unit_elim", thm "fresh_prod_elim"]); |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
28 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
29 |
|
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
30 |
(* inst_rule conclusion: ?P fresh_struct ... insts *) |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
31 |
|
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
32 |
fun inst_rule thy insts fresh rule = |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
33 |
let |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
34 |
val vars = InductAttrib.vars_of (Thm.concl_of rule); |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
35 |
val m = length vars and n = length insts; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
36 |
val _ = if m >= n + 2 then () else error "Too few variables in conclusion of rule"; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
37 |
val P :: x :: ys = vars; |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
38 |
val zs = Library.drop (m - n - 2, ys); |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
39 |
|
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
40 |
val subst = |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
41 |
(P, tuple_fun (map Term.fastype_of fresh) (Term.dest_Var P)) :: |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
42 |
(x, tuple fresh) :: |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
43 |
List.mapPartial (fn (z, SOME t) => SOME (z, t) | _ => NONE) (zs ~~ insts); |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
44 |
in |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
45 |
rule |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
46 |
|> Drule.cterm_instantiate (PolyML.print (map (pairself (Thm.cterm_of thy)) subst)) |
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
47 |
|> PolyML.print |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
48 |
end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
49 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
50 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
51 |
(* nominal_induct_tac *) |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
52 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
53 |
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
|
54 |
let |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
55 |
val thy = ProofContext.theory_of ctxt; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
56 |
val cert = Thm.cterm_of thy; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
57 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
58 |
val ((insts, defs), defs_ctxt) = InductMethod.add_defs def_insts ctxt; |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
59 |
val atomized_defs = map ObjectLogic.atomize_thm defs; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
60 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
61 |
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
|
62 |
in |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
63 |
SUBGOAL_CASES (fn (goal, i) => fn st => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
64 |
rule |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
65 |
|> `RuleCases.get |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
66 |
||> inst_rule thy insts fresh |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
67 |
|> RuleCases.consume defs facts |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
68 |
|> Seq.maps (fn ((cases, (k, more_facts)), r) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
69 |
(CONJUNCTS (ALLGOALS (fn j => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
70 |
Method.insert_tac (more_facts @ atomized_defs) j |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
71 |
THEN InductMethod.fix_tac defs_ctxt k (Library.nth_list fixing (j - 1)) j)) |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
72 |
THEN' InductMethod.atomize_tac) i st |> Seq.maps (fn st' => |
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
73 |
InductMethod.guess_instance (split_all_tuples r) i st' |
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
74 |
|> Seq.maps (fn r' => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
75 |
CASES (rule_cases r' cases) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
76 |
(Tactic.rtac r' i THEN |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
77 |
PRIMSEQ (ProofContext.exports defs_ctxt ctxt)) st')))) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
78 |
THEN_ALL_NEW_CASES InductMethod.rulify_tac |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
79 |
end; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
80 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
81 |
|
18288
feb79a6b274b
proper treatment of tuple/tuple_fun -- nest to the left!
wenzelm
parents:
18283
diff
changeset
|
82 |
(* concrete syntax *) |
17870 | 83 |
|
84 |
local |
|
85 |
||
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
86 |
val freshN = "fresh"; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
87 |
val fixingN = "fixing"; |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
88 |
val ruleN = "rule"; |
17870 | 89 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
90 |
val inst = Scan.lift (Args.$$$ "_") >> K NONE || Args.local_term >> SOME; |
17870 | 91 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
92 |
val def_inst = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
93 |
((Scan.lift (Args.name --| (Args.$$$ "\\<equiv>" || Args.$$$ "==")) >> SOME) |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
94 |
-- Args.local_term) >> SOME || |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
95 |
inst >> Option.map (pair NONE); |
18099 | 96 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
97 |
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
|
98 |
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
|
99 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
100 |
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
|
101 |
((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
|
102 |
|
17870 | 103 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
104 |
val def_insts = Scan.repeat (unless_more_args def_inst); |
17870 | 105 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
106 |
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
|
107 |
Scan.repeat (unless_more_args Args.local_term)) []; |
17870 | 108 |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
109 |
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
|
110 |
Args.and_list1 (Scan.repeat (unless_more_args free))) []; |
17870 | 111 |
|
112 |
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm; |
|
113 |
||
114 |
in |
|
115 |
||
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
116 |
fun nominal_induct_method src = |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
117 |
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
|
118 |
#> (fn (ctxt, (((x, y), z), w)) => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
119 |
Method.RAW_METHOD_CASES (fn facts => |
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
120 |
HEADGOAL (nominal_induct_tac ctxt x y z w facts))); |
17870 | 121 |
|
122 |
end; |
|
18283
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
123 |
|
f8a49f09a202
reworked version with proper support for defs, fixes, fresh specification;
wenzelm
parents:
18265
diff
changeset
|
124 |
end; |