# [isabelle] trying to convince Isabelle to accept some programming

```Hello,

I have proved the consistency of specialized theorem prover
in Isabelle, but when I am trying to use it, I find serious problems
with "executing"/simplifying some functions that initally looked to me
very amenable to simplification.&nbsp;

Particularly, I have the following problems:
-- Isabelle won't simplify underneath&nbsp; existential quantifiers, and would loop
if I try to simplify after replacing the existentially quantified variables
with schematic variables (via existential introduction) or if try
to enforce an "under-exists" simplification rule
-- in cases when simplification does
what I wish (using auto
for some
trivial FOL
arrangements to help
simplification), it takes too much time (I think
auto tries to hard)

I have tried to capture these problems with the following small example,
where:
-- a term is either a basic term "Bas n" or a compound term "Cpd Ts";
-- a rule deduces terms (conclusions) from lists of terms (hypotheses);
-- there are only five rules: R1, R2, R1', R1'', R2';
-- the function mdr mathes a term against these rules constructing
&nbsp;&nbsp; backwards a proof subject to some constraints (that the term is the
&nbsp;&nbsp; conclusion of the rule and its immediate
&nbsp;&nbsp; subterms are less or equal to (le) the hypotheses of the rule -- I
&nbsp;&nbsp; have added this complication with "le" so that I do not have
&nbsp;&nbsp; unique proofs).

Here is the theory (I am also attaching it as a thy file):&nbsp;

--------------------------------------
datatype trm = Bas nat | Cpd "trm list"

record rule =

&nbsp; hyps :: "trm list"
&nbsp; cnc :: "trm"

constdefs
R1 :: "rule"&nbsp;
"R1 == (| hyps = [Bas 1, Cpd[Bas 2, Bas 3]],
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp;&nbsp; &nbsp; cnc = Cpd [Bas 1, Cpd[Bas 2, Bas 3]] |)"
R2 :: "rule"&nbsp;
"R2 == (|hyps = [Bas 2, Cpd[Bas 3, Bas 4]],
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; cnc = Cpd [Bas 1, Cpd[Bas 2, Bas 3]] |)"&nbsp;
R1' :: "rule"&nbsp;
"R1' == (|hyps = [Bas 2, Bas 3],
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp;&nbsp; cnc = Cpd [Bas 2, Bas 3] |)"
R1'' :: "rule"&nbsp;
"R1'' == (|hyps = [Bas 3, Bas 4],
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp;&nbsp; cnc = Cpd [Bas 2, Bas 3] |)"
R2' :: "rule"&nbsp;
"R2' == (|hyps = [Bas 4, Bas 5],
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp;&nbsp; &nbsp; cnc = Cpd [Bas 3, Bas 4] |)"

constdefs Rls :: "rule
set"
"Rls == {R1, R2, R1', R1'', R2'}"

consts le :: "trm =&gt; rm =&gt; bool"
axioms le_simps_Bas:
"ge (Bas n) T' = True"

axioms le_simps_Ind:
"le (Cpd Ts) T' =
&nbsp; (case T' of Bas n' =&gt; False
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; |Cpd Ts' =&gt; length Ts = length Ts' /\
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp; (ALL i &lt; length Ts. le (Ts!i) (Ts'!i)))"
lemmas le_simps = le_simps_Bas le_simps_Ind
declare le_simps [simp]

lemmas rules_defs = Rls_def R1_def R2_def R1'_def R1''_def R2'_def&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
declare rules_defs [simp]
&nbsp;
consts mdr :: "trm =&gt; rule set"
axioms mdr_simps_Bas:
"mdr (Bas n) = {(| hyps = [Bas n], cnc = Bas n
|)}"

axioms mdr_simps_Cpd:
"mdr (Cpd Ts) =
&nbsp; {(|hyps = concat (map hyps drls),
&nbsp;&nbsp;&nbsp;&nbsp; cnc = Cpd Ts |)
&nbsp;&nbsp; |rl drls.&nbsp;
&nbsp;&nbsp;&nbsp; rl: Rls /\
&nbsp;&nbsp;&nbsp; cnc rl = Cpd Ts /\
&nbsp;&nbsp;&nbsp; length (hyps rl) = length Ts /\
&nbsp;&nbsp;&nbsp; length drls = length Ts /\
&nbsp;&nbsp;&nbsp; (ALL i &lt; length Ts. le (Ts ! i) (hyps rl ! i) /\
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp; &nbsp; &nbsp;&nbsp; drls!i : mdr (hyps rl ! i))}"

lemmas mdr_simps = mdr_simps_Bas mdr_simps_Cpd
declare mdr_simps [simp]
-------------------------------------------

I would like to be able to execute mdr, so that I always obtain, for example,
of "x : mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])", a disjunction of 6 facts
(according to the six
possible decompositions), where, for example, one of the dijuncts would be

"x = (| hyps = [Bas (Suc 0), Bas 2, Bas 3],
&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp; cnc = Cpd [Bas (Suc 0), Cpd [Bas 2, Bas 3]]&nbsp; |)"

In order to achieve this, I try to help the engine by adding the following simplification rules:
&nbsp;
--------------------------------------
lemma help_map0[simp]:
"length xs = 0 ==&gt; map f xs = []"
sorry

lemma help_map1[simp]:
&nbsp;"length xs = Suc n ==&gt;
&nbsp; map f xs = map f (butlast xs) @ [f(xs ! n)]"
sorry

lemma help_butlast[simp]:
"i &lt; length xs ==&gt; butlast xs ! i = xs ! i"
sorry

lemma help_finite_pred[simp]:
"(ALL j &lt; Suc n. phi j) = ((ALL j &lt; n. phi j) /\ phi n)"
sorry
------------------------------------------------

With these, auto is able to reduce a goal like

"mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]]) &lt;= X"

to six goals having conclusions of the form "rl : X" for
each of the six elements rl of "mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])",
which is satisfactory, although the reduction is quite slow for this

The above reduction is clearly safe, which would make me hope for the possibility of a dual reduction to a disjunction.&nbsp; However, if I place
"mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])" on a positive position
in a goal, as in "x : mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])",
I am not able to decompose the goal into a disjunction no matter how I try.&nbsp;
For instance, if I try (adding a seemingly useful distributive law)

lemma "x : mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])"

it will not apply the needed simplifications.&nbsp;

If I try (at&nbsp; the same lemma),&nbsp;

apply (auto simp add: conj_disj_distribR, rule exI, rule exI, auto)

it will loop,

and also if I add the further lemma

lemma simp_inside_EX:
"(!! x y. P x y = Q x y) ==&gt; (EX x y. P x y) = (EX x y. Q x y)"
by blast

and then try

&nbsp;&nbsp;&nbsp;&nbsp; &nbsp; &nbsp; simp add: simp_inside_EX)

it will loop again.

So my question is: do I need to write my own rewrite engine/tactical, or
would a proper use of existing ones in Isabelle solve my problems regarding the
possibility of decomposition and its computational complexity ?