*To*: Chris Capel <pdf23ds at gmail.com>*Subject*: Re: [isabelle] apply (rule exI) diverging*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 24 Feb 2009 12:05:54 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <737b61f30902231935w5084fc8dnc8ecbb270e5e24c0@mail.gmail.com>*References*: <737b61f30902231935w5084fc8dnc8ecbb270e5e24c0@mail.gmail.com>

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)

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 xsp)" |"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 (tlos))"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, TrmoID 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 oldIDoldEl];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" functionparse_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 tidel])) =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 (ruleexI)qed

**References**:**[isabelle] apply (rule exI) diverging***From:*Chris Capel

- Previous by Date: Re: [isabelle] cases/induction on existential/free variables
- Next by Date: Re: [isabelle] "\include{}" for theory files?
- Previous by Thread: [isabelle] apply (rule exI) diverging
- Next by Thread: [isabelle] Interfacing with Isabelle
- Cl-isabelle-users February 2009 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