*Subject*: Re: [isabelle] monotonicity for inductive*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Fri, 08 Jun 2012 09:29:47 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4FD06F1C.8060501@jaist.ac.jp>*References*: <4FD06F1C.8060501@jaist.ac.jp>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.27) Gecko/20120216 Thunderbird/3.1.19

Dear Christian,

!!x y xa xb f g ss ts. x (?x33 x y xa xb f g ss ts) (?x34 x y xa xb f g ss ts) --> y (?x33 x y xa xb f g ss ts) (?x34 x y xa xb f g ss ts) ==> emb x ss ts --> emb y ss ts

Note that you could also have used the following monotonicity rule: "P <= Q ==> emp P s t --> emp Q s t" Andreas Am 07.06.2012 11:06, schrieb Christian Sternagel:

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

-- Karlsruher Institut für Technologie IPD Snelting Andreas Lochbihler wissenschaftlicher Mitarbeiter Am Fasanengarten 5, Geb. 50.34, Raum 025 76131 Karlsruhe Telefon: +49 721 608-47399 Fax: +49 721 608-48457 E-Mail: andreas.lochbihler at kit.edu http://pp.info.uni-karlsruhe.de

**References**:**[isabelle] monotonicity for inductive***From:*Christian Sternagel

- Previous by Date: [isabelle] monotonicity for inductive
- Next by Date: [isabelle] 6th International School on Rewriting (ISR 2012) - Early registration (250 euro): June 15!!
- Previous by Thread: [isabelle] monotonicity for inductive
- Next by Thread: [isabelle] 6th International School on Rewriting (ISR 2012) - Early registration (250 euro): June 15!!
- Cl-isabelle-users June 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list