17870
|
1 |
(* $Id$ *)
|
|
2 |
|
|
3 |
local
|
|
4 |
|
|
5 |
(* A function that takes a list of Variables and a term t; *)
|
|
6 |
(* it builds up an abstraction of the Variables packaged in a tuple(!) *)
|
|
7 |
(* over the term t. *)
|
|
8 |
(* E.g tuple_lambda [] t produces %x . t where x is a dummy Variable *)
|
|
9 |
(* tuple_lambda [a] t produces %a . t *)
|
|
10 |
(* tuple_lambda [a,b,c] t produces %(a,b,c). t *)
|
|
11 |
|
|
12 |
fun tuple_lambda [] t = Abs ("x", HOLogic.unitT, t)
|
|
13 |
| tuple_lambda [x] t = lambda x t
|
|
14 |
| tuple_lambda (x::xs) t =
|
|
15 |
let
|
|
16 |
val t' = tuple_lambda xs t;
|
|
17 |
val Type ("fun", [T,U]) = fastype_of t';
|
|
18 |
in
|
|
19 |
HOLogic.split_const (fastype_of x,T,U) $ lambda x t'
|
|
20 |
end;
|
|
21 |
|
|
22 |
fun find_var frees name =
|
|
23 |
(case Library.find_first (equal name o fst o dest_Free) frees of
|
|
24 |
NONE => error ("No such Variable in term: " ^ quote name)
|
|
25 |
| SOME v => v);
|
|
26 |
|
|
27 |
fun nominal_induct_tac (names, rule) facts state =
|
|
28 |
let
|
|
29 |
val sg = Thm.sign_of_thm state;
|
|
30 |
val cert = Thm.cterm_of sg;
|
|
31 |
val goal :: _ = Thm.prems_of state; (*exception Subscript*)
|
|
32 |
val frees = Term.term_frees goal;
|
|
33 |
val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees;
|
|
34 |
val vars = map (find_var frees) names;
|
|
35 |
|
|
36 |
fun inst_rule rule =
|
|
37 |
let
|
|
38 |
val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) []));
|
|
39 |
val (P :: ts, x) = split_last concl_vars
|
|
40 |
handle Empty => error "Malformed conclusion of induction rule"
|
|
41 |
| Bind => error "Malformed conclusion of induction rule";
|
|
42 |
in
|
|
43 |
cterm_instantiate
|
|
44 |
((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) ::
|
|
45 |
(cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) ::
|
|
46 |
(map cert ts ~~ map cert vars)) rule
|
|
47 |
end;
|
|
48 |
|
|
49 |
val simplify_rule =
|
|
50 |
Simplifier.full_simplify (HOL_basic_ss addsimps
|
|
51 |
[split_conv, split_paired_All, split_paired_all]);
|
|
52 |
|
|
53 |
val facts1 = Library.take (1, facts);
|
|
54 |
val facts2 = Library.drop (1, facts);
|
|
55 |
|
|
56 |
in
|
|
57 |
rule
|
|
58 |
|> inst_rule
|
|
59 |
|> Method.multi_resolve facts1
|
|
60 |
|> Seq.map simplify_rule
|
|
61 |
|> Seq.map (RuleCases.save rule)
|
|
62 |
|> Seq.map RuleCases.add
|
|
63 |
|> Seq.map (fn (r, (cases, _)) =>
|
|
64 |
HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state
|
|
65 |
|> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases)))
|
|
66 |
|> Seq.flat
|
|
67 |
end
|
|
68 |
handle Subscript => Seq.empty;
|
|
69 |
|
|
70 |
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm;
|
|
71 |
|
|
72 |
val nominal_induct_args =
|
|
73 |
Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec;
|
|
74 |
|
|
75 |
in
|
|
76 |
|
|
77 |
val nominal_induct_method =
|
|
78 |
Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args);
|
|
79 |
|
|
80 |
(* nominal_induc_method needs to have the type
|
|
81 |
|
|
82 |
Args.src -> Proof.context -> Proof.method
|
|
83 |
|
|
84 |
CHECK THAT
|
|
85 |
|
|
86 |
*)
|
|
87 |
|
|
88 |
end;
|