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