[isabelle] recdef hint ignored



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,
- Reto



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)









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