author | wenzelm |
Mon, 09 Mar 2015 10:52:23 +0100 | |
changeset 59655 | 5d1b4ab7d173 |
parent 59653 | 20695aeaba6f |
child 61841 | 4d3527b94f2a |
permissions | -rw-r--r-- |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/function_elims.ML |
53609 | 2 |
Author: Manuel Eberl, TU Muenchen |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
3 |
|
53666 | 4 |
Generate the pelims rules for a function. These are of the shape |
53664 | 5 |
[|f x y z = w; !!\<dots>. [|x = \<dots>; y = \<dots>; z = \<dots>; w = \<dots>|] ==> P; \<dots>|] ==> P |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
6 |
and are derived from the cases rule. There is at least one pelim rule for |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
7 |
each function (cf. mutually recursive functions) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
8 |
There may be more than one pelim rule for a function in case of functions |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
9 |
that return a boolean. For such a function, e.g. P x, not only the normal |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
10 |
elim rule with the premise P x = z is generated, but also two additional |
53664 | 11 |
elim rules with P x resp. \<not>P x as premises. |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
12 |
*) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
13 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
14 |
signature FUNCTION_ELIMS = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
15 |
sig |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
16 |
val dest_funprop : term -> (term * term list) * term |
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
17 |
val mk_partial_elim_rules : Proof.context -> |
53666 | 18 |
Function_Common.function_result -> thm list list |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
19 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
20 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
21 |
structure Function_Elims : FUNCTION_ELIMS = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
22 |
struct |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
23 |
|
53669
6ede465b5be8
more antiquotations -- avoid unchecked string literals;
wenzelm
parents:
53667
diff
changeset
|
24 |
(* Extract a function and its arguments from a proposition that is |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
25 |
either of the form "f x y z = ..." or, in case of function that |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
26 |
returns a boolean, "f x y z" *) |
53669
6ede465b5be8
more antiquotations -- avoid unchecked string literals;
wenzelm
parents:
53667
diff
changeset
|
27 |
fun dest_funprop (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = (strip_comb lhs, rhs) |
59652 | 28 |
| dest_funprop (Const (@{const_name Not}, _) $ t) = (strip_comb t, @{term False}) |
29 |
| dest_funprop t = (strip_comb t, @{term True}); |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
30 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
31 |
local |
53666 | 32 |
|
54738 | 33 |
fun propagate_tac ctxt i = |
54736 | 34 |
let |
35 |
fun inspect eq = |
|
36 |
(case eq of |
|
37 |
Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) => |
|
38 |
if Logic.occs (Free x, t) then raise Match else true |
|
39 |
| Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) => |
|
40 |
if Logic.occs (Free x, t) then raise Match else false |
|
41 |
| _ => raise Match); |
|
42 |
fun mk_eq thm = |
|
59582 | 43 |
(if inspect (Thm.prop_of thm) then [thm RS eq_reflection] |
54736 | 44 |
else [Thm.symmetric (thm RS eq_reflection)]) |
45 |
handle Match => []; |
|
54738 | 46 |
val simpset = |
47 |
empty_simpset ctxt |
|
54736 | 48 |
|> Simplifier.set_mksimps (K mk_eq); |
53666 | 49 |
in |
54738 | 50 |
asm_lr_simp_tac simpset i |
53666 | 51 |
end; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
52 |
|
59652 | 53 |
val eq_boolI = @{lemma "\<And>P. P \<Longrightarrow> P = True" "\<And>P. \<not> P \<Longrightarrow> P = False" by iprover+}; |
54736 | 54 |
val boolE = @{thms HOL.TrueE HOL.FalseE}; |
59652 | 55 |
val boolD = @{lemma "\<And>P. True = P \<Longrightarrow> P" "\<And>P. False = P \<Longrightarrow> \<not> P" by iprover+}; |
54737 | 56 |
val eq_bool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
57 |
|
53666 | 58 |
fun bool_subst_tac ctxt i = |
54737 | 59 |
REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i) |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59454
diff
changeset
|
60 |
THEN REPEAT (dresolve_tac ctxt boolD i) |
59653 | 61 |
THEN REPEAT (eresolve_tac ctxt boolE i); |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
62 |
|
53666 | 63 |
fun mk_bool_elims ctxt elim = |
54736 | 64 |
let |
65 |
fun mk_bool_elim b = |
|
66 |
elim |
|
67 |
|> Thm.forall_elim b |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59454
diff
changeset
|
68 |
|> Tactic.rule_by_tactic ctxt (TRY (resolve_tac ctxt eq_boolI 1)) |
59652 | 69 |
|> Tactic.rule_by_tactic ctxt (ALLGOALS (bool_subst_tac ctxt)); |
53666 | 70 |
in |
54736 | 71 |
map mk_bool_elim [@{cterm True}, @{cterm False}] |
53666 | 72 |
end; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
73 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
74 |
in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
75 |
|
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
76 |
fun mk_partial_elim_rules ctxt result = |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
77 |
let |
59655 | 78 |
val Function_Common.FunctionResult {fs, R, dom, psimps, cases, ...} = result; |
54736 | 79 |
val n_fs = length fs; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
80 |
|
59653 | 81 |
fun variant_free used_term v = |
82 |
Free (singleton (Variable.variant_frees ctxt [used_term]) v); |
|
83 |
||
54736 | 84 |
fun mk_partial_elim_rule (idx, f) = |
85 |
let |
|
59653 | 86 |
fun mk_funeq 0 T (acc_args, acc_lhs) = |
87 |
let val y = variant_free acc_lhs ("y", T) |
|
88 |
in (y, rev acc_args, HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))) end |
|
89 |
| mk_funeq n (Type (@{type_name fun}, [S, T])) (acc_args, acc_lhs) = |
|
90 |
let val x = variant_free acc_lhs ("x", S) |
|
91 |
in mk_funeq (n - 1) T (x :: acc_args, acc_lhs $ x) end |
|
92 |
| mk_funeq _ _ _ = raise TERM ("Not a function", [f]); |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
93 |
|
54736 | 94 |
val f_simps = |
95 |
filter (fn r => |
|
59652 | 96 |
(Thm.prop_of r |
97 |
|> Logic.strip_assums_concl |
|
54736 | 98 |
|> HOLogic.dest_Trueprop |
99 |
|> dest_funprop |> fst |> fst) = f) |
|
100 |
psimps; |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
101 |
|
54736 | 102 |
val arity = |
103 |
hd f_simps |
|
59582 | 104 |
|> Thm.prop_of |
54736 | 105 |
|> Logic.strip_assums_concl |
106 |
|> HOLogic.dest_Trueprop |
|
107 |
|> snd o fst o dest_funprop |
|
108 |
|> length; |
|
59652 | 109 |
|
59653 | 110 |
val (rhs_var, arg_vars, prop) = mk_funeq arity (fastype_of f) ([], f); |
54736 | 111 |
val args = HOLogic.mk_tuple arg_vars; |
112 |
val domT = R |> dest_Free |> snd |> hd o snd o dest_Type; |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
113 |
|
59653 | 114 |
val P = Thm.cterm_of ctxt (variant_free prop ("P", @{typ bool})); |
115 |
val sumtree_inj = Sum_Tree.mk_inj domT n_fs (idx + 1) args; |
|
54736 | 116 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
117 |
val cprop = Thm.cterm_of ctxt prop; |
54736 | 118 |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
119 |
val asms = [cprop, Thm.cterm_of ctxt (HOLogic.mk_Trueprop (dom $ sumtree_inj))]; |
54736 | 120 |
val asms_thms = map Thm.assume asms; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
121 |
|
54737 | 122 |
fun prep_subgoal_tac i = |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59454
diff
changeset
|
123 |
REPEAT (eresolve_tac ctxt @{thms Pair_inject} i) |
54736 | 124 |
THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i |
54738 | 125 |
THEN propagate_tac ctxt i |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
55968
diff
changeset
|
126 |
THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i) |
54736 | 127 |
THEN bool_subst_tac ctxt i; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
128 |
|
59454 | 129 |
val elim_stripped = |
130 |
nth cases idx |
|
131 |
|> Thm.forall_elim P |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
132 |
|> Thm.forall_elim (Thm.cterm_of ctxt args) |
59454 | 133 |
|> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac) |
134 |
|> fold_rev Thm.implies_intr asms |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
135 |
|> Thm.forall_intr (Thm.cterm_of ctxt rhs_var); |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
136 |
|
59454 | 137 |
val bool_elims = |
59655 | 138 |
if fastype_of rhs_var = @{typ bool} |
139 |
then mk_bool_elims ctxt elim_stripped |
|
140 |
else []; |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
141 |
|
59454 | 142 |
fun unstrip rl = |
143 |
rl |
|
59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59618
diff
changeset
|
144 |
|> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) arg_vars |
59454 | 145 |
|> Thm.forall_intr P |
146 |
in |
|
147 |
map unstrip (elim_stripped :: bool_elims) |
|
148 |
end; |
|
53666 | 149 |
in |
150 |
map_index mk_partial_elim_rule fs |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
151 |
end; |
53666 | 152 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
153 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
154 |
|
53666 | 155 |
end; |