author | Manuel Eberl |
Sun, 08 Sep 2013 22:32:47 +0200 | |
changeset 53603 | 59ef06cda7b9 |
child 53609 | 0f472e7063af |
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 |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
2 |
Author: Manuel Eberl <eberlm@in.tum.de>, TU München |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
3 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
4 |
Generates the pelims rules for a function. These are of the shape |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
5 |
[|f x y z = w; !!…. [|x = …; y = …; z = …; w = …|] ==> P; …|] ==> P |
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 |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
11 |
elim rules with P x resp. ¬P x as premises. |
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 |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
17 |
val mk_partial_elim_rules : |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
18 |
local_theory -> Function_Common.function_result -> thm list list |
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 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
27 |
(* Extracts a function and its arguments from a proposition that is |
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" *) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
30 |
fun dest_funprop (Const ("HOL.eq", _) $ lhs $ rhs) = (strip_comb lhs, rhs) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
31 |
| dest_funprop (Const ("HOL.Not", _) $ trm) = (strip_comb trm, @{term "False"}) |
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 |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
35 |
fun propagate_tac i thm = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
36 |
let fun inspect eq = case eq of |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
37 |
Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ Free x $ t) => |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
38 |
if Logic.occs (Free x, t) then raise Match else true |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
39 |
| Const ("HOL.Trueprop",_) $ (Const ("HOL.eq",_) $ t $ Free x) => |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
40 |
if Logic.occs (Free x, t) then raise Match else false |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
41 |
| _ => raise Match; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
42 |
fun mk_eq thm = (if inspect (prop_of thm) then |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
43 |
[thm RS eq_reflection] |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
44 |
else |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
45 |
[Thm.symmetric (thm RS eq_reflection)]) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
46 |
handle Match => []; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
47 |
val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
48 |
|> Simplifier.set_mksimps (K mk_eq) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
49 |
in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
50 |
asm_lr_simp_tac ss i thm |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
51 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
52 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
53 |
val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+} |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
54 |
val boolE = @{thms HOL.TrueE HOL.FalseE} |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
55 |
val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+} |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
56 |
val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False} |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
57 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
58 |
fun bool_subst_tac ctxt i = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
59 |
REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
60 |
THEN REPEAT (dresolve_tac boolD i) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
61 |
THEN REPEAT (eresolve_tac boolE i) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
62 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
63 |
fun mk_bool_elims ctxt elim = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
64 |
let val tac = ALLGOALS (bool_subst_tac ctxt) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
65 |
fun mk_bool_elim b = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
66 |
elim |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
67 |
|> Thm.forall_elim b |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
68 |
|> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1)) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
69 |
|> Tactic.rule_by_tactic ctxt tac |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
70 |
in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
71 |
map mk_bool_elim [@{cterm True}, @{cterm False}] |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
72 |
end; |
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 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
76 |
fun mk_partial_elim_rules ctxt result= |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
77 |
let val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases, |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
78 |
termination, domintros, ...} = result; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
79 |
val n_fs = length fs; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
80 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
81 |
fun mk_partial_elim_rule (idx,f) = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
82 |
let fun mk_funeq 0 T (acc_vars, acc_lhs) = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
83 |
let val y = Free("y",T) in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
84 |
(y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
85 |
end |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
86 |
| mk_funeq n (Type("fun",[S,T])) (acc_vars, acc_lhs) = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
87 |
let val xn = Free ("x" ^ Int.toString n,S) in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
88 |
mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
89 |
end |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
90 |
| mk_funeq _ _ _ = raise (TERM ("Not a function.", [f])) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
91 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
92 |
val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
93 |
|> HOLogic.dest_Trueprop |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
94 |
|> dest_funprop |> fst |> fst) = f) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
95 |
psimps |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
96 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
97 |
val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
98 |
|> HOLogic.dest_Trueprop |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
99 |
|> snd o fst o dest_funprop |> length; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
100 |
val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
101 |
val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
102 |
val args = HOLogic.mk_tuple arg_vars; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
103 |
val domT = R |> dest_Free |> snd |> hd o snd o dest_Type |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
104 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
105 |
val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
106 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
107 |
val thy = Proof_Context.theory_of ctxt; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
108 |
val cprop = cterm_of thy prop |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
109 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
110 |
val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))]; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
111 |
val asms_thms = map Thm.assume asms; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
112 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
113 |
fun prep_subgoal i = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
114 |
REPEAT (eresolve_tac @{thms Pair_inject} i) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
115 |
THEN Method.insert_tac (case asms_thms of |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
116 |
thm::thms => (thm RS sym) :: thms) i |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
117 |
THEN propagate_tac i |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
118 |
THEN TRY |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
119 |
((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
120 |
THEN bool_subst_tac ctxt i; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
121 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
122 |
val tac = ALLGOALS prep_subgoal; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
123 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
124 |
val elim_stripped = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
125 |
nth cases idx |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
126 |
|> Thm.forall_elim @{cterm "P::bool"} |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
127 |
|> Thm.forall_elim (cterm_of thy args) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
128 |
|> Tactic.rule_by_tactic ctxt tac |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
129 |
|> fold_rev Thm.implies_intr asms |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
130 |
|> Thm.forall_intr (cterm_of thy rhs_var) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
131 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
132 |
val bool_elims = (case ranT of |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
133 |
Type ("HOL.bool", []) => mk_bool_elims ctxt elim_stripped |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
134 |
| _ => []); |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
135 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
136 |
fun unstrip rl = |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
137 |
rl |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
138 |
(map (cterm_of thy) arg_vars)) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
139 |
|> Thm.forall_intr @{cterm "P::bool"} |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
140 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
141 |
in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
142 |
map unstrip (elim_stripped :: bool_elims) |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
143 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
144 |
|
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
145 |
in |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
146 |
map_index mk_partial_elim_rule fs |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
147 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
148 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
149 |
end; |
59ef06cda7b9
generate elim rules for elimination of function equalities;
Manuel Eberl
parents:
diff
changeset
|
150 |