author | wenzelm |
Sun, 17 May 2015 22:33:34 +0200 | |
changeset 60287 | adde5ce1e0a7 |
parent 60285 | b4f1a0a701ae |
child 60367 | e201bd8973db |
permissions | -rw-r--r-- |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
1 |
(* Title: HOL/Eisbach/match_method.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 |
Setup for "match" proof method. It provides basic fact/term matching in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
5 |
addition to premise/conclusion matching through Subgoal.focus, and binds |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
6 |
fact names from matches as well as term patterns within matches. |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
7 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
8 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
9 |
signature MATCH_METHOD = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
10 |
sig |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
11 |
val focus_schematics: Proof.context -> Envir.tenv |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
12 |
val focus_params: Proof.context -> term list |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
13 |
(* FIXME proper ML interface for the main thing *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
14 |
end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
15 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
16 |
structure Match_Method : MATCH_METHOD = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
17 |
struct |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
18 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
19 |
(*Variant of filter_prems_tac with auxiliary configuration; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
20 |
recovers premise order afterwards.*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
21 |
fun filter_prems_tac' ctxt prep pred a = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
22 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
23 |
fun Then NONE tac = SOME tac |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
24 |
| Then (SOME tac) tac' = SOME (tac THEN' tac'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
25 |
fun thins H (tac, n, a, i) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
26 |
(case pred a H of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
27 |
NONE => (tac, n + 1, a, i) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
28 |
| SOME a' => (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, a', i + n)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
29 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
30 |
SUBGOAL (fn (goal, i) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
31 |
let val Hs = Logic.strip_assums_hyp (prep goal) in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
32 |
(case fold thins Hs (NONE, 0, a, 0) of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
33 |
(NONE, _, _, _) => no_tac |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
34 |
| (SOME tac, _, _, n) => tac i THEN rotate_tac (~ n) i) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
35 |
end) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
36 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
37 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
38 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
39 |
datatype match_kind = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
40 |
Match_Term of term Item_Net.T |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
41 |
| Match_Fact of thm Item_Net.T |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
42 |
| Match_Concl |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
43 |
| Match_Prems of bool; |
60119
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 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
46 |
val aconv_net = Item_Net.init (op aconv) single; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
47 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
48 |
val parse_match_kind = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
49 |
Scan.lift @{keyword "conclusion"} >> K Match_Concl || |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
50 |
Scan.lift (@{keyword "premises"} |-- Args.mode "local") >> Match_Prems || |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
51 |
Scan.lift (@{keyword "("}) |-- Args.term --| Scan.lift (@{keyword ")"}) >> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
52 |
(fn t => Match_Term (Item_Net.update t aconv_net)) || |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
53 |
Attrib.thms >> (fn thms => Match_Fact (fold Item_Net.update thms Thm.full_rules)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
54 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
55 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
56 |
fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems _ => true | _ => false); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
57 |
fun prop_match m = (case m of Match_Term _ => false | _ => true); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
58 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
59 |
val bound_term : (term, binding) Parse_Tools.parse_val parser = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
60 |
Parse_Tools.parse_term_val Parse.binding; |
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 |
val fixes = |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
63 |
Parse.and_list1 (Scan.repeat1 (Parse.position bound_term) -- |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
64 |
Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
65 |
>> (fn (xs, T) => map (fn (x, pos) => ((x, T), pos)) xs)) >> flat; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
66 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
67 |
val for_fixes = Scan.optional (@{keyword "for"} |-- fixes) []; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
68 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
69 |
fun pos_of dyn = Parse_Tools.the_parse_val dyn |> Binding.pos_of; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
70 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
71 |
(*FIXME: Dynamic facts modify the background theory, so we have to resort |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
72 |
to token replacement for matched facts. *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
73 |
fun dynamic_fact ctxt = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
74 |
bound_term -- Args.opt_attribs (Attrib.check_name ctxt); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
75 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
76 |
type match_args = {multi : bool, cut : int}; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
77 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
78 |
val parse_match_args = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
79 |
Scan.optional (Args.parens (Parse.enum1 "," |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
80 |
(Args.$$$ "multi" -- Scan.succeed ~1 || Args.$$$ "cut" -- Scan.optional Parse.nat 1))) [] >> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
81 |
(fn ss => |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
82 |
fold (fn s => fn {multi, cut} => |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
83 |
(case s of |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
84 |
("multi", _) => {multi = true, cut = cut} |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
85 |
| ("cut", n) => {multi = multi, cut = n})) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
86 |
ss {multi = false, cut = ~1}); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
87 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
88 |
fun parse_named_pats match_kind = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
89 |
Args.context :|-- (fn ctxt => |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
90 |
Scan.lift (Parse.and_list1 |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
91 |
(Scan.option (dynamic_fact ctxt --| Args.colon) :-- |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
92 |
(fn opt_dyn => |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
93 |
if is_none opt_dyn orelse nameable_match match_kind |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
94 |
then Parse_Tools.name_term -- parse_match_args |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
95 |
else |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
96 |
let val b = #1 (the opt_dyn) |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
97 |
in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
98 |
-- for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.cartouche)) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
99 |
>> (fn ((ts, fixes), cartouche) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
100 |
(case Token.get_value cartouche of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
101 |
SOME (Token.Source src) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
102 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
103 |
val text = Method_Closure.read_inner_method ctxt src |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
104 |
val ts' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
105 |
map |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
106 |
(fn (b, (Parse_Tools.Real_Val v, match_args)) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
107 |
((Option.map (fn (b, att) => |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
108 |
(Parse_Tools.the_real_val b, att)) b, match_args), v) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
109 |
| _ => raise Fail "Expected closed term") ts |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
110 |
val fixes' = map (fn ((p, _), _) => Parse_Tools.the_real_val p) fixes |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
111 |
in (ts', fixes', text) end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
112 |
| SOME _ => error "Unexpected token value in match cartouche" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
113 |
| NONE => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
114 |
let |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
115 |
val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
116 |
val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
117 |
val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
118 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
119 |
val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
120 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
121 |
fun parse_term term = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
122 |
if prop_match match_kind |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
123 |
then Syntax.parse_prop ctxt3 term |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
124 |
else Syntax.parse_term ctxt3 term; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
125 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
126 |
fun drop_Trueprop_dummy t = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
127 |
(case t of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
128 |
Const (@{const_name Trueprop}, _) $ |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
129 |
(Const (@{syntax_const "_type_constraint_"}, T) $ |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
130 |
Const (@{const_name Pure.dummy_pattern}, _)) => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
131 |
Const (@{syntax_const "_type_constraint_"}, T) $ |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
132 |
Const (@{const_name Pure.dummy_pattern}, propT) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
133 |
| t1 $ t2 => drop_Trueprop_dummy t1 $ drop_Trueprop_dummy t2 |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
134 |
| Abs (a, T, b) => Abs (a, T, drop_Trueprop_dummy b) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
135 |
| _ => t); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
136 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
137 |
val pats = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
138 |
map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
139 |
|> map drop_Trueprop_dummy |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
140 |
|> (fn ts => fold_map Term.replace_dummy_patterns ts (Variable.maxidx_of ctxt3 + 1)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
141 |
|> fst |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
142 |
|> Syntax.check_terms ctxt3; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
143 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
144 |
val pat_fixes = fold (Term.add_frees) pats [] |> map fst; |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
145 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
146 |
val _ = |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
147 |
map2 (fn nm => fn (_, pos) => |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
148 |
member (op =) pat_fixes nm orelse |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
149 |
error ("For-fixed variable must be bound in some pattern" ^ Position.here pos)) |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
150 |
fix_nms fixes; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
151 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
152 |
val _ = map (Term.map_types Type.no_tvars) pats; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
153 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
154 |
val ctxt4 = fold Variable.declare_term pats ctxt3; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
155 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
156 |
val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
157 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
158 |
val real_fixes = map Free (fix_nms ~~ Ts); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
159 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
160 |
fun reject_extra_free (Free (x, _)) () = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
161 |
if Variable.is_fixed ctxt5 x then () |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
162 |
else error ("Illegal use of free (unfixed) variable " ^ quote x) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
163 |
| reject_extra_free _ () = (); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
164 |
val _ = (fold o fold_aterms) reject_extra_free pats (); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
165 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
166 |
val binds = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
167 |
map (fn (b, _) => Option.map (fn (b, att) => (Parse_Tools.the_parse_val b, att)) b) ts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
168 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
169 |
fun upd_ctxt (SOME (b, att)) pat (tms, ctxt) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
170 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
171 |
val ([nm], ctxt') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
172 |
Variable.variant_fixes [Name.internal (Binding.name_of b)] ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
173 |
val abs_nms = Term.strip_all_vars pat; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
174 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
175 |
val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
176 |
|> Conjunction.intr_balanced |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
177 |
|> Drule.generalize ([], map fst abs_nms) |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
178 |
|> Method_Closure.tag_free_thm; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
179 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
180 |
val atts = map (Attrib.attribute ctxt') att; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
181 |
val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt'; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
182 |
|
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
183 |
fun label_thm thm = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
184 |
Thm.cterm_of ctxt' (Free (nm, propT)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
185 |
|> Drule.mk_term |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
186 |
|> not (null abs_nms) ? Conjunction.intr thm |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
187 |
|
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
188 |
val [head_thm, body_thm] = |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
189 |
Drule.zero_var_indexes_list (map label_thm [param_thm, param_thm']) |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
190 |
|> map Method_Closure.tag_free_thm; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
191 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
192 |
val ctxt''' = |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
193 |
Attrib.local_notes "" [((b, []), [([body_thm], [])])] ctxt'' |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
194 |
|> snd |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
195 |
|> Variable.declare_maxidx (Thm.maxidx_of head_thm); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
196 |
in |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
197 |
(SOME (Thm.prop_of head_thm, att) :: tms, ctxt''') |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
198 |
end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
199 |
| upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
200 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
201 |
val (binds, ctxt6) = ctxt5 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
202 |
|> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
203 |
||> Proof_Context.restore_mode ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
204 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
205 |
val (src, text) = Method_Closure.read_inner_text_closure ctxt6 (Token.input_of cartouche); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
206 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
207 |
val morphism = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
208 |
Variable.export_morphism ctxt6 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
209 |
(ctxt |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
210 |
|> Token.declare_maxidx_src src |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
211 |
|> Variable.declare_maxidx (Variable.maxidx_of ctxt6)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
212 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
213 |
val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats; |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
214 |
val _ = ListPair.app (fn ((_, (v, _)), t) => Parse_Tools.the_parse_fun v t) (ts, pats'); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
215 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
216 |
fun close_src src = |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
217 |
let |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
218 |
val src' = Token.closure_src src |> Token.transform_src morphism; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
219 |
val _ = |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
220 |
map2 (fn tok1 => fn tok2 => |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
221 |
(case Token.get_value tok2 of |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
222 |
SOME value => Token.assign (SOME value) tok1 |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
223 |
| NONE => ())) |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
224 |
(Token.args_of_src src) |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
225 |
(Token.args_of_src src'); |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
226 |
in src' end; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
227 |
|
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
228 |
val binds' = |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
229 |
map (Option.map (fn (t, atts) => (Morphism.term morphism t, map close_src atts))) binds; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
230 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
231 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
232 |
ListPair.app |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
233 |
(fn ((SOME ((v, _)), _), SOME (t, _)) => Parse_Tools.the_parse_fun v t |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
234 |
| ((NONE, _), NONE) => () |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
235 |
| _ => error "Mismatch between real and parsed bound variables") |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
236 |
(ts, binds'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
237 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
238 |
val real_fixes' = map (Morphism.term morphism) real_fixes; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
239 |
val _ = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
240 |
ListPair.app (fn (((v, _) , _), t) => Parse_Tools.the_parse_fun v t) |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
241 |
(fixes, real_fixes'); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
242 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
243 |
val match_args = map (fn (_, (_, match_args)) => match_args) ts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
244 |
val binds'' = (binds' ~~ match_args) ~~ pats'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
245 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
246 |
val src' = Token.transform_src morphism src; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
247 |
val _ = Token.assign (SOME (Token.Source src')) cartouche; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
248 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
249 |
(binds'', real_fixes', text) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
250 |
end))); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
251 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
252 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
253 |
fun dest_internal_fact t = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
254 |
(case try Logic.dest_conjunction t of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
255 |
SOME (params, head) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
256 |
(params |> Logic.dest_conjunctions |> map Logic.dest_term, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
257 |
head |> Logic.dest_term) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
258 |
| NONE => ([], t |> Logic.dest_term)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
259 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
260 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
261 |
fun inst_thm ctxt env ts params thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
262 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
263 |
val ts' = map (Envir.norm_term env) ts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
264 |
val insts = map (Thm.cterm_of ctxt) ts' ~~ map (Thm.cterm_of ctxt) params; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
265 |
in |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
266 |
Drule.cterm_instantiate insts thm |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
267 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
268 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
269 |
fun do_inst fact_insts' env text ctxt = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
270 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
271 |
val fact_insts = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
272 |
map_filter |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
273 |
(fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
274 |
| _ => NONE) fact_insts'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
275 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
276 |
fun try_dest_term thm = try (Thm.prop_of #> dest_internal_fact #> snd) thm; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
277 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
278 |
fun expand_fact fact_insts thm = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
279 |
the_default [thm] |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
280 |
(case try_dest_term thm of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
281 |
SOME t_ident => AList.lookup (op aconv) fact_insts t_ident |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
282 |
| NONE => NONE); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
283 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
284 |
fun fact_morphism fact_insts = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
285 |
Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $> |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
286 |
Morphism.typ_morphism "do_inst.type" (Envir.norm_type (Envir.type_env env)) $> |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
287 |
Morphism.fact_morphism "do_inst.fact" (maps (expand_fact fact_insts)); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
288 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
289 |
fun apply_attribute (head, (fact, atts)) (fact_insts, ctxt) = |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
290 |
let |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
291 |
val morphism = fact_morphism fact_insts; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
292 |
val atts' = map (Attrib.attribute ctxt o Token.transform_src morphism) atts; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
293 |
val (fact'', ctxt') = fold_map (Thm.proof_attributes atts') fact ctxt; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
294 |
in ((head, fact'') :: fact_insts, ctxt') end; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
295 |
|
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
296 |
(*TODO: What to do about attributes that raise errors?*) |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
297 |
val (fact_insts', ctxt') = fold_rev (apply_attribute) fact_insts ([], ctxt); |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
298 |
|
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
299 |
val text' = Method.map_source (Token.transform_src (fact_morphism fact_insts')) text; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
300 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
301 |
(text', ctxt') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
302 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
303 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
304 |
fun DROP_CASES (tac: cases_tactic) : tactic = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
305 |
tac #> Seq.map (fn (_, st) => st); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
306 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
307 |
fun prep_fact_pat ((x, args), pat) ctxt = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
308 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
309 |
val ((params, pat'), ctxt') = Variable.focus pat ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
310 |
val params' = map (Free o snd) params; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
311 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
312 |
val morphism = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
313 |
Variable.export_morphism ctxt' |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
314 |
(ctxt |> Variable.declare_maxidx (Variable.maxidx_of ctxt')); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
315 |
val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
316 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
317 |
fun prep_head (t, att) = (dest_internal_fact t, att); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
318 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
319 |
((((Option.map prep_head x, args), params''), pat''), ctxt') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
320 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
321 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
322 |
fun recalculate_maxidx env = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
323 |
let |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
324 |
val tenv = Envir.term_env env; |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
325 |
val tyenv = Envir.type_env env; |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
326 |
val max_tidx = Vartab.fold (fn (_, (_, t)) => curry Int.max (maxidx_of_term t)) tenv ~1; |
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
327 |
val max_Tidx = Vartab.fold (fn (_, (_, T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
328 |
in |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
329 |
Envir.Envir |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
330 |
{maxidx = Int.max (Int.max (max_tidx, max_Tidx), Envir.maxidx_of env), |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
331 |
tenv = tenv, tyenv = tyenv} |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
332 |
end |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
333 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
334 |
fun morphism_env morphism env = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
335 |
let |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
336 |
val tenv = Envir.term_env env |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
337 |
|> Vartab.map (K (fn (T, t) => (Morphism.typ morphism T, Morphism.term morphism t))); |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
338 |
val tyenv = Envir.type_env env |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
339 |
|> Vartab.map (K (fn (S, T) => (S, Morphism.typ morphism T))); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
340 |
in Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv, tyenv = tyenv} end; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
341 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
342 |
fun export_with_params ctxt morphism (SOME ts, params) thm env = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
343 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
344 |
val outer_env = morphism_env morphism env; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
345 |
val thm' = Morphism.thm morphism thm; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
346 |
in inst_thm ctxt outer_env params ts thm' end |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
347 |
| export_with_params _ morphism (NONE,_) thm _ = Morphism.thm morphism thm; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
348 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
349 |
fun match_filter_env is_newly_fixed pat_vars fixes params env = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
350 |
let |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
351 |
val param_vars = map Term.dest_Var params; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
352 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
353 |
val tenv = Envir.term_env env; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
354 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
355 |
val params' = map (fn (xi, _) => Vartab.lookup tenv xi) param_vars; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
356 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
357 |
val fixes_vars = map Term.dest_Var fixes; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
358 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
359 |
val all_vars = Vartab.keys tenv; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
360 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
361 |
val extra_vars = subtract (fn ((xi, _), xi') => xi = xi') fixes_vars all_vars; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
362 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
363 |
val tenv' = tenv |> fold (Vartab.delete_safe) extra_vars; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
364 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
365 |
val env' = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
366 |
Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env} |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
367 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
368 |
val all_params_bound = forall (fn SOME (_, Free (x,_)) => is_newly_fixed x | _ => false) params'; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
369 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
370 |
val all_params_distinct = not (has_duplicates (op =) params'); |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
371 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
372 |
val pat_fixes = inter (eq_fst (op =)) fixes_vars pat_vars; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
373 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
374 |
val all_pat_fixes_bound = forall (fn (xi, _) => is_some (Vartab.lookup tenv' xi)) pat_fixes; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
375 |
in |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
376 |
if all_params_bound andalso all_pat_fixes_bound andalso all_params_distinct |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
377 |
then SOME env' |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
378 |
else NONE |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
379 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
380 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
381 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
382 |
(* Slightly hacky way of uniquely identifying focus premises *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
383 |
val prem_idN = "premise_id"; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
384 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
385 |
fun prem_id_eq ((id, _ : thm), (id', _ : thm)) = id = id'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
386 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
387 |
val prem_rules : (int * thm) Item_Net.T = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
388 |
Item_Net.init prem_id_eq (single o Thm.full_prop_of o snd); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
389 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
390 |
fun raw_thm_to_id thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
391 |
(case Properties.get (Thm.get_tags thm) prem_idN of NONE => NONE | SOME id => Int.fromString id) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
392 |
|> the_default ~1; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
393 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
394 |
structure Focus_Data = Proof_Data |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
395 |
( |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
396 |
type T = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
397 |
(int * (int * thm) Item_Net.T) * (*prems*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
398 |
Envir.tenv * (*schematics*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
399 |
term list (*params*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
400 |
fun init _ : T = ((0, prem_rules), Vartab.empty, []) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
401 |
); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
402 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
403 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
404 |
(* focus prems *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
405 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
406 |
val focus_prems = #1 o Focus_Data.get; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
407 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
408 |
fun hyp_from_premid ctxt (ident, prem) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
409 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
410 |
val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
411 |
val hyp = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
412 |
(case #hyps (Thm.crep_thm prem) of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
413 |
[hyp] => hyp |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
414 |
| _ => error "Prem should have exactly one hyp"); (* FIXME error vs. raise Fail !? *) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
415 |
val ct = Drule.mk_term (hyp) |> Thm.cprop_of; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
416 |
in Drule.protect (Conjunction.mk_conjunction (ident, ct)) end; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
417 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
418 |
fun hyp_from_ctermid ctxt (ident,cterm) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
419 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
420 |
val ident = Thm.cterm_of ctxt (HOLogic.mk_number @{typ nat} ident |> Logic.mk_term); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
421 |
in Drule.protect (Conjunction.mk_conjunction (ident, cterm)) end; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
422 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
423 |
fun add_premid_hyp premid ctxt = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
424 |
Thm.declare_hyps (hyp_from_premid ctxt premid) ctxt; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
425 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
426 |
fun add_focus_prem prem = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
427 |
`(Focus_Data.get #> #1 #> #1) ##> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
428 |
(Focus_Data.map o @{apply 3(1)}) (fn (next, net) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
429 |
(next + 1, Item_Net.update (next, Thm.tag_rule (prem_idN, string_of_int next) prem) net)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
430 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
431 |
fun remove_focus_prem' (ident, thm) = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
432 |
(Focus_Data.map o @{apply 3(1)} o apsnd) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
433 |
(Item_Net.remove (ident, thm)); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
434 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
435 |
fun remove_focus_prem thm = remove_focus_prem' (raw_thm_to_id thm, thm); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
436 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
437 |
(*TODO: Preliminary analysis to see if we're trying to clear in a non-focus match?*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
438 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
439 |
Theory.setup |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
440 |
(Attrib.setup @{binding "thin"} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
441 |
(Scan.succeed |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
442 |
(Thm.declaration_attribute (fn th => Context.mapping I (remove_focus_prem th)))) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
443 |
"clear premise inside match method"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
444 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
445 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
446 |
(* focus schematics *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
447 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
448 |
val focus_schematics = #2 o Focus_Data.get; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
449 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
450 |
fun add_focus_schematics cterms = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
451 |
(Focus_Data.map o @{apply 3(2)}) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
452 |
(fold (fn (Var (xi, T), t) => Vartab.update_new (xi, (T, t))) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
453 |
(map (apply2 Thm.term_of) cterms)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
454 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
455 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
456 |
(* focus params *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
457 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
458 |
val focus_params = #3 o Focus_Data.get; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
459 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
460 |
fun add_focus_params params = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
461 |
(Focus_Data.map o @{apply 3(3)}) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
462 |
(append (map (fn (_, ct) => Thm.term_of ct) params)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
463 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
464 |
fun solve_term ct = Thm.trivial ct OF [Drule.termI]; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
465 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
466 |
fun get_thinned_prems goal = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
467 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
468 |
val chyps = Thm.crep_thm goal |> #hyps; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
469 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
470 |
fun prem_from_hyp hyp goal = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
471 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
472 |
val asm = Thm.assume hyp; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
473 |
val (identt,ct) = asm |> Goal.conclude |> Thm.cprop_of |> Conjunction.dest_conjunction; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
474 |
val ident = HOLogic.dest_number (Thm.term_of identt |> Logic.dest_term) |> snd; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
475 |
val thm = Conjunction.intr (solve_term identt) (solve_term ct) |> Goal.protect 0 |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
476 |
val goal' = Thm.implies_elim (Thm.implies_intr hyp goal) thm; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
477 |
in |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
478 |
(SOME (ident,ct),goal') |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
479 |
end handle TERM _ => (NONE,goal) | THM _ => (NONE,goal); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
480 |
in |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
481 |
fold_map prem_from_hyp chyps goal |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
482 |
|>> map_filter I |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
483 |
end; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
484 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
485 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
486 |
(* Add focus elements as proof data *) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
487 |
fun augment_focus (focus: Subgoal.focus) : (int list * Subgoal.focus) = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
488 |
let |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
489 |
val {context, params, prems, asms, concl, schematics} = focus; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
490 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
491 |
val (prem_ids,ctxt') = context |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
492 |
|> add_focus_params params |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
493 |
|> add_focus_schematics (snd schematics) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
494 |
|> fold_map add_focus_prem (rev prems) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
495 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
496 |
val local_prems = map2 pair prem_ids (rev prems); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
497 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
498 |
val ctxt'' = fold add_premid_hyp local_prems ctxt'; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
499 |
in |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
500 |
(prem_ids,{context = ctxt'', |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
501 |
params = params, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
502 |
prems = prems, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
503 |
concl = concl, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
504 |
schematics = schematics, |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
505 |
asms = asms}) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
506 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
507 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
508 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
509 |
(* Fix schematics in the goal *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
510 |
fun focus_concl ctxt i goal = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
511 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
512 |
val ({context, concl, params, prems, asms, schematics}, goal') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
513 |
Subgoal.focus_params ctxt i goal; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
514 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
515 |
val ((_, schematic_terms), context') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
516 |
Variable.import_inst true [Thm.term_of concl] context |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
517 |
|>> Thm.certify_inst (Thm.theory_of_thm goal'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
518 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
519 |
val goal'' = Thm.instantiate ([], schematic_terms) goal'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
520 |
val concl' = Thm.instantiate_cterm ([], schematic_terms) concl; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
521 |
val (schematic_types, schematic_terms') = schematics; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
522 |
val schematics' = (schematic_types, schematic_terms @ schematic_terms'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
523 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
524 |
({context = context', concl = concl', params = params, prems = prems, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
525 |
schematics = schematics', asms = asms} : Subgoal.focus, goal'') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
526 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
527 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
528 |
|
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
529 |
fun deduplicate eq prev seq = |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
530 |
Seq.make (fn () => |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
531 |
(case Seq.pull seq of |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
532 |
SOME (x, seq') => |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
533 |
if member eq prev x |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
534 |
then Seq.pull (deduplicate eq prev seq') |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
535 |
else SOME (x, deduplicate eq (x :: prev) seq') |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
536 |
| NONE => NONE)); |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
537 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
538 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
539 |
fun consistent_env env = |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
540 |
let |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
541 |
val tenv = Envir.term_env env; |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
542 |
val tyenv = Envir.type_env env; |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
543 |
in |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
544 |
forall (fn (_, (T, t)) => Envir.norm_type tyenv T = fastype_of t) (Vartab.dest tenv) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
545 |
end; |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
546 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
547 |
fun term_eq_wrt (env1,env2) (t1,t2) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
548 |
Envir.eta_contract (Envir.norm_term env1 t1) aconv |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
549 |
Envir.eta_contract (Envir.norm_term env2 t2); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
550 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
551 |
fun type_eq_wrt (env1,env2) (T1,T2) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
552 |
Envir.norm_type (Envir.type_env env1) T1 = Envir.norm_type (Envir.type_env env2) T2 |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
553 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
554 |
|
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
555 |
fun eq_env (env1, env2) = |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
556 |
Envir.maxidx_of env1 = Envir.maxidx_of env1 andalso |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
557 |
ListPair.allEq (fn ((var, (_, t)), (var', (_, t'))) => |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
558 |
(var = var' andalso term_eq_wrt (env1,env2) (t,t'))) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
559 |
(apply2 Vartab.dest (Envir.term_env env1, Envir.term_env env2)) |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
560 |
andalso |
60248
f7e4294216d2
updated Eisbach, using version fb741500f533 of its Bitbucket repository;
wenzelm
parents:
60209
diff
changeset
|
561 |
ListPair.allEq (fn ((var, (_, T)), (var', (_, T'))) => |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
562 |
var = var' andalso type_eq_wrt (env1,env2) (T,T')) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
563 |
(apply2 Vartab.dest (Envir.type_env env1, Envir.type_env env2)); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
564 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
565 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
566 |
fun merge_env (env1,env2) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
567 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
568 |
val tenv = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
569 |
Vartab.merge (eq_snd (term_eq_wrt (env1, env2))) (Envir.term_env env1, Envir.term_env env2); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
570 |
val tyenv = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
571 |
Vartab.merge (eq_snd (type_eq_wrt (env1, env2)) andf eq_fst (op =)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
572 |
(Envir.type_env env1,Envir.type_env env2); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
573 |
val maxidx = Int.max (Envir.maxidx_of env1, Envir.maxidx_of env2); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
574 |
in Envir.Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv} end; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
575 |
|
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
576 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
577 |
fun import_with_tags thms ctxt = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
578 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
579 |
val ((_, thms'), ctxt') = Variable.import false thms ctxt; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
580 |
val thms'' = map2 (fn thm => Thm.map_tags (K (Thm.get_tags thm))) thms thms'; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
581 |
in (thms'', ctxt') end; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
582 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
583 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
584 |
fun try_merge (env, env') = SOME (merge_env (env, env')) handle Vartab.DUP _ => NONE |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
585 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
586 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
587 |
fun Seq_retrieve seq f = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
588 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
589 |
fun retrieve' (list, seq) f = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
590 |
(case Seq.pull seq of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
591 |
SOME (x, seq') => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
592 |
if f x then (SOME x, (list, seq')) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
593 |
else retrieve' (list @ [x], seq') f |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
594 |
| NONE => (NONE, (list, seq))); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
595 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
596 |
val (result, (list, seq)) = retrieve' ([], seq) f; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
597 |
in (result, Seq.append (Seq.of_list list) seq) end; |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
598 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
599 |
fun match_facts ctxt fixes prop_pats get = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
600 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
601 |
fun is_multi (((_, x : match_args), _), _) = #multi x; |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
602 |
fun get_cut (((_, x : match_args), _), _) = #cut x; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
603 |
fun do_cut n = if n = ~1 then I else Seq.take n; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
604 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
605 |
val raw_thmss = map (get o snd) prop_pats; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
606 |
val (thmss,ctxt') = fold_burrow import_with_tags raw_thmss ctxt; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
607 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
608 |
val newly_fixed = Variable.is_newly_fixed ctxt' ctxt; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
609 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
610 |
val morphism = Variable.export_morphism ctxt' ctxt; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
611 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
612 |
fun match_thm (((x, params), pat), thm) = |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
613 |
let |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
614 |
val pat_vars = Term.add_vars pat []; |
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
615 |
|
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
616 |
val ts = Option.map (fst o fst) (fst x); |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
617 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
618 |
val item' = Thm.prop_of thm; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
619 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
620 |
val matches = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
621 |
(Unify.matchers (Context.Proof ctxt) [(pat, item')]) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
622 |
|> Seq.filter consistent_env |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
623 |
|> Seq.map_filter (fn env' => |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
624 |
(case match_filter_env newly_fixed pat_vars fixes params env' of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
625 |
SOME env'' => SOME (export_with_params ctxt morphism (ts,params) thm env',env'') |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
626 |
| NONE => NONE)) |
60209
022ca2799c73
updated Eisbach, using version 5df3d8c72403 of its Bitbucket repository;
wenzelm
parents:
60119
diff
changeset
|
627 |
|> Seq.map (apfst (Thm.map_tags (K (Thm.get_tags thm)))) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
628 |
|> deduplicate (eq_pair Thm.eq_thm_prop eq_env) [] |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
629 |
in matches end; |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
630 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
631 |
val all_matches = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
632 |
map2 pair prop_pats thmss |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
633 |
|> map (fn (pat, matches) => (pat, map (fn thm => match_thm (pat, thm)) matches)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
634 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
635 |
fun proc_multi_match (pat, thmenvs) (pats, env) = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
636 |
do_cut (get_cut pat) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
637 |
(if is_multi pat then |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
638 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
639 |
fun maximal_set tail seq envthms = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
640 |
Seq.make (fn () => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
641 |
(case Seq.pull seq of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
642 |
SOME ((thm, env'), seq') => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
643 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
644 |
val (result, envthms') = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
645 |
Seq_retrieve envthms (fn (env, _) => eq_env (env, env')); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
646 |
in |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
647 |
(case result of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
648 |
SOME (_,thms) => SOME ((env', thm :: thms), maximal_set tail seq' envthms') |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
649 |
| NONE => Seq.pull (maximal_set (tail @ [(env', [thm])]) seq' envthms')) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
650 |
end |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
651 |
| NONE => Seq.pull (Seq.append envthms (Seq.of_list tail)))); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
652 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
653 |
val maximal_sets = fold (maximal_set []) thmenvs Seq.empty; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
654 |
in |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
655 |
maximal_sets |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
656 |
|> Seq.map swap |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
657 |
|> Seq.filter (fn (thms, _) => not (null thms)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
658 |
|> Seq.map_filter (fn (thms, env') => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
659 |
(case try_merge (env, env') of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
660 |
SOME env'' => SOME ((pat, thms) :: pats, env'') |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
661 |
| NONE => NONE)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
662 |
end |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
663 |
else |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
664 |
let |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
665 |
fun just_one (thm, env') = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
666 |
(case try_merge (env,env') of |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
667 |
SOME env'' => SOME ((pat,[thm]) :: pats, env'') |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
668 |
| NONE => NONE); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
669 |
in fold (fn seq => Seq.append (Seq.map_filter just_one seq)) thmenvs Seq.empty end); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
670 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
671 |
val all_matches = |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
672 |
Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
673 |
in |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
674 |
all_matches |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
675 |
|> Seq.map (apsnd (morphism_env morphism)) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
676 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
677 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
678 |
fun real_match using ctxt fixes m text pats goal = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
679 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
680 |
fun make_fact_matches ctxt get = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
681 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
682 |
val (pats', ctxt') = fold_map prep_fact_pat pats ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
683 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
684 |
match_facts ctxt' fixes pats' get |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
685 |
|> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
686 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
687 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
688 |
fun make_term_matches ctxt get = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
689 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
690 |
val pats' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
691 |
map |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
692 |
(fn ((SOME _, _), _) => error "Cannot name term match" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
693 |
| ((_, x), t) => (((NONE, x), []), Logic.mk_term t)) pats; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
694 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
695 |
val thm_of = Drule.mk_term o Thm.cterm_of ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
696 |
fun get' t = get (Logic.dest_term t) |> map thm_of; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
697 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
698 |
match_facts ctxt fixes pats' get' |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
699 |
|> Seq.map (fn (fact_insts, env) => do_inst fact_insts env text ctxt) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
700 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
701 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
702 |
(case m of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
703 |
Match_Fact net => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
704 |
Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using goal) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
705 |
(make_fact_matches ctxt (Item_Net.retrieve net)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
706 |
| Match_Term net => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
707 |
Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using goal) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
708 |
(make_term_matches ctxt (Item_Net.retrieve net)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
709 |
| match_kind => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
710 |
if Thm.no_prems goal then Seq.empty |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
711 |
else |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
712 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
713 |
fun focus_cases f g = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
714 |
(case match_kind of |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
715 |
Match_Prems b => f b |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
716 |
| Match_Concl => g |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
717 |
| _ => raise Fail "Match kind fell through"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
718 |
|
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
719 |
val (goal_thins,goal) = get_thinned_prems goal; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
720 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
721 |
val ((local_premids,{context = focus_ctxt, params, asms, concl, ...}), focused_goal) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
722 |
focus_cases (K Subgoal.focus_prems) (focus_concl) ctxt 1 goal |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
723 |
|>> augment_focus; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
724 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
725 |
val texts = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
726 |
focus_cases |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
727 |
(fn is_local => fn _ => |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
728 |
make_fact_matches focus_ctxt |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
729 |
(Item_Net.retrieve (focus_prems focus_ctxt |> snd) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
730 |
#> filter_out (member (eq_fst (op =)) goal_thins) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
731 |
#> is_local ? filter (fn (p,_) => exists (fn id' => id' = p) local_premids) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
732 |
#> order_list)) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
733 |
(fn _ => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
734 |
make_term_matches focus_ctxt (fn _ => [Logic.strip_imp_concl (Thm.term_of concl)])) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
735 |
(); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
736 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
737 |
(*TODO: How to handle cases? *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
738 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
739 |
fun do_retrofit inner_ctxt goal' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
740 |
let |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
741 |
val (goal'_thins,goal') = get_thinned_prems goal'; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
742 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
743 |
val thinned_prems = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
744 |
((subtract (eq_fst (op =)) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
745 |
(focus_prems inner_ctxt |> snd |> Item_Net.content) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
746 |
(focus_prems focus_ctxt |> snd |> Item_Net.content)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
747 |
|> map (fn (id, thm) => |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
748 |
#hyps (Thm.crep_thm thm) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
749 |
|> (fn [chyp] => (id, (SOME chyp, NONE)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
750 |
| _ => error "Prem should have only one hyp"))); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
751 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
752 |
val all_thinned_prems = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
753 |
thinned_prems @ |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
754 |
map (fn (id, prem) => (id, (NONE, SOME prem))) (goal'_thins @ goal_thins); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
755 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
756 |
val (thinned_local_prems,thinned_extra_prems) = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
757 |
List.partition (fn (id, _) => member (op =) local_premids id) all_thinned_prems; |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
758 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
759 |
val local_thins = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
760 |
thinned_local_prems |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
761 |
|> map (fn (_, (SOME t, _)) => Thm.term_of t |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
762 |
| (_, (_, SOME pt)) => Thm.term_of pt |> Logic.dest_term); |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
763 |
|
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
764 |
val extra_thins = |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
765 |
thinned_extra_prems |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
766 |
|> map (fn (id, (SOME ct, _)) => (id, Drule.mk_term ct |> Thm.cprop_of) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
767 |
| (id, (_, SOME pt)) => (id, pt)) |
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
768 |
|> map (hyp_from_ctermid inner_ctxt); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
769 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
770 |
val n_subgoals = Thm.nprems_of goal'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
771 |
fun prep_filter t = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
772 |
Term.subst_bounds (map (Thm.term_of o snd) params |> rev, Term.strip_all_body t); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
773 |
fun filter_test prems t = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
774 |
if member (op =) prems t then SOME (remove1 (op aconv) t prems) else NONE; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
775 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
776 |
Subgoal.retrofit inner_ctxt ctxt params asms 1 goal' goal |> |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
777 |
(if n_subgoals = 0 orelse null local_thins then I |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
778 |
else |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
779 |
Seq.map (Goal.restrict 1 n_subgoals) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
780 |
#> Seq.maps (ALLGOALS (fn i => |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
781 |
DETERM (filter_prems_tac' ctxt prep_filter filter_test local_thins i))) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
782 |
#> Seq.map (Goal.unrestrict 1)) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
783 |
|> Seq.map (fold Thm.weaken extra_thins) |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
784 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
785 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
786 |
fun apply_text (text, ctxt') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
787 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
788 |
val goal' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
789 |
DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
790 |
|> Seq.maps (DETERM (do_retrofit ctxt')) |
60285
b4f1a0a701ae
updated Eisbach, using version 4863020a8fe9 of its Bitbucket repository;
wenzelm
parents:
60248
diff
changeset
|
791 |
|> Seq.map (fn goal => ([]: cases, goal)); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
792 |
in goal' end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
793 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
794 |
Seq.map apply_text texts |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
795 |
end) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
796 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
797 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
798 |
val match_parser = |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
799 |
parse_match_kind :-- (fn kind => |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
800 |
Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >> |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
801 |
(fn (matches, bodies) => fn ctxt => fn using => fn goal => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
802 |
if Method_Closure.is_dummy goal then Seq.empty |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
803 |
else |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
804 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
805 |
fun exec (pats, fixes, text) goal = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
806 |
let |
60287
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
807 |
val ctxt' = |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
808 |
fold Variable.declare_term fixes ctxt |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
809 |
|> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*) |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
810 |
in real_match using ctxt' fixes matches text pats goal end; |
adde5ce1e0a7
updated Eisbach, using version 134bc592909c of its Bitbucket repository;
wenzelm
parents:
60285
diff
changeset
|
811 |
in Seq.flat (Seq.FIRST (map exec bodies) goal) end); |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
812 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
813 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
814 |
Theory.setup |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
815 |
(Method.setup @{binding match} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
816 |
(match_parser >> (fn m => fn ctxt => METHOD_CASES (m ctxt))) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
817 |
"structural analysis/matching on goals"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
818 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
819 |
end; |