*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] trying to convince Isabelle to accept some programming*From*: Andrei Popescu <uuomul at yahoo.com>*Date*: Fri, 13 Jun 2008 15:40:04 -0700 (PDT)

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. 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, 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 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" constdefs 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 set" "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, instead 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 = []" sorry lemma help_map1[simp]: "length xs = Suc n ==> map f xs = map f (butlast xs) @ [f(xs ! n)]" sorry lemma help_butlast[simp]: "i < length xs ==> butlast xs ! i = xs ! i" sorry lemma help_finite_pred[simp]: "(ALL j < Suc n. phi j) = ((ALL j < 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]]) <= 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**

**Follow-Ups**:**Re: [isabelle] trying to convince Isabelle to accept some programming***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Recursion on finite, lazy lists (llists)
- Next by Date: Re: [isabelle] trying to convince Isabelle to accept some programming
- Previous by Thread: [isabelle] Call for Participation: Conferences on Intelligent Computer Mathematics
- Next by Thread: Re: [isabelle] trying to convince Isabelle to accept some programming
- Cl-isabelle-users June 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list