Email Gateway (Aug 18 2022 at 11:55): Email Gateway (Aug 18 2022 at 11:55):From: Louise Dennis <l.a.dennis@liverpool.ac.uk>
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
foannat foterm ann_term_list)
foannat foterm ann_term_list)
foannat foterm ann_term_list)
recdef_tc erase
gets me the Isabelle output
proof (prove): step 0
goal (1 subgoal):
--
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
Last updated: May 03 2024 at 04:19 UTC