Re: [isabelle] apply (rule exI) diverging



The inclusion of the previous result (by your use of "thus" rather than "show") seems to be part of the problem, though I am not sure why.

Another part of your problem is that the previous result does not appear to match up with the new result that you want to prove. Higher- order unification can get out of control quite quickly when you have a big search space but no solutions.

I was able to make some progress with the following fragment:

 have l: "?LinGr [Prod [[1, 2]], PTrm (Start tid), PTrm (Trm tid el)]"
   sorry
 -- {* hence "EX gr. ?LinGr gr" ..*}
have "EX gr X Y.
      parse_len_dom (gr, gr ! 0, rm_elided st) -->
      nat (parse_len gr (gr ! 0) (rm_elided st)) =
      length (rm_elided st) &
      length gr
      < X * length (rm_elided st) * length mapt +
        Y * length (rm_elided st)"
by (rule exI, rule l)

The previous result is now labelled l. We no longer include it in the next proof (no "from"). I have corrected the statement to be proved so that it matches. Now the proof is instantaneous. Alternatively, you can include the previous result and prove the next one using blast with no arguments.

So the problem appears to be the interaction between the rule method and piped in facts.

Larry Paulson


On 24 Feb 2009, at 03:35, Chris Capel wrote:

Isabelle is running for 30+ seconds when I try to apply (rule exI) in
the middle of my structured proof, eating memory at about 20 MB/sec. I
ran out of memory after that point. At first I thought it was
unification exploding but then I got rid of my function schematic
variable. Could this be a bug? (I'm running from rev
29862:17d1e32ef867, BTW. I can try updating if needed.)

The below theory ought to reproduce this.

Chris Capel


theory Lojban
imports Main
begin

datatype token =
   Start nat -- {* nat is phrase id *}
 | Trm nat bool -- {* phrase id, is elided *}

-- {* Allowable phrase to phrase relations *}
consts
 mapPhPh :: "nat => nat set"
 mapMem :: "nat => nat => bool" (infix ":*" 50)
 mapNotMem :: "nat => nat => bool" (infix "~:*" 50)
translations
 "a :* b" == "a : mapPhPh b"
 "a ~:* b" == "a ~: mapPhPh b"

-- {* ({({ } _) _} ) *}

fun canAppend1 :: "token list => nat => bool" where
"canAppend1 ((Trm pid el)#xs) p = (~el | p ~:* pid & canAppend1 xs p)" |
 "canAppend1 ((Start _ )#xs) p = True"
fun canAppend :: "token list => nat => nat => bool" where
 "canAppend xs p outID  = (p :* outID & canAppend1 (rev xs) p)"

primrec insert_list :: "'a list => nat => 'a list => 'a list" where
 "insert_list list 0 outer = list @ outer" |
"insert_list list (Suc n) os = (hd os) # (insert_list list n (tl os))"

fun rmTrm where
"rmTrm lst = filter (% y. case y of Trm _ _ => False | _ => True) lst"

inductive_set P :: "token list set" where
 base:   "[Start tid, Trm tid el] : P" |
beside: "[| base : P; take 2 (drop pos base) = [Trm aID el1, Trm oID el2];
             canAppend ((take pos base) @ [Trm aID el1]) newID oID |]
          ==> insert_list [Start newID, Trm newID elided]
                          (Suc pos) base
                : P" |

 inside: "[| base : P; 0 < pos;
take 2 (drop (pos - 1) base) = [Start oldID, Trm oldID oldEl];
	      rmTrm (drop pos base) = [];
             newID :* oldID |]
==> insert_list [Start newID, Trm newID elided] pos base : P"

datatype 'tok prod =
   PTrm 'tok
 | Prod "nat list list"

primrec powerlist :: "'a list => 'a list list" where
 "powerlist [] = []" |
 "powerlist (x # xs) = (x # xs) # powerlist xs"

function
parse_len :: "'tok prod list => 'tok prod => 'tok list => int" where

"parse_len gr (PTrm tok) toks = (if ((hd toks) = tok) then 1 else -1)"
| "parse_len gr (Prod pl) toks =
     last (sort (map (%p. foldl (% (len::int) (p, l).
                                   if len = -1 then -1
                                   else len + parse_len gr (gr!p) l)
                                0 (zip p (powerlist toks)))
                 pl))"

by pat_completeness auto

fun getPhMap :: "(nat * nat) list => nat => nat set" where
 "getPhMap ls x = set (map snd (filter (%y. (fst y) = x) ls))"

fun rm_elided :: "token list => token list" where
"rm_elided st = filter (%s. case s of Start _ => True | Trm _ el => ~el) st"

lemma assumes "st : P" and "mapt ~= []" and "mapPhPh = getPhMap mapt"
 shows "EX gr X Y. parse_len_dom (gr, gr!0, (rm_elided st)) -->
(nat (parse_len gr (gr!0) (rm_elided st)) = length (rm_elided st))
            & size gr < X * length (rm_elided st) * length mapt
                        + Y * length (rm_elided st)"
 (is "EX gr. ?LinGr gr")
using assms(1) proof (induct st rule: P.induct)
 fix gr tid el
 have "?LinGr [Prod [[1, 2]], PTrm (Start tid), PTrm (Trm tid el)]"
   sorry
 -- {* hence "EX gr. ?LinGr gr" ..*}
 thus "EX gr X Y.
parse_len_dom (gr, gr ! 0, rm_elided [Start tid, Trm tid el]) --> nat (parse_len gr (gr ! 0) (rm_elided [Start tid, Trm tid el])) =
      length (rm_elided [Start tid, Trm tid el]) &
      length gr
      < X * length (rm_elided [Start tid, Trm tid el]) * length mapt +
Y * length (rm_elided [Start tid, Trm tid el])" apply (rule exI)
qed







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