[isabelle] Problem with recdef



I'm trying to define a function using recdef and, as far as I can make out, the goal preventing the termination proof going through is one that I've both already proved and is quickly discharged by simp.

I include the relevant bit of the theory below and the relevant Isabelle output in the hope that someone can see what I'm missing or suggest some way to get closer to the actual problem.

All the erase_measure_lem lemmas are proofs I've done following previous attempts to get the definition through based on output from recdef or recdef_tc erase.

-- fragment of theory file missing the lemma proofs including miscellaneous lemmas and the recdef definition at the bottom

lemma erase_measure_lem1 [simp, rule_format]: "ALL ann_term_list foannat foterm x.
   (EX t. x = WaveHole t) & x : set ann_term_list -->
   ann_term_size (WaveHole_dest x)
   < ann_term_size (WaveFront foannat foterm ann_term_list)" by simp

lemma erase_measure_lem2 [simp, rule_format]: "ALL ann_term_list foannat foterm x.
   (ALL t. x = WaveHole t) & x : set ann_term_list -->
   ann_term_size x
   < ann_term_size (WaveFront foannat foterm ann_term_list)"
proof (clarify)
   some proof
  qed

lemma erase_measure_lem3 [simp, rule_format]: "(EX t. x = WaveHole t) & x : set ann_term_list -->
       ann_term_size (WaveHole_dest x)
       < ann_term_size (WaveFront foannat foterm ann_term_list)" by simp

lemma erase_measure_lem4 [simp, rule_format]: "ALL ann_term_list foannat foterm x.
      (ALL t. x ~= WaveHole t) & x : set ann_term_list -->
ann_term_size x < ann_term_size (WaveFront foannat foterm ann_term_list)"
proof (clarify)
    some proof
   qed

lemma erase_measure_lem5 [simp, rule_format] : "ALL anterm_list foterm x.
x : set anterm_list --> ann_term_size x < ann_term_size (anApp foterm anterm_list)"
proof (clarify)
some proof
qed

recdef (permissive) erase "measure ann_term_size"
 erase_foterm: "erase (FoTerm (t)) = t"
erase_anApp: "erase (anApp foterm anterm_list) = foApp foterm (map erase anterm_list)" erase_wf: "erase (WaveFront foannat foterm ann_term_list) = foApp foterm (map (%x. (if (EX t. x = (WaveHole t)) then (erase (WaveHole_dest x)) else (erase x))) ann_term_list)"
 erase_wh: "erase (WaveHole t) = arbitrary"
(hints recdef_simp add: erase_measure_lem1 erase_measure_lem2 erase_measure_lem3 erase_measure_lem4 erase_measure_lem5)

-- Isabelle output at this point

### Trying Presburger arithmetic ...

### Trying Presburger arithmetic ...

### Proof failed.
### ALL ann_term_list foannat foterm x.
###    (EX t. x = WaveHole t) & x : set ann_term_list -->
### ann_term_size (WaveHole_dest x) < ann_term_size (WaveFront foannat foterm ann_term_list)
###  1. ALL ann_term_list foannat foterm x.
###        (EX t. x = WaveHole t) & x : set ann_term_list -->
### ann_term_size (WaveHole_dest x) < ann_term_size (WaveFront foannat foterm ann_term_list)
### 1 unsolved goal(s)!
### The error(s) above occurred for the goal statement:
### ALL ann_term_list foannat foterm x.
###    (EX t. x = WaveHole t) & x : set ann_term_list -->
### ann_term_size (WaveHole_dest x) < ann_term_size (WaveFront foannat foterm ann_term_list)

### Trying Presburger arithmetic ...

---

recdef_tc erase

gets me the Isabelle output

proof (prove): step 0

goal (1 subgoal):
1. ALL ann_term_list foannat foterm x.
      (EX t. x = WaveHole t) & x : set ann_term_list -->
ann_term_size (WaveHole_dest x) < ann_term_size (WaveFront foannat foterm ann_term_list)


--

and

recdef_tc erase
proof(simp)

gets me the Isabelle output

proof (state): step 1

goal:
No subgoals!

--

Any help or advice?

Louise

--
Dr. Louise Dennis, Department of Computer Science, Room 117, Ashton Building,
University of  Liverpool, Liverpool, L69 3BX,  UK.
http://www.csc.liv.ac.uk/~lad/  phone: +44 151 795 4237






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