Re: [isabelle] Problem with monotonicity proof

Hi Mark,

The monotonicity prover of the inductive package requires a specific format for monotonicity rules. In particular, there is no point in proven the monotonicity statement yourself and adding it.

In general, you need a separate monotonicity preservation statement for every higher-order combinator that is apply to the inductively defined constant. For your definition of Q' with List.list_all, you have to prove and declare the corresponding monotonicity rule. In the other definition, you use bounded universal quantification, for which there is already a monotonicity rule in place.

You can infer the format by looking at the goal state of the failed proof attempt. For list_all, the right rule is this:

  (!!x. P x --> Q x) ==> list_all P xs --> list_all Q xs

Monotonicity must be expressed using HOL implication and Pure quantification.

Another remark: I recommend to use universal quantification instead of list_all, because list_all is used almost exclusively for code generation, i.e., proof automation will be less good. In particular, the proof method induction works much better with universal quantifiers than any other higher-order combinator.


On 26/11/16 15:06, Mark Wassell wrote:

I have a simple inductive predicate:

inductive Q' :: "nat â bool" where
Q'0: "Q' 0" |
Q'n: "List.list_all (Îk. Q' k) [0..<n] â Q' n"

The monotonicity proof for this fails. I take the goal from the error
window and prove it:

lemma xx [mono]: "mono (Îp x. x = 0 â (ân. x = n â list_all p [0..<n]))"
unfolding pred_list_def mono_def
proof((rule allI)+,rule impI)
  fix x and y::"natâbool"
  assume "xây"
  show "(Îxa. xa = 0 â (ân. xa = n â Ball (set [0..<n]) x))
           â (Îx. x = 0 â (ân. x = n â Ball (set [0..<n]) y))" using âx â
yâ by blast

However the monotonicity proof for the predicate still doesn't work. It has
been added to the 'mono' list and if I include the line 'monos xx' after
the inductive predicate definition, there is still no proof.

The  inductive predicate

inductive Q :: "nat â bool" where
Q0: "Q 0" |
Qn: "(âkâset[0..<n]. Q k) â Q n"

is ok. I believe that Q' and Q and equivalent.



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