[STATEMENT]
lemma chain_pred_terminates:
  assumes "constr F E" "mono F"
  shows "(\<Sqinter> (range E) \<and> \<mu> F) = (\<Sqinter> (range E) \<and> \<nu> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Or>range E \<and> \<mu> F) = (\<Or>range E \<and> \<nu> F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Or>range E \<and> \<mu> F) = (\<Or>range E \<and> \<nu> F)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
constr F E
Monotonic F
[PROOF STEP]
have "\<forall> n. (E n \<and> \<mu> F) = (E n \<and> \<nu> F)"
[PROOF STATE]
proof (prove)
using this:
constr F E
Monotonic F

goal (1 subgoal):
 1. \<forall>n. (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
[PROOF STEP]
proof (rule_tac allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
constr F E
Monotonic F
[PROOF STEP]
show "(E n \<and> \<mu> F) = (E n \<and> \<nu> F)"
[PROOF STATE]
proof (prove)
using this:
constr F E
Monotonic F

goal (1 subgoal):
 1. (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E 0 \<and> \<mu> F) = (E 0 \<and> \<nu> F)
 2. \<And>n. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
constr F E
Monotonic F

goal (2 subgoals):
 1. \<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E 0 \<and> \<mu> F) = (E 0 \<and> \<nu> F)
 2. \<And>n. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
constr F E
Monotonic F

goal (1 subgoal):
 1. (E 0 \<and> \<mu> F) = (E 0 \<and> \<nu> F)
[PROOF STEP]
by (simp add: constr_def)
[PROOF STATE]
proof (state)
this:
(E 0 \<and> \<mu> F) = (E 0 \<and> \<nu> F)

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
note hyp = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F

goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F

goal (1 subgoal):
 1. (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
have "(E (n + 1) \<and> \<mu> F) = (E (n + 1) \<and> F (\<mu> F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (E (n + 1) \<and> \<mu> F) = (E (n + 1) \<and> F (\<mu> F))
[PROOF STEP]
using gfp_unfold[OF hyp(3), THEN sym]
[PROOF STATE]
proof (prove)
using this:
F (\<mu> F) = \<mu> F

goal (1 subgoal):
 1. (E (n + 1) \<and> \<mu> F) = (E (n + 1) \<and> F (\<mu> F))
[PROOF STEP]
by (simp add: constr_def)
[PROOF STATE]
proof (state)
this:
(E (n + 1) \<and> \<mu> F) = (E (n + 1) \<and> F (\<mu> F))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(E (n + 1) \<and> \<mu> F) = (E (n + 1) \<and> F (\<mu> F))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
from hyp
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F
[PROOF STEP]
have "... = (E (n + 1) \<and> F (E n \<and> \<mu> F))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F

goal (1 subgoal):
 1. (E (n + 1) \<and> F (\<mu> F)) = (E (n + 1) \<and> F (E n \<and> \<mu> F))
[PROOF STEP]
by (metis conj_comm constr_def)
[PROOF STATE]
proof (state)
this:
(E (n + 1) \<and> F (\<mu> F)) = (E (n + 1) \<and> F (E n \<and> \<mu> F))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(E (n + 1) \<and> F (\<mu> F)) = (E (n + 1) \<and> F (E n \<and> \<mu> F))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
from hyp
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F
[PROOF STEP]
have "... = (E (n + 1) \<and> F (E n \<and> \<nu> F))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F

goal (1 subgoal):
 1. (E (n + 1) \<and> F (E n \<and> \<mu> F)) = (E (n + 1) \<and> F (E n \<and> \<nu> F))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(E (n + 1) \<and> F (E n \<and> \<mu> F)) = (E (n + 1) \<and> F (E n \<and> \<nu> F))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(E (n + 1) \<and> F (E n \<and> \<mu> F)) = (E (n + 1) \<and> F (E n \<and> \<nu> F))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
from hyp
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F
[PROOF STEP]
have "... = (E (n + 1) \<and> \<nu> F)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F)
constr F E
Monotonic F

goal (1 subgoal):
 1. (E (n + 1) \<and> F (E n \<and> \<nu> F)) = (E (n + 1) \<and> \<nu> F)
[PROOF STEP]
by (metis (no_types, lifting) conj_comm constr_def lfp_unfold)
[PROOF STATE]
proof (state)
this:
(E (n + 1) \<and> F (E n \<and> \<nu> F)) = (E (n + 1) \<and> \<nu> F)

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E n \<and> \<mu> F) = (E n \<and> \<nu> F); constr F E; Monotonic F\<rbrakk> \<Longrightarrow> (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(E (n + 1) \<and> \<mu> F) = (E (n + 1) \<and> F (E n \<and> \<nu> F))
(E (n + 1) \<and> F (E n \<and> \<nu> F)) = (E (n + 1) \<and> \<nu> F)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(E (n + 1) \<and> \<mu> F) = (E (n + 1) \<and> F (E n \<and> \<nu> F))
(E (n + 1) \<and> F (E n \<and> \<nu> F)) = (E (n + 1) \<and> \<nu> F)

goal (1 subgoal):
 1. (E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(E (Suc n) \<and> \<mu> F) = (E (Suc n) \<and> \<nu> F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(E n \<and> \<mu> F) = (E n \<and> \<nu> F)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>n. (E n \<and> \<mu> F) = (E n \<and> \<nu> F)

goal (1 subgoal):
 1. (\<Or>range E \<and> \<mu> F) = (\<Or>range E \<and> \<nu> F)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>n. (E n \<and> \<mu> F) = (E n \<and> \<nu> F)

goal (1 subgoal):
 1. (\<Or>range E \<and> \<mu> F) = (\<Or>range E \<and> \<nu> F)
[PROOF STEP]
by (auto intro: L274)
[PROOF STATE]
proof (state)
this:
(\<Or>range E \<and> \<mu> F) = (\<Or>range E \<and> \<nu> F)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem constr_fp_uniq:
  assumes "constr F E" "mono F" "\<Sqinter> (range E) = C"
  shows "(C \<and> \<mu> F) = (C \<and> \<nu> F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C \<and> \<mu> F) = (C \<and> \<nu> F)
[PROOF STEP]
using assms(1) assms(2) assms(3) chain_pred_terminates
[PROOF STATE]
proof (prove)
using this:
constr F E
Monotonic F
\<Or>range E = C
\<lbrakk>constr ?F ?E; Monotonic ?F\<rbrakk> \<Longrightarrow> (\<Or>range ?E \<and> \<mu> ?F) = (\<Or>range ?E \<and> \<nu> ?F)

goal (1 subgoal):
 1. (C \<and> \<mu> F) = (C \<and> \<nu> F)
[PROOF STEP]
by blast


[STATEMENT]
lemma  wf_fixp_uinduct_pure_ueq_gen:
  assumes fixp_unfold: "fp B = B (fp B)"
  and              WF: "wf R"
  and     induct_step:
          "\<And>f st. \<lbrakk>\<And>st'. (st',st) \<in> R  \<Longrightarrow> (((Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright>) \<Rightarrow> Post) \<sqsubseteq> f)\<rbrakk>
               \<Longrightarrow> fp B = f \<Longrightarrow>((Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright>) \<Rightarrow> Post) \<sqsubseteq> (B f)"
        shows "((Pre \<Rightarrow> Post) \<sqsubseteq> fp B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
fix st
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
have "((Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright>) \<Rightarrow> Post) \<sqsubseteq> (fp B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
using WF
[PROOF STATE]
proof (prove)
using this:
wf R

goal (1 subgoal):
 1. (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
proof (induction rule: wf_induct_rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>y\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B) \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
case (less x)
[PROOF STATE]
proof (state)
this:
(?y, x) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?y\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>y\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B) \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
hence "(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B (fp B)"
[PROOF STATE]
proof (prove)
using this:
(?y, x) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?y\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B

goal (1 subgoal):
 1. (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B (fp B)
[PROOF STEP]
by (rule induct_step, rel_blast, simp)
[PROOF STATE]
proof (state)
this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B (fp B)

goal (1 subgoal):
 1. \<And>x. (\<And>y. (y, x) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>y\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B) \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B (fp B)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B (fp B)

goal (1 subgoal):
 1. (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
using fixp_unfold
[PROOF STATE]
proof (prove)
using this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B (fp B)
fp B = B (fp B)

goal (1 subgoal):
 1. (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>x\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B

goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?st2\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B

goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?st2\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> fp B

goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> fp B
[PROOF STEP]
by pred_simp
[PROOF STATE]
proof (state)
this:
(Pre \<Rightarrow> Post) \<sqsubseteq> fp B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma refine_usubst_to_ueq:
  "vwb_lens E \<Longrightarrow> (Pre \<Rightarrow> Post)\<lbrakk>\<guillemotleft>st'\<guillemotright>/$E\<rbrakk> \<sqsubseteq> f\<lbrakk>\<guillemotleft>st'\<guillemotright>/$E\<rbrakk> = (((Pre \<and> $E =\<^sub>u \<guillemotleft>st'\<guillemotright>) \<Rightarrow> Post) \<sqsubseteq> f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vwb_lens E \<Longrightarrow> ((Pre \<Rightarrow> Post)\<lbrakk>\<guillemotleft>st'\<guillemotright>/$E\<rbrakk> \<sqsubseteq> f\<lbrakk>\<guillemotleft>st'\<guillemotright>/$E\<rbrakk>) = ((Pre \<and> $E =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f)
[PROOF STEP]
by (rel_auto, metis vwb_lens_wb wb_lens.get_put)


[STATEMENT]
lemma mu_rec_total_pure_rule:
  assumes WF: "wf R"
  and     M: "mono B"
  and     induct_step:
          "\<And> f st.  \<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><,\<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f\<rbrakk>
               \<Longrightarrow> \<mu> B = f \<Longrightarrow>(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> (B f)"
        shows "(Pre \<Rightarrow> Post) \<sqsubseteq> \<mu> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> \<mu> B
[PROOF STEP]
proof (rule wf_fixp_uinduct_pure_ueq_gen[where fp=\<mu> and Pre=Pre and B=B and R=R and e=e])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<mu> B = B (\<mu> B)
 2. wf R
 3. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<mu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "\<mu> B = B (\<mu> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> B = B (\<mu> B)
[PROOF STEP]
by (simp add: M def_gfp_unfold)
[PROOF STATE]
proof (state)
this:
\<mu> B = B (\<mu> B)

goal (2 subgoals):
 1. wf R
 2. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<mu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "wf R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf R
[PROOF STEP]
by (fact WF)
[PROOF STATE]
proof (state)
this:
wf R

goal (1 subgoal):
 1. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<mu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "\<And>f st. (\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f) \<Longrightarrow>
                \<mu> B = f \<Longrightarrow>
                (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<mu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
by (rule induct_step, rel_simp, simp)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>st'. (st', ?st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> ?f; \<mu> B = ?f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B ?f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nu_rec_total_pure_rule:
  assumes WF: "wf R"
  and     M: "mono B"
  and     induct_step:
          "\<And> f st.  \<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><,\<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f\<rbrakk>
               \<Longrightarrow> \<nu> B = f \<Longrightarrow>(Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> (B f)"
        shows "(Pre \<Rightarrow> Post) \<sqsubseteq> \<nu> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> \<nu> B
[PROOF STEP]
proof (rule wf_fixp_uinduct_pure_ueq_gen[where fp=\<nu> and Pre=Pre and B=B and R=R and e=e])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<nu> B = B (\<nu> B)
 2. wf R
 3. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<nu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "\<nu> B = B (\<nu> B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nu> B = B (\<nu> B)
[PROOF STEP]
by (simp add: M def_lfp_unfold)
[PROOF STATE]
proof (state)
this:
\<nu> B = B (\<nu> B)

goal (2 subgoals):
 1. wf R
 2. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<nu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "wf R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf R
[PROOF STEP]
by (fact WF)
[PROOF STATE]
proof (state)
this:
wf R

goal (1 subgoal):
 1. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<nu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "\<And>f st. (\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f) \<Longrightarrow>
                \<nu> B = f \<Longrightarrow>
                (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f st. \<lbrakk>\<And>st'. (st', st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<nu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
by (rule induct_step, rel_simp, simp)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>st'. (st', ?st) \<in> R \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st'\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> ?f; \<nu> B = ?f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B ?f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mu_rec_total_utp_rule:
  assumes WF: "wf R"
    and     M: "mono B"
    and     induct_step:
    "\<And>st. (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> (B ((Pre \<and> (\<lceil>e\<rceil>\<^sub><,\<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post)))"
  shows "(Pre \<Rightarrow> Post) \<sqsubseteq> \<mu> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> \<mu> B
[PROOF STEP]
proof (rule mu_rec_total_pure_rule[where R=R and e=e], simp_all add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f st. \<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<mu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "\<And>f st. (Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f \<Longrightarrow> \<mu> B = f \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f st. \<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<mu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
by (simp add: M induct_step monoD order_subst2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>?st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> ?f; \<mu> B = ?f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B ?f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nu_rec_total_utp_rule:
  assumes WF: "wf R"
    and     M: "mono B"
    and     induct_step:
    "\<And>st. (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> (B ((Pre \<and> (\<lceil>e\<rceil>\<^sub><,\<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post)))"
  shows "(Pre \<Rightarrow> Post) \<sqsubseteq> \<nu> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Pre \<Rightarrow> Post) \<sqsubseteq> \<nu> B
[PROOF STEP]
proof (rule nu_rec_total_pure_rule[where R=R and e=e], simp_all add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f st. \<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<nu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
show "\<And>f st. (Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f \<Longrightarrow> \<nu> B = f \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f st. \<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> f; \<nu> B = f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B f
[PROOF STEP]
by (simp add: M induct_step monoD order_subst2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>(Pre \<and> (\<lceil>e\<rceil>\<^sub><, \<guillemotleft>?st\<guillemotright>)\<^sub>u \<in>\<^sub>u \<guillemotleft>R\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> ?f; \<nu> B = ?f\<rbrakk> \<Longrightarrow> (Pre \<and> \<lceil>e\<rceil>\<^sub>< =\<^sub>u \<guillemotleft>?st\<guillemotright> \<Rightarrow> Post) \<sqsubseteq> B ?f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma div_conv_mult_inverse: "a / b = a \<cdot> (inverse b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a / b = a \<cdot> inverse b
[PROOF STEP]
by simp


[STATEMENT]
lemma diff_self [simp]: "a / a = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a / a = (1::'a)
[PROOF STEP]
using mult.right_inverse
[PROOF STATE]
proof (prove)
using this:
?a \<cdot> inverse ?a = (1::'a)

goal (1 subgoal):
 1. a / a = (1::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma mult_distrib_inverse [simp]: "(a * b) / b = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b / b = a
[PROOF STEP]
by (metis local.mult_1_right local.multi_inverse_conv_div mult.right_inverse mult_assoc)


[STATEMENT]
lemma mult_distrib_inverse' [simp]: "(a * b) / a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cdot> b / a = b
[PROOF STEP]
using local.mult_distrib_inverse mult_commute
[PROOF STATE]
proof (prove)
using this:
?a \<cdot> ?b / ?b = ?a
?a \<cdot> ?b = ?b \<cdot> ?a

goal (1 subgoal):
 1. a \<cdot> b / a = b
[PROOF STEP]
by fastforce


[STATEMENT]
lemma inverse_distrib: "inverse (a * b)  =  (inverse a) * (inverse b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (a \<cdot> b) = inverse a \<cdot> inverse b
[PROOF STEP]
by (simp add: local.mult.inverse_distrib_swap mult_commute)


[STATEMENT]
lemma inverse_divide [simp]: "inverse (a / b) = b / a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse (a / b) = b / a
[PROOF STEP]
by (metis div_conv_mult_inverse inverse_distrib mult.commute mult.inverse_inverse)


[STATEMENT]
lemma inf_wf_to_step_inf_wf:
  assumes "well_founded order"
  shows "inf_wf r order n x \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_wf r order n x \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
proof (induction n arbitrary: x rule: well_founded.induct[OF assms(1)])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>y xa. \<lbrakk>order y x; inf_wf r order y xa\<rbrakk> \<Longrightarrow> \<exists>y m. r xa y \<and> inf_wf r order m y; inf_wf r order x xa\<rbrakk> \<Longrightarrow> \<exists>y m. r xa y \<and> inf_wf r order m y
[PROOF STEP]
case (1 n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>order ?y n; inf_wf r order ?y ?x\<rbrakk> \<Longrightarrow> \<exists>y m. r ?x y \<and> inf_wf r order m y
inf_wf r order n x

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>\<And>y xa. \<lbrakk>order y x; inf_wf r order y xa\<rbrakk> \<Longrightarrow> \<exists>y m. r xa y \<and> inf_wf r order m y; inf_wf r order x xa\<rbrakk> \<Longrightarrow> \<exists>y m. r xa y \<and> inf_wf r order m y
[PROOF STEP]
from "1.prems"(1)
[PROOF STATE]
proof (chain)
picking this:
inf_wf r order n x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inf_wf r order n x

goal (1 subgoal):
 1. \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
proof (induction rule: inf_wf.cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n m x. \<lbrakk>n = m; x = x; order n m; inf_wf r order n x\<rbrakk> \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
 2. \<And>x y n m. \<lbrakk>n = m; x = x; r\<^sup>+\<^sup>+ x y; inf_wf r order n y\<rbrakk> \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
case (inf_wf m n' x')
[PROOF STATE]
proof (state)
this:
n = n'
x = x'
order m n'
inf_wf r order m x'

goal (2 subgoals):
 1. \<And>n m x. \<lbrakk>n = m; x = x; order n m; inf_wf r order n x\<rbrakk> \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
 2. \<And>x y n m. \<lbrakk>n = m; x = x; r\<^sup>+\<^sup>+ x y; inf_wf r order n y\<rbrakk> \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = n'
x = x'
order m n'
inf_wf r order m x'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n = n'
x = x'
order m n'
inf_wf r order m x'

goal (1 subgoal):
 1. \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
using "1.IH"
[PROOF STATE]
proof (prove)
using this:
n = n'
x = x'
order m n'
inf_wf r order m x'
\<lbrakk>order ?y n; inf_wf r order ?y ?x\<rbrakk> \<Longrightarrow> \<exists>y m. r ?x y \<and> inf_wf r order m y

goal (1 subgoal):
 1. \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>y m. r x y \<and> inf_wf r order m y

goal (1 subgoal):
 1. \<And>x y n m. \<lbrakk>n = m; x = x; r\<^sup>+\<^sup>+ x y; inf_wf r order n y\<rbrakk> \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y n m. \<lbrakk>n = m; x = x; r\<^sup>+\<^sup>+ x y; inf_wf r order n y\<rbrakk> \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
case (inf_wf_step x' y m n')
[PROOF STATE]
proof (state)
this:
n = n'
x = x'
r\<^sup>+\<^sup>+ x' y
inf_wf r order m y

goal (1 subgoal):
 1. \<And>x y n m. \<lbrakk>n = m; x = x; r\<^sup>+\<^sup>+ x y; inf_wf r order n y\<rbrakk> \<Longrightarrow> \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = n'
x = x'
r\<^sup>+\<^sup>+ x' y
inf_wf r order m y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n = n'
x = x'
r\<^sup>+\<^sup>+ x' y
inf_wf r order m y

goal (1 subgoal):
 1. \<exists>y m. r x y \<and> inf_wf r order m y
[PROOF STEP]
by (metis converse_tranclpE inf_wf.inf_wf_step)
[PROOF STATE]
proof (state)
this:
\<exists>y m. r x y \<and> inf_wf r order m y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>y m. r x y \<and> inf_wf r order m y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_wf_to_inf:
  assumes "well_founded order"
  shows "inf_wf r order n x \<Longrightarrow> inf r x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_wf r order n x \<Longrightarrow> Inf.inf r x
[PROOF STEP]
proof (coinduction arbitrary: x n rule: inf.coinduct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa n. inf_wf r order n xa \<Longrightarrow> \<exists>x y. xa = x \<and> r x y \<and> ((\<exists>x n. y = x \<and> inf_wf r order n x) \<or> Inf.inf r y)
[PROOF STEP]
case (inf x n)
[PROOF STATE]
proof (state)
this:
inf_wf r order n x

goal (1 subgoal):
 1. \<And>xa n. inf_wf r order n xa \<Longrightarrow> \<exists>x y. xa = x \<and> r x y \<and> ((\<exists>x n. y = x \<and> inf_wf r order n x) \<or> Inf.inf r y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inf_wf r order n x
[PROOF STEP]
obtain y m where "r x y" and "inf_wf r order m y"
[PROOF STATE]
proof (prove)
using this:
inf_wf r order n x

goal (1 subgoal):
 1. (\<And>y m. \<lbrakk>r x y; inf_wf r order m y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_wf_to_step_inf_wf[OF assms(1) inf(1)]
[PROOF STATE]
proof (prove)
using this:
inf_wf r order n x
\<exists>y m. r x y \<and> inf_wf r order m y

goal (1 subgoal):
 1. (\<And>y m. \<lbrakk>r x y; inf_wf r order m y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
r x y
inf_wf r order m y

goal (1 subgoal):
 1. \<And>xa n. inf_wf r order n xa \<Longrightarrow> \<exists>x y. xa = x \<and> r x y \<and> ((\<exists>x n. y = x \<and> inf_wf r order n x) \<or> Inf.inf r y)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
r x y
inf_wf r order m y

goal (1 subgoal):
 1. \<exists>x y. x = x \<and> r x y \<and> ((\<exists>x n. y = x \<and> inf_wf r order n x) \<or> Inf.inf r y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x y. x = x \<and> r x y \<and> ((\<exists>x n. y = x \<and> inf_wf r order n x) \<or> Inf.inf r y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma step_inf:
  assumes "right_unique r"
  shows "r x y \<Longrightarrow> inf r x \<Longrightarrow> inf r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r x y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r y
[PROOF STEP]
using right_uniqueD[OF \<open>right_unique r\<close>]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>r ?x ?y; r ?x ?z\<rbrakk> \<Longrightarrow> ?y = ?z

goal (1 subgoal):
 1. \<lbrakk>r x y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r y
[PROOF STEP]
by (metis inf.cases)


[STATEMENT]
lemma star_inf:
  assumes "right_unique r"
  shows "r\<^sup>*\<^sup>* x y \<Longrightarrow> inf r x \<Longrightarrow> inf r y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r\<^sup>*\<^sup>* x y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r y
[PROOF STEP]
proof (induction y rule: rtranclp_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Inf.inf r x \<Longrightarrow> Inf.inf r x
 2. \<And>y z. \<lbrakk>r\<^sup>*\<^sup>* x y; r y z; Inf.inf r x \<Longrightarrow> Inf.inf r y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r z
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:
Inf.inf r x

goal (2 subgoals):
 1. Inf.inf r x \<Longrightarrow> Inf.inf r x
 2. \<And>y z. \<lbrakk>r\<^sup>*\<^sup>* x y; r y z; Inf.inf r x \<Longrightarrow> Inf.inf r y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Inf.inf r x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Inf.inf r x

goal (1 subgoal):
 1. Inf.inf r x
[PROOF STEP]
by assumption
[PROOF STATE]
proof (state)
this:
Inf.inf r x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>r\<^sup>*\<^sup>* x y; r y z; Inf.inf r x \<Longrightarrow> Inf.inf r y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>r\<^sup>*\<^sup>* x y; r y z; Inf.inf r x \<Longrightarrow> Inf.inf r y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r z
[PROOF STEP]
case (step y z)
[PROOF STATE]
proof (state)
this:
r\<^sup>*\<^sup>* x y
r y z
Inf.inf r x \<Longrightarrow> Inf.inf r y
Inf.inf r x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>r\<^sup>*\<^sup>* x y; r y z; Inf.inf r x \<Longrightarrow> Inf.inf r y; Inf.inf r x\<rbrakk> \<Longrightarrow> Inf.inf r z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r\<^sup>*\<^sup>* x y
r y z
Inf.inf r x \<Longrightarrow> Inf.inf r y
Inf.inf r x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
r\<^sup>*\<^sup>* x y
r y z
Inf.inf r x \<Longrightarrow> Inf.inf r y
Inf.inf r x

goal (1 subgoal):
 1. Inf.inf r z
[PROOF STEP]
using step_inf[OF \<open>right_unique r\<close>]
[PROOF STATE]
proof (prove)
using this:
r\<^sup>*\<^sup>* x y
r y z
Inf.inf r x \<Longrightarrow> Inf.inf r y
Inf.inf r x
\<lbrakk>r ?x ?y; Inf.inf r ?x\<rbrakk> \<Longrightarrow> Inf.inf r ?y

goal (1 subgoal):
 1. Inf.inf r z
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Inf.inf r z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma selectlenhelp: "length (selecthelp l i) = (i + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (selecthelp l i) = i + 1
[PROOF STEP]
proof (induct i arbitrary: l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l. length (selecthelp l 0) = 0 + 1
 2. \<And>i l. (\<And>l. length (selecthelp l i) = i + 1) \<Longrightarrow> length (selecthelp l (Suc i)) = Suc i + 1
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>l. length (selecthelp l 0) = 0 + 1
 2. \<And>i l. (\<And>l. length (selecthelp l i) = i + 1) \<Longrightarrow> length (selecthelp l (Suc i)) = Suc i + 1
[PROOF STEP]
show "length (selecthelp l 0) = 0 + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (selecthelp l 0) = 0 + 1
[PROOF STEP]
proof (cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> length (selecthelp l 0) = 0 + 1
 2. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l 0) = 0 + 1
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> length (selecthelp l 0) = 0 + 1
 2. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l 0) = 0 + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
have "selecthelp l 0 = [Zero]"
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. selecthelp l 0 = [\<zero>]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
selecthelp l 0 = [\<zero>]

goal (2 subgoals):
 1. l = [] \<Longrightarrow> length (selecthelp l 0) = 0 + 1
 2. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l 0) = 0 + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
selecthelp l 0 = [\<zero>]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
selecthelp l 0 = [\<zero>]

goal (1 subgoal):
 1. length (selecthelp l 0) = 0 + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (selecthelp l 0) = 0 + 1

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l 0) = 0 + 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l 0) = 0 + 1
[PROOF STEP]
case (Cons a as)
[PROOF STATE]
proof (state)
this:
l = a # as

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l 0) = 0 + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = a # as
[PROOF STEP]
have "selecthelp l 0 = [a]"
[PROOF STATE]
proof (prove)
using this:
l = a # as

goal (1 subgoal):
 1. selecthelp l 0 = [a]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
selecthelp l 0 = [a]

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l 0) = 0 + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
selecthelp l 0 = [a]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
selecthelp l 0 = [a]

goal (1 subgoal):
 1. length (selecthelp l 0) = 0 + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (selecthelp l 0) = 0 + 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (selecthelp l 0) = 0 + 1

goal (1 subgoal):
 1. \<And>i l. (\<And>l. length (selecthelp l i) = i + 1) \<Longrightarrow> length (selecthelp l (Suc i)) = Suc i + 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i l. (\<And>l. length (selecthelp l i) = i + 1) \<Longrightarrow> length (selecthelp l (Suc i)) = Suc i + 1
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
length (selecthelp ?l x) = x + 1

goal (1 subgoal):
 1. \<And>i l. (\<And>l. length (selecthelp l i) = i + 1) \<Longrightarrow> length (selecthelp l (Suc i)) = Suc i + 1
[PROOF STEP]
show "length (selecthelp l (Suc x)) = (Suc x) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
proof (cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
 2. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
 2. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
have "selecthelp l (Suc x) = Zero # selecthelp l x"
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. selecthelp l (Suc x) = \<zero> # selecthelp l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
selecthelp l (Suc x) = \<zero> # selecthelp l x

goal (2 subgoals):
 1. l = [] \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
 2. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
selecthelp l (Suc x) = \<zero> # selecthelp l x
[PROOF STEP]
show "length (selecthelp l (Suc x)) = Suc x + 1"
[PROOF STATE]
proof (prove)
using this:
selecthelp l (Suc x) = \<zero> # selecthelp l x

goal (1 subgoal):
 1. length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
selecthelp l (Suc x) = \<zero> # selecthelp l x
length (selecthelp ?l x) = x + 1

goal (1 subgoal):
 1. length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (selecthelp l (Suc x)) = Suc x + 1

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
case (Cons a b)
[PROOF STATE]
proof (state)
this:
l = a # b

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = a # b
[PROOF STEP]
have "selecthelp l (Suc x) = a # selecthelp b x"
[PROOF STATE]
proof (prove)
using this:
l = a # b

goal (1 subgoal):
 1. selecthelp l (Suc x) = a # selecthelp b x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
selecthelp l (Suc x) = a # selecthelp b x

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
selecthelp l (Suc x) = a # selecthelp b x
[PROOF STEP]
have "length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)"
[PROOF STATE]
proof (prove)
using this:
selecthelp l (Suc x) = a # selecthelp b x

goal (1 subgoal):
 1. length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)
[PROOF STEP]
show "length (selecthelp l (Suc x)) = Suc x + 1"
[PROOF STATE]
proof (prove)
using this:
length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)

goal (1 subgoal):
 1. length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
length (selecthelp l (Suc x)) = 1 + length (selecthelp b x)
length (selecthelp ?l x) = x + 1

goal (1 subgoal):
 1. length (selecthelp l (Suc x)) = Suc x + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (selecthelp l (Suc x)) = Suc x + 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
length (selecthelp l (Suc x)) = Suc x + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma selectlenhelp2:  "\<And>i. \<forall>l j. \<exists>k. select l i j = select k 0 (j - i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<forall>l j. \<exists>k. select l i j = select k 0 (j - i)
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i l j. \<exists>k. select l i j = select k 0 (j - i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i l j. \<exists>k. select l i j = select k 0 (j - i)
[PROOF STEP]
show "\<And>l j. \<exists>k. select l i j = select k 0 (j - i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l j. \<exists>k. select l i j = select k 0 (j - i)
[PROOF STEP]
proof (induct i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l j. \<exists>k. select l 0 j = select k 0 (j - 0)
 2. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
fix l and j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>l j. \<exists>k. select l 0 j = select k 0 (j - 0)
 2. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
have "select l 0 j = select l 0 (j-(0::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select l 0 j = select l 0 (j - 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select l 0 j = select l 0 (j - 0)

goal (2 subgoals):
 1. \<And>l j. \<exists>k. select l 0 j = select k 0 (j - 0)
 2. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
select l 0 j = select l 0 (j - 0)
[PROOF STEP]
show "\<exists>k. select l 0 j = select k 0 (j - (0::nat))"
[PROOF STATE]
proof (prove)
using this:
select l 0 j = select l 0 (j - 0)

goal (1 subgoal):
 1. \<exists>k. select l 0 j = select k 0 (j - 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. select l 0 j = select k 0 (j - 0)

goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
case (Suc x)
[PROOF STATE]
proof (state)
this:
\<exists>k. select ?l x ?j = select k 0 (?j - x)

goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
have b: "select l (Suc x) j = select (tl l) x (j-(1::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
proof (cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
 2. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
 2. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
have "select l (Suc x) j = select l x (j-(1::nat))"
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. select l (Suc x) j = select l x (j - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select l (Suc x) j = select l x (j - 1)

goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
 2. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
select l (Suc x) j = select l x (j - 1)

goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
 2. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
have "tl l = l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl l = l
[PROOF STEP]
using Nil
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. tl l = l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tl l = l

goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
 2. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
select l (Suc x) j = select l x (j - 1)
tl l = l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
select l (Suc x) j = select l x (j - 1)
tl l = l

goal (1 subgoal):
 1. select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
by (simp)
[PROOF STATE]
proof (state)
this:
select l (Suc x) j = select (tl l) x (j - 1)

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
case (Cons head tail)
[PROOF STATE]
proof (state)
this:
l = head # tail

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = head # tail
[PROOF STEP]
have "select l (Suc x) j = select tail x (j-(1::nat))"
[PROOF STATE]
proof (prove)
using this:
l = head # tail

goal (1 subgoal):
 1. select l (Suc x) j = select tail x (j - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select l (Suc x) j = select tail x (j - 1)

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
select l (Suc x) j = select tail x (j - 1)

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
have "tail = tl l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tail = tl l
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
l = head # tail

goal (1 subgoal):
 1. tail = tl l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
tail = tl l

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
select l (Suc x) j = select tail x (j - 1)
tail = tl l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
select l (Suc x) j = select tail x (j - 1)
tail = tl l

goal (1 subgoal):
 1. select l (Suc x) j = select (tl l) x (j - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select l (Suc x) j = select (tl l) x (j - 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
select l (Suc x) j = select (tl l) x (j - 1)

goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
have "\<exists>k. select l x j = select k 0 (j - (x::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. select l x j = select k 0 (j - x)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<exists>k. select ?l x ?j = select k 0 (?j - x)

goal (1 subgoal):
 1. \<exists>k. select l x j = select k 0 (j - x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k. select l x j = select k 0 (j - x)

goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<exists>k. select l x j = select k 0 (j - x)

goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
have  "\<exists>k. select (tl l) x (j-(1::nat)) = select k 0 (j-(1::nat)-(x::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. select (tl l) x (j - 1) = select k 0 (j - 1 - x)
[PROOF STEP]
using Suc[of "tl l" "j-(1::nat)"]
[PROOF STATE]
proof (prove)
using this:
\<exists>k. select (tl l) x (j - 1) = select k 0 (j - 1 - x)

goal (1 subgoal):
 1. \<exists>k. select (tl l) x (j - 1) = select k 0 (j - 1 - x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. select (tl l) x (j - 1) = select k 0 (j - 1 - x)

goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. select l x j = select k 0 (j - x)
\<exists>k. select (tl l) x (j - 1) = select k 0 (j - 1 - x)
[PROOF STEP]
have "\<exists>k. select l (Suc x) j = select k 0 (j-(1::nat) - (x::nat))"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. select l x j = select k 0 (j - x)
\<exists>k. select (tl l) x (j - 1) = select k 0 (j - 1 - x)

goal (1 subgoal):
 1. \<exists>k. select l (Suc x) j = select k 0 (j - 1 - x)
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
\<exists>k. select l x j = select k 0 (j - x)
\<exists>k. select (tl l) x (j - 1) = select k 0 (j - 1 - x)
select l (Suc x) j = select (tl l) x (j - 1)

goal (1 subgoal):
 1. \<exists>k. select l (Suc x) j = select k 0 (j - 1 - x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. select l (Suc x) j = select k 0 (j - 1 - x)

goal (1 subgoal):
 1. \<And>i l j. (\<And>l j. \<exists>k. select l i j = select k 0 (j - i)) \<Longrightarrow> \<exists>k. select l (Suc i) j = select k 0 (j - Suc i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. select l (Suc x) j = select k 0 (j - 1 - x)
[PROOF STEP]
show "\<exists>k. select l (Suc x) j = select k 0 (j - Suc x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. select l (Suc x) j = select k 0 (j - 1 - x)

goal (1 subgoal):
 1. \<exists>k. select l (Suc x) j = select k 0 (j - Suc x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k. select l (Suc x) j = select k 0 (j - Suc x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. select ?l i ?j = select k 0 (?j - i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma selectlenhelp3: "\<forall>j. select l 0 j = selecthelp l j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. select l 0 j = selecthelp l j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. select l 0 j = selecthelp l j
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. select l 0 j = selecthelp l j
[PROOF STEP]
show "select l 0 j = selecthelp l j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. select l 0 j = selecthelp l j
[PROOF STEP]
proof (cases l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l 0 j = selecthelp l j
 2. \<And>a list. l = a # list \<Longrightarrow> select l 0 j = selecthelp l j
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l 0 j = selecthelp l j
 2. \<And>a list. l = a # list \<Longrightarrow> select l 0 j = selecthelp l j
[PROOF STEP]
assume "l=[]"
[PROOF STATE]
proof (state)
this:
l = []

goal (2 subgoals):
 1. l = [] \<Longrightarrow> select l 0 j = selecthelp l j
 2. \<And>a list. l = a # list \<Longrightarrow> select l 0 j = selecthelp l j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = []
[PROOF STEP]
show "select l 0 j = selecthelp l j"
[PROOF STATE]
proof (prove)
using this:
l = []

goal (1 subgoal):
 1. select l 0 j = selecthelp l j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select l 0 j = selecthelp l j

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l 0 j = selecthelp l j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l 0 j = selecthelp l j
[PROOF STEP]
case (Cons a b)
[PROOF STATE]
proof (state)
this:
l = a # b

goal (1 subgoal):
 1. \<And>a list. l = a # list \<Longrightarrow> select l 0 j = selecthelp l j
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = a # b
[PROOF STEP]
show "select l 0 j = selecthelp l j"
[PROOF STATE]
proof (prove)
using this:
l = a # b

goal (1 subgoal):
 1. select l 0 j = selecthelp l j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
select l 0 j = selecthelp l j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
select l 0 j = selecthelp l j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma selectlen: "length (select l i j) = j - i + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
from selectlenhelp2
[PROOF STATE]
proof (chain)
picking this:
\<forall>l j. \<exists>k. select l ?i j = select k 0 (j - ?i)
[PROOF STEP]
have "\<exists>k. select l i j = select k 0 (j-i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>l j. \<exists>k. select l ?i j = select k 0 (j - ?i)

goal (1 subgoal):
 1. \<exists>k. select l i j = select k 0 (j - i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k. select l i j = select k 0 (j - i)

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. select l i j = select k 0 (j - i)
[PROOF STEP]
have "\<exists>k. length (select l i j) = length (select k 0 (j-i))"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. select l i j = select k 0 (j - i)

goal (1 subgoal):
 1. \<exists>k. length (select l i j) = length (select k 0 (j - i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>k. length (select l i j) = length (select k 0 (j - i))

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. length (select l i j) = length (select k 0 (j - i))
[PROOF STEP]
have c: "\<exists>k. length (select l i j) = length (selecthelp k (j-i))"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. length (select l i j) = length (select k 0 (j - i))

goal (1 subgoal):
 1. \<exists>k. length (select l i j) = length (selecthelp k (j - i))
[PROOF STEP]
using selectlenhelp3
[PROOF STATE]
proof (prove)
using this:
\<exists>k. length (select l i j) = length (select k 0 (j - i))
\<forall>j. select ?l 0 j = selecthelp ?l j

goal (1 subgoal):
 1. \<exists>k. length (select l i j) = length (selecthelp k (j - i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>k. length (select l i j) = length (selecthelp k (j - i))

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
\<exists>k. length (select l i j) = length (selecthelp k (j - i))
[PROOF STEP]
obtain k where d: "length (select l i j) = length (selecthelp k (j-i))"
[PROOF STATE]
proof (prove)
using this:
\<exists>k. length (select l i j) = length (selecthelp k (j - i))

goal (1 subgoal):
 1. (\<And>k. length (select l i j) = length (selecthelp k (j - i)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (select l i j) = length (selecthelp k (j - i))

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
have "0<=j-i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> j - i
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
0 \<le> j - i

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 \<le> j - i
[PROOF STEP]
have "length (selecthelp k (j-i)) = j-i+1"
[PROOF STATE]
proof (prove)
using this:
0 \<le> j - i

goal (1 subgoal):
 1. length (selecthelp k (j - i)) = j - i + 1
[PROOF STEP]
using selectlenhelp
[PROOF STATE]
proof (prove)
using this:
0 \<le> j - i
length (selecthelp ?l ?i) = ?i + 1

goal (1 subgoal):
 1. length (selecthelp k (j - i)) = j - i + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (selecthelp k (j - i)) = j - i + 1

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (selecthelp k (j - i)) = j - i + 1
[PROOF STEP]
show "length (select l i j) = j-i+1"
[PROOF STATE]
proof (prove)
using this:
length (selecthelp k (j - i)) = j - i + 1

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
using d
[PROOF STATE]
proof (prove)
using this:
length (selecthelp k (j - i)) = j - i + 1
length (select l i j) = length (selecthelp k (j - i))

goal (1 subgoal):
 1. length (select l i j) = j - i + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (select l i j) = j - i + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma addmod32len: "\<And> a b. length (addmod32 a b) = 32"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. length (addmod32 a b) = 32
[PROOF STEP]
using selectlen [of _ 0 31] addmod32
[PROOF STATE]
proof (prove)
using this:
length (select ?l 0 31) = 31 - 0 + 1
addmod32 ?a ?b = rev (select (rev (nat_to_bv (bv_to_nat ?a + bv_to_nat ?b))) 0 31)

goal (1 subgoal):
 1. \<And>a b. length (addmod32 a b) = 32
[PROOF STEP]
by simp


[STATEMENT]
lemma equiv_out_refl: "equiv_out a a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equiv_out a a
[PROOF STEP]
using equiv_class_eq_iff equiv_out_equiv
[PROOF STATE]
proof (prove)
using this:
equiv ?A ?r \<Longrightarrow> ((?x, ?y) \<in> ?r) = (?r `` {?x} = ?r `` {?y} \<and> ?x \<in> ?A \<and> ?y \<in> ?A)
equiv UNIV {(x, y). equiv_out x y}

goal (1 subgoal):
 1. equiv_out a a
[PROOF STEP]
by fastforce


[STATEMENT]
lemma equiv_out_trans: "\<lbrakk> equiv_out a b; equiv_out b c \<rbrakk> \<Longrightarrow> equiv_out a c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_out a b; equiv_out b c\<rbrakk> \<Longrightarrow> equiv_out a c
[PROOF STEP]
using equiv_class_eq_iff equiv_out_equiv
[PROOF STATE]
proof (prove)
using this:
equiv ?A ?r \<Longrightarrow> ((?x, ?y) \<in> ?r) = (?r `` {?x} = ?r `` {?y} \<and> ?x \<in> ?A \<and> ?y \<in> ?A)
equiv UNIV {(x, y). equiv_out x y}

goal (1 subgoal):
 1. \<lbrakk>equiv_out a b; equiv_out b c\<rbrakk> \<Longrightarrow> equiv_out a c
[PROOF STEP]
by fastforce