Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Reto Kramer <kramer@acm.org>
The recdef matchE below fails with:
*** Bad final proof state:
*** matchE (a, b) \<and> matchE (b, a) \<and> e = Diff x y
\<longrightarrow>
*** Suc (depthE x + depthE y) < depthE e + (depthE a + depthE b)
*** 1. matchE (a, b) \<and> matchE (b, a) \<and> e = Diff x y
\<longrightarrow>
*** Suc (depthE x + depthE y) < depthE e + (depthE a + depthE b)
*** 1 unsolved goals!
*** Proof failed!
*** At command "recdef".
despite lemma depth2E_bg_1 being a recdef-hint, stating the truth of
this very subgoal. I'm puzzled that the depth2E_bg_1 lemma isn't
taken into account in the recdef proof.
How can I help the system prove the above subgoal, or how do I ensure
the hint is effective?
Thanks,
theory idc = List:
types
element = "nat"
path = "element list"
consts inOrEq :: "path \<Rightarrow> path \<Rightarrow> bool" (*
(infix "\<subseteq>" 500) *)
primrec
"inOrEq [] q = (case q of [] \<Rightarrow> True (* * in
*)
| y#ys \<Rightarrow> False)" (* * in
a* *)
"inOrEq (x#xs) q = (case q of [] \<Rightarrow> True (* a* in
*)
| y#ys \<Rightarrow> (x = y) & (inOrEq
xs ys))"
types
node = "path \<times> element"
consts path :: "node \<Rightarrow> path"
primrec
"path (p,n) = p"
consts node :: "node \<Rightarrow> element"
primrec
"node (p,n) = n"
constdefs
eqN :: "node \<Rightarrow> node \<Rightarrow> bool"
"eqN a b == a = b"
datatype expr = Empty
| Node node
| Descendents path (* a.b.* translates to Descendents
[a,b] *)
| Children path (* a.b.# translates to Children [a,b] *)
| Sum expr expr
| Diff expr expr
consts depthE :: "expr \<Rightarrow> nat" (* helper for termination
proof of matchE *)
primrec
"depthE (Empty) = 1"
"depthE (Node x) = 1"
"depthE (Descendents x) = 1"
"depthE (Children x) = 1"
"depthE (Sum x y) = (depthE x) + (depthE y)"
"depthE (Diff x y) = (depthE x) + (depthE y)"
lemma depthE_bg_0: "0 < depthE e"
apply (induct_tac e)
apply simp_all
done
lemma depth2E_bg_1:
"matchE (a,b) \<and> matchE (b,a) \<and> e = Diff x y
\<longrightarrow> Suc (depthE x + depthE y) < depthE e + (depthE
a + depthE b)"
apply (rule impI)
apply simp
apply (induct_tac a)
apply (simp_all add: depthE_bg_0)
done
consts matchE :: "expr \<times> expr \<Rightarrow> bool"
recdef matchE "measure (\<lambda>(e1,e2). depthE e1 + depthE e2)"
"matchE (e,(Empty)) = (case e of
Empty \<Rightarrow> True
| Node x \<Rightarrow> False
| Descendents x \<Rightarrow> False
| Children x \<Rightarrow> False
| Sum x y \<Rightarrow> matchE (x,
Empty)
& matchE (y, Empty)
| Diff x y \<Rightarrow> matchE (y, x)
| matchE (x, Empty))"
"matchE (e,(Node n)) = (case e of
Empty \<Rightarrow> True
| Node x \<Rightarrow> eqN n x
| Descendents x \<Rightarrow> False
| Children x \<Rightarrow> False
| Sum x y \<Rightarrow> matchE (x,
Node n)
& matchE (x, Node n)
| Diff x y \<Rightarrow> matchE
(x, Node n)
& ~matchE (Node n, y))"
"matchE (e,(Descendents p)) = (case e of
Empty \<Rightarrow> True
| Node (q,m) \<Rightarrow> inOrEq
q p
| Descendents x \<Rightarrow> p = x
| Children x \<Rightarrow> inOrEq
x p
| Sum x y \<Rightarrow> matchE
(x, Descendents p)
& matchE (x,
Descendents p)
| Diff x y \<Rightarrow> matchE
(x, Descendents p)
& ~matchE
(Descendents p, y))"
"matchE (e,(Children p)) = (case e of
Empty \<Rightarrow> True
| Node (q,m) \<Rightarrow> p = q
| Descendents x \<Rightarrow> False
| Children x \<Rightarrow> p = x
| Sum x y \<Rightarrow>
matchE (x, Children p)
& matchE (x,
Children p)
| Diff x y \<Rightarrow>
matchE (x, Children p)
& ~matchE
(Children p, y))"
"matchE (e,(Sum a b)) = (case e of
Empty \<Rightarrow> True
| Node x \<Rightarrow> (matchE
(e,a))|(matchE (e,b))
| Descendents x \<Rightarrow> (matchE
(e,a))|(matchE (e,b))
| Children x \<Rightarrow> (matchE
(e,a))|(matchE (e,b))
| Sum x y \<Rightarrow> matchE
(x, Sum a b)
& matchE (y, Sum a b)
| Diff x y \<Rightarrow> matchE
(Diff x y, a)
| matchE (Diff x y,
b))"
"matchE (e,(Diff a b)) = (case e of
Empty \<Rightarrow> True
| Node x \<Rightarrow> (matchE
(e,a))&~(matchE (e,b))
| Descendents x \<Rightarrow> (matchE
(e,a))&~(matchE (e,b))
| Children x \<Rightarrow> (matchE
(e,a))&~(matchE (e,b))
| Sum x y \<Rightarrow> matchE
(Sum x y, a)
& ~matchE (Sum x y, b)
| Diff x y \<Rightarrow>
(if (matchE (a,b) & matchE (b,a))
then matchE (Diff x y, Empty)
else matchE (Diff x y, a)
& ~matchE (Diff x y, b)))"
(hints recdef_simp: depth2E_bg_1 depthE_bg_0)
Last updated: May 03 2024 at 08:18 UTC