# [isabelle] monotonicity for inductive

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] monotonicity for inductive
*From*: Christian Sternagel <c-sterna at jaist.ac.jp>
*Date*: Thu, 07 Jun 2012 18:06:36 +0900
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:12.0) Gecko/20120430 Thunderbird/12.0.1

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