author | wenzelm |
Sat, 27 Jul 2013 16:35:51 +0200 | |
changeset 52732 | b4da1f2ec73f |
parent 52230 | 1105b3b5aa77 |
child 54742 | 7a86358a3c0b |
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 |
|
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 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
27 |
fun print_tac options s = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
28 |
if show_proof_trace options then Tactical.print_tac s else Seq.single; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
29 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
30 |
(** auxiliary **) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
31 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
32 |
datatype assertion = Max_number_of_subgoals of int |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
33 |
fun assert_tac (Max_number_of_subgoals i) st = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
34 |
if (nprems_of st <= i) then Seq.single st |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
35 |
else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
36 |
^ "\n" ^ Pretty.string_of (Pretty.chunks |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
37 |
(Goal_Display.pretty_goals_without_context st))); |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
38 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
39 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
40 |
(** special setup for simpset **) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
41 |
val HOL_basic_ss' = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
42 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
43 |
addsimps @{thms simp_thms Pair_eq} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
44 |
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
|
45 |
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
|
46 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
47 |
(* auxillary functions *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
48 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
49 |
fun is_Type (Type _) = true |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
50 |
| is_Type _ = false |
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 |
(* returns true if t is an application of an datatype constructor *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
53 |
(* which then consequently would be splitted *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
54 |
(* else false *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
55 |
fun is_constructor thy t = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
56 |
if (is_Type (fastype_of t)) then |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
57 |
(case Datatype.get_info thy ((fst o dest_Type o fastype_of) t) of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
58 |
NONE => false |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
59 |
| SOME info => (let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
60 |
val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
61 |
val (c, _) = strip_comb t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
62 |
in (case c of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
63 |
Const (name, _) => member (op =) constr_consts name |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
64 |
| _ => false) end)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
65 |
else false |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
66 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
67 |
(* 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
|
68 |
- different form of introrule for parameters ? *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
69 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
70 |
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
|
71 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
72 |
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
|
73 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
val f_tac = case f of |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
77 |
Const (name, _) => 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
|
78 |
[@{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
|
79 |
@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
80 |
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
81 |
| Free _ => |
50056 | 82 |
Subgoal.FOCUS_PREMS (fn {context, params = params, prems, asms, concl, schematics} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
83 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
84 |
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
|
85 |
in |
52732 | 86 |
rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
87 |
end) ctxt 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
88 |
| Abs _ => raise Fail "prove_param: No valid parameter term" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
89 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
90 |
REPEAT_DETERM (rtac @{thm ext} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
91 |
THEN print_tac options "prove_param" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
92 |
THEN f_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
93 |
THEN print_tac options "after prove_param" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
94 |
THEN (REPEAT_DETERM (atac 1)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
95 |
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
|
96 |
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
|
97 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
98 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
99 |
fun prove_expr options ctxt nargs (premposition : int) (t, deriv) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
100 |
case strip_comb t of |
50056 | 101 |
(Const (name, _), args) => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
102 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
103 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
104 |
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
|
105 |
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
|
106 |
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
|
107 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
108 |
print_tac options "before intro rule:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
109 |
THEN rtac introrule 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
110 |
THEN print_tac options "after intro rule" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
111 |
(* 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
|
112 |
THEN rotate_tac premposition 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
113 |
THEN atac 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
114 |
THEN print_tac options "parameter goal" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
115 |
(* work with parameter arguments *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
116 |
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
|
117 |
THEN (REPEAT_DETERM (atac 1)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
118 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
119 |
| (Free _, _) => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
120 |
print_tac options "proving parameter call.." |
50056 | 121 |
THEN Subgoal.FOCUS_PREMS (fn {context, params, prems, asms, concl, schematics} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
122 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
123 |
val param_prem = nth prems premposition |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
124 |
val (param, _) = strip_comb (HOLogic.dest_Trueprop (prop_of param_prem)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
125 |
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
|
126 |
fun param_rewrite prem = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
127 |
param = snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of prem))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
128 |
val SOME rew_eq = find_first param_rewrite prems' |
52230 | 129 |
val param_prem' = rewrite_rule |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
130 |
(map (fn th => th RS @{thm eq_reflection}) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
131 |
[rew_eq RS @{thm sym}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}]) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
132 |
param_prem |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
133 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
134 |
rtac param_prem' 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
135 |
end) ctxt 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
136 |
THEN print_tac options "after prove parameter call" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
137 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
138 |
fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
139 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
140 |
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
|
141 |
let |
42361 | 142 |
val thy = Proof_Context.theory_of ctxt |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
143 |
val eval_if_P = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
144 |
@{lemma "P ==> Predicate.eval x z ==> Predicate.eval (if P then x else y) z" by simp} |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
145 |
fun get_case_rewrite t = |
45701 | 146 |
if (is_constructor thy t) then |
147 |
let |
|
148 |
val {case_rewrites, ...} = Datatype.the_info thy (fst (dest_Type (fastype_of t))) |
|
149 |
in |
|
150 |
fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) [] |
|
151 |
end |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
152 |
else [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
153 |
val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"} |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
154 |
(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
|
155 |
(* 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
|
156 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
157 |
(* make this simpset better! *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
158 |
asm_full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps simprules) 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
159 |
THEN print_tac options "after prove_match:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
160 |
THEN (DETERM (TRY |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
161 |
(rtac eval_if_P 1 |
50056 | 162 |
THEN (SUBPROOF (fn {context, params, prems, asms, concl, schematics} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
163 |
(REPEAT_DETERM (rtac @{thm conjI} 1 |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
164 |
THEN (SOLVED (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
|
165 |
THEN print_tac options "if condition to be solved:" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
166 |
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
|
167 |
THEN TRY ( |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
168 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
169 |
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
|
170 |
in |
52732 | 171 |
rewrite_goal_tac |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
172 |
(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
|
173 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
174 |
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
|
175 |
THEN print_tac options "after if simp; in SUBPROOF") ctxt 1)))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
176 |
THEN print_tac options "after if simplification" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
177 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
178 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
179 |
(* 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
|
180 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
181 |
fun prove_sidecond ctxt t = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
182 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
183 |
fun preds_of t nameTs = case strip_comb t of |
50056 | 184 |
(Const (name, T), args) => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
185 |
if is_registered ctxt name then (name, T) :: nameTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
186 |
else fold preds_of args nameTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
187 |
| _ => nameTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
188 |
val preds = preds_of t [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
189 |
val defs = map |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
190 |
(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
|
191 |
(all_input_of T)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
192 |
preds |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
193 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
194 |
simp_tac (put_simpset HOL_basic_ss ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
195 |
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
|
196 |
(* need better control here! *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
197 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
198 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
199 |
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
|
200 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
201 |
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
|
202 |
fun prove_prems out_ts [] = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
203 |
(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
|
204 |
THEN print_tac options "before simplifying assumptions" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
205 |
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
|
206 |
THEN print_tac options "before single intro rule" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
207 |
THEN Subgoal.FOCUS_PREMS |
50056 | 208 |
(fn {context, params, prems, asms, concl, schematics} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
209 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
210 |
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
|
211 |
in |
52732 | 212 |
rewrite_goal_tac (map (fn th => th RS @{thm sym} RS @{thm eq_reflection}) prems') 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
213 |
end) ctxt 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
214 |
THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
215 |
| prove_prems out_ts ((p, deriv) :: ps) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
216 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
217 |
val premposition = (find_index (equal p) clauses) + nargs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
218 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
219 |
val rest_tac = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
220 |
rtac @{thm bindI} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
221 |
THEN (case p of Prem t => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
222 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
223 |
val (_, us) = strip_comb t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
224 |
val (_, out_ts''') = split_mode mode us |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
225 |
val rec_tac = prove_prems out_ts''' ps |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
226 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
227 |
print_tac options "before clause:" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
228 |
(*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
|
229 |
THEN print_tac options "before prove_expr:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
230 |
THEN prove_expr options ctxt nargs premposition (t, deriv) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
231 |
THEN print_tac options "after prove_expr:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
232 |
THEN rec_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
233 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
234 |
| Negprem t => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
235 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
236 |
val (t, args) = strip_comb t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
237 |
val (_, out_ts''') = split_mode mode args |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
238 |
val rec_tac = prove_prems out_ts''' ps |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
239 |
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
240 |
val neg_intro_rule = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
241 |
Option.map (fn name => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
242 |
the (predfun_neg_intro_of ctxt name mode)) name |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
243 |
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
|
244 |
val params = ho_args_of mode args |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
245 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
246 |
print_tac options "before prove_neg_expr:" |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
247 |
THEN 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
|
248 |
[@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
249 |
@{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
250 |
THEN (if (is_some name) then |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
251 |
print_tac options "before applying not introduction rule" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
252 |
THEN Subgoal.FOCUS_PREMS |
50056 | 253 |
(fn {context, params = params, prems, asms, concl, schematics} => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
254 |
rtac (the neg_intro_rule) 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
255 |
THEN rtac (nth prems premposition) 1) ctxt 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
256 |
THEN print_tac options "after applying not introduction rule" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
257 |
THEN (EVERY (map2 (prove_param options ctxt nargs) params param_derivations)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
258 |
THEN (REPEAT_DETERM (atac 1)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
259 |
else |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
260 |
rtac @{thm not_predI'} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
261 |
(* test: *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
262 |
THEN dtac @{thm sym} 1 |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
263 |
THEN asm_full_simp_tac |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
264 |
(put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
265 |
THEN simp_tac |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
266 |
(put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
267 |
THEN rec_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
268 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
269 |
| Sidecond t => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
270 |
rtac @{thm if_predI} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
271 |
THEN print_tac options "before sidecond:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
272 |
THEN prove_sidecond ctxt t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
273 |
THEN print_tac options "after sidecond:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
274 |
THEN prove_prems [] ps) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
275 |
in (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
|
276 |
THEN rest_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
277 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
278 |
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
|
279 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
280 |
print_tac options "Proving clause..." |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
281 |
THEN rtac @{thm bindI} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
282 |
THEN rtac @{thm singleI} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
283 |
THEN prems_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
284 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
285 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
286 |
fun select_sup 1 1 = [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
287 |
| select_sup _ 1 = [rtac @{thm supI1}] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
288 |
| 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
|
289 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
290 |
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
|
291 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
292 |
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
|
293 |
val nargs = length (binder_types T) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
294 |
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
|
295 |
in |
46460 | 296 |
REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all})) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
297 |
THEN print_tac options "before applying elim rule" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
298 |
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
|
299 |
THEN etac pred_case_rule 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
300 |
THEN print_tac options "after applying elim rule" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
301 |
THEN (EVERY (map |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
302 |
(fn i => EVERY' (select_sup (length moded_clauses) i) i) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
303 |
(1 upto (length moded_clauses)))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
304 |
THEN (EVERY (map2 (prove_clause options ctxt nargs mode) clauses moded_clauses)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
305 |
THEN print_tac options "proved one direction" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
306 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
307 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
308 |
(** Proof in the other direction **) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
309 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
310 |
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
|
311 |
let |
42361 | 312 |
val thy = Proof_Context.theory_of ctxt |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
313 |
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
|
314 |
| split_term_tac t = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
315 |
if (is_constructor thy t) then |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
316 |
let |
45701 | 317 |
val {case_rewrites, split_asm, ...} = |
318 |
Datatype.the_info thy (fst (dest_Type (fastype_of t))) |
|
319 |
val num_of_constrs = length case_rewrites |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
320 |
val (_, ts) = strip_comb t |
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 |
print_tac options ("Term " ^ (Syntax.string_of_term ctxt t) ^ |
45701 | 323 |
"splitting with rules \n" ^ Display.string_of_thm ctxt split_asm) |
324 |
THEN TRY (Splitter.split_asm_tac [split_asm] 1 |
|
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
325 |
THEN (print_tac options "after splitting with split_asm rules") |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
326 |
(* 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
|
327 |
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
|
328 |
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
|
329 |
(etac @{thm botE} 1 ORELSE etac @{thm botE} 2))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
330 |
THEN (assert_tac (Max_number_of_subgoals 2)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
331 |
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
|
332 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
333 |
else all_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
334 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
335 |
split_term_tac (HOLogic.mk_tuple out_ts) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
336 |
THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
337 |
THEN (etac @{thm botE} 2)))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
338 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
339 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
340 |
(* VERY LARGE SIMILIRATIY to function prove_param |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
341 |
-- join both functions |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
342 |
*) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
343 |
(* TODO: remove function *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
344 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
345 |
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
|
346 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
347 |
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
|
348 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
349 |
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
|
350 |
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
|
351 |
val f_tac = case f of |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
352 |
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
|
353 |
(@{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
|
354 |
:: @{thm "Product_Type.split_conv"}::[])) 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
355 |
| Free _ => all_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
356 |
| _ => error "prove_param2: illegal parameter term" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
357 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
358 |
print_tac options "before simplification in prove_args:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
359 |
THEN f_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
360 |
THEN print_tac options "after simplification in prove_args" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
361 |
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
|
362 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
363 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
364 |
fun prove_expr2 options ctxt (t, deriv) = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
365 |
(case strip_comb t of |
50056 | 366 |
(Const (name, _), args) => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
367 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
368 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
369 |
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
|
370 |
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
|
371 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
372 |
etac @{thm bindE} 1 |
46460 | 373 |
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
374 |
THEN print_tac options "prove_expr2-before" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
375 |
THEN etac (predfun_elim_of ctxt name mode) 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
376 |
THEN print_tac options "prove_expr2" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
377 |
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
|
378 |
THEN print_tac options "finished prove_expr2" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
379 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
380 |
| _ => etac @{thm bindE} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
381 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
382 |
fun prove_sidecond2 options ctxt t = let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
383 |
fun preds_of t nameTs = case strip_comb t of |
50056 | 384 |
(Const (name, T), args) => |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
385 |
if is_registered ctxt name then (name, T) :: nameTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
386 |
else fold preds_of args nameTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
387 |
| _ => nameTs |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
388 |
val preds = preds_of t [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
389 |
val defs = map |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
390 |
(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
|
391 |
(all_input_of T)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
392 |
preds |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
393 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
394 |
(* only simplify the one assumption *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
395 |
full_simp_tac (put_simpset HOL_basic_ss' ctxt addsimps @{thm eval_pred} :: defs) 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
396 |
(* need better control here! *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
397 |
THEN print_tac options "after sidecond2 simplification" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
398 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
399 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
400 |
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
|
401 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
402 |
val pred_intro_rule = nth (intros_of ctxt pred) (i - 1) |
50056 | 403 |
val (in_ts, _) = split_mode mode ts; |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
404 |
val split_simpset = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
405 |
put_simpset HOL_basic_ss' ctxt |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
406 |
addsimps [@{thm split_eta}, @{thm split_beta}, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
407 |
@{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
|
408 |
fun prove_prems2 out_ts [] = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
409 |
print_tac options "before prove_match2 - last call:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
410 |
THEN prove_match2 options ctxt out_ts |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
411 |
THEN print_tac options "after prove_match2 - last call:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
412 |
THEN (etac @{thm singleE} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
413 |
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
|
414 |
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
|
415 |
THEN TRY ( |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
416 |
(REPEAT_DETERM (etac @{thm Pair_inject} 1)) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
417 |
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
|
418 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
419 |
THEN SOLVED (print_tac options "state before applying intro rule:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
420 |
THEN (rtac pred_intro_rule |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
421 |
(* How to handle equality correctly? *) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
422 |
THEN_ALL_NEW (K (print_tac options "state before assumption matching") |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
423 |
THEN' (atac ORELSE' ((CHANGED o asm_full_simp_tac split_simpset) THEN' (TRY o atac))) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
424 |
THEN' (K (print_tac options "state after pre-simplification:")) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
425 |
THEN' (K (print_tac options "state after assumption matching:")))) 1)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
426 |
| 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
|
427 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
428 |
val mode = head_mode_of deriv |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
429 |
val rest_tac = (case p of |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
430 |
Prem t => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
431 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
432 |
val (_, us) = strip_comb t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
433 |
val (_, out_ts''') = split_mode mode us |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
434 |
val rec_tac = prove_prems2 out_ts''' ps |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
435 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
436 |
(prove_expr2 options ctxt (t, deriv)) THEN rec_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
437 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
438 |
| Negprem t => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
439 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
440 |
val (_, args) = strip_comb t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
441 |
val (_, out_ts''') = split_mode mode args |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
442 |
val rec_tac = prove_prems2 out_ts''' ps |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
443 |
val name = (case strip_comb t of (Const (c, _), _) => SOME c | _ => NONE) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
444 |
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
|
445 |
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
|
446 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
447 |
print_tac options "before neg prem 2" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
448 |
THEN etac @{thm bindE} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
449 |
THEN (if is_some name then |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
450 |
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
|
451 |
[predfun_definition_of ctxt (the name) mode]) 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
452 |
THEN etac @{thm not_predE} 1 |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51552
diff
changeset
|
453 |
THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm not_False_eq_True}]) 1 |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
454 |
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
|
455 |
else |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
456 |
etac @{thm not_predE'} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
457 |
THEN rec_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
458 |
end |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
459 |
| Sidecond t => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
460 |
etac @{thm bindE} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
461 |
THEN etac @{thm if_predE} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
462 |
THEN prove_sidecond2 options ctxt t |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
463 |
THEN prove_prems2 [] ps) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
464 |
in print_tac options "before prove_match2:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
465 |
THEN prove_match2 options ctxt out_ts |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
466 |
THEN print_tac options "after prove_match2:" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
467 |
THEN rest_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
468 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
469 |
val prems_tac = prove_prems2 in_ts ps |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
470 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
471 |
print_tac options "starting prove_clause2" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
472 |
THEN etac @{thm bindE} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
473 |
THEN (etac @{thm singleE'} 1) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
474 |
THEN (TRY (etac @{thm Pair_inject} 1)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
475 |
THEN print_tac options "after singleE':" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
476 |
THEN prems_tac |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
477 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
478 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
479 |
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
|
480 |
let |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
481 |
fun prove_clause clause i = |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
482 |
(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
|
483 |
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
|
484 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
485 |
(DETERM (TRY (rtac @{thm unit.induct} 1))) |
46460 | 486 |
THEN (REPEAT_DETERM (CHANGED (rewrite_goals_tac @{thms split_paired_all}))) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
487 |
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
|
488 |
THEN (REPEAT_DETERM (rtac @{thm refl} 2)) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
489 |
THEN (if null moded_clauses then |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
490 |
etac @{thm botE} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
491 |
else EVERY (map2 prove_clause moded_clauses (1 upto (length moded_clauses)))) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
492 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
493 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
494 |
(** proof procedure **) |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
495 |
|
50056 | 496 |
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
|
497 |
let |
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
50056
diff
changeset
|
498 |
val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
499 |
val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => [] |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
500 |
in |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
501 |
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
|
502 |
(if not (skip_proof options) then |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
503 |
(fn _ => |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
504 |
rtac @{thm pred_iffI} 1 |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
505 |
THEN print_tac options "after pred_iffI" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
506 |
THEN 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
|
507 |
THEN print_tac options "proved one direction" |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
508 |
THEN 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
|
509 |
THEN print_tac options "proved other direction") |
51552
c713c9505f68
clarified Skip_Proof.cheat_tac: more standard tactic;
wenzelm
parents:
50056
diff
changeset
|
510 |
else (fn _ => ALLGOALS Skip_Proof.cheat_tac)) |
40052
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
511 |
end; |
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
512 |
|
ea46574ca815
splitting large core file into core_data, mode_inference and predicate_compile_proof
bulwahn
parents:
diff
changeset
|
513 |
end; |