# [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.*