Email Gateway (Aug 18 2022 at 20:21): Email Gateway (Aug 18 2022 at 20:21):From: Christian Sternagel <c-sterna@jaist.ac.jp>
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
Email Gateway (Aug 18 2022 at 20:21):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
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
Last updated: Apr 16 2024 at 08:18 UTC