[STATEMENT]
lemma (in preorder) dc_open_induct [consumes 2, case_names less]:
  assumes "dc_on (\<le>) UNIV"
    and "open_on (\<le>) Q UNIV"
    and "\<And>x. (\<And>y. y < x \<Longrightarrow> Q y) \<Longrightarrow> Q x"
  shows "Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q x
[PROOF STEP]
have "qo_on (\<le>) UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qo_on (\<le>) UNIV
[PROOF STEP]
by (auto simp: qo_on_def transp_on_def reflp_on_def dest: order_trans)
[PROOF STATE]
proof (state)
this:
qo_on (\<le>) UNIV

goal (1 subgoal):
 1. Q x
[PROOF STEP]
from open_induct_on [OF this assms(1,2)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x
[PROOF STEP]
show "Q x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. Q x
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x
(\<And>y. y < ?x \<Longrightarrow> Q y) \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. Q x
[PROOF STEP]
unfolding less_le_not_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x
(\<And>y. strict (\<le>) y ?x \<Longrightarrow> Q y) \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. Q x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q x

goal:
No subgoals!
[PROOF STEP]
qed