Re: [isabelle] monotonicity for inductive



Dear Christian,

your monotonicity rule looks totally normal to me. When I need to supply custom monotonicity rules, I usually start by looking at the unsolved goals in the monotonicity proof. In your example, it looks like this:

!!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

The monotonicity solver essentially applies the declared monotonicity rules as introduction rules until all goals are finished. Hence, the above goal says that you need to provide a rule with conclusion "emb x ss ts --> emb y ss ts" which may assume that "x a b" implies "y a b".

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
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





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