author | urbanc |
Sun, 13 Nov 2005 22:36:30 +0100 | |
changeset 18158 | 57cba2a340f2 |
parent 18157 | 72e1956440ad |
child 18265 | f3f81becc1f1 |
permissions | -rw-r--r-- |
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 |
||
18052 | 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; |
|
17870 | 21 |
|
22 |
fun find_var frees name = |
|
23 |
(case Library.find_first (equal name o fst o dest_Free) frees of |
|
18099 | 24 |
NONE => error ("No such Variable in term: " ^ quote name) |
17870 | 25 |
| SOME v => v); |
26 |
||
18052 | 27 |
(* - names specifies the variables that are involved in the *) |
28 |
(* induction *) |
|
29 |
(* - rule is the induction rule to be applied *) |
|
17870 | 30 |
fun nominal_induct_tac (names, rule) facts state = |
31 |
let |
|
32 |
val sg = Thm.sign_of_thm state; |
|
33 |
val cert = Thm.cterm_of sg; |
|
18099 | 34 |
|
35 |
val facts1 = Library.take (1, facts); |
|
36 |
val facts2 = Library.drop (1, facts); |
|
37 |
||
17870 | 38 |
val goal :: _ = Thm.prems_of state; (*exception Subscript*) |
18099 | 39 |
val frees = foldl Term.add_term_frees [] (goal :: map concl_of facts1); |
17870 | 40 |
val frees' = filter_out (fn Free (x, _) => exists (equal x) names) frees; |
18099 | 41 |
val vars = map (find_var frees) names; |
42 |
(* FIXME - check what one can do in case of *) |
|
43 |
(* rule inductions *) |
|
17870 | 44 |
|
45 |
fun inst_rule rule = |
|
46 |
let |
|
47 |
val concl_vars = map Var (rev (Term.add_vars (Thm.concl_of rule) [])); |
|
48 |
val (P :: ts, x) = split_last concl_vars |
|
49 |
handle Empty => error "Malformed conclusion of induction rule" |
|
18052 | 50 |
| Bind => error "Malformed conclusion of induction rule"; |
17870 | 51 |
in |
52 |
cterm_instantiate |
|
53 |
((cert P, cert (fold_rev lambda vars (tuple_lambda frees' (HOLogic.dest_Trueprop goal)))) :: |
|
54 |
(cert x, cert (if null frees' then HOLogic.unit else foldr1 HOLogic.mk_prod frees')) :: |
|
55 |
(map cert ts ~~ map cert vars)) rule |
|
56 |
end; |
|
57 |
||
58 |
val simplify_rule = |
|
18158
57cba2a340f2
changed the HOL_basic_ss back and selectively added
urbanc
parents:
18157
diff
changeset
|
59 |
Simplifier.full_simplify (HOL_basic_ss addsimps |
57cba2a340f2
changed the HOL_basic_ss back and selectively added
urbanc
parents:
18157
diff
changeset
|
60 |
simp_thms @ [triv_forall_equality, split_conv, split_paired_All, split_paired_all]); |
17870 | 61 |
|
62 |
in |
|
63 |
rule |
|
64 |
|> inst_rule |
|
65 |
|> Method.multi_resolve facts1 |
|
18157
72e1956440ad
exchanged HOL_ss for HOL_basic_ss in the simplification
urbanc
parents:
18099
diff
changeset
|
66 |
|> Seq.map simplify_rule |
17870 | 67 |
|> Seq.map (RuleCases.save rule) |
68 |
|> Seq.map RuleCases.add |
|
69 |
|> Seq.map (fn (r, (cases, _)) => |
|
70 |
HEADGOAL (Method.insert_tac facts2 THEN' Tactic.rtac r) state |
|
71 |
|> Seq.map (rpair (RuleCases.make false NONE (sg, Thm.prop_of r) cases))) |
|
72 |
|> Seq.flat |
|
73 |
end |
|
74 |
handle Subscript => Seq.empty; |
|
75 |
||
76 |
val rule_spec = Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.local_thm; |
|
77 |
||
78 |
val nominal_induct_args = |
|
79 |
Scan.repeat (Scan.unless rule_spec (Scan.lift Args.name)) -- rule_spec; |
|
80 |
||
81 |
in |
|
82 |
||
83 |
val nominal_induct_method = |
|
84 |
Method.RAW_METHOD_CASES o nominal_induct_tac oo (#2 oo Method.syntax nominal_induct_args); |
|
85 |
||
86 |
(* nominal_induc_method needs to have the type |
|
87 |
||
88 |
Args.src -> Proof.context -> Proof.method |
|
89 |
||
90 |
CHECK THAT |
|
91 |
||
92 |
*) |
|
93 |
||
94 |
end; |