[STATEMENT]
lemma reachable_constraints_fv_bvars_disj:
  fixes \::"('fun,'atom,'sets,'lbl) prot_constr"
  assumes \_reach: "\ \<in> reachable_constraints P"
    and P: "\<forall>S \<in> set P. admissible_transaction S"
  shows "fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
let ?X = "\<Union>T \<in> set P. bvars_transaction T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
note 0 = admissible_transactions_fv_bvars_disj[OF P]
[PROOF STATE]
proof (state)
this:
\<Union> (fv_transaction ` set P) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
have 1: "bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
using \_reach
[PROOF STATE]
proof (prove)
using this:
\ \<in> reachable_constraints P

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
proof (induction \ rule: reachable_constraints.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
case (step \ T \<xi> \<sigma> \<alpha>)
[PROOF STATE]
proof (state)
this:
\ \<in> reachable_constraints P
T \<in> set P
transaction_decl_subst \<xi> T
transaction_fresh_subst \<sigma> T \
transaction_renaming_subst \<alpha> P \
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P)

goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
have "bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T
[PROOF STEP]
using bvars\<^sub>s\<^sub>s\<^sub>t_subst[of "unlabel (transaction_strand T)" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            bvars\<^sub>s\<^sub>s\<^sub>t_unlabel_dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_eq[of "transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            unlabel_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>s\<^sub>s\<^sub>t (unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) = bvars_transaction T
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) = dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T) \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>
unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha> = unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T
[PROOF STEP]
by argo
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T

goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
hence "bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> ?X"
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
using step.hyps(2)
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = bvars_transaction T
T \<in> set P

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)

goal (2 subgoals):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P); T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
using step.IH bvars\<^sub>s\<^sub>s\<^sub>t_append
[PROOF STATE]
proof (prove)
using this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P)
bvars\<^sub>s\<^sub>s\<^sub>t (?A @ ?B) = bvars\<^sub>s\<^sub>s\<^sub>t ?A \<union> bvars\<^sub>s\<^sub>s\<^sub>t ?B

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<subseteq> \<Union> (bvars_transaction ` set P)

goal (1 subgoal):
 1. bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<subseteq> \<Union> (bvars_transaction ` set P)
[PROOF STEP]
qed (simp add: unlabel_def)
[PROOF STATE]
proof (state)
this:
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P)

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
have 2: "fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> ?X = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
using \_reach
[PROOF STATE]
proof (prove)
using this:
\ \<in> reachable_constraints P

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
proof (induction \ rule: reachable_constraints.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
case (step \ T \<xi> \<sigma> \<alpha>)
[PROOF STATE]
proof (state)
this:
\ \<in> reachable_constraints P
T \<in> set P
transaction_decl_subst \<xi> T
transaction_fresh_subst \<sigma> T \
transaction_renaming_subst \<alpha> P \
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
have "x \<noteq> y" when x: "x \<in> ?X" and y: "y \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
obtain y' where y': "y' \<in> fv_transaction T" "y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>y' \<in> fv_transaction T; y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using y unlabel_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
[PROOF STATE]
proof (prove)
using this:
y \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha> = unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>y' \<in> fv_transaction T; y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis fv\<^sub>s\<^sub>s\<^sub>t_subst_obtain_var)
[PROOF STATE]
proof (state)
this:
y' \<in> fv_transaction T
y \<in> fv ((\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y')

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
have "y \<notin> \<Union>(vars_transaction ` set P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> \<Union> (vars_transaction ` set P)
[PROOF STEP]
using transaction_decl_fresh_renaming_substs_range''[OF step.hyps(3-5) y'(2)]
              transaction_renaming_subst_range_notin_vars[OF step.hyps(5), of y']
[PROOF STATE]
proof (prove)
using this:
\<xi> y' = Var y'
\<sigma> y' = Var y'
\<alpha> y' = Var y
(\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) y' = Var y
\<exists>y. \<alpha> y' = Var y \<and> y \<notin> \<Union> (vars_transaction ` set P) \<union> vars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \

goal (1 subgoal):
 1. y \<notin> \<Union> (vars_transaction ` set P)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<notin> \<Union> (vars_transaction ` set P)

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<notin> \<Union> (vars_transaction ` set P)

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using x vars\<^sub>s\<^sub>s\<^sub>t_is_fv\<^sub>s\<^sub>s\<^sub>t_bvars\<^sub>s\<^sub>s\<^sub>t
[PROOF STATE]
proof (prove)
using this:
y \<notin> \<Union> (vars_transaction ` set P)
x \<in> \<Union> (bvars_transaction ` set P)
vars\<^sub>s\<^sub>s\<^sub>t ?S = fv\<^sub>s\<^sub>s\<^sub>t ?S \<union> bvars\<^sub>s\<^sub>s\<^sub>t ?S

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x24 \<in> \<Union> (bvars_transaction ` set P); ?y24 \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)\<rbrakk> \<Longrightarrow> ?x24 \<noteq> ?y24

goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
hence "fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> ?X = {}"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x24 \<in> \<Union> (bvars_transaction ` set P); ?y24 \<in> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)\<rbrakk> \<Longrightarrow> ?x24 \<noteq> ?y24

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (2 subgoals):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
 2. \<And>\ T \<xi> \<sigma> \<alpha>. \<lbrakk>\ \<in> reachable_constraints P; fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}; T \<in> set P; transaction_decl_subst \<xi> T; transaction_fresh_subst \<sigma> T \; transaction_renaming_subst \<alpha> P \\<rbrakk> \<Longrightarrow> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
using step.IH
            fv\<^sub>s\<^sub>s\<^sub>t_unlabel_dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_eq[of "transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            unlabel_subst[of "transaction_strand T" "\<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>"]
            fv\<^sub>s\<^sub>s\<^sub>t_append[of "unlabel \" "unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)"]
            unlabel_append[of \ "transaction_strand T"]
[PROOF STATE]
proof (prove)
using this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) \<inter> \<Union> (bvars_transaction ` set P) = {}
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>) = dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T) \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>
unlabel (transaction_strand T) \<cdot>\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha> = unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
fv\<^sub>s\<^sub>s\<^sub>t (unlabel \ @ unlabel (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) = fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<union> fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)
unlabel (\ @ transaction_strand T) = unlabel \ @ unlabel (transaction_strand T)

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t (\ @ dual\<^sub>l\<^sub>s\<^sub>s\<^sub>t (transaction_strand T \<cdot>\<^sub>l\<^sub>s\<^sub>s\<^sub>t \<xi> \<circ>\<^sub>s \<sigma> \<circ>\<^sub>s \<alpha>)) \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t [] \<inter> \<Union> (bvars_transaction ` set P) = {}
[PROOF STEP]
qed (simp add: unlabel_def)
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
using 0 1 2
[PROOF STATE]
proof (prove)
using this:
\<Union> (fv_transaction ` set P) \<inter> \<Union> (bvars_transaction ` set P) = {}
bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<subseteq> \<Union> (bvars_transaction ` set P)
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> \<Union> (bvars_transaction ` set P) = {}

goal (1 subgoal):
 1. fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fv\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ \<inter> bvars\<^sub>l\<^sub>s\<^sub>s\<^sub>t \ = {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem completenessForUNSAT:
  fixes F0 :: Formula and decisionVars :: "Variable set" and state0 :: State and state :: State
  assumes
  "vars F0 \<subseteq> decisionVars" and

  "\<not> satisfiable F0" and

  "isInitialState state0 F0" and
  "(state0, state) \<in> transitionRelation F0 decisionVars" and
  "isFinalState state F0 decisionVars"

  shows
  "getConflictFlag state = True \<and> getC state = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
(************************************************************************)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
[PROOF STEP]
have *: "(getConflictFlag state = False \<and>
               \<not>formulaFalse (getF state) (elements (getM state)) \<and>
               vars (elements (getM state)) \<supseteq> decisionVars) \<or>
           (getConflictFlag state = True \<and>
               getC state = [])"
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars

goal (1 subgoal):
 1. getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
using finalStateCharacterization[of "state0" "F0" "state" "decisionVars"]
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
\<lbrakk>isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; isFinalState state F0 decisionVars\<rbrakk> \<Longrightarrow> getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []

goal (1 subgoal):
 1. getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
assume "\<not> getConflictFlag state = True"
[PROOF STATE]
proof (state)
this:
getConflictFlag state \<noteq> True

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True
[PROOF STEP]
have "getConflictFlag state = False \<and> \<not>formulaFalse (getF state) (elements (getM state)) \<and> vars (elements (getM state)) \<supseteq> decisionVars"
[PROOF STATE]
proof (prove)
using this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True

goal (1 subgoal):
 1. getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
[PROOF STEP]
have "satisfiable F0"
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))

goal (1 subgoal):
 1. satisfiable F0
[PROOF STEP]
using soundnessForSAT[of "F0" "decisionVars" "state0" "state"]
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<not> satisfiable F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
\<lbrakk>vars F0 \<subseteq> decisionVars; isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; getConflictFlag state = False; \<not> formulaFalse (getF state) (elements (getM state)); decisionVars \<subseteq> vars (elements (getM state))\<rbrakk> \<Longrightarrow> model (elements (getM state)) F0

goal (1 subgoal):
 1. satisfiable F0
[PROOF STEP]
unfolding satisfiable_def
[PROOF STATE]
proof (prove)
using this:
vars F0 \<subseteq> decisionVars
\<nexists>valuation. model valuation F0
isInitialState state0 F0
(state0, state) \<in> transitionRelation F0 decisionVars
isFinalState state F0 decisionVars
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state))
\<lbrakk>vars F0 \<subseteq> decisionVars; isInitialState state0 F0; (state0, state) \<in> transitionRelation F0 decisionVars; getConflictFlag state = False; \<not> formulaFalse (getF state) (elements (getM state)); decisionVars \<subseteq> vars (elements (getM state))\<rbrakk> \<Longrightarrow> model (elements (getM state)) F0

goal (1 subgoal):
 1. \<exists>valuation. model valuation F0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
satisfiable F0

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with \<open>\<not> satisfiable F0\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> satisfiable F0
satisfiable F0
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
\<not> satisfiable F0
satisfiable F0

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

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
getConflictFlag state \<noteq> True \<Longrightarrow> False

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
getConflictFlag state = False \<and> \<not> formulaFalse (getF state) (elements (getM state)) \<and> decisionVars \<subseteq> vars (elements (getM state)) \<or> getConflictFlag state = True \<and> getC state = []
getConflictFlag state \<noteq> True \<Longrightarrow> False

goal (1 subgoal):
 1. getConflictFlag state = True \<and> getC state = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
getConflictFlag state = True \<and> getC state = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma shift_inj[simp]:
"shift cl n I1 = shift cl n I2 \<longleftrightarrow> I1 = I2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (local.shift cl n I1 = local.shift cl n I2) = (I1 = I2)
[PROOF STEP]
unfolding shift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((+) (brnL cl n) ` I1 = (+) (brnL cl n) ` I2) = (I1 = I2)
[PROOF STEP]
by force


[STATEMENT]
lemma emp_UNlift01_UNpart1:
assumes l: "length cl = length dl"
and P: "\<And> n. n < length cl \<Longrightarrow> part {..< brn (cl!n)} (P n) \<and> {} \<notin> P n"
and FP: "\<And> n. n < length dl \<Longrightarrow> {} \<notin> F n ` (P n)"
shows "{} \<notin> (UNlift01 cl dl P F) ` (UNpart1 cl dl P)" (is "{} \<notin> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
have R: "?R = UNpart1 dl cl (%n. F n ` (P n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNlift01 cl dl P F ` UNpart1 cl dl P = UNpart1 dl cl (\<lambda>n. F n ` P n)
[PROOF STEP]
apply(rule UNlift01_UNpart1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length cl = length dl
 2. \<And>n. n < length cl \<Longrightarrow> part {..<brn (cl ! n)} (P n) \<and> {} \<notin> P n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length cl = length dl
?n5 < length cl \<Longrightarrow> part {..<brn (cl ! ?n5)} (P ?n5) \<and> {} \<notin> P ?n5
?n5 < length dl \<Longrightarrow> {} \<notin> F ?n5 ` P ?n5

goal (2 subgoals):
 1. length cl = length dl
 2. \<And>n. n < length cl \<Longrightarrow> part {..<brn (cl ! n)} (P n) \<and> {} \<notin> P n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UNlift01 cl dl P F ` UNpart1 cl dl P = UNpart1 dl cl (\<lambda>n. F n ` P n)

goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P
[PROOF STEP]
unfolding R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<notin> UNpart1 dl cl (\<lambda>n. F n ` P n)
[PROOF STEP]
apply(rule emp_UNpart1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length dl \<Longrightarrow> {} \<notin> F n ` P n
[PROOF STEP]
using FP
[PROOF STATE]
proof (prove)
using this:
?n5 < length dl \<Longrightarrow> {} \<notin> F ?n5 ` P ?n5

goal (1 subgoal):
 1. \<And>n. n < length dl \<Longrightarrow> {} \<notin> F n ` P n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{} \<notin> UNlift01 cl dl P F ` UNpart1 cl dl P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eint_add_left_cancel_le: "a + b \<le> a + c \<longleftrightarrow> a = (\<infinity>::eint) \<or> b \<le> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a + b \<le> a + c) = (a = \<infinity> \<or> b \<le> c)
[PROOF STEP]
unfolding plus_eint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case a of eint m \<Rightarrow> case b of eint n \<Rightarrow> eint (m + n) | \<infinity> \<Rightarrow> \<infinity> | \<infinity> \<Rightarrow> \<infinity>) \<le> (case a of eint m \<Rightarrow> case c of eint n \<Rightarrow> eint (m + n) | \<infinity> \<Rightarrow> \<infinity> | \<infinity> \<Rightarrow> \<infinity>)) = (a = \<infinity> \<or> b \<le> c)
[PROOF STEP]
by (simp split: eint.split)


[STATEMENT]
lemma eint_min_ineq:
  assumes "(b::eint) \<ge> min c d"
  assumes "c > e"
  assumes "d > e"
  shows "b > e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. e < b
[PROOF STEP]
by (meson assms(1) assms(2) assms(3) less_le_trans min_le_iff_disj)


[STATEMENT]
lemma poincare_collinear3_between:
  assumes "u \<in> unit_disc" and "v \<in> unit_disc" and "w \<in> unit_disc"
  assumes "poincare_collinear {u, v, w}"
  shows "poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w" (is "?P' u v w")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
proof (cases "u=v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. u = v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 2. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
u = v

goal (2 subgoals):
 1. u = v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 2. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u = v
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
poincare_collinear {u, v, w}

goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
u \<noteq> v

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
have "\<forall> w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> ?P' u v w" (is "?P u v")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
proof (rule wlog_positive_x_axis[where P="?P"])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
assume x: "is_real x" "0 < Re x" "Re x < 1"
[PROOF STATE]
proof (state)
this:
is_real x
0 < Re x
Re x < 1

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
hence "x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. x \<noteq> 0
[PROOF STEP]
using complex.expand[of x 0]
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1
Re x = Re 0 \<and> Im x = Im 0 \<Longrightarrow> x = 0

goal (1 subgoal):
 1. x \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
hence *: "poincare_line 0\<^sub>h (of_complex x) = x_axis"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
using x poincare_line_0_real_is_x_axis[of "of_complex x"]
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
is_real x
0 < Re x
Re x < 1
\<lbrakk>of_complex x \<in> circline_set x_axis; of_complex x \<noteq> 0\<^sub>h; of_complex x \<noteq> \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
is_real x
0 < Re x
Re x < 1
\<lbrakk>of_complex x \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}; of_complex x \<noteq> 0\<^sub>h; of_complex x \<noteq> \<infinity>\<^sub>h\<rbrakk> \<Longrightarrow> poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (1 subgoal):
 1. poincare_line 0\<^sub>h (of_complex x) = x_axis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_line 0\<^sub>h (of_complex x) = x_axis

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
have "of_complex x \<in> unit_disc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<in> unit_disc
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
is_real x
0 < Re x
Re x < 1

goal (1 subgoal):
 1. of_complex x \<in> unit_disc
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
of_complex x \<in> unit_disc

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
have "of_complex x \<noteq> 0\<^sub>h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h
[PROOF STEP]
using \<open>x \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. of_complex x \<noteq> 0\<^sub>h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_complex x \<noteq> 0\<^sub>h

goal (5 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
 5. \<And>x. \<lbrakk>is_real x; 0 < Re x; Re x < 1\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
show "?P 0\<^sub>h (of_complex x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume "w \<in> unit_disc"
[PROOF STATE]
proof (state)
this:
w \<in> unit_disc

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume "poincare_collinear {0\<^sub>h, of_complex x, w}"
[PROOF STATE]
proof (state)
this:
poincare_collinear {0\<^sub>h, of_complex x, w}

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "w \<in> circline_set x_axis"
[PROOF STATE]
proof (prove)
using this:
poincare_collinear {0\<^sub>h, of_complex x, w}

goal (1 subgoal):
 1. w \<in> circline_set x_axis
[PROOF STEP]
using * unique_poincare_line[of "0\<^sub>h" "of_complex x"] \<open>of_complex x \<in> unit_disc\<close> \<open>x \<noteq> 0\<close> \<open>of_complex x \<noteq> 0\<^sub>h\<close>
[PROOF STATE]
proof (prove)
using this:
poincare_collinear {0\<^sub>h, of_complex x, w}
poincare_line 0\<^sub>h (of_complex x) = x_axis
\<lbrakk>0\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc; 0\<^sub>h \<in> circline_set ?l; of_complex x \<in> circline_set ?l; is_poincare_line ?l\<rbrakk> \<Longrightarrow> ?l = poincare_line 0\<^sub>h (of_complex x)
of_complex x \<in> unit_disc
x \<noteq> 0
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. w \<in> circline_set x_axis
[PROOF STEP]
unfolding poincare_collinear_def
[PROOF STATE]
proof (prove)
using this:
\<exists>p. is_poincare_line p \<and> {0\<^sub>h, of_complex x, w} \<subseteq> circline_set p
poincare_line 0\<^sub>h (of_complex x) = x_axis
\<lbrakk>0\<^sub>h \<noteq> of_complex x; 0\<^sub>h \<in> unit_disc; of_complex x \<in> unit_disc; 0\<^sub>h \<in> circline_set ?l; of_complex x \<in> circline_set ?l; is_poincare_line ?l\<rbrakk> \<Longrightarrow> ?l = poincare_line 0\<^sub>h (of_complex x)
of_complex x \<in> unit_disc
x \<noteq> 0
of_complex x \<noteq> 0\<^sub>h

goal (1 subgoal):
 1. w \<in> circline_set x_axis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> circline_set x_axis

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
w \<in> circline_set x_axis
[PROOF STEP]
obtain w' where w': "w = of_complex w'" "is_real w'"
[PROOF STATE]
proof (prove)
using this:
w \<in> circline_set x_axis

goal (1 subgoal):
 1. (\<And>w'. \<lbrakk>w = of_complex w'; is_real w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>w \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
w \<in> circline_set x_axis
w \<in> unit_disc

goal (1 subgoal):
 1. (\<And>w'. \<lbrakk>w = of_complex w'; is_real w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using inf_or_of_complex[of w]
[PROOF STATE]
proof (prove)
using this:
w \<in> circline_set x_axis
w \<in> unit_disc
w = \<infinity>\<^sub>h \<or> (\<exists>x. w = of_complex x)

goal (1 subgoal):
 1. (\<And>w'. \<lbrakk>w = of_complex w'; is_real w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding circline_set_x_axis
[PROOF STATE]
proof (prove)
using this:
w \<in> of_complex ` {x. is_real x} \<union> {\<infinity>\<^sub>h}
w \<in> unit_disc
w = \<infinity>\<^sub>h \<or> (\<exists>x. w = of_complex x)

goal (1 subgoal):
 1. (\<And>w'. \<lbrakk>w = of_complex w'; is_real w'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "-1 < Re w'" "Re w' < 1"
[PROOF STATE]
proof (prove)
using this:
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. - 1 < Re w' &&& Re w' < 1
[PROOF STEP]
using \<open>w \<in> unit_disc\<close>
[PROOF STATE]
proof (prove)
using this:
w = of_complex w'
is_real w'
w \<in> unit_disc

goal (1 subgoal):
 1. - 1 < Re w' &&& Re w' < 1
[PROOF STEP]
by (auto simp add: cmod_eq_Re)
[PROOF STATE]
proof (state)
this:
- 1 < Re w'
Re w' < 1

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume 1: "\<not> poincare_between (of_complex x) 0\<^sub>h w"
[PROOF STATE]
proof (state)
this:
\<not> poincare_between (of_complex x) 0\<^sub>h w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "w \<noteq> 0\<^sub>h" "w' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w

goal (1 subgoal):
 1. w \<noteq> 0\<^sub>h &&& w' \<noteq> 0
[PROOF STEP]
using w'
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. w \<noteq> 0\<^sub>h &&& w' \<noteq> 0
[PROOF STEP]
unfolding poincare_between_def
[PROOF STATE]
proof (prove)
using this:
\<not> (of_complex x = 0\<^sub>h \<or> 0\<^sub>h = w \<or> (let cr = cross_ratio (of_complex x) 0\<^sub>h w (inversion 0\<^sub>h) in is_real (to_complex cr) \<and> Re (to_complex cr) < 0))
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. w \<noteq> 0\<^sub>h &&& w' \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<noteq> 0\<^sub>h
w' \<noteq> 0

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "Re w' \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0\<^sub>h
w' \<noteq> 0

goal (1 subgoal):
 1. Re w' \<noteq> 0
[PROOF STEP]
using w' complex.expand[of w' 0]
[PROOF STATE]
proof (prove)
using this:
w \<noteq> 0\<^sub>h
w' \<noteq> 0
w = of_complex w'
is_real w'
Re w' = Re 0 \<and> Im w' = Im 0 \<Longrightarrow> w' = 0

goal (1 subgoal):
 1. Re w' \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re w' \<noteq> 0

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
have "Re w' \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> Re w'
[PROOF STEP]
using 1 poincare_between_x_axis_u0v[of x w'] \<open>Re x > 0\<close> \<open>is_real x\<close> \<open>x \<noteq> 0\<close> \<open>w' \<noteq> 0\<close> w'
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w
\<lbrakk>is_real x; x \<noteq> 0; w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between (of_complex x) 0\<^sub>h (of_complex w') = (is_real w' \<and> Re x * Re w' < 0)
0 < Re x
is_real x
x \<noteq> 0
w' \<noteq> 0
w = of_complex w'
is_real w'

goal (1 subgoal):
 1. 0 \<le> Re w'
[PROOF STEP]
using mult_pos_neg
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between (of_complex x) 0\<^sub>h w
\<lbrakk>is_real x; x \<noteq> 0; w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between (of_complex x) 0\<^sub>h (of_complex w') = (is_real w' \<and> Re x * Re w' < 0)
0 < Re x
is_real x
x \<noteq> 0
w' \<noteq> 0
w = of_complex w'
is_real w'
\<lbrakk>(0::?'a) < ?a; ?b < (0::?'a)\<rbrakk> \<Longrightarrow> ?a * ?b < (0::?'a)

goal (1 subgoal):
 1. 0 \<le> Re w'
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 \<le> Re w'

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 \<le> Re w'

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
assume "\<not> poincare_between 0\<^sub>h (of_complex x) w"
[PROOF STATE]
proof (state)
this:
\<not> poincare_between 0\<^sub>h (of_complex x) w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
hence "Re w' < Re x"
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between 0\<^sub>h (of_complex x) w

goal (1 subgoal):
 1. Re w' < Re x
[PROOF STEP]
using poincare_between_x_axis_0uv[of "Re x" "Re w'"]
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between 0\<^sub>h (of_complex x) w
\<lbrakk>- 1 < Re x; Re x < 1; Re x \<noteq> 0; - 1 < Re w'; Re w' < 1; Re w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re x))) (of_complex (cor (Re w'))) = (Re x < 0 \<and> Re w' < 0 \<and> Re w' \<le> Re x \<or> 0 < Re x \<and> 0 < Re w' \<and> Re x \<le> Re w')

goal (1 subgoal):
 1. Re w' < Re x
[PROOF STEP]
using w' x \<open>-1 < Re w'\<close> \<open>Re w' < 1\<close> \<open>Re w' \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> poincare_between 0\<^sub>h (of_complex x) w
\<lbrakk>- 1 < Re x; Re x < 1; Re x \<noteq> 0; - 1 < Re w'; Re w' < 1; Re w' \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re x))) (of_complex (cor (Re w'))) = (Re x < 0 \<and> Re w' < 0 \<and> Re w' \<le> Re x \<or> 0 < Re x \<and> 0 < Re w' \<and> Re x \<le> Re w')
w = of_complex w'
is_real w'
is_real x
0 < Re x
Re x < 1
- 1 < Re w'
Re w' < 1
Re w' \<noteq> 0

goal (1 subgoal):
 1. Re w' < Re x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Re w' < Re x

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {0\<^sub>h, of_complex x, w}; \<not> poincare_between 0\<^sub>h (of_complex x) w; \<not> poincare_between (of_complex x) 0\<^sub>h w\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 \<le> Re w'
Re w' < Re x
[PROOF STEP]
show "poincare_between 0\<^sub>h w (of_complex x)"
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re w'
Re w' < Re x

goal (1 subgoal):
 1. poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
using poincare_between_x_axis_0uv[of "Re w'" "Re x"]
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re w'
Re w' < Re x
\<lbrakk>- 1 < Re w'; Re w' < 1; Re w' \<noteq> 0; - 1 < Re x; Re x < 1; Re x \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re w'))) (of_complex (cor (Re x))) = (Re w' < 0 \<and> Re x < 0 \<and> Re x \<le> Re w' \<or> 0 < Re w' \<and> 0 < Re x \<and> Re w' \<le> Re x)

goal (1 subgoal):
 1. poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
using w' x \<open>-1 < Re w'\<close> \<open>Re w' < 1\<close> \<open>Re w' \<noteq> 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 \<le> Re w'
Re w' < Re x
\<lbrakk>- 1 < Re w'; Re w' < 1; Re w' \<noteq> 0; - 1 < Re x; Re x < 1; Re x \<noteq> 0\<rbrakk> \<Longrightarrow> poincare_between 0\<^sub>h (of_complex (cor (Re w'))) (of_complex (cor (Re x))) = (Re w' < 0 \<and> Re x < 0 \<and> Re x \<le> Re w' \<or> 0 < Re w' \<and> 0 < Re x \<and> Re w' \<le> Re x)
w = of_complex w'
is_real w'
is_real x
0 < Re x
Re x < 1
- 1 < Re w'
Re w' < 1
Re w' \<noteq> 0

goal (1 subgoal):
 1. poincare_between 0\<^sub>h w (of_complex x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poincare_between 0\<^sub>h w (of_complex x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {0\<^sub>h, of_complex x, w} \<longrightarrow> poincare_between 0\<^sub>h (of_complex x) w \<or> poincare_between 0\<^sub>h w (of_complex x) \<or> poincare_between (of_complex x) 0\<^sub>h w

goal (4 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. u \<in> unit_disc
 2. v \<in> unit_disc
 3. u \<noteq> v
 4. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
show "u \<in> unit_disc" "v \<in> unit_disc" "u \<noteq> v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> unit_disc &&& v \<in> unit_disc &&& u \<noteq> v
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
fix M u v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
assume 1: "unit_disc_fix M" "u \<in> unit_disc" "v \<in> unit_disc" "u \<noteq> v"
[PROOF STATE]
proof (state)
this:
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
let ?Mu = "moebius_pt M u" and ?Mv = "moebius_pt M v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
assume 2: "?P ?Mu ?Mv"
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w

goal (1 subgoal):
 1. \<And>M u v. \<lbrakk>unit_disc_fix M; u \<in> unit_disc; v \<in> unit_disc; u \<noteq> v; \<forall>w. w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, w} \<longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) w \<or> poincare_between (moebius_pt M u) w (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) w\<rbrakk> \<Longrightarrow> \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
show "?P u v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {u, v, w}; \<not> poincare_between u v w; \<not> poincare_between v u w\<rbrakk> \<Longrightarrow> poincare_between u w v
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {u, v, w}; \<not> poincare_between u v w; \<not> poincare_between v u w\<rbrakk> \<Longrightarrow> poincare_between u w v
[PROOF STEP]
assume "w \<in> unit_disc" "poincare_collinear {u, v, w}" "\<not> poincare_between u v w" "\<not> poincare_between v u w"
[PROOF STATE]
proof (state)
this:
w \<in> unit_disc
poincare_collinear {u, v, w}
\<not> poincare_between u v w
\<not> poincare_between v u w

goal (1 subgoal):
 1. \<And>w. \<lbrakk>w \<in> unit_disc; poincare_collinear {u, v, w}; \<not> poincare_between u v w; \<not> poincare_between v u w\<rbrakk> \<Longrightarrow> poincare_between u w v
[PROOF STEP]
thus "poincare_between u w v"
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc
poincare_collinear {u, v, w}
\<not> poincare_between u v w
\<not> poincare_between v u w

goal (1 subgoal):
 1. poincare_between u w v
[PROOF STEP]
using 1 2[rule_format, of "moebius_pt M w"]
[PROOF STATE]
proof (prove)
using this:
w \<in> unit_disc
poincare_collinear {u, v, w}
\<not> poincare_between u v w
\<not> poincare_between v u w
unit_disc_fix M
u \<in> unit_disc
v \<in> unit_disc
u \<noteq> v
moebius_pt M w \<in> unit_disc \<and> poincare_collinear {moebius_pt M u, moebius_pt M v, moebius_pt M w} \<Longrightarrow> poincare_between (moebius_pt M u) (moebius_pt M v) (moebius_pt M w) \<or> poincare_between (moebius_pt M u) (moebius_pt M w) (moebius_pt M v) \<or> poincare_between (moebius_pt M v) (moebius_pt M u) (moebius_pt M w)

goal (1 subgoal):
 1. poincare_between u w v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_between u w v

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal (1 subgoal):
 1. u \<noteq> v \<Longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>w. w \<in> unit_disc \<and> poincare_collinear {u, v, w} \<longrightarrow> poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
u \<in> unit_disc
v \<in> unit_disc
w \<in> unit_disc
poincare_collinear {u, v, w}

goal (1 subgoal):
 1. poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
poincare_between u v w \<or> poincare_between u w v \<or> poincare_between v u w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "dec_string_of_word0 (3::2 word) = ''11''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dec_string_of_word0 3 = ''11''
[PROOF STEP]
by eval


[STATEMENT]
lemma test_mult_comm_var: "test p \<Longrightarrow> test q \<Longrightarrow> p \<cdot> q = q \<cdot> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test p; test q\<rbrakk> \<Longrightarrow> p \<cdot> q = q \<cdot> p
[PROOF STEP]
using n_mult_comm
[PROOF STATE]
proof (prove)
using this:
!?x \<cdot> !?y = !?y \<cdot> !?x

goal (1 subgoal):
 1. \<lbrakk>test p; test q\<rbrakk> \<Longrightarrow> p \<cdot> q = q \<cdot> p
[PROOF STEP]
by auto


[STATEMENT]
lemma test_one_var: "test 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (1::'a)
[PROOF STEP]
by (simp add: test_def)


[STATEMENT]
lemma Fun_add_pow_apply:
  assumes "b \<in> carrier (Fun\<^bsub>n\<^esub> Q\<^sub>p)"
  assumes "a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)"
  shows "([(m::nat)]\<cdot>\<^bsub>Fun\<^bsub>n\<^esub> Q\<^sub>p\<^esub> b) a = [m]\<cdot>( b a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
have 0: "b a \<in> carrier Q\<^sub>p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b a \<in> carrier Q\<^sub>p
[PROOF STEP]
using Qp.function_ring_car_mem_closed assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f \<in> carrier (function_ring ?S Q\<^sub>p); ?s \<in> ?S\<rbrakk> \<Longrightarrow> ?f ?s \<in> carrier Q\<^sub>p
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. b a \<in> carrier Q\<^sub>p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
b a \<in> carrier Q\<^sub>p

goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
have 1: "ring (Fun\<^bsub>n\<^esub> Q\<^sub>p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
[PROOF STEP]
using function_ring_is_ring
[PROOF STATE]
proof (prove)
using this:
ring (function_ring (carrier (Q\<^sub>p\<^bsup>?n\<^esup>)) Q\<^sub>p)

goal (1 subgoal):
 1. ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)

goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
proof(induction m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
 2. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
 2. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
have "([(0::nat)] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) = \<zero>\<^bsub>Fun\<^bsub>n\<^esub> Q\<^sub>p\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
[PROOF STEP]
using 1 ring.add_pow_zero[of "Fun\<^bsub>n\<^esub> Q\<^sub>p" b ] assms
[PROOF STATE]
proof (prove)
using this:
ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
\<lbrakk>ring (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p); b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)\<rbrakk> \<Longrightarrow> [0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. [0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>

goal (2 subgoals):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
 2. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>

goal (1 subgoal):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
[PROOF STEP]
using  function_zero_eval Qp.nat_mult_zero assms
[PROOF STATE]
proof (prove)
using this:
[0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b = \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub>
?a \<in> carrier (Q\<^sub>p\<^bsup>?n\<^esup>) \<Longrightarrow> \<zero>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>?n\<^esup>)) Q\<^sub>p\<^esub> ?a = \<zero>
[0] \<cdot> ?x = \<zero>
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. ([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
([0] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [0] \<cdot> b a

goal (1 subgoal):
 1. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a

goal (1 subgoal):
 1. \<And>m. ([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a \<Longrightarrow> ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a

goal (1 subgoal):
 1. ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
using Suc ring.add_pow_Suc[of "SA n" b m] assms
[PROOF STATE]
proof (prove)
using this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a
\<lbrakk>ring (SA n); b \<in> carrier (SA n)\<rbrakk> \<Longrightarrow> [Suc m] \<cdot>\<^bsub>SA n\<^esub> b = [m] \<cdot>\<^bsub>SA n\<^esub> b \<oplus>\<^bsub>SA n\<^esub> b
b \<in> carrier (function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p)
a \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)

goal (1 subgoal):
 1. ([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a
[PROOF STEP]
by (metis (no_types, lifting) "0" "1" Qp.ring_axioms SA_add SA_plus ring.add_pow_Suc)
[PROOF STATE]
proof (state)
this:
([Suc m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [Suc m] \<cdot> b a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
([m] \<cdot>\<^bsub>function_ring (carrier (Q\<^sub>p\<^bsup>n\<^esup>)) Q\<^sub>p\<^esub> b) a = [m] \<cdot> b a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma UP_SA_n_is_cring:
  shows "cring (UP (SA n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cring (UP (SA n))
[PROOF STEP]
using SA_is_cring
[PROOF STATE]
proof (prove)
using this:
cring (SA ?n)

goal (1 subgoal):
 1. cring (UP (SA n))
[PROOF STEP]
by (simp add: UP_cring.UP_cring UP_cring.intro)


[STATEMENT]
lemma SA_poly_to_SA_fun_monom':
  assumes "f \<in> carrier (SA n)"
  assumes "x \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)"
  assumes "t \<in> carrier Q\<^sub>p"
  shows "SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t#x) = (f x)\<otimes>t[^]\<^bsub>Q\<^sub>p\<^esub>k "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
have 0: "hd (t#x) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff (t # x) = t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lead_coeff (t # x) = t

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
have 1: "tl (t#x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl (t # x) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
tl (t # x) = x

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
have 2: "(t#x) \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)
[PROOF STEP]
by (metis add.commute assms  cartesian_power_cons plus_1_eq_Suc)
[PROOF STATE]
proof (state)
this:
t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
using 0 1 2 SA_poly_to_SA_fun_monom[of f n "t#x" k] assms SA_poly_to_SA_fun_monom
[PROOF STATE]
proof (prove)
using this:
lead_coeff (t # x) = t
tl (t # x) = x
t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)
\<lbrakk>f \<in> carrier (SA n); t # x \<in> carrier (Q\<^sub>p\<^bsup>Suc n\<^esup>)\<rbrakk> \<Longrightarrow> SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f (tl (t # x)) \<otimes> lead_coeff (t # x) [^] k
f \<in> carrier (SA n)
x \<in> carrier (Q\<^sub>p\<^bsup>n\<^esup>)
t \<in> carrier Q\<^sub>p
\<lbrakk>?f \<in> carrier (SA ?n); ?a \<in> carrier (Q\<^sub>p\<^bsup>Suc ?n\<^esup>)\<rbrakk> \<Longrightarrow> SA_poly_to_SA_fun ?n (up_ring.monom (UP (SA ?n)) ?f ?k) ?a = ?f (tl ?a) \<otimes> lead_coeff ?a [^] ?k

goal (1 subgoal):
 1. SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
SA_poly_to_SA_fun n (up_ring.monom (UP (SA n)) f k) (t # x) = f x \<otimes> t [^] k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma E_sup_mono:
  "(\<And>\<omega>. f \<omega> \<le> g \<omega>) \<Longrightarrow> E_sup s f \<le> E_sup s g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<omega>. f \<omega> \<le> g \<omega>) \<Longrightarrow> E_sup s f \<le> E_sup s g
[PROOF STEP]
unfolding E_sup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<omega>. f \<omega> \<le> g \<omega>) \<Longrightarrow> (\<Squnion>cfg\<in>cfg_on s. integral\<^sup>N (T cfg) f) \<le> (\<Squnion>cfg\<in>cfg_on s. integral\<^sup>N (T cfg) g)
[PROOF STEP]
by (intro SUP_subset_mono order_refl nn_integral_mono)


[STATEMENT]
lemma le_of_comp_set_less_eq:
  "le_of_comp (comp_of_ords (ord.set_less_eq le) (ord.set_less le)) = ord.set_less_eq le"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le_of_comp (comp_of_ords (ord.set_less_eq le) (ord.set_less le)) = ord.set_less_eq le
[PROOF STEP]
by (rule le_of_comp_of_ords_gen, simp add: ord.set_less_def)


[STATEMENT]
lemma eprod_rule[refine_vcg]:
  "\<lbrakk>\<And>a b. p=(a,b) \<Longrightarrow> S a b \<le> ESPEC \<Phi> \<Psi>\<rbrakk> \<Longrightarrow> (case p of (a,b) \<Rightarrow> S a b) \<le> ESPEC \<Phi> \<Psi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b. p = (a, b) \<Longrightarrow> S a b \<le> ESPEC \<Phi> \<Psi>) \<Longrightarrow> (case p of (a, b) \<Rightarrow> S a b) \<le> ESPEC \<Phi> \<Psi>
[PROOF STEP]
by (auto split: prod.split)


[STATEMENT]
lemma intro_eLet_refine:
  assumes "f x \<le> \<Down>\<^sub>E E R M'"
  shows "Let x f \<le> \<Down>\<^sub>E E R M'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Let x f \<le> \<Down>\<^sub>E E R M'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f x \<le> \<Down>\<^sub>E E R M'

goal (1 subgoal):
 1. Let x f \<le> \<Down>\<^sub>E E R M'
[PROOF STEP]
by auto


[STATEMENT]
lemma cp_OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_Person_OclAny: "cp P \<Longrightarrow> cp(\<lambda>X.(P(X::Person)::OclAny).oclIsKindOf(Person))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cp P \<Longrightarrow> cp (\<lambda>X. P X.oclIsKindOf(Person))
[PROOF STEP]
by(rule cpI1, simp_all add: OclIsKindOf\<^sub>P\<^sub>e\<^sub>r\<^sub>s\<^sub>o\<^sub>n_OclAny)


[STATEMENT]
lemma marked_morph_lcp: "f (r \<and>\<^sub>p s) = f r \<and>\<^sub>p f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (r \<and>\<^sub>p s) = f r \<and>\<^sub>p f s
[PROOF STEP]
by (simp add:
      marked_concat_lcp[of "map f\<^sup>\<C> r" "map f\<^sup>\<C> s", unfolded map_lcp_conv[OF inj_core] morph_concat_map])


[STATEMENT]
lemma minsolD': "s \<in> g =\<^sub>M h \<Longrightarrow> s \<noteq> \<epsilon>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<in> g =\<^sub>M h \<Longrightarrow> s \<noteq> \<epsilon>
[PROOF STEP]
using minsoldef
[PROOF STATE]
proof (prove)
using this:
?s \<in> ?g =\<^sub>M ?h \<equiv> ?s \<noteq> \<epsilon> \<and> ?g ?s = ?h ?s \<and> (\<forall>s'. s' \<le>np ?s \<and> ?g s' = ?h s' \<longrightarrow> s' = ?s)

goal (1 subgoal):
 1. s \<in> g =\<^sub>M h \<Longrightarrow> s \<noteq> \<epsilon>
[PROOF STEP]
by blast


[STATEMENT]
lemma dropWhile_Cons: "(dropWhile P xs) = x#ys \<Longrightarrow> \<not> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dropWhile P xs = x # ys \<Longrightarrow> \<not> P x
[PROOF STEP]
apply (induct xs)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dropWhile P [] = x # ys \<Longrightarrow> \<not> P x
 2. \<And>a xs. \<lbrakk>dropWhile P xs = x # ys \<Longrightarrow> \<not> P x; dropWhile P (a # xs) = x # ys\<rbrakk> \<Longrightarrow> \<not> P x
[PROOF STEP]
apply (auto split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma aux4[rule_format]:
  "applied_rule_rev Cp x (a#p) = Some a \<longrightarrow> a \<notin> set (p) \<longrightarrow> applied_rule_rev Cp x p = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. applied_rule_rev Cp x (a # p) = \<lfloor>a\<rfloor> \<longrightarrow> a \<notin> set p \<longrightarrow> applied_rule_rev Cp x p = \<bottom>
[PROOF STEP]
by (rule rev_induct, simp_all) (intro impI,simp add: applied_rule_rev_def split: if_splits)


[STATEMENT]
lemma C_eq_rd[rule_format]:
  "p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) = Cp (list2FWpolicy p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) = Cp (list2FWpolicy p)
[PROOF STEP]
proof (rule ext, induct p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. [] \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x
 2. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
[] \<noteq> []

goal (2 subgoals):
 1. \<And>x. [] \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x
 2. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
[] \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups [])) x = Cp (list2FWpolicy []) x

goal (1 subgoal):
 1. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) ?x = Cp (list2FWpolicy ys) ?x
y # ys \<noteq> []

goal (1 subgoal):
 1. \<And>a p x. \<lbrakk>\<And>x. p \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups p)) x = Cp (list2FWpolicy p) x; a # p \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (a # p))) x = Cp (list2FWpolicy (a # p)) x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) ?x = Cp (list2FWpolicy ys) ?x
y # ys \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
proof (cases "ys = []")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys = []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
 2. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ys = []

goal (2 subgoals):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys = []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
 2. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ys = []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x

goal (1 subgoal):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
ys \<noteq> []

goal (1 subgoal):
 1. \<lbrakk>\<And>x. ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y # ys \<noteq> []; ys \<noteq> []\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []
ys \<noteq> [] \<Longrightarrow> Cp (list2FWpolicy (remdups ys)) ?x = Cp (list2FWpolicy ys) ?x
y # ys \<noteq> []

goal (1 subgoal):
 1. Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x\<rbrakk> \<Longrightarrow> (y \<in> set ys \<longrightarrow> Cp (list2FWpolicy ys) x = Cp (list2FWpolicy (y # ys)) x) \<and> (y \<notin> set ys \<longrightarrow> Cp (list2FWpolicy (y # remdups ys)) x = Cp (list2FWpolicy (y # ys)) x)
[PROOF STEP]
apply (intro conjI impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y \<in> set ys\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy ys) x = Cp (list2FWpolicy (y # ys)) x
 2. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y \<notin> set ys\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (y # remdups ys)) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
apply (metis Cdom2 nlpaux notindom domIff l2p_aux)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ys \<noteq> []; \<And>x. Cp (list2FWpolicy (remdups ys)) x = Cp (list2FWpolicy ys) x; y \<notin> set ys\<rbrakk> \<Longrightarrow> Cp (list2FWpolicy (y # remdups ys)) x = Cp (list2FWpolicy (y # ys)) x
[PROOF STEP]
by (metis (no_types, lifting) Cdom2 nlpaux domIff l2p_aux remDupsNMT)
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Cp (list2FWpolicy (remdups (y # ys))) x = Cp (list2FWpolicy (y # ys)) x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma AbstrLevels_A1_A12:
  assumes "sA1 \<in> AbstrLevel i"
  shows "sA12 \<notin> AbstrLevel i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sA12 \<notin> AbstrLevel i
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sA12 \<notin> AbstrLevel i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sA1 \<in> AbstrLevel i

goal (1 subgoal):
 1. sA12 \<notin> AbstrLevel i
[PROOF STEP]
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)


[STATEMENT]
lemma AbstrLevels_S10_A71:
  assumes "sS10 \<in> AbstrLevel i"
  shows "sA71 \<notin> AbstrLevel i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sA71 \<notin> AbstrLevel i
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sA71 \<notin> AbstrLevel i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sS10 \<in> AbstrLevel i

goal (1 subgoal):
 1. sA71 \<notin> AbstrLevel i
[PROOF STEP]
by (induct i, simp add: AbstrLevel0, simp add:  AbstrLevel1, simp add:  AbstrLevel2,  simp add:  AbstrLevel3)


[STATEMENT]
lemma OUTfromChCorrect_data8: "OUTfromChCorrect data8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OUTfromChCorrect data8
[PROOF STEP]
by (simp add: OUTfromChCorrect_def, metis IN.simps(18) OUT.simps(18) insertI1)