author | nipkow |
Tue, 23 Feb 2016 16:41:14 +0100 | |
changeset 62391 | 1658fc9b2618 |
parent 62121 | c8a93680b80d |
child 64542 | c7d76708379f |
permissions | -rw-r--r-- |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_proof.ML |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
3 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
4 |
Proof procedure for the compiler from predicates specified by intro/elim rules to equations. |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
5 |
*) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
6 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
7 |
signature PREDICATE_COMPILE_PROOF = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
8 |
sig |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
9 |
type indprem = Predicate_Compile_Aux.indprem; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
10 |
type mode = Predicate_Compile_Aux.mode |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
11 |
val prove_pred : Predicate_Compile_Aux.options -> theory |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
12 |
-> (string * (term list * indprem list) list) list |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
13 |
-> (string * typ) list -> string -> bool * mode |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
14 |
-> (term list * (indprem * Mode_Inference.mode_derivation) list) list * term |
61114 | 15 |
-> thm |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
16 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
17 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
18 |
structure Predicate_Compile_Proof : PREDICATE_COMPILE_PROOF = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
19 |
struct |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
20 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
21 |
open Predicate_Compile_Aux; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
22 |
open Mode_Inference; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
23 |
|
55437 | 24 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
25 |
(* debug stuff *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
26 |
|
56491 | 27 |
fun trace_tac ctxt options s = |
28 |
if show_proof_trace options then print_tac ctxt s else Seq.single; |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
29 |
|
56491 | 30 |
fun assert_tac ctxt pos pred = |
31 |
COND pred all_tac (print_tac ctxt ("Assertion failed" ^ Position.here pos) THEN no_tac); |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
32 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
33 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
34 |
(** special setup for simpset **) |
55437 | 35 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
36 |
val HOL_basic_ss' = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
37 |
simpset_of (put_simpset HOL_basic_ss @{context} |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset
|
38 |
addsimps @{thms simp_thms prod.inject} |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
39 |
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac)) |
60752 | 40 |
setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI}))) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
41 |
|
55437 | 42 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
43 |
(* auxillary functions *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
44 |
|
55399 | 45 |
(* returns true if t is an application of a datatype constructor *) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
46 |
(* which then consequently would be splitted *) |
55399 | 47 |
fun is_constructor ctxt t = |
48 |
(case fastype_of t of |
|
49 |
Type (s, _) => s <> @{type_name fun} andalso can (Ctr_Sugar.dest_ctr ctxt s) t |
|
55440 | 50 |
| _ => false) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
51 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
52 |
(* MAJOR FIXME: prove_params should be simple |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
53 |
- different form of introrule for parameters ? *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
54 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
55 |
fun prove_param options ctxt nargs t deriv = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
56 |
let |
55399 | 57 |
val (f, args) = strip_comb (Envir.eta_contract t) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
58 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
59 |
val param_derivations = param_derivations_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
60 |
val ho_args = ho_args_of mode args |
55437 | 61 |
val f_tac = |
62 |
(case f of |
|
63 |
Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps |
|
61114 | 64 |
[@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode, |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset
|
65 |
@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv}, |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset
|
66 |
@{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1 |
55437 | 67 |
| Free _ => |
56490 | 68 |
Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} => |
55437 | 69 |
let |
70 |
val prems' = maps dest_conjunct_prem (take nargs prems) |
|
71 |
in |
|
72 |
rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
|
73 |
end) ctxt 1 |
|
74 |
| Abs _ => raise Fail "prove_param: No valid parameter term") |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
75 |
in |
60752 | 76 |
REPEAT_DETERM (resolve_tac ctxt @{thms ext} 1) |
56491 | 77 |
THEN trace_tac ctxt options "prove_param" |
56490 | 78 |
THEN f_tac |
56491 | 79 |
THEN trace_tac ctxt options "after prove_param" |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
80 |
THEN (REPEAT_DETERM (assume_tac ctxt 1)) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
81 |
THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) |
60752 | 82 |
THEN REPEAT_DETERM (resolve_tac ctxt @{thms refl} 1) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
83 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
84 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
85 |
fun prove_expr options ctxt nargs (premposition : int) (t, deriv) = |
55437 | 86 |
(case strip_comb t of |
50056 | 87 |
(Const (name, _), args) => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
88 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
89 |
val mode = head_mode_of deriv |
61114 | 90 |
val introrule = Core_Data.predfun_intro_of ctxt name mode |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
91 |
val param_derivations = param_derivations_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
92 |
val ho_args = ho_args_of mode args |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
93 |
in |
56491 | 94 |
trace_tac ctxt options "before intro rule:" |
60752 | 95 |
THEN resolve_tac ctxt [introrule] 1 |
56491 | 96 |
THEN trace_tac ctxt options "after intro rule" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
97 |
(* for the right assumption in first position *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
98 |
THEN rotate_tac premposition 1 |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
99 |
THEN assume_tac ctxt 1 |
56491 | 100 |
THEN trace_tac ctxt options "parameter goal" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
101 |
(* work with parameter arguments *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
102 |
THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
103 |
THEN (REPEAT_DETERM (assume_tac ctxt 1)) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
104 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
105 |
| (Free _, _) => |
56491 | 106 |
trace_tac ctxt options "proving parameter call.." |
56490 | 107 |
THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} => |
55437 | 108 |
let |
109 |
val param_prem = nth prems premposition |
|
59582 | 110 |
val (param, _) = strip_comb (HOLogic.dest_Trueprop (Thm.prop_of param_prem)) |
55437 | 111 |
val prems' = maps dest_conjunct_prem (take nargs prems) |
112 |
fun param_rewrite prem = |
|
59582 | 113 |
param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of prem))) |
55437 | 114 |
val SOME rew_eq = find_first param_rewrite prems' |
115 |
val param_prem' = rewrite_rule ctxt' |
|
116 |
(map (fn th => th RS @{thm eq_reflection}) |
|
117 |
[rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}]) |
|
118 |
param_prem |
|
119 |
in |
|
60752 | 120 |
resolve_tac ctxt' [param_prem'] 1 |
55437 | 121 |
end) ctxt 1 |
56491 | 122 |
THEN trace_tac ctxt options "after prove parameter call") |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
123 |
|
59582 | 124 |
fun SOLVED tac st = FILTER (fn st' => Thm.nprems_of st' = Thm.nprems_of st - 1) tac st |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
125 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
126 |
fun prove_match options ctxt nargs out_ts = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
127 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
128 |
val eval_if_P = |
56490 | 129 |
@{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
130 |
fun get_case_rewrite t = |
55399 | 131 |
if is_constructor ctxt t then |
45701 | 132 |
let |
55399 | 133 |
val SOME {case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t))) |
45701 | 134 |
in |
55399 | 135 |
fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) [] |
45701 | 136 |
end |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
137 |
else [] |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55440
diff
changeset
|
138 |
val simprules = insert Thm.eq_thm @{thm "unit.case"} (insert Thm.eq_thm @{thm "prod.case"} |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
139 |
(fold (union Thm.eq_thm) (map get_case_rewrite out_ts) [])) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
140 |
(* replace TRY by determining if it necessary - are there equations when calling compile match? *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
141 |
in |
55437 | 142 |
(* make this simpset better! *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
143 |
asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1 |
56491 | 144 |
THEN trace_tac ctxt options "after prove_match:" |
56490 | 145 |
THEN (DETERM (TRY |
60752 | 146 |
(resolve_tac ctxt [eval_if_P] 1 |
60696 | 147 |
THEN (SUBPROOF (fn {prems, context = ctxt', ...} => |
60752 | 148 |
(REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 |
60696 | 149 |
THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1)))) |
150 |
THEN trace_tac ctxt' options "if condition to be solved:" |
|
151 |
THEN asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
152 |
THEN TRY ( |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
153 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
154 |
val prems' = maps dest_conjunct_prem (take nargs prems) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
155 |
in |
60696 | 156 |
rewrite_goal_tac ctxt' |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
157 |
(map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
158 |
end |
60752 | 159 |
THEN REPEAT_DETERM (resolve_tac ctxt' @{thms refl} 1)) |
60696 | 160 |
THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1)))) |
56491 | 161 |
THEN trace_tac ctxt options "after if simplification" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
162 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
163 |
|
55437 | 164 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
165 |
(* corresponds to compile_fun -- maybe call that also compile_sidecond? *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
166 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
167 |
fun prove_sidecond ctxt t = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
168 |
let |
55437 | 169 |
fun preds_of t nameTs = |
170 |
(case strip_comb t of |
|
171 |
(Const (name, T), args) => |
|
61114 | 172 |
if Core_Data.is_registered ctxt name then (name, T) :: nameTs |
173 |
else fold preds_of args nameTs |
|
55437 | 174 |
| _ => nameTs) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
175 |
val preds = preds_of t [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
176 |
val defs = map |
61114 | 177 |
(fn (pred, T) => Core_Data.predfun_definition_of ctxt pred |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
178 |
(all_input_of T)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
179 |
preds |
56490 | 180 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
181 |
simp_tac (put_simpset HOL_basic_ss ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
182 |
addsimps (@{thms HOL.simp_thms eval_pred} @ defs)) 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
183 |
(* need better control here! *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
184 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
185 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
186 |
fun prove_clause options ctxt nargs mode (_, clauses) (ts, moded_ps) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
187 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
188 |
val (in_ts, clause_out_ts) = split_mode mode ts; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
189 |
fun prove_prems out_ts [] = |
55437 | 190 |
(prove_match options ctxt nargs out_ts) |
56491 | 191 |
THEN trace_tac ctxt options "before simplifying assumptions" |
55437 | 192 |
THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1 |
56491 | 193 |
THEN trace_tac ctxt options "before single intro rule" |
55437 | 194 |
THEN Subgoal.FOCUS_PREMS |
56490 | 195 |
(fn {context = ctxt', prems, ...} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
196 |
let |
55437 | 197 |
val prems' = maps dest_conjunct_prem (take nargs prems) |
62121
c8a93680b80d
filter non-matching prems rather than fail in proof procedure in rare cases; include derived example motivating change and some similar other ones
Lukas Bulwahn <lukas.bulwahn@gmail.com>
parents:
61424
diff
changeset
|
198 |
|> filter is_equationlike |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
199 |
in |
55437 | 200 |
rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
201 |
end) ctxt 1 |
|
60752 | 202 |
THEN (resolve_tac ctxt [if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}] 1) |
55437 | 203 |
| prove_prems out_ts ((p, deriv) :: ps) = |
204 |
let |
|
205 |
val premposition = (find_index (equal p) clauses) + nargs |
|
206 |
val mode = head_mode_of deriv |
|
207 |
val rest_tac = |
|
60752 | 208 |
resolve_tac ctxt @{thms bindI} 1 |
55437 | 209 |
THEN (case p of Prem t => |
210 |
let |
|
211 |
val (_, us) = strip_comb t |
|
212 |
val (_, out_ts''') = split_mode mode us |
|
213 |
val rec_tac = prove_prems out_ts''' ps |
|
214 |
in |
|
56491 | 215 |
trace_tac ctxt options "before clause:" |
55437 | 216 |
(*THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1*) |
56491 | 217 |
THEN trace_tac ctxt options "before prove_expr:" |
55437 | 218 |
THEN prove_expr options ctxt nargs premposition (t, deriv) |
56491 | 219 |
THEN trace_tac ctxt options "after prove_expr:" |
55437 | 220 |
THEN rec_tac |
221 |
end |
|
222 |
| Negprem t => |
|
223 |
let |
|
224 |
val (t, args) = strip_comb t |
|
225 |
val (_, out_ts''') = split_mode mode args |
|
226 |
val rec_tac = prove_prems out_ts''' ps |
|
227 |
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) |
|
228 |
val neg_intro_rule = |
|
229 |
Option.map (fn name => |
|
61114 | 230 |
the (Core_Data.predfun_neg_intro_of ctxt name mode)) name |
55437 | 231 |
val param_derivations = param_derivations_of deriv |
232 |
val params = ho_args_of mode args |
|
233 |
in |
|
56491 | 234 |
trace_tac ctxt options "before prove_neg_expr:" |
55437 | 235 |
THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset
|
236 |
[@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv}, |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset
|
237 |
@{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1 |
55437 | 238 |
THEN (if (is_some name) then |
56491 | 239 |
trace_tac ctxt options "before applying not introduction rule" |
56490 | 240 |
THEN Subgoal.FOCUS_PREMS (fn {prems, ...} => |
60752 | 241 |
resolve_tac ctxt [the neg_intro_rule] 1 |
242 |
THEN resolve_tac ctxt [nth prems premposition] 1) ctxt 1 |
|
56491 | 243 |
THEN trace_tac ctxt options "after applying not introduction rule" |
55437 | 244 |
THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations)) |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
245 |
THEN (REPEAT_DETERM (assume_tac ctxt 1)) |
55437 | 246 |
else |
60752 | 247 |
resolve_tac ctxt @{thms not_predI'} 1 |
55437 | 248 |
(* test: *) |
60752 | 249 |
THEN dresolve_tac ctxt @{thms sym} 1 |
55437 | 250 |
THEN asm_full_simp_tac |
251 |
(put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1) |
|
252 |
THEN simp_tac |
|
253 |
(put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1 |
|
254 |
THEN rec_tac |
|
255 |
end |
|
256 |
| Sidecond t => |
|
60752 | 257 |
resolve_tac ctxt @{thms if_predI} 1 |
56491 | 258 |
THEN trace_tac ctxt options "before sidecond:" |
55437 | 259 |
THEN prove_sidecond ctxt t |
56491 | 260 |
THEN trace_tac ctxt options "after sidecond:" |
55437 | 261 |
THEN prove_prems [] ps) |
262 |
in (prove_match options ctxt nargs out_ts) |
|
263 |
THEN rest_tac |
|
264 |
end |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
265 |
val prems_tac = prove_prems in_ts moded_ps |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
266 |
in |
56491 | 267 |
trace_tac ctxt options "Proving clause..." |
60752 | 268 |
THEN resolve_tac ctxt @{thms bindI} 1 |
269 |
THEN resolve_tac ctxt @{thms singleI} 1 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
270 |
THEN prems_tac |
55437 | 271 |
end |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
272 |
|
60752 | 273 |
fun select_sup _ 1 1 = [] |
274 |
| select_sup ctxt _ 1 = [resolve_tac ctxt @{thms supI1}] |
|
275 |
| select_sup ctxt n i = resolve_tac ctxt @{thms supI2} :: select_sup ctxt (n - 1) (i - 1); |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
276 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
277 |
fun prove_one_direction options ctxt clauses preds pred mode moded_clauses = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
278 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
279 |
val T = the (AList.lookup (op =) preds pred) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
280 |
val nargs = length (binder_types T) |
61114 | 281 |
val pred_case_rule = Core_Data.the_elim_of ctxt pred |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
282 |
in |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
283 |
REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all})) |
56491 | 284 |
THEN trace_tac ctxt options "before applying elim rule" |
61114 | 285 |
THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt pred mode] 1 |
60752 | 286 |
THEN eresolve_tac ctxt [pred_case_rule] 1 |
56491 | 287 |
THEN trace_tac ctxt options "after applying elim rule" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
288 |
THEN (EVERY (map |
60752 | 289 |
(fn i => EVERY' (select_sup ctxt (length moded_clauses) i) i) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
290 |
(1 upto (length moded_clauses)))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
291 |
THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses)) |
56491 | 292 |
THEN trace_tac ctxt options "proved one direction" |
55437 | 293 |
end |
294 |
||
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
295 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
296 |
(** Proof in the other direction **) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
297 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
298 |
fun prove_match2 options ctxt out_ts = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
299 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
300 |
fun split_term_tac (Free _) = all_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
301 |
| split_term_tac t = |
55399 | 302 |
if is_constructor ctxt t then |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
303 |
let |
55399 | 304 |
val SOME {case_thms, split_asm, ...} = |
305 |
Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t))) |
|
306 |
val num_of_constrs = length case_thms |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
307 |
val (_, ts) = strip_comb t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
308 |
in |
56491 | 309 |
trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^ |
61268 | 310 |
" splitting with rules \n" ^ Thm.string_of_thm ctxt split_asm) |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
56491
diff
changeset
|
311 |
THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1 |
56491 | 312 |
THEN (trace_tac ctxt options "after splitting with split_asm rules") |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
313 |
(* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
314 |
THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
315 |
THEN (REPEAT_DETERM_N (num_of_constrs - 1) |
60752 | 316 |
(eresolve_tac ctxt @{thms botE} 1 ORELSE eresolve_tac ctxt @{thms botE} 2))) |
56491 | 317 |
THEN assert_tac ctxt @{here} (fn st => Thm.nprems_of st <= 2) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
318 |
THEN (EVERY (map split_term_tac ts)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
319 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
320 |
else all_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
321 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
322 |
split_term_tac (HOLogic.mk_tuple out_ts) |
62391 | 323 |
THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt @{thms if_split_asm} 1) |
60752 | 324 |
THEN (eresolve_tac ctxt @{thms botE} 2)))) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
325 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
326 |
|
56490 | 327 |
(* VERY LARGE SIMILIRATIY to function prove_param |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
328 |
-- join both functions |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
329 |
*) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
330 |
(* TODO: remove function *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
331 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
332 |
fun prove_param2 options ctxt t deriv = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
333 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
334 |
val (f, args) = strip_comb (Envir.eta_contract t) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
335 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
336 |
val param_derivations = param_derivations_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
337 |
val ho_args = ho_args_of mode args |
55437 | 338 |
val f_tac = |
339 |
(case f of |
|
56490 | 340 |
Const (name, _) => full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps |
61114 | 341 |
[@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode, |
342 |
@{thm Product_Type.split_conv}]) 1 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
343 |
| Free _ => all_tac |
55437 | 344 |
| _ => error "prove_param2: illegal parameter term") |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
345 |
in |
56491 | 346 |
trace_tac ctxt options "before simplification in prove_args:" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
347 |
THEN f_tac |
56491 | 348 |
THEN trace_tac ctxt options "after simplification in prove_args" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
349 |
THEN EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
350 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
351 |
|
56490 | 352 |
fun prove_expr2 options ctxt (t, deriv) = |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
353 |
(case strip_comb t of |
50056 | 354 |
(Const (name, _), args) => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
355 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
356 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
357 |
val param_derivations = param_derivations_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
358 |
val ho_args = ho_args_of mode args |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
359 |
in |
60752 | 360 |
eresolve_tac ctxt @{thms bindE} 1 |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
361 |
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))) |
56491 | 362 |
THEN trace_tac ctxt options "prove_expr2-before" |
61114 | 363 |
THEN eresolve_tac ctxt [Core_Data.predfun_elim_of ctxt name mode] 1 |
56491 | 364 |
THEN trace_tac ctxt options "prove_expr2" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
365 |
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) |
56491 | 366 |
THEN trace_tac ctxt options "finished prove_expr2" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
367 |
end |
60752 | 368 |
| _ => eresolve_tac ctxt @{thms bindE} 1) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
369 |
|
55437 | 370 |
fun prove_sidecond2 options ctxt t = |
371 |
let |
|
372 |
fun preds_of t nameTs = |
|
373 |
(case strip_comb t of |
|
374 |
(Const (name, T), args) => |
|
61114 | 375 |
if Core_Data.is_registered ctxt name then (name, T) :: nameTs |
376 |
else fold preds_of args nameTs |
|
55437 | 377 |
| _ => nameTs) |
378 |
val preds = preds_of t [] |
|
379 |
val defs = map |
|
61114 | 380 |
(fn (pred, T) => Core_Data.predfun_definition_of ctxt pred |
55437 | 381 |
(all_input_of T)) |
382 |
preds |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
383 |
in |
55437 | 384 |
(* only simplify the one assumption *) |
56490 | 385 |
full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 |
55437 | 386 |
(* need better control here! *) |
56491 | 387 |
THEN trace_tac ctxt options "after sidecond2 simplification" |
55437 | 388 |
end |
56490 | 389 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
390 |
fun prove_clause2 options ctxt pred mode (ts, ps) i = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
391 |
let |
61114 | 392 |
val pred_intro_rule = nth (Core_Data.intros_of ctxt pred) (i - 1) |
50056 | 393 |
val (in_ts, _) = split_mode mode ts; |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
394 |
val split_simpset = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
395 |
put_simpset HOL_basic_ss' ctxt |
61424
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset
|
396 |
addsimps [@{thm case_prod_eta}, @{thm case_prod_beta}, |
c3658c18b7bc
prod_case as canonical name for product type eliminator
haftmann
parents:
61268
diff
changeset
|
397 |
@{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}] |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
398 |
fun prove_prems2 out_ts [] = |
56491 | 399 |
trace_tac ctxt options "before prove_match2 - last call:" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
400 |
THEN prove_match2 options ctxt out_ts |
56491 | 401 |
THEN trace_tac ctxt options "after prove_match2 - last call:" |
60752 | 402 |
THEN (eresolve_tac ctxt @{thms singleE} 1) |
403 |
THEN (REPEAT_DETERM (eresolve_tac ctxt @{thms Pair_inject} 1)) |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
404 |
THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
405 |
THEN TRY ( |
60752 | 406 |
(REPEAT_DETERM (eresolve_tac ctxt @{thms Pair_inject} 1)) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
407 |
THEN (asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1) |
56490 | 408 |
|
56491 | 409 |
THEN SOLVED (trace_tac ctxt options "state before applying intro rule:" |
60752 | 410 |
THEN (resolve_tac ctxt [pred_intro_rule] |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
411 |
(* How to handle equality correctly? *) |
56491 | 412 |
THEN_ALL_NEW (K (trace_tac ctxt options "state before assumption matching") |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
413 |
THEN' (assume_tac ctxt ORELSE' |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
414 |
((CHANGED o asm_full_simp_tac split_simpset) THEN' |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
415 |
(TRY o assume_tac ctxt))) THEN' |
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
416 |
(K (trace_tac ctxt options "state after pre-simplification:")) |
56491 | 417 |
THEN' (K (trace_tac ctxt options "state after assumption matching:")))) 1)) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
418 |
| prove_prems2 out_ts ((p, deriv) :: ps) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
419 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
420 |
val mode = head_mode_of deriv |
55437 | 421 |
val rest_tac = |
422 |
(case p of |
|
423 |
Prem t => |
|
424 |
let |
|
425 |
val (_, us) = strip_comb t |
|
426 |
val (_, out_ts''') = split_mode mode us |
|
427 |
val rec_tac = prove_prems2 out_ts''' ps |
|
428 |
in |
|
429 |
(prove_expr2 options ctxt (t, deriv)) THEN rec_tac |
|
430 |
end |
|
431 |
| Negprem t => |
|
432 |
let |
|
433 |
val (_, args) = strip_comb t |
|
434 |
val (_, out_ts''') = split_mode mode args |
|
435 |
val rec_tac = prove_prems2 out_ts''' ps |
|
436 |
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) |
|
437 |
val param_derivations = param_derivations_of deriv |
|
438 |
val ho_args = ho_args_of mode args |
|
439 |
in |
|
56491 | 440 |
trace_tac ctxt options "before neg prem 2" |
60752 | 441 |
THEN eresolve_tac ctxt @{thms bindE} 1 |
55437 | 442 |
THEN (if is_some name then |
443 |
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps |
|
61114 | 444 |
[Core_Data.predfun_definition_of ctxt (the name) mode]) 1 |
60752 | 445 |
THEN eresolve_tac ctxt @{thms not_predE} 1 |
61114 | 446 |
THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms not_False_eq_True}) 1 |
55437 | 447 |
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) |
448 |
else |
|
60752 | 449 |
eresolve_tac ctxt @{thms not_predE'} 1) |
55437 | 450 |
THEN rec_tac |
56490 | 451 |
end |
55437 | 452 |
| Sidecond t => |
60752 | 453 |
eresolve_tac ctxt @{thms bindE} 1 |
454 |
THEN eresolve_tac ctxt @{thms if_predE} 1 |
|
55437 | 455 |
THEN prove_sidecond2 options ctxt t |
456 |
THEN prove_prems2 [] ps) |
|
457 |
in |
|
56491 | 458 |
trace_tac ctxt options "before prove_match2:" |
55437 | 459 |
THEN prove_match2 options ctxt out_ts |
56491 | 460 |
THEN trace_tac ctxt options "after prove_match2:" |
55437 | 461 |
THEN rest_tac |
462 |
end |
|
56490 | 463 |
val prems_tac = prove_prems2 in_ts ps |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
464 |
in |
56491 | 465 |
trace_tac ctxt options "starting prove_clause2" |
60752 | 466 |
THEN eresolve_tac ctxt @{thms bindE} 1 |
467 |
THEN (eresolve_tac ctxt @{thms singleE'} 1) |
|
468 |
THEN (TRY (eresolve_tac ctxt @{thms Pair_inject} 1)) |
|
56491 | 469 |
THEN trace_tac ctxt options "after singleE':" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
470 |
THEN prems_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
471 |
end; |
56490 | 472 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
473 |
fun prove_other_direction options ctxt pred mode moded_clauses = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
474 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
475 |
fun prove_clause clause i = |
60752 | 476 |
(if i < length moded_clauses then eresolve_tac ctxt @{thms supE} 1 else all_tac) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
477 |
THEN (prove_clause2 options ctxt pred mode clause i) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
478 |
in |
60752 | 479 |
(DETERM (TRY (resolve_tac ctxt @{thms unit.induct} 1))) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
480 |
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac ctxt @{thms split_paired_all}))) |
61114 | 481 |
THEN (resolve_tac ctxt [Core_Data.predfun_intro_of ctxt pred mode] 1) |
60752 | 482 |
THEN (REPEAT_DETERM (resolve_tac ctxt @{thms refl} 2)) |
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
483 |
THEN ( |
60752 | 484 |
if null moded_clauses then eresolve_tac ctxt @{thms botE} 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
485 |
else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses)))) |
55437 | 486 |
end |
487 |
||
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
488 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
489 |
(** proof procedure **) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
490 |
|
50056 | 491 |
fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) = |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
492 |
let |
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
50056
diff
changeset
|
493 |
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
55437 | 494 |
val clauses = (case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
495 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
496 |
Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
497 |
(if not (skip_proof options) then |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
498 |
(fn _ => |
60752 | 499 |
resolve_tac ctxt @{thms pred_iffI} 1 |
56491 | 500 |
THEN trace_tac ctxt options "after pred_iffI" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
501 |
THEN prove_one_direction options ctxt clauses preds pred mode moded_clauses |
56491 | 502 |
THEN trace_tac ctxt options "proved one direction" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
503 |
THEN prove_other_direction options ctxt pred mode moded_clauses |
56491 | 504 |
THEN trace_tac ctxt options "proved other direction") |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
505 |
else (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt))) |
55437 | 506 |
end |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
507 |
|
62391 | 508 |
end |