[isabelle] monotonicity for inductive



Dear all,

The below inductive definition did (not surprisingly) only work after introducing a monotonicity rule for emb. However, I came up with the mono rule by "pattern-matching" against existing monotonicity rules. Since the resulting induction schema is slightly odd, I was wondering whether I did something strange and what others do in such cases (when monotonicity is an issue).


datatype 'a tree = Empty | Node 'a "'a tree list"

inductive
  emb :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ 'a list ⇒ bool"
  for P :: "('a ⇒ 'a ⇒ bool)"
where
  emb_Nil [intro, simp]: "emb P [] ys"
| emb_Cons [intro] : "emb P xs ys ⟹ emb P xs (y#ys)"
| emb_Cons2 [intro]: "P x y ⟹ emb P xs ys ⟹ emb P (x#xs) (y#ys)"

lemma emb_mono:
  assumes "⋀x y. P x y ⟶ Q x y"
  shows "emb P s t ⟶ emb Q s t"
proof
  assume "emb P s t"
  thus "emb Q s t"
    by (induct) (auto simp: assms)
qed

inductive
  hemb :: "('a ⇒ 'a ⇒ bool) ⇒ 'a tree ⇒ 'a tree ⇒ bool"
  for P :: "'a ⇒ 'a ⇒ bool"
where
  hemb_Empty [intro, simp]: "hemb P Empty t" |
  hemb_Node [intro]: "hemb P s t ⟹ t ∈ set ts ⟹ hemb P s (Node f ts)" |
hemb_Node2 [intro]: "P f g ⟹ emb (hemb P) ss ts ⟹ hemb P (Node f ss) (Node g ts)"
monos emb_mono

cheers

chris





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