[isabelle] trying to convince Isabelle to accept some programming


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.  

Particularly, I have the following problems: 
-- Isabelle won't simplify underneath  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, 
-- 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 
   backwards a proof subject to some constraints (that the term is the 
   conclusion of the rule and its immediate 
   subterms are less or equal to (le) the hypotheses of the rule -- I 
   have added this complication with "le" so that I do not have 
   unique proofs). 

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

datatype trm = Bas nat | Cpd "trm list"

record rule =
  hyps :: "trm list"
  cnc :: "trm" 

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

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

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

axioms le_simps_Ind: 
"le (Cpd Ts) T' = 
  (case T' of Bas n' => False 
             |Cpd Ts' => length Ts = length Ts' /\ 
                               (ALL i < 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                  
declare rules_defs [simp]
consts mdr :: "trm => rule set" 
axioms mdr_simps_Bas: 
"mdr (Bas n) = {(| hyps = [Bas n], cnc = Bas n

axioms mdr_simps_Cpd: 
"mdr (Cpd Ts) = 
  {(|hyps = concat (map hyps drls), 
     cnc = Cpd Ts |) 
   |rl drls.  
    rl: Rls /\ 
    cnc rl = Cpd Ts /\ 
    length (hyps rl) = length Ts /\ 
    length drls = length Ts /\
    (ALL i < length Ts. le (Ts ! i) (hyps rl ! i) /\
                                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], 
         cnc = Cpd [Bas (Suc 0), Cpd [Bas 2, Bas 3]]  |)"

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

lemma help_map1[simp]: 
 "length xs = Suc n ==> 
  map f xs = map f (butlast xs) @ [f(xs ! n)]" 

lemma help_butlast[simp]:
"i < length xs ==> butlast xs ! i = xs ! i"

lemma help_finite_pred[simp]:
"(ALL j < Suc n. phi j) = ((ALL j < n. phi j) /\ phi n)"

With these, auto is able to reduce a goal like

"mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]]) <= 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 
small example already. 

The above reduction is clearly safe, which would make me hope for the possibility of a dual reduction to a disjunction.  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.  
For instance, if I try (adding a seemingly useful distributive law) 

lemma "x : mdr(Cpd [Bas 1, Cpd[Bas 2, Bas 3]])"
apply (auto simp add: conj_disj_distribR)

it will not apply the needed simplifications.  

If I try (at  the same lemma), 

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) ==> (EX x y. P x y) = (EX x y. Q x y)"
by blast

and then try 

apply (auto simp add: conj_disj_distribR, 
         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 ? 

Many thanks in advance for any advice regarding this matter, 
    Andrei Popescu 


Attachment: miniTest.thy
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.