author | wenzelm |
Fri, 17 Apr 2015 17:49:19 +0200 | |
changeset 60119 | 54bea620e54f |
child 60209 | 022ca2799c73 |
permissions | -rw-r--r-- |
60119
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: match_method.ML |
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 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
43 |
| Match_Prems; |
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 = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
49 |
Scan.lift @{keyword "concl"} >> K Match_Concl || |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
50 |
Scan.lift @{keyword "prems"} >> K Match_Prems || |
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 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
56 |
fun nameable_match m = (case m of Match_Fact _ => true | Match_Prems => true | _ => false); |
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 = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
63 |
Parse.and_list1 (Scan.repeat1 bound_term -- |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
64 |
Scan.option (@{keyword "::"} |-- Parse.!!! Parse.typ) >> (fn (xs, T) => map (rpair T) xs)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
65 |
>> flat; |
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 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
69 |
fun pos_of dyn = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
70 |
(case dyn of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
71 |
Parse_Tools.Parse_Val (b, _) => Binding.pos_of b |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
72 |
| _ => raise Fail "Not a parse value"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
73 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
74 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
75 |
(*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
|
76 |
to token replacement for matched facts. *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
77 |
fun dynamic_fact ctxt = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
78 |
bound_term -- Args.opt_attribs (Attrib.check_name ctxt); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
79 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
80 |
type match_args = {unify : bool, multi : bool, cut : bool}; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
81 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
82 |
val parse_match_args = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
83 |
Scan.optional (Args.parens (Parse.enum1 "," |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
84 |
(Args.$$$ "unify" || Args.$$$ "multi" || Args.$$$ "cut"))) [] >> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
85 |
(fn ss => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
86 |
fold (fn s => fn {unify, multi, cut} => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
87 |
(case s of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
88 |
"unify" => {unify = true, multi = multi, cut = cut} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
89 |
| "multi" => {unify = unify, multi = true, cut = cut} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
90 |
| "cut" => {unify = unify, multi = multi, cut = true})) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
91 |
ss {unify = false, multi = false, cut = false}); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
92 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
93 |
(*TODO: Shape holes in thms *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
94 |
fun parse_named_pats match_kind = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
95 |
Args.context :|-- (fn ctxt => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
96 |
Scan.lift (Parse.and_list1 (Scan.option (dynamic_fact ctxt --| Args.colon) :-- |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
97 |
(fn opt_dyn => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
98 |
if is_none opt_dyn orelse nameable_match match_kind |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
99 |
then Parse_Tools.name_term -- parse_match_args |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
100 |
else |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
101 |
let val b = #1 (the opt_dyn) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
102 |
in error ("Cannot bind fact name in term match" ^ Position.here (pos_of b)) end)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
103 |
-- for_fixes -- (@{keyword "\<Rightarrow>"} |-- Parse.token Parse.cartouche)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
104 |
>> (fn ((ts, fixes), cartouche) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
105 |
(case Token.get_value cartouche of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
106 |
SOME (Token.Source src) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
107 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
108 |
val text = Method_Closure.read_inner_method ctxt src |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
109 |
(*TODO: Correct parse context for attributes?*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
110 |
val ts' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
111 |
map |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
112 |
(fn (b, (Parse_Tools.Real_Val v, match_args)) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
113 |
((Option.map (fn (b, att) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
114 |
(Parse_Tools.the_real_val b, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
115 |
map (Attrib.attribute ctxt) att)) b, match_args), v) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
116 |
| _ => raise Fail "Expected closed term") ts |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
117 |
val fixes' = map (fn (p, _) => Parse_Tools.the_real_val p) fixes |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
118 |
in (ts', fixes', text) end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
119 |
| SOME _ => error "Unexpected token value in match cartouche" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
120 |
| NONE => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
121 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
122 |
val fixes' = map (fn (pb, otyp) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
123 |
val (fixes'', ctxt1) = Proof_Context.read_vars fixes' ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
124 |
val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
125 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
126 |
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
|
127 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
128 |
fun parse_term term = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
129 |
if prop_match match_kind |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
130 |
then Syntax.parse_prop ctxt3 term |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
131 |
else Syntax.parse_term ctxt3 term; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
132 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
133 |
val pats = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
134 |
map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
135 |
|> Syntax.check_terms ctxt3; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
136 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
137 |
val ctxt4 = fold Variable.declare_term pats ctxt3; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
138 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
139 |
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
|
140 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
141 |
val real_fixes = map Free (fix_nms ~~ Ts); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
142 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
143 |
fun reject_extra_free (Free (x, _)) () = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
144 |
if Variable.is_fixed ctxt5 x then () |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
145 |
else error ("Illegal use of free (unfixed) variable " ^ quote x) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
146 |
| reject_extra_free _ () = (); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
147 |
val _ = (fold o fold_aterms) reject_extra_free pats (); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
148 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
149 |
(*fun test_multi_bind {multi = multi, ...} pat = multi andalso |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
150 |
not (null (inter (op =) (map Free (Term.add_frees pat [])) real_fixes)) andalso |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
151 |
error "Cannot fix terms in multi-match. Use a schematic instead." |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
152 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
153 |
val _ = map2 (fn pat => fn (_, (_, match_args)) => test_multi_bind match_args pat) pats ts*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
154 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
155 |
val binds = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
156 |
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
|
157 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
158 |
fun upd_ctxt (SOME (b, att)) pat (tms, ctxt) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
159 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
160 |
val ([nm], ctxt') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
161 |
Variable.variant_fixes [Name.internal (Binding.name_of b)] ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
162 |
val abs_nms = Term.strip_all_vars pat; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
163 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
164 |
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
|
165 |
|> Conjunction.intr_balanced |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
166 |
|> Drule.generalize ([], map fst abs_nms); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
167 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
168 |
val thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
169 |
Thm.cterm_of ctxt' (Free (nm, propT)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
170 |
|> Drule.mk_term |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
171 |
|> not (null abs_nms) ? Conjunction.intr param_thm |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
172 |
|> Drule.zero_var_indexes |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
173 |
|> Method_Closure.tag_free_thm; |
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 |
(*TODO: Preprocess attributes here?*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
176 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
177 |
val (_, ctxt'') = Proof_Context.note_thmss "" [((b, []), [([thm], [])])] ctxt'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
178 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
179 |
(SOME (Thm.prop_of thm, map (Attrib.attribute ctxt) att) :: tms, ctxt'') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
180 |
end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
181 |
| upd_ctxt NONE _ (tms, ctxt) = (NONE :: tms, ctxt); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
182 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
183 |
val (binds, ctxt6) = ctxt5 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
184 |
|> (fn ctxt => fold2 upd_ctxt binds pats ([], ctxt) |> apfst rev) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
185 |
||> Proof_Context.restore_mode ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
186 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
187 |
val (src, text) = Method_Closure.read_text_closure ctxt6 (Token.input_of cartouche); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
188 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
189 |
val morphism = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
190 |
Variable.export_morphism ctxt6 |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
191 |
(ctxt |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
192 |
|> Token.declare_maxidx_src src |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
193 |
|> Variable.declare_maxidx (Variable.maxidx_of ctxt6)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
194 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
195 |
val pats' = map (Term.map_types Type_Infer.paramify_vars #> Morphism.term morphism) pats; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
196 |
val _ = ListPair.app (fn ((_, (Parse_Tools.Parse_Val (_, f), _)), t) => f t) (ts, pats'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
197 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
198 |
val binds' = map (Option.map (fn (t, atts) => (Morphism.term morphism t, atts))) binds; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
199 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
200 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
201 |
ListPair.app |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
202 |
(fn ((SOME ((Parse_Tools.Parse_Val (_, f), _)), _), SOME (t, _)) => f t |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
203 |
| ((NONE, _), NONE) => () |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
204 |
| _ => error "Mismatch between real and parsed bound variables") |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
205 |
(ts, binds'); |
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 real_fixes' = map (Morphism.term morphism) real_fixes; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
208 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
209 |
ListPair.app (fn ((Parse_Tools.Parse_Val (_, f), _), t) => f t) (fixes, real_fixes'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
210 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
211 |
val match_args = map (fn (_, (_, match_args)) => match_args) ts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
212 |
val binds'' = (binds' ~~ match_args) ~~ pats'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
213 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
214 |
val src' = Token.transform_src morphism src; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
215 |
val _ = Token.assign (SOME (Token.Source src')) cartouche; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
216 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
217 |
(binds'', real_fixes', text) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
218 |
end))); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
219 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
220 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
221 |
fun parse_match_bodies match_kind = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
222 |
Parse.enum1' "\<bar>" (parse_named_pats match_kind); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
223 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
224 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
225 |
fun dest_internal_fact t = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
226 |
(case try Logic.dest_conjunction t of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
227 |
SOME (params, head) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
228 |
(params |> Logic.dest_conjunctions |> map Logic.dest_term, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
229 |
head |> Logic.dest_term) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
230 |
| NONE => ([], t |> Logic.dest_term)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
231 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
232 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
233 |
fun inst_thm ctxt env ts params thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
234 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
235 |
val ts' = map (Envir.norm_term env) ts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
236 |
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
|
237 |
val tags = Thm.get_tags thm; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
238 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
239 |
(* |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
240 |
val Tinsts = Type.raw_matches ((map (fastype_of) params), (map (fastype_of) ts')) Vartab.empty |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
241 |
|> Vartab.dest |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
242 |
|> map (fn (xi, (S, typ)) => (certT (TVar (xi, S)), certT typ)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
243 |
*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
244 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
245 |
val thm' = Drule.cterm_instantiate insts thm |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
246 |
(*|> Thm.instantiate (Tinsts, [])*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
247 |
|> Thm.map_tags (K tags); |
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 |
thm' |
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 |
fun do_inst fact_insts' env text ctxt = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
253 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
254 |
val fact_insts = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
255 |
map_filter |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
256 |
(fn ((((SOME ((_, head), att), _), _), _), thms) => SOME (head, (thms, att)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
257 |
| _ => NONE) fact_insts'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
258 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
259 |
fun apply_attribute thm att ctxt = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
260 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
261 |
val (opt_context', thm') = att (Context.Proof ctxt, thm) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
262 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
263 |
(case thm' of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
264 |
SOME _ => error "Rule attributes cannot be applied here" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
265 |
| _ => the_default ctxt (Option.map Context.proof_of opt_context')) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
266 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
267 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
268 |
fun apply_attributes atts thm = fold (apply_attribute thm) atts; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
269 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
270 |
(*TODO: What to do about attributes that raise errors?*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
271 |
val (fact_insts, ctxt') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
272 |
fold_map (fn (head, (thms, atts : attribute list)) => fn ctxt => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
273 |
((head, thms), fold (apply_attributes atts) thms ctxt)) fact_insts ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
274 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
275 |
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
|
276 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
277 |
fun expand_fact thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
278 |
the_default [thm] |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
279 |
(case try_dest_term thm of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
280 |
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
|
281 |
| NONE => NONE); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
282 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
283 |
val morphism = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
284 |
Morphism.term_morphism "do_inst.term" (Envir.norm_term env) $> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
285 |
Morphism.fact_morphism "do_inst.fact" (maps expand_fact); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
286 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
287 |
val text' = Method.map_source (Token.transform_src morphism) text; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
288 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
289 |
(text', ctxt') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
290 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
291 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
292 |
fun DROP_CASES (tac: cases_tactic) : tactic = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
293 |
tac #> Seq.map (fn (_, st) => st); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
294 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
295 |
fun prep_fact_pat ((x, args), pat) ctxt = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
296 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
297 |
val ((params, pat'), ctxt') = Variable.focus pat ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
298 |
val params' = map (Free o snd) params; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
299 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
300 |
val morphism = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
301 |
Variable.export_morphism ctxt' |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
302 |
(ctxt |> Variable.declare_maxidx (Variable.maxidx_of ctxt')); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
303 |
val pat'' :: params'' = map (Morphism.term morphism) (pat' :: params'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
304 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
305 |
fun prep_head (t, att) = (dest_internal_fact t, att); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
306 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
307 |
((((Option.map prep_head x, args), params''), pat''), ctxt') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
308 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
309 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
310 |
fun match_filter_env ctxt fixes (ts, params) thm env = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
311 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
312 |
val param_vars = map Term.dest_Var params; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
313 |
val params' = map (Envir.lookup env) param_vars; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
314 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
315 |
val fixes_vars = map Term.dest_Var fixes; |
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 |
val tenv = Envir.term_env env; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
318 |
val all_vars = Vartab.keys tenv; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
319 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
320 |
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
|
321 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
322 |
val tenv' = Envir.term_env env |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
323 |
|> fold (Vartab.delete_safe) extra_vars; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
324 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
325 |
val env' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
326 |
Envir.Envir {maxidx = Envir.maxidx_of env, tenv = tenv', tyenv = Envir.type_env env}; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
327 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
328 |
val all_params_bound = forall (fn SOME (Var _) => true | _ => false) params'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
329 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
330 |
if all_params_bound |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
331 |
then SOME (case ts of SOME ts => inst_thm ctxt env params ts thm | _ => thm, env') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
332 |
else NONE |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
333 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
334 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
335 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
336 |
(* Slightly hacky way of uniquely identifying focus premises *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
337 |
val prem_idN = "premise_id"; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
338 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
339 |
fun prem_id_eq ((id, _ : thm), (id', _ : thm)) = id = id'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
340 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
341 |
val prem_rules : (int * thm) Item_Net.T = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
342 |
Item_Net.init prem_id_eq (single o Thm.full_prop_of o snd); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
343 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
344 |
fun raw_thm_to_id thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
345 |
(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
|
346 |
|> the_default ~1; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
347 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
348 |
structure Focus_Data = Proof_Data |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
349 |
( |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
350 |
type T = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
351 |
(int * (int * thm) Item_Net.T) * (*prems*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
352 |
Envir.tenv * (*schematics*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
353 |
term list (*params*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
354 |
fun init _ : T = ((0, prem_rules), Vartab.empty, []) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
355 |
); |
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 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
358 |
(* focus prems *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
359 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
360 |
val focus_prems = #1 o Focus_Data.get; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
361 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
362 |
fun add_focus_prem prem = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
363 |
(Focus_Data.map o @{apply 3(1)}) (fn (next, net) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
364 |
(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
|
365 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
366 |
fun remove_focus_prem thm = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
367 |
(Focus_Data.map o @{apply 3(1)} o apsnd) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
368 |
(Item_Net.remove (raw_thm_to_id thm, thm)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
369 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
370 |
(*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
|
371 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
372 |
Theory.setup |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
373 |
(Attrib.setup @{binding "thin"} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
374 |
(Scan.succeed |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
375 |
(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
|
376 |
"clear premise inside match method"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
377 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
378 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
379 |
(* focus schematics *) |
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 |
val focus_schematics = #2 o Focus_Data.get; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
382 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
383 |
fun add_focus_schematics cterms = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
384 |
(Focus_Data.map o @{apply 3(2)}) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
385 |
(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
|
386 |
(map (apply2 Thm.term_of) cterms)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
387 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
388 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
389 |
(* focus params *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
390 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
391 |
val focus_params = #3 o Focus_Data.get; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
392 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
393 |
fun add_focus_params params = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
394 |
(Focus_Data.map o @{apply 3(3)}) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
395 |
(append (map (fn (_, ct) => Thm.term_of ct) params)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
396 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
397 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
398 |
(* Add focus elements as proof data *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
399 |
fun augment_focus |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
400 |
({context, params, prems, asms, concl, schematics} : Subgoal.focus) : Subgoal.focus = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
401 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
402 |
val context' = context |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
403 |
|> add_focus_params params |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
404 |
|> add_focus_schematics (snd schematics) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
405 |
|> fold add_focus_prem (rev prems); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
406 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
407 |
{context = context', |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
408 |
params = params, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
409 |
prems = prems, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
410 |
concl = concl, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
411 |
schematics = schematics, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
412 |
asms = asms} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
413 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
414 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
415 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
416 |
(* Fix schematics in the goal *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
417 |
fun focus_concl ctxt i goal = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
418 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
419 |
val ({context, concl, params, prems, asms, schematics}, goal') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
420 |
Subgoal.focus_params ctxt i goal; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
421 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
422 |
val ((_, schematic_terms), context') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
423 |
Variable.import_inst true [Thm.term_of concl] context |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
424 |
|>> Thm.certify_inst (Thm.theory_of_thm goal'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
425 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
426 |
val goal'' = Thm.instantiate ([], schematic_terms) goal'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
427 |
val concl' = Thm.instantiate_cterm ([], schematic_terms) concl; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
428 |
val (schematic_types, schematic_terms') = schematics; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
429 |
val schematics' = (schematic_types, schematic_terms @ schematic_terms'); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
430 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
431 |
({context = context', concl = concl', params = params, prems = prems, |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
432 |
schematics = schematics', asms = asms} : Subgoal.focus, goal'') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
433 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
434 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
435 |
exception MATCH_CUT; |
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 |
val raise_match : (thm * Envir.env) Seq.seq = Seq.make (fn () => raise MATCH_CUT); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
438 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
439 |
fun match_facts ctxt fixes prop_pats get = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
440 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
441 |
fun is_multi (((_, x : match_args), _), _) = #multi x; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
442 |
fun is_unify (_, x : match_args) = #unify x; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
443 |
fun is_cut (_, x : match_args) = #cut x; |
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 |
fun match_thm (((x, params), pat), thm) env = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
446 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
447 |
fun try_dest_term term = the_default term (try Logic.dest_term term); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
448 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
449 |
val pat' = pat |> Envir.norm_term env |> try_dest_term; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
450 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
451 |
val item' = Thm.prop_of thm |> try_dest_term; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
452 |
val ts = Option.map (fst o fst) (fst x); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
453 |
(*FIXME: Do we need to move one of these patterns above the other?*) |
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 |
val matches = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
456 |
(if is_unify x |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
457 |
then Unify.smash_unifiers (Context.Proof ctxt) [(pat', item') ] env |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
458 |
else Unify.matchers (Context.Proof ctxt) [(pat', item')]) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
459 |
|> Seq.map_filter (fn env' => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
460 |
match_filter_env ctxt fixes (ts, params) thm (Envir.merge (env, env'))) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
461 |
|> is_cut x ? (fn t => Seq.make (fn () => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
462 |
Option.map (fn (x, _) => (x, raise_match)) (Seq.pull t))); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
463 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
464 |
matches |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
465 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
466 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
467 |
val all_matches = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
468 |
map (fn pat => (pat, get (snd pat))) prop_pats |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
469 |
|> 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
|
470 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
471 |
fun proc_multi_match (pat, thmenvs) (pats, env) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
472 |
if is_multi pat then |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
473 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
474 |
val empty = ([], Envir.empty ~1); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
475 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
476 |
val thmenvs' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
477 |
Seq.EVERY (map (fn e => fn (thms, env) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
478 |
Seq.append (Seq.map (fn (thm, env') => (thm :: thms, env')) (e env)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
479 |
(Seq.single (thms, env))) thmenvs) empty; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
480 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
481 |
Seq.map_filter (fn (fact, env') => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
482 |
if not (null fact) then SOME ((pat, fact) :: pats, env') else NONE) thmenvs' |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
483 |
end |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
484 |
else |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
485 |
fold (fn e => Seq.append (Seq.map (fn (thm, env') => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
486 |
((pat, [thm]) :: pats, env')) (e env))) thmenvs Seq.empty; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
487 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
488 |
val all_matches = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
489 |
Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
490 |
|> Seq.filter (fn (_, e) => forall (is_some o Envir.lookup e o Term.dest_Var) fixes); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
491 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
492 |
fun map_handle seq = Seq.make (fn () => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
493 |
(case (Seq.pull seq handle MATCH_CUT => NONE) of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
494 |
SOME (x, seq') => SOME (x, map_handle seq') |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
495 |
| NONE => NONE)); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
496 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
497 |
map_handle all_matches |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
498 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
499 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
500 |
fun real_match using ctxt fixes m text pats goal = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
501 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
502 |
fun make_fact_matches ctxt get = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
503 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
504 |
val (pats', ctxt') = fold_map prep_fact_pat pats ctxt; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
505 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
506 |
match_facts ctxt' fixes pats' get |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
507 |
|> 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
|
508 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
509 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
510 |
(*TODO: Slightly hacky re-use of fact match implementation in plain term matching *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
511 |
fun make_term_matches ctxt get = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
512 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
513 |
val pats' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
514 |
map |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
515 |
(fn ((SOME _, _), _) => error "Cannot name term match" |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
516 |
| ((_, x), t) => (((NONE, x), []), Logic.mk_term t)) pats; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
517 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
518 |
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
|
519 |
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
|
520 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
521 |
match_facts ctxt fixes pats' get' |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
522 |
|> 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
|
523 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
524 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
525 |
(case m of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
526 |
Match_Fact net => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
527 |
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
|
528 |
(make_fact_matches ctxt (Item_Net.retrieve net)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
529 |
| Match_Term net => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
530 |
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
|
531 |
(make_term_matches ctxt (Item_Net.retrieve net)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
532 |
| match_kind => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
533 |
if Thm.no_prems goal then Seq.empty |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
534 |
else |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
535 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
536 |
fun focus_cases f g = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
537 |
(case match_kind of |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
538 |
Match_Prems => f |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
539 |
| Match_Concl => g |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
540 |
| _ => raise Fail "Match kind fell through"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
541 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
542 |
val ({context = focus_ctxt, params, asms, concl, ...}, focused_goal) = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
543 |
focus_cases (Subgoal.focus_prems) (focus_concl) ctxt 1 goal |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
544 |
|>> augment_focus; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
545 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
546 |
val texts = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
547 |
focus_cases |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
548 |
(fn _ => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
549 |
make_fact_matches focus_ctxt |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
550 |
(Item_Net.retrieve (focus_prems focus_ctxt |> snd) #> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
551 |
order_list)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
552 |
(fn _ => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
553 |
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
|
554 |
(); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
555 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
556 |
(*TODO: How to handle cases? *) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
557 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
558 |
fun do_retrofit inner_ctxt goal' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
559 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
560 |
val cleared_prems = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
561 |
subtract (eq_fst (op =)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
562 |
(focus_prems inner_ctxt |> snd |> Item_Net.content) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
563 |
(focus_prems focus_ctxt |> snd |> Item_Net.content) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
564 |
|> map (fn (_, thm) => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
565 |
Thm.hyps_of thm |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
566 |
|> (fn [hyp] => hyp | _ => error "Prem should have only one hyp")); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
567 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
568 |
val n_subgoals = Thm.nprems_of goal'; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
569 |
fun prep_filter t = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
570 |
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
|
571 |
fun filter_test prems t = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
572 |
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
|
573 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
574 |
Subgoal.retrofit inner_ctxt ctxt params asms 1 goal' goal |> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
575 |
(if n_subgoals = 0 orelse null cleared_prems then I |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
576 |
else |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
577 |
Seq.map (Goal.restrict 1 n_subgoals) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
578 |
#> Seq.maps (ALLGOALS (fn i => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
579 |
DETERM (filter_prems_tac' ctxt prep_filter filter_test cleared_prems i))) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
580 |
#> Seq.map (Goal.unrestrict 1)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
581 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
582 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
583 |
fun apply_text (text, ctxt') = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
584 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
585 |
val goal' = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
586 |
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
|
587 |
|> Seq.maps (DETERM (do_retrofit ctxt')) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
588 |
|> Seq.map (fn goal => ([]: cases, goal)) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
589 |
in goal' end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
590 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
591 |
Seq.map apply_text texts |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
592 |
end) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
593 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
594 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
595 |
val match_parser = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
596 |
parse_match_kind :-- (fn kind => Scan.lift @{keyword "in"} |-- parse_match_bodies kind) >> |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
597 |
(fn (matches, bodies) => fn ctxt => fn using => fn goal => |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
598 |
if Method_Closure.is_dummy goal then Seq.empty |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
599 |
else |
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 exec (pats, fixes, text) goal = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
602 |
let |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
603 |
val ctxt' = fold Variable.declare_term fixes ctxt |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
604 |
|> fold (fn (_, t) => Variable.declare_term t) pats; (*Is this a good idea? We really only care about the maxidx*) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
605 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
606 |
real_match using ctxt' fixes matches text pats goal |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
607 |
end; |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
608 |
in |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
609 |
Seq.FIRST (map exec bodies) goal |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
610 |
|> Seq.flat |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
611 |
end); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
612 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
613 |
val _ = |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
614 |
Theory.setup |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
615 |
(Method.setup @{binding match} |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
616 |
(match_parser >> (fn m => fn ctxt => METHOD_CASES (m ctxt))) |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
617 |
"structural analysis/matching on goals"); |
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
618 |
|
54bea620e54f
added Eisbach, using version 3752768caa17 of its Bitbucket repository;
wenzelm
parents:
diff
changeset
|
619 |
end; |