author | wenzelm |
Wed, 08 Jul 2015 21:33:00 +0200 | |
changeset 60696 | 8304fb4fb823 |
parent 59582 | 0fbed69ff081 |
child 60752 | b48830b670a1 |
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 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
15 |
-> Thm.thm |
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 Core_Data; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
23 |
open Mode_Inference; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
24 |
|
55437 | 25 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
26 |
(* debug stuff *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
27 |
|
56491 | 28 |
fun trace_tac ctxt options s = |
29 |
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
|
30 |
|
56491 | 31 |
fun assert_tac ctxt pos pred = |
32 |
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
|
33 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
34 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
35 |
(** special setup for simpset **) |
55437 | 36 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
37 |
val HOL_basic_ss' = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
38 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
39 |
addsimps @{thms simp_thms Pair_eq} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
40 |
setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac)) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
41 |
setSolver (mk_solver "True_solver" (fn _ => rtac @{thm TrueI}))) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
42 |
|
55437 | 43 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
44 |
(* auxillary functions *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
45 |
|
55399 | 46 |
(* 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
|
47 |
(* which then consequently would be splitted *) |
55399 | 48 |
fun is_constructor ctxt t = |
49 |
(case fastype_of t of |
|
50 |
Type (s, _) => s <> @{type_name fun} andalso can (Ctr_Sugar.dest_ctr ctxt s) t |
|
55440 | 51 |
| _ => false) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
52 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
53 |
(* 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
|
54 |
- different form of introrule for parameters ? *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
55 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
56 |
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
|
57 |
let |
55399 | 58 |
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
|
59 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
60 |
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
|
61 |
val ho_args = ho_args_of mode args |
55437 | 62 |
val f_tac = |
63 |
(case f of |
|
64 |
Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps |
|
65 |
[@{thm eval_pred}, predfun_definition_of ctxt name mode, |
|
66 |
@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, |
|
67 |
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 |
|
68 |
| Free _ => |
|
56490 | 69 |
Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} => |
55437 | 70 |
let |
71 |
val prems' = maps dest_conjunct_prem (take nargs prems) |
|
72 |
in |
|
73 |
rewrite_goal_tac ctxt' (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
|
74 |
end) ctxt 1 |
|
75 |
| 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
|
76 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
77 |
REPEAT_DETERM (rtac @{thm ext} 1) |
56491 | 78 |
THEN trace_tac ctxt options "prove_param" |
56490 | 79 |
THEN f_tac |
56491 | 80 |
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
|
81 |
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
|
82 |
THEN (EVERY (map2 (prove_param options ctxt nargs) ho_args param_derivations)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
83 |
THEN REPEAT_DETERM (rtac @{thm refl} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
84 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
85 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
86 |
fun prove_expr options ctxt nargs (premposition : int) (t, deriv) = |
55437 | 87 |
(case strip_comb t of |
50056 | 88 |
(Const (name, _), args) => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
89 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
90 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
91 |
val introrule = predfun_intro_of ctxt name mode |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
92 |
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
|
93 |
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
|
94 |
in |
56491 | 95 |
trace_tac ctxt options "before intro rule:" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
96 |
THEN rtac introrule 1 |
56491 | 97 |
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
|
98 |
(* 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
|
99 |
THEN rotate_tac premposition 1 |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58956
diff
changeset
|
100 |
THEN assume_tac ctxt 1 |
56491 | 101 |
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
|
102 |
(* work with parameter arguments *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
103 |
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
|
104 |
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
|
105 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
106 |
| (Free _, _) => |
56491 | 107 |
trace_tac ctxt options "proving parameter call.." |
56490 | 108 |
THEN Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, concl, ...} => |
55437 | 109 |
let |
110 |
val param_prem = nth prems premposition |
|
59582 | 111 |
val (param, _) = strip_comb (HOLogic.dest_Trueprop (Thm.prop_of param_prem)) |
55437 | 112 |
val prems' = maps dest_conjunct_prem (take nargs prems) |
113 |
fun param_rewrite prem = |
|
59582 | 114 |
param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of prem))) |
55437 | 115 |
val SOME rew_eq = find_first param_rewrite prems' |
116 |
val param_prem' = rewrite_rule ctxt' |
|
117 |
(map (fn th => th RS @{thm eq_reflection}) |
|
118 |
[rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}]) |
|
119 |
param_prem |
|
120 |
in |
|
121 |
rtac param_prem' 1 |
|
122 |
end) ctxt 1 |
|
56491 | 123 |
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
|
124 |
|
59582 | 125 |
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
|
126 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
127 |
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
|
128 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
129 |
val eval_if_P = |
56490 | 130 |
@{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
|
131 |
fun get_case_rewrite t = |
55399 | 132 |
if is_constructor ctxt t then |
45701 | 133 |
let |
55399 | 134 |
val SOME {case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type (fastype_of t))) |
45701 | 135 |
in |
55399 | 136 |
fold (union Thm.eq_thm) (case_thms :: map get_case_rewrite (snd (strip_comb t))) [] |
45701 | 137 |
end |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
138 |
else [] |
55642
63beb38e9258
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
blanchet
parents:
55440
diff
changeset
|
139 |
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
|
140 |
(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
|
141 |
(* 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
|
142 |
in |
55437 | 143 |
(* make this simpset better! *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
144 |
asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1 |
56491 | 145 |
THEN trace_tac ctxt options "after prove_match:" |
56490 | 146 |
THEN (DETERM (TRY |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
147 |
(rtac eval_if_P 1 |
60696 | 148 |
THEN (SUBPROOF (fn {prems, context = ctxt', ...} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
149 |
(REPEAT_DETERM (rtac @{thm conjI} 1 |
60696 | 150 |
THEN (SOLVED (asm_simp_tac (put_simpset HOL_basic_ss' ctxt') 1)))) |
151 |
THEN trace_tac ctxt' options "if condition to be solved:" |
|
152 |
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
|
153 |
THEN TRY ( |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
154 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
155 |
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
|
156 |
in |
60696 | 157 |
rewrite_goal_tac ctxt' |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
158 |
(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
|
159 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
160 |
THEN REPEAT_DETERM (rtac @{thm refl} 1)) |
60696 | 161 |
THEN trace_tac ctxt' options "after if simp; in SUBPROOF") ctxt 1)))) |
56491 | 162 |
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
|
163 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
164 |
|
55437 | 165 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
166 |
(* 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
|
167 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
168 |
fun prove_sidecond ctxt t = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
169 |
let |
55437 | 170 |
fun preds_of t nameTs = |
171 |
(case strip_comb t of |
|
172 |
(Const (name, T), args) => |
|
173 |
if is_registered ctxt name then (name, T) :: nameTs |
|
174 |
else fold preds_of args nameTs |
|
175 |
| _ => nameTs) |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
176 |
val preds = preds_of t [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
177 |
val defs = map |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
178 |
(fn (pred, T) => predfun_definition_of ctxt pred |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
179 |
(all_input_of T)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
180 |
preds |
56490 | 181 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
182 |
simp_tac (put_simpset HOL_basic_ss ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
183 |
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
|
184 |
(* need better control here! *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
185 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
186 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
187 |
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
|
188 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
189 |
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
|
190 |
fun prove_prems out_ts [] = |
55437 | 191 |
(prove_match options ctxt nargs out_ts) |
56491 | 192 |
THEN trace_tac ctxt options "before simplifying assumptions" |
55437 | 193 |
THEN asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt) 1 |
56491 | 194 |
THEN trace_tac ctxt options "before single intro rule" |
55437 | 195 |
THEN Subgoal.FOCUS_PREMS |
56490 | 196 |
(fn {context = ctxt', prems, ...} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
197 |
let |
55437 | 198 |
val prems' = maps dest_conjunct_prem (take nargs prems) |
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 |
|
202 |
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) |
|
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 = |
|
208 |
rtac @{thm bindI} 1 |
|
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 => |
|
230 |
the (predfun_neg_intro_of ctxt name mode)) name |
|
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 |
236 |
[@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, |
|
237 |
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 |
|
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, ...} => |
241 |
rtac (the neg_intro_rule) 1 |
|
242 |
THEN rtac (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 |
247 |
rtac @{thm not_predI'} 1 |
|
248 |
(* test: *) |
|
249 |
THEN dtac @{thm sym} 1 |
|
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 => |
|
257 |
rtac @{thm 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..." |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
268 |
THEN rtac @{thm bindI} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
269 |
THEN rtac @{thm singleI} 1 |
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 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
273 |
fun select_sup 1 1 = [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
274 |
| select_sup _ 1 = [rtac @{thm supI1}] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
275 |
| select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1)); |
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) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
281 |
val pred_case_rule = the_elim_of ctxt pred |
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" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
285 |
THEN etac (predfun_elim_of ctxt pred mode) 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
286 |
THEN etac 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 |
56490 | 289 |
(fn i => EVERY' (select_sup (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) ^ |
55420 | 310 |
" splitting with rules \n" ^ Display.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) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
316 |
(etac @{thm botE} 1 ORELSE etac @{thm 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) |
58956
a816aa3ff391
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
wenzelm
parents:
56491
diff
changeset
|
323 |
THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
324 |
THEN (etac @{thm botE} 2)))) |
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 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
341 |
(@{thm eval_pred}::(predfun_definition_of ctxt name mode) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
342 |
:: @{thm "Product_Type.split_conv"}::[])) 1 |
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 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
360 |
etac @{thm 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" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
363 |
THEN etac (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 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
368 |
| _ => etac @{thm bindE} 1) |
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) => |
|
375 |
if is_registered ctxt name then (name, T) :: nameTs |
|
376 |
else fold preds_of args nameTs |
|
377 |
| _ => nameTs) |
|
378 |
val preds = preds_of t [] |
|
379 |
val defs = map |
|
56490 | 380 |
(fn (pred, T) => 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 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
392 |
val pred_intro_rule = nth (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 |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
396 |
addsimps [@{thm split_eta}, @{thm split_beta}, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
397 |
@{thm fst_conv}, @{thm snd_conv}, @{thm pair_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:" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
402 |
THEN (etac @{thm singleE} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
403 |
THEN (REPEAT_DETERM (etac @{thm 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 ( |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
406 |
(REPEAT_DETERM (etac @{thm 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:" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
410 |
THEN (rtac pred_intro_rule |
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" |
55437 | 441 |
THEN etac @{thm bindE} 1 |
442 |
THEN (if is_some name then |
|
443 |
full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps |
|
444 |
[predfun_definition_of ctxt (the name) mode]) 1 |
|
445 |
THEN etac @{thm not_predE} 1 |
|
446 |
THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1 |
|
447 |
THEN (EVERY (map2 (prove_param2 options ctxt) ho_args param_derivations)) |
|
448 |
else |
|
449 |
etac @{thm not_predE'} 1) |
|
450 |
THEN rec_tac |
|
56490 | 451 |
end |
55437 | 452 |
| Sidecond t => |
453 |
etac @{thm bindE} 1 |
|
454 |
THEN etac @{thm if_predE} 1 |
|
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" |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
466 |
THEN etac @{thm bindE} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
467 |
THEN (etac @{thm singleE'} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
468 |
THEN (TRY (etac @{thm 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 = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
476 |
(if i < length moded_clauses then etac @{thm supE} 1 else all_tac) |
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 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
479 |
(DETERM (TRY (rtac @{thm 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}))) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
481 |
THEN (rtac (predfun_intro_of ctxt pred mode) 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
482 |
THEN (REPEAT_DETERM (rtac @{thm 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 ( |
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
52732
diff
changeset
|
484 |
if null moded_clauses then etac @{thm 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 _ => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
499 |
rtac @{thm 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 |
|
55437 | 508 |
end |