[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"
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