# [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.