[isabelle] apply (rule exI) diverging



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.