[isabelle] Problem with monotonicity proof


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.