author | wenzelm |
Fri, 13 Dec 2013 14:15:52 +0100 | |
changeset 54738 | ddada9ed12f6 |
parent 54737 | 6a19eb3bd255 |
child 54739 | d41099c829bf |
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 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
24 |
open Function_Lib |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
25 |
open Function_Common |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
26 |
|
53669
6ede465b5be8
more antiquotations -- avoid unchecked string literals;
wenzelm
parents:
53667
diff
changeset
|
27 |
(* 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
|
28 |
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
|
29 |
returns a boolean, "f x y z" *) |
53669
6ede465b5be8
more antiquotations -- avoid unchecked string literals;
wenzelm
parents:
53667
diff
changeset
|
30 |
fun dest_funprop (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = (strip_comb lhs, rhs) |
6ede465b5be8
more antiquotations -- avoid unchecked string literals;
wenzelm
parents:
53667
diff
changeset
|
31 |
| dest_funprop (Const (@{const_name Not}, _) $ trm) = (strip_comb trm, @{term "False"}) |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
32 |
| dest_funprop trm = (strip_comb trm, @{term "True"}); |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
33 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
34 |
local |
53666 | 35 |
|
54738 | 36 |
fun propagate_tac ctxt i = |
54736 | 37 |
let |
38 |
fun inspect eq = |
|
39 |
(case eq of |
|
40 |
Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) => |
|
41 |
if Logic.occs (Free x, t) then raise Match else true |
|
42 |
| Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) => |
|
43 |
if Logic.occs (Free x, t) then raise Match else false |
|
44 |
| _ => raise Match); |
|
45 |
fun mk_eq thm = |
|
46 |
(if inspect (prop_of thm) then [thm RS eq_reflection] |
|
47 |
else [Thm.symmetric (thm RS eq_reflection)]) |
|
48 |
handle Match => []; |
|
54738 | 49 |
val simpset = |
50 |
empty_simpset ctxt |
|
54736 | 51 |
|> Simplifier.set_mksimps (K mk_eq); |
53666 | 52 |
in |
54738 | 53 |
asm_lr_simp_tac simpset i |
53666 | 54 |
end; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
55 |
|
54737 | 56 |
val eq_boolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}; |
54736 | 57 |
val boolE = @{thms HOL.TrueE HOL.FalseE}; |
58 |
val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}; |
|
54737 | 59 |
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
|
60 |
|
53666 | 61 |
fun bool_subst_tac ctxt i = |
54737 | 62 |
REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eq_bool i) |
54736 | 63 |
THEN REPEAT (dresolve_tac boolD i) |
64 |
THEN REPEAT (eresolve_tac boolE i) |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
65 |
|
53666 | 66 |
fun mk_bool_elims ctxt elim = |
54736 | 67 |
let |
68 |
val tac = ALLGOALS (bool_subst_tac ctxt); |
|
69 |
fun mk_bool_elim b = |
|
70 |
elim |
|
71 |
|> Thm.forall_elim b |
|
54737 | 72 |
|> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eq_boolI 1)) |
54736 | 73 |
|> Tactic.rule_by_tactic ctxt tac; |
53666 | 74 |
in |
54736 | 75 |
map mk_bool_elim [@{cterm True}, @{cterm False}] |
53666 | 76 |
end; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
77 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
78 |
in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
79 |
|
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
80 |
fun mk_partial_elim_rules ctxt result = |
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
81 |
let |
54736 | 82 |
val thy = Proof_Context.theory_of ctxt; |
54738 | 83 |
val cert = cterm_of thy; |
53667
0aefb31e27e0
distinguish Proof.context vs. local_theory semantically, with corresponding naming conventions;
wenzelm
parents:
53666
diff
changeset
|
84 |
|
54737 | 85 |
val FunctionResult {fs, R, dom, psimps, cases, ...} = result; |
54736 | 86 |
val n_fs = length fs; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
87 |
|
54736 | 88 |
fun mk_partial_elim_rule (idx, f) = |
89 |
let |
|
90 |
fun mk_funeq 0 T (acc_vars, acc_lhs) = |
|
91 |
let val y = Free("y", T) |
|
92 |
in (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T) end |
|
93 |
| mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) = |
|
94 |
let val xn = Free ("x" ^ Int.toString n, S) |
|
95 |
in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end |
|
54737 | 96 |
| mk_funeq _ _ _ = raise TERM ("Not a function.", [f]); |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
97 |
|
54736 | 98 |
val f_simps = |
99 |
filter (fn r => |
|
100 |
(prop_of r |> Logic.strip_assums_concl |
|
101 |
|> HOLogic.dest_Trueprop |
|
102 |
|> dest_funprop |> fst |> fst) = f) |
|
103 |
psimps; |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
104 |
|
54736 | 105 |
val arity = |
106 |
hd f_simps |
|
107 |
|> prop_of |
|
108 |
|> Logic.strip_assums_concl |
|
109 |
|> HOLogic.dest_Trueprop |
|
110 |
|> snd o fst o dest_funprop |
|
111 |
|> length; |
|
112 |
val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([], f); |
|
113 |
val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs)); |
|
114 |
val args = HOLogic.mk_tuple arg_vars; |
|
115 |
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
|
116 |
|
54736 | 117 |
val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args; |
118 |
||
54738 | 119 |
val cprop = cert prop; |
54736 | 120 |
|
54738 | 121 |
val asms = [cprop, cert (HOLogic.mk_Trueprop (dom $ sumtree_inj))]; |
54736 | 122 |
val asms_thms = map Thm.assume asms; |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
123 |
|
54737 | 124 |
fun prep_subgoal_tac i = |
54736 | 125 |
REPEAT (eresolve_tac @{thms Pair_inject} i) |
126 |
THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i |
|
54738 | 127 |
THEN propagate_tac ctxt i |
54736 | 128 |
THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i) |
129 |
THEN bool_subst_tac ctxt i; |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
130 |
|
54736 | 131 |
val elim_stripped = |
132 |
nth cases idx |
|
133 |
|> Thm.forall_elim @{cterm "P::bool"} |
|
54738 | 134 |
|> Thm.forall_elim (cert args) |
54737 | 135 |
|> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac) |
54736 | 136 |
|> fold_rev Thm.implies_intr asms |
54738 | 137 |
|> Thm.forall_intr (cert rhs_var); |
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
138 |
|
54736 | 139 |
val bool_elims = |
140 |
(case ranT of |
|
141 |
Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped |
|
142 |
| _ => []); |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
143 |
|
54736 | 144 |
fun unstrip rl = |
145 |
rl |
|
54738 | 146 |
|> (fn thm => List.foldr (uncurry Thm.forall_intr) thm (map cert arg_vars)) |
54736 | 147 |
|> Thm.forall_intr @{cterm "P::bool"}; |
148 |
in |
|
149 |
map unstrip (elim_stripped :: bool_elims) |
|
150 |
end; |
|
53666 | 151 |
in |
152 |
map_index mk_partial_elim_rule fs |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
153 |
end; |
53666 | 154 |
|
53603
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
155 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
156 |
|
53666 | 157 |
end; |
158 |