author | haftmann |
Thu, 08 Nov 2018 09:11:52 +0100 | |
changeset 69260 | 0a9688695a1b |
parent 62162 | dca35981c8fb |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
1 |
(* Title: HOL/Eisbach/eisbach_rule_insts.ML |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
2 |
Author: Daniel Matichuk, NICTA/UNSW |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
3 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
4 |
Eisbach-aware variants of the "where" and "of" attributes. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
5 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
6 |
Alternate syntax for rule_insts.ML participates in token closures by |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
7 |
examining the behaviour of Rule_Insts.where_rule and instantiating token |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
8 |
values accordingly. Instantiations in re-interpretation are done with |
60791 | 9 |
infer_instantiate. |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
10 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
11 |
|
60653 | 12 |
structure Eisbach_Rule_Insts: sig end = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
13 |
struct |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
14 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
15 |
fun restore_tags thm = Thm.map_tags (K (Thm.get_tags thm)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
16 |
|
60909
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
17 |
val mk_term_type_internal = Logic.protect o Logic.mk_term o Logic.mk_type; |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
18 |
|
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
19 |
fun term_type_cases f g t = |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
20 |
(case (try (Logic.dest_type o Logic.dest_term o Logic.unprotect) t) of |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
21 |
SOME T => f T |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
22 |
| NONE => |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
23 |
(case (try Logic.dest_term t) of |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
24 |
SOME t => g t |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
25 |
| NONE => raise Fail "Lost encoded instantiation")) |
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
26 |
|
60653 | 27 |
fun add_thm_insts ctxt thm = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
28 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
29 |
val tyvars = Thm.fold_terms Term.add_tvars thm []; |
60909
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
30 |
val tyvars' = tyvars |> map (mk_term_type_internal o TVar); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
31 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
32 |
val tvars = Thm.fold_terms Term.add_vars thm []; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
33 |
val tvars' = tvars |> map (Logic.mk_term o Var); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
34 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
35 |
val conj = |
60653 | 36 |
Logic.mk_conjunction_list (tyvars' @ tvars') |> Thm.cterm_of ctxt |> Drule.mk_term; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
37 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
38 |
((tyvars, tvars), Conjunction.intr thm conj) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
39 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
40 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
41 |
fun get_thm_insts thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
42 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
43 |
val (thm', insts) = Conjunction.elim thm; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
44 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
45 |
val insts' = insts |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
46 |
|> Drule.dest_term |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
47 |
|> Thm.term_of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
48 |
|> Logic.dest_conjunction_list |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
49 |
|> (fn f => fold (fn t => fn (tys, ts) => |
60909
3db3f4154e18
clarify type vs. term instantiation when forming closure;
Daniel Matichuk <daniel.matichuk@nicta.com.au>
parents:
60791
diff
changeset
|
50 |
term_type_cases (fn T => (T :: tys, ts)) (fn t => (tys, t :: ts)) t) f ([], [])) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
51 |
||> rev |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
52 |
|>> rev; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
53 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
54 |
(thm', insts') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
55 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
56 |
|
60653 | 57 |
fun instantiate_xis ctxt insts thm = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
58 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
59 |
val tyvars = Thm.fold_terms Term.add_tvars thm []; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
60 |
val tvars = Thm.fold_terms Term.add_vars thm []; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
61 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
62 |
fun add_inst (xi, t) (Ts, ts) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
63 |
(case AList.lookup (op =) tyvars xi of |
60653 | 64 |
SOME S => (((xi, S), Thm.ctyp_of ctxt (Logic.dest_type t)) :: Ts, ts) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
65 |
| NONE => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
66 |
(case AList.lookup (op =) tvars xi of |
60791 | 67 |
SOME _ => (Ts, (xi, Thm.cterm_of ctxt t) :: ts) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
68 |
| NONE => error "indexname not found in thm")); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
69 |
|
60791 | 70 |
val (instT, inst) = fold add_inst insts ([], []); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
71 |
in |
60791 | 72 |
(Thm.instantiate (instT, []) thm |
73 |
|> infer_instantiate ctxt inst |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
74 |
COMP_INCR asm_rl) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
75 |
|> Thm.adjust_maxidx_thm ~1 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
76 |
|> restore_tags thm |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
77 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
78 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
79 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
80 |
datatype rule_inst = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
81 |
Named_Insts of ((indexname * string) * (term -> unit)) list * (binding * string option * mixfix) list |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
82 |
| Term_Insts of (indexname * term) list |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
83 |
| Unchecked_Term_Insts of term option list * term option list; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
84 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
85 |
fun mk_pair (t, t') = Logic.mk_conjunction (Logic.mk_term t, Logic.mk_term t'); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
86 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
87 |
fun dest_pair t = apply2 Logic.dest_term (Logic.dest_conjunction t); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
88 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
89 |
fun embed_indexname ((xi, s), f) = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
90 |
let fun wrap_xi xi t = mk_pair (Var (xi, fastype_of t), t); |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
91 |
in ((xi, s), f o wrap_xi xi) end; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
92 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
93 |
fun unembed_indexname t = dest_pair t |> apfst (Term.dest_Var #> fst); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
94 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
95 |
fun read_where_insts (insts, fixes) = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
96 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
97 |
val insts' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
98 |
if forall (fn (_, v) => Parse_Tools.is_real_val v) insts |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
99 |
then Term_Insts (map (unembed_indexname o Parse_Tools.the_real_val o snd) insts) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
100 |
else |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
101 |
Named_Insts (map (fn (xi, p) => embed_indexname |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
102 |
((xi, Parse_Tools.the_parse_val p), Parse_Tools.the_parse_fun p)) insts, fixes); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
103 |
in insts' end; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
104 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
105 |
fun of_rule thm (args, concl_args) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
106 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
107 |
fun zip_vars _ [] = [] |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
108 |
| zip_vars (_ :: xs) (NONE :: rest) = zip_vars xs rest |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
109 |
| zip_vars ((x, _) :: xs) (SOME t :: rest) = (x, t) :: zip_vars xs rest |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
110 |
| zip_vars [] _ = error "More instantiations than variables in theorem"; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
111 |
val insts = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
112 |
zip_vars (rev (Term.add_vars (Thm.full_prop_of thm) [])) args @ |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
113 |
zip_vars (rev (Term.add_vars (Thm.concl_of thm) [])) concl_args; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
114 |
in insts end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
115 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
116 |
val inst = Args.maybe Parse_Tools.name_term; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
117 |
val concl = Args.$$$ "concl" -- Args.colon; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
118 |
|
60469 | 119 |
fun close_unchecked_insts context ((insts, concl_inst), fixes) = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
120 |
let |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
121 |
val ctxt = Context.proof_of context; |
60469 | 122 |
val ctxt1 = ctxt |> Proof_Context.add_fixes_cmd fixes |> #2; |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
123 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
124 |
val insts' = insts @ concl_inst; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
125 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
126 |
val term_insts = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
127 |
map (the_list o (Option.map Parse_Tools.the_parse_val)) insts' |
60486 | 128 |
|> burrow (Syntax.read_terms ctxt1 #> Variable.export_terms ctxt1 ctxt) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
129 |
|> map (try the_single); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
130 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
131 |
val _ = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
132 |
(insts', term_insts) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
133 |
|> ListPair.app (fn (SOME p, SOME t) => Parse_Tools.the_parse_fun p t | _ => ()); |
60552 | 134 |
val (insts'', concl_insts'') = chop (length insts) term_insts; |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
135 |
in Unchecked_Term_Insts (insts'', concl_insts'') end; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
136 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
137 |
fun read_of_insts checked context ((insts, concl_insts), fixes) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
138 |
if forall (fn SOME t => Parse_Tools.is_real_val t | NONE => true) (insts @ concl_insts) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
139 |
then |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
140 |
if checked |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
141 |
then |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
142 |
(fn _ => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
143 |
Term_Insts |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
144 |
(map (unembed_indexname o Parse_Tools.the_real_val) (map_filter I (insts @ concl_insts)))) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
145 |
else |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
146 |
(fn _ => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
147 |
Unchecked_Term_Insts |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
148 |
(map (Option.map Parse_Tools.the_real_val) insts, |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
149 |
map (Option.map Parse_Tools.the_real_val) concl_insts)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
150 |
else |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
151 |
if checked |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
152 |
then |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
153 |
(fn thm => |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
154 |
Named_Insts |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
155 |
(apply2 |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
156 |
(map (Option.map (fn p => (Parse_Tools.the_parse_val p, Parse_Tools.the_parse_fun p)))) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
157 |
(insts, concl_insts) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
158 |
|> of_rule thm |> map ((fn (xi, (nm, f)) => embed_indexname ((xi, nm), f))), fixes)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
159 |
else |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
160 |
let val result = close_unchecked_insts context ((insts, concl_insts), fixes); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
161 |
in fn _ => result end; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
162 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
163 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
164 |
fun read_instantiate_closed ctxt (Named_Insts (insts, fixes)) thm = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
165 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
166 |
val insts' = map (fn ((v, t), _) => ((v, Position.none), t)) insts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
167 |
|
60653 | 168 |
val (thm_insts, thm') = add_thm_insts ctxt thm; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
169 |
val (thm'', thm_insts') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
170 |
Rule_Insts.where_rule ctxt insts' fixes thm' |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
171 |
|> get_thm_insts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
172 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
173 |
val tyinst = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
174 |
ListPair.zip (fst thm_insts, fst thm_insts') |> map (fn ((xi, _), typ) => (xi, typ)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
175 |
val tinst = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
176 |
ListPair.zip (snd thm_insts, snd thm_insts') |> map (fn ((xi, _), t) => (xi, t)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
177 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
178 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
179 |
map (fn ((xi, _), f) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
180 |
(case AList.lookup (op =) tyinst xi of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
181 |
SOME typ => f (Logic.mk_type typ) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
182 |
| NONE => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
183 |
(case AList.lookup (op =) tinst xi of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
184 |
SOME t => f t |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
185 |
| NONE => error "Lost indexname in instantiated theorem"))) insts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
186 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
187 |
(thm'' |> restore_tags thm) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
188 |
end |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
189 |
| read_instantiate_closed ctxt (Unchecked_Term_Insts insts) thm = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
190 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
191 |
val (xis, ts) = ListPair.unzip (of_rule thm insts); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
192 |
val ctxt' = Variable.declare_maxidx (Thm.maxidx_of thm) ctxt; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
193 |
val (ts', ctxt'') = Variable.import_terms false ts ctxt'; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
194 |
val ts'' = Variable.export_terms ctxt'' ctxt ts'; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
195 |
val insts' = ListPair.zip (xis, ts''); |
60653 | 196 |
in instantiate_xis ctxt insts' thm end |
197 |
| read_instantiate_closed ctxt (Term_Insts insts) thm = |
|
198 |
instantiate_xis ctxt insts thm; |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
199 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
200 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
201 |
Theory.setup |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
202 |
(Attrib.setup @{binding "where"} |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
203 |
(Scan.lift |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
204 |
(Parse.and_list1 (Args.var -- (Args.$$$ "=" |-- Parse_Tools.name_term)) -- Parse.for_fixes) |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
205 |
>> (fn args => |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
206 |
let val args' = read_where_insts args in |
62162
dca35981c8fb
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents:
62135
diff
changeset
|
207 |
fn (context, thm) => |
dca35981c8fb
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents:
62135
diff
changeset
|
208 |
(NONE, SOME (read_instantiate_closed (Context.proof_of context) args' thm)) |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
209 |
end)) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
210 |
"named instantiation of theorem"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
211 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
212 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
213 |
Theory.setup |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
214 |
(Attrib.setup @{binding "of"} |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
215 |
(Scan.lift |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
216 |
(Args.mode "unchecked" -- |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
217 |
(Scan.repeat (Scan.unless concl inst) -- |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
218 |
Scan.optional (concl |-- Scan.repeat inst) [] -- |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
219 |
Parse.for_fixes)) -- Scan.state >> |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
220 |
(fn ((unchecked, args), context) => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
221 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
222 |
val read_insts = read_of_insts (not unchecked) context args; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
223 |
in |
62162
dca35981c8fb
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents:
62135
diff
changeset
|
224 |
fn (context, thm) => |
61853
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
225 |
let val thm' = |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
226 |
if Thm.is_free_dummy thm andalso unchecked |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
227 |
then Drule.free_dummy_thm |
fb7756087101
rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
wenzelm
parents:
61852
diff
changeset
|
228 |
else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm |
62162
dca35981c8fb
Eisbach instantiation attributes are like Thm.rule_attribute (in correspondence to Pure versions), but without the built-in treatment of free dummy thms (see also fb7756087101);
wenzelm
parents:
62135
diff
changeset
|
229 |
in (NONE, SOME thm') end |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
230 |
end)) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
231 |
"positional instantiation of theorem"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
232 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
233 |
end; |