[STATEMENT]
lemma semantics_put_imps:
  \<open>(e,f,g,z \<Turnstile> p) = eval e f g (put_imps p z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e,f,g,z \<Turnstile> p) = eval e f g (put_imps p z)
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (list_all (eval e f g) z \<longrightarrow> eval e f g p) = eval e f g (put_imps p z)
[PROOF STEP]
by (induct z) auto


[STATEMENT]
lemma shift_imp_assum:
  fixes p :: \<open>('a, 'b) form\<close>
  assumes inf_params: \<open>infinite (UNIV :: 'a set)\<close>
    and \<open>z \<turnstile> Impl p q\<close>
  shows \<open>p # z \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
have \<open>set z \<subseteq> set (p # z)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set z \<subseteq> set (p # z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set z \<subseteq> set (p # z)

goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set z \<subseteq> set (p # z)
[PROOF STEP]
have \<open>p # z \<turnstile> Impl p q\<close>
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set (p # z)

goal (1 subgoal):
 1. p # z \<turnstile> Impl p q
[PROOF STEP]
using assms weaken_assumptions inf_params
[PROOF STATE]
proof (prove)
using this:
set z \<subseteq> set (p # z)
infinite UNIV
z \<turnstile> Impl p q
\<lbrakk>infinite UNIV; ?z \<turnstile> ?p; set ?z \<subseteq> set ?z'\<rbrakk> \<Longrightarrow> ?z' \<turnstile> ?p
infinite UNIV

goal (1 subgoal):
 1. p # z \<turnstile> Impl p q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p # z \<turnstile> Impl p q

goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p # z \<turnstile> Impl p q

goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
have \<open>p # z \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p # z \<turnstile> p
[PROOF STEP]
by (simp add: Assum)
[PROOF STATE]
proof (state)
this:
p # z \<turnstile> p

goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p # z \<turnstile> Impl p q
p # z \<turnstile> p
[PROOF STEP]
show \<open>p # z \<turnstile> q\<close>
[PROOF STATE]
proof (prove)
using this:
p # z \<turnstile> Impl p q
p # z \<turnstile> p

goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
using ImplE
[PROOF STATE]
proof (prove)
using this:
p # z \<turnstile> Impl p q
p # z \<turnstile> p
\<lbrakk>?G \<turnstile> Impl ?a ?b; ?G \<turnstile> ?a\<rbrakk> \<Longrightarrow> ?G \<turnstile> ?b

goal (1 subgoal):
 1. p # z \<turnstile> q
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p # z \<turnstile> q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma remove_imps:
  assumes \<open>infinite (- params p)\<close>
  shows \<open>z' \<turnstile> put_imps p z \<Longrightarrow> rev z @ z' \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z' \<turnstile> put_imps p z \<Longrightarrow> rev z @ z' \<turnstile> p
[PROOF STEP]
using assms shift_imp_assum
[PROOF STATE]
proof (prove)
using this:
infinite (- params p)
\<lbrakk>infinite UNIV; ?z \<turnstile> Impl ?p ?q\<rbrakk> \<Longrightarrow> ?p # ?z \<turnstile> ?q

goal (1 subgoal):
 1. z' \<turnstile> put_imps p z \<Longrightarrow> rev z @ z' \<turnstile> p
[PROOF STEP]
by (induct z arbitrary: z') auto


[STATEMENT]
lemma subc_sub_closed_var' [simp]:
  \<open>new_term c t \<Longrightarrow> closedt (Suc m) t \<Longrightarrow> subc_term c (Var m) (substt t (App c []) m) = t\<close>
  \<open>new_list c l \<Longrightarrow> closedts (Suc m) l \<Longrightarrow> subc_list c (Var m) (substts l (App c []) m) = l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>new_term c t; closedt (Suc m) t\<rbrakk> \<Longrightarrow> subc_term c (Var m) (t[App c []/m]) = t) &&& (\<lbrakk>new_list c l; closedts (Suc m) l\<rbrakk> \<Longrightarrow> subc_list c (Var m) (l[App c []/m]) = l)
[PROOF STEP]
by (induct t and l rule: substt.induct substts.induct) auto


[STATEMENT]
lemma subc_sub_closed_var [simp]: \<open>new c p \<Longrightarrow> closed (Suc m) p \<Longrightarrow>
    subc c (Var m) (subst p (App c []) m) = p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>new c p; closed (Suc m) p\<rbrakk> \<Longrightarrow> subc c (Var m) (p[App c []/m]) = p
[PROOF STEP]
by (induct p arbitrary: m) simp_all


[STATEMENT]
lemma sub_put_unis [simp]:
  \<open>subst (put_unis k p) (App c []) i = put_unis k (subst p (App c []) (i + k))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. put_unis k p[App c []/i] = put_unis k (p[App c []/i + k])
[PROOF STEP]
by (induct k arbitrary: i) simp_all


[STATEMENT]
lemma valid_put_unis: \<open>\<forall>(e :: nat \<Rightarrow> 'a) f g. eval e f g p \<Longrightarrow>
    eval (e :: nat \<Rightarrow> 'a) f g (put_unis m p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e f g. eval e f g p \<Longrightarrow> eval e f g (put_unis m p)
[PROOF STEP]
by (induct m arbitrary: e) simp_all


[STATEMENT]
lemma put_unis_collapse: \<open>put_unis m (put_unis n p) = put_unis (m + n) p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. put_unis m (put_unis n p) = put_unis (m + n) p
[PROOF STEP]
by (induct m) simp_all


[STATEMENT]
lemma consts_for_unis: \<open>[] \<turnstile> put_unis (length cs) p \<Longrightarrow>
  [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<turnstile> put_unis (length cs) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs
[PROOF STEP]
proof (induct cs arbitrary: p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. [] \<turnstile> put_unis (length []) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length []) p) []
 2. \<And>a cs p. \<lbrakk>\<And>p. [] \<turnstile> put_unis (length cs) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs; [] \<turnstile> put_unis (length (a # cs)) p\<rbrakk> \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length (a # cs)) p) (a # cs)
[PROOF STEP]
case (Cons c cs)
[PROOF STATE]
proof (state)
this:
[] \<turnstile> put_unis (length cs) ?p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) ?p) cs
[] \<turnstile> put_unis (length (c # cs)) p

goal (2 subgoals):
 1. \<And>p. [] \<turnstile> put_unis (length []) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length []) p) []
 2. \<And>a cs p. \<lbrakk>\<And>p. [] \<turnstile> put_unis (length cs) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs; [] \<turnstile> put_unis (length (a # cs)) p\<rbrakk> \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length (a # cs)) p) (a # cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<turnstile> put_unis (length cs) ?p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) ?p) cs
[] \<turnstile> put_unis (length (c # cs)) p
[PROOF STEP]
have \<open>[] \<turnstile> Forall (put_unis (length cs) p)\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> put_unis (length cs) ?p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) ?p) cs
[] \<turnstile> put_unis (length (c # cs)) p

goal (1 subgoal):
 1. [] \<turnstile> Forall (put_unis (length cs) p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] \<turnstile> Forall (put_unis (length cs) p)

goal (2 subgoals):
 1. \<And>p. [] \<turnstile> put_unis (length []) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length []) p) []
 2. \<And>a cs p. \<lbrakk>\<And>p. [] \<turnstile> put_unis (length cs) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs; [] \<turnstile> put_unis (length (a # cs)) p\<rbrakk> \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length (a # cs)) p) (a # cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<turnstile> Forall (put_unis (length cs) p)
[PROOF STEP]
have \<open>[] \<turnstile> subst (put_unis (length cs) p) (App c []) 0\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> Forall (put_unis (length cs) p)

goal (1 subgoal):
 1. [] \<turnstile> put_unis (length cs) p[App c []/0]
[PROOF STEP]
using ForallE
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> Forall (put_unis (length cs) p)
?G \<turnstile> Forall ?a \<Longrightarrow> ?G \<turnstile> ?a[?t/0]

goal (1 subgoal):
 1. [] \<turnstile> put_unis (length cs) p[App c []/0]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[] \<turnstile> put_unis (length cs) p[App c []/0]

goal (2 subgoals):
 1. \<And>p. [] \<turnstile> put_unis (length []) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length []) p) []
 2. \<And>a cs p. \<lbrakk>\<And>p. [] \<turnstile> put_unis (length cs) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs; [] \<turnstile> put_unis (length (a # cs)) p\<rbrakk> \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length (a # cs)) p) (a # cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<turnstile> put_unis (length cs) p[App c []/0]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> put_unis (length cs) p[App c []/0]

goal (1 subgoal):
 1. [] \<turnstile> consts_for_unis (put_unis (length (c # cs)) p) (c # cs)
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> put_unis (length cs) p[App c []/0]
[] \<turnstile> put_unis (length cs) ?p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length cs) ?p) cs
[] \<turnstile> put_unis (length (c # cs)) p

goal (1 subgoal):
 1. [] \<turnstile> consts_for_unis (put_unis (length (c # cs)) p) (c # cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[] \<turnstile> consts_for_unis (put_unis (length (c # cs)) p) (c # cs)

goal (1 subgoal):
 1. \<And>p. [] \<turnstile> put_unis (length []) p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length []) p) []
[PROOF STEP]
qed simp


[STATEMENT]
lemma vars_for_consts:
  assumes \<open>infinite (- params p)\<close>
  shows \<open>[] \<turnstile> p \<Longrightarrow> [] \<turnstile> vars_for_consts p xs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<turnstile> p \<Longrightarrow> [] \<turnstile> vars_for_consts p xs
[PROOF STEP]
using assms deriv_subc
[PROOF STATE]
proof (prove)
using this:
infinite (- params p)
\<lbrakk>infinite UNIV; ?z \<turnstile> ?p\<rbrakk> \<Longrightarrow> subcs ?c ?s ?z \<turnstile> subc ?c ?s ?p

goal (1 subgoal):
 1. [] \<turnstile> p \<Longrightarrow> [] \<turnstile> vars_for_consts p xs
[PROOF STEP]
by (induct xs arbitrary: p) fastforce+


[STATEMENT]
lemma vars_for_consts_for_unis:
  \<open>closed (length cs) p \<Longrightarrow> list_all (\<lambda>c. new c p) cs \<Longrightarrow> distinct cs \<Longrightarrow>
   vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs = p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>closed (length cs) p; list_all (\<lambda>c. new c p) cs; distinct cs\<rbrakk> \<Longrightarrow> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs = p
[PROOF STEP]
by (induct cs arbitrary: p) (simp_all add: subst_new_all)


[STATEMENT]
lemma fresh_constant:
  fixes p :: \<open>('a, 'b) form\<close>
  assumes \<open>infinite (UNIV :: 'a set)\<close>
  shows \<open>\<exists>c. c \<notin> set cs \<and> new c p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. c \<notin> set cs \<and> new c p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>c. c \<notin> set cs \<and> new c p
[PROOF STEP]
have \<open>finite (set cs \<union> params p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set cs \<union> params p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (set cs \<union> params p)

goal (1 subgoal):
 1. \<exists>c. c \<notin> set cs \<and> new c p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite (set cs \<union> params p)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (set cs \<union> params p)

goal (1 subgoal):
 1. \<exists>c. c \<notin> set cs \<and> new c p
[PROOF STEP]
using assms ex_new_if_finite UnI1 UnI2
[PROOF STATE]
proof (prove)
using this:
finite (set cs \<union> params p)
infinite UNIV
\<lbrakk>infinite UNIV; finite ?A\<rbrakk> \<Longrightarrow> \<exists>a. a \<notin> ?A
?c \<in> ?A \<Longrightarrow> ?c \<in> ?A \<union> ?B
?c \<in> ?B \<Longrightarrow> ?c \<in> ?A \<union> ?B

goal (1 subgoal):
 1. \<exists>c. c \<notin> set cs \<and> new c p
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>c. c \<notin> set cs \<and> new c p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fresh_constants:
  fixes p :: \<open>('a, 'b) form\<close>
  assumes \<open>infinite (UNIV :: 'a set)\<close>
  shows \<open>\<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
proof (induct m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>cs. length cs = 0 \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
 2. \<And>m. \<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs \<Longrightarrow> \<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
\<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs

goal (2 subgoals):
 1. \<exists>cs. length cs = 0 \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
 2. \<And>m. \<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs \<Longrightarrow> \<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
obtain cs where \<open>length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs

goal (1 subgoal):
 1. (\<And>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs

goal (2 subgoals):
 1. \<exists>cs. length cs = 0 \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
 2. \<And>m. \<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs \<Longrightarrow> \<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs

goal (2 subgoals):
 1. \<exists>cs. length cs = 0 \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
 2. \<And>m. \<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs \<Longrightarrow> \<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
obtain c where \<open>c \<notin> set cs \<and> new c p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. c \<notin> set cs \<and> new c p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Suc assms fresh_constant
[PROOF STATE]
proof (prove)
using this:
\<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
infinite UNIV
infinite UNIV \<Longrightarrow> \<exists>c. c \<notin> set ?cs \<and> new c ?p

goal (1 subgoal):
 1. (\<And>c. c \<notin> set cs \<and> new c p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c \<notin> set cs \<and> new c p

goal (2 subgoals):
 1. \<exists>cs. length cs = 0 \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
 2. \<And>m. \<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs \<Longrightarrow> \<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
c \<notin> set cs \<and> new c p
[PROOF STEP]
have \<open>length (c # cs) = Suc m \<and> list_all (\<lambda>c. new c p) (c # cs) \<and> distinct (c # cs)\<close>
[PROOF STATE]
proof (prove)
using this:
length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
c \<notin> set cs \<and> new c p

goal (1 subgoal):
 1. length (c # cs) = Suc m \<and> list_all (\<lambda>c. new c p) (c # cs) \<and> distinct (c # cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (c # cs) = Suc m \<and> list_all (\<lambda>c. new c p) (c # cs) \<and> distinct (c # cs)

goal (2 subgoals):
 1. \<exists>cs. length cs = 0 \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
 2. \<And>m. \<exists>cs. length cs = m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs \<Longrightarrow> \<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (c # cs) = Suc m \<and> list_all (\<lambda>c. new c p) (c # cs) \<and> distinct (c # cs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length (c # cs) = Suc m \<and> list_all (\<lambda>c. new c p) (c # cs) \<and> distinct (c # cs)

goal (1 subgoal):
 1. \<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>cs. length cs = Suc m \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs

goal (1 subgoal):
 1. \<exists>cs. length cs = 0 \<and> list_all (\<lambda>c. new c p) cs \<and> distinct cs
[PROOF STEP]
qed simp


[STATEMENT]
lemma closed_max:
  assumes \<open>closed m p\<close> \<open>closed n q\<close>
  shows \<open>closed (max m n) p \<and> closed (max m n) q\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (max m n) p \<and> closed (max m n) q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closed (max m n) p \<and> closed (max m n) q
[PROOF STEP]
have \<open>m \<le> max m n\<close> and \<open>n \<le> max m n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> max m n &&& n \<le> max m n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
m \<le> max m n
n \<le> max m n

goal (1 subgoal):
 1. closed (max m n) p \<and> closed (max m n) q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<le> max m n
n \<le> max m n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m \<le> max m n
n \<le> max m n

goal (1 subgoal):
 1. closed (max m n) p \<and> closed (max m n) q
[PROOF STEP]
using assms closed_mono
[PROOF STATE]
proof (prove)
using this:
m \<le> max m n
n \<le> max m n
closed m p
closed n q
\<lbrakk>?i \<le> ?j; closed ?i ?p\<rbrakk> \<Longrightarrow> closed ?j ?p

goal (1 subgoal):
 1. closed (max m n) p \<and> closed (max m n) q
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
closed (max m n) p \<and> closed (max m n) q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_closed' [simp]:
  fixes t :: \<open>'a term\<close> and l :: \<open>'a term list\<close>
  shows \<open>\<exists>m. closedt m t\<close> \<open>\<exists>n. closedts n l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. closedt m t &&& \<exists>n. closedts n l
[PROOF STEP]
proof (induct t and l rule: closedt.induct closedts.induct)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x. \<exists>m. closedt m (Var x)
 2. \<And>x1 x2. \<exists>n. closedts n x2 \<Longrightarrow> \<exists>m. closedt m (App x1 x2)
 3. \<exists>n. closedts n []
 4. \<And>x1 x2. \<lbrakk>\<exists>m. closedt m x1; \<exists>n. closedts n x2\<rbrakk> \<Longrightarrow> \<exists>n. closedts n (x1 # x2)
[PROOF STEP]
case (Cons_term t l)
[PROOF STATE]
proof (state)
this:
\<exists>m. closedt m t
\<exists>n. closedts n l

goal (4 subgoals):
 1. \<And>x. \<exists>m. closedt m (Var x)
 2. \<And>x1 x2. \<exists>n. closedts n x2 \<Longrightarrow> \<exists>m. closedt m (App x1 x2)
 3. \<exists>n. closedts n []
 4. \<And>x1 x2. \<lbrakk>\<exists>m. closedt m x1; \<exists>n. closedts n x2\<rbrakk> \<Longrightarrow> \<exists>n. closedts n (x1 # x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. closedt m t
\<exists>n. closedts n l
[PROOF STEP]
obtain m and n where \<open>closedt m t\<close> and \<open>closedts n l\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closedt m t
\<exists>n. closedts n l

goal (1 subgoal):
 1. (\<And>m n. \<lbrakk>closedt m t; closedts n l\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closedt m t
closedts n l

goal (4 subgoals):
 1. \<And>x. \<exists>m. closedt m (Var x)
 2. \<And>x1 x2. \<exists>n. closedts n x2 \<Longrightarrow> \<exists>m. closedt m (App x1 x2)
 3. \<exists>n. closedts n []
 4. \<And>x1 x2. \<lbrakk>\<exists>m. closedt m x1; \<exists>n. closedts n x2\<rbrakk> \<Longrightarrow> \<exists>n. closedts n (x1 # x2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
closedt m t
closedts n l

goal (4 subgoals):
 1. \<And>x. \<exists>m. closedt m (Var x)
 2. \<And>x1 x2. \<exists>n. closedts n x2 \<Longrightarrow> \<exists>m. closedt m (App x1 x2)
 3. \<exists>n. closedts n []
 4. \<And>x1 x2. \<lbrakk>\<exists>m. closedt m x1; \<exists>n. closedts n x2\<rbrakk> \<Longrightarrow> \<exists>n. closedts n (x1 # x2)
[PROOF STEP]
have \<open>m \<le> max m n\<close> and \<open>n \<le> max m n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<le> max m n &&& n \<le> max m n
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
m \<le> max m n
n \<le> max m n

goal (4 subgoals):
 1. \<And>x. \<exists>m. closedt m (Var x)
 2. \<And>x1 x2. \<exists>n. closedts n x2 \<Longrightarrow> \<exists>m. closedt m (App x1 x2)
 3. \<exists>n. closedts n []
 4. \<And>x1 x2. \<lbrakk>\<exists>m. closedt m x1; \<exists>n. closedts n x2\<rbrakk> \<Longrightarrow> \<exists>n. closedts n (x1 # x2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
closedt m t
closedts n l
m \<le> max m n
n \<le> max m n
[PROOF STEP]
have \<open>closedt (max m n) t\<close> and \<open>closedts (max m n) l\<close>
[PROOF STATE]
proof (prove)
using this:
closedt m t
closedts n l
m \<le> max m n
n \<le> max m n

goal (1 subgoal):
 1. closedt (max m n) t &&& closedts (max m n) l
[PROOF STEP]
using closedt_mono
[PROOF STATE]
proof (prove)
using this:
closedt m t
closedts n l
m \<le> max m n
n \<le> max m n
\<lbrakk>?i \<le> ?j; closedt ?i ?t\<rbrakk> \<Longrightarrow> closedt ?j ?t
\<lbrakk>?i \<le> ?j; closedts ?i ?ts\<rbrakk> \<Longrightarrow> closedts ?j ?ts

goal (1 subgoal):
 1. closedt (max m n) t &&& closedts (max m n) l
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
closedt (max m n) t
closedts (max m n) l

goal (4 subgoals):
 1. \<And>x. \<exists>m. closedt m (Var x)
 2. \<And>x1 x2. \<exists>n. closedts n x2 \<Longrightarrow> \<exists>m. closedt m (App x1 x2)
 3. \<exists>n. closedts n []
 4. \<And>x1 x2. \<lbrakk>\<exists>m. closedt m x1; \<exists>n. closedts n x2\<rbrakk> \<Longrightarrow> \<exists>n. closedts n (x1 # x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closedt (max m n) t
closedts (max m n) l
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
closedt (max m n) t
closedts (max m n) l

goal (1 subgoal):
 1. \<exists>n. closedts n (t # l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>n. closedts n (t # l)

goal (3 subgoals):
 1. \<And>x. \<exists>m. closedt m (Var x)
 2. \<And>x1 x2. \<exists>n. closedts n x2 \<Longrightarrow> \<exists>m. closedt m (App x1 x2)
 3. \<exists>n. closedts n []
[PROOF STEP]
qed auto


[STATEMENT]
lemma ex_closed [simp]: \<open>\<exists>m. closed m p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. closed m p
[PROOF STEP]
proof (induct p)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<exists>m. closed m FF
 2. \<exists>m. closed m TT
 3. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 5. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 6. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 8. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 9. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
case FF
[PROOF STATE]
proof (state)
this:

goal (9 subgoals):
 1. \<exists>m. closed m FF
 2. \<exists>m. closed m TT
 3. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 5. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 6. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 8. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 9. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. closed m FF
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m FF

goal (8 subgoals):
 1. \<exists>m. closed m TT
 2. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 5. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 8. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<exists>m. closed m TT
 2. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 5. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 8. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
case TT
[PROOF STATE]
proof (state)
this:

goal (8 subgoals):
 1. \<exists>m. closed m TT
 2. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 5. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 8. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. closed m TT
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m TT

goal (7 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
case (Neg p)
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m p

goal (7 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Neg p)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 7. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. closed m p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p

goal (1 subgoal):
 1. \<exists>m. closed m (Neg p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m (Neg p)

goal (6 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
case (Impl p q)
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m p
\<exists>m. closed m q

goal (6 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Impl p1 p2)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 6. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. closed m p
\<exists>m. closed m q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p
\<exists>m. closed m q

goal (1 subgoal):
 1. \<exists>m. closed m (Impl p q)
[PROOF STEP]
using closed_max
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p
\<exists>m. closed m q
\<lbrakk>closed ?m ?p; closed ?n ?q\<rbrakk> \<Longrightarrow> closed (max ?m ?n) ?p \<and> closed (max ?m ?n) ?q

goal (1 subgoal):
 1. \<exists>m. closed m (Impl p q)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m (Impl p q)

goal (5 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
case (Or p q)
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m p
\<exists>m. closed m q

goal (5 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (Or p1 p2)
 4. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 5. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. closed m p
\<exists>m. closed m q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p
\<exists>m. closed m q

goal (1 subgoal):
 1. \<exists>m. closed m (Or p q)
[PROOF STEP]
using closed_max
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p
\<exists>m. closed m q
\<lbrakk>closed ?m ?p; closed ?n ?q\<rbrakk> \<Longrightarrow> closed (max ?m ?n) ?p \<and> closed (max ?m ?n) ?q

goal (1 subgoal):
 1. \<exists>m. closed m (Or p q)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m (Or p q)

goal (4 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 4. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 4. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
case (And p q)
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m p
\<exists>m. closed m q

goal (4 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p1 p2. \<lbrakk>\<exists>m. closed m p1; \<exists>m. closed m p2\<rbrakk> \<Longrightarrow> \<exists>m. closed m (And p1 p2)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 4. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. closed m p
\<exists>m. closed m q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p
\<exists>m. closed m q

goal (1 subgoal):
 1. \<exists>m. closed m (And p q)
[PROOF STEP]
using closed_max
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p
\<exists>m. closed m q
\<lbrakk>closed ?m ?p; closed ?n ?q\<rbrakk> \<Longrightarrow> closed (max ?m ?n) ?p \<and> closed (max ?m ?n) ?q

goal (1 subgoal):
 1. \<exists>m. closed m (And p q)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m (And p q)

goal (3 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
case (Exists p)
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m p

goal (3 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. closed m p
[PROOF STEP]
obtain m where \<open>closed m p\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p

goal (1 subgoal):
 1. (\<And>m. closed m p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closed m p

goal (3 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed m p
[PROOF STEP]
have \<open>closed (Suc m) p\<close>
[PROOF STATE]
proof (prove)
using this:
closed m p

goal (1 subgoal):
 1. closed (Suc m) p
[PROOF STEP]
using closed_mono Suc_n_not_le_n nat_le_linear
[PROOF STATE]
proof (prove)
using this:
closed m p
\<lbrakk>?i \<le> ?j; closed ?i ?p\<rbrakk> \<Longrightarrow> closed ?j ?p
\<not> Suc ?n \<le> ?n
?m \<le> ?n \<or> ?n \<le> ?m

goal (1 subgoal):
 1. closed (Suc m) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closed (Suc m) p

goal (3 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
 3. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Exists p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed (Suc m) p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
closed (Suc m) p

goal (1 subgoal):
 1. \<exists>m. closed m (Exists p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m (Exists p)

goal (2 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
[PROOF STEP]
case (Forall p)
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m p

goal (2 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>m. closed m p
[PROOF STEP]
obtain m where \<open>closed m p\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed m p

goal (1 subgoal):
 1. (\<And>m. closed m p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closed m p

goal (2 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed m p
[PROOF STEP]
have \<open>closed (Suc m) p\<close>
[PROOF STATE]
proof (prove)
using this:
closed m p

goal (1 subgoal):
 1. closed (Suc m) p
[PROOF STEP]
using closed_mono Suc_n_not_le_n nat_le_linear
[PROOF STATE]
proof (prove)
using this:
closed m p
\<lbrakk>?i \<le> ?j; closed ?i ?p\<rbrakk> \<Longrightarrow> closed ?j ?p
\<not> Suc ?n \<le> ?n
?m \<le> ?n \<or> ?n \<le> ?m

goal (1 subgoal):
 1. closed (Suc m) p
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closed (Suc m) p

goal (2 subgoals):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
 2. \<And>p. \<exists>m. closed m p \<Longrightarrow> \<exists>m. closed m (Forall p)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
closed (Suc m) p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
closed (Suc m) p

goal (1 subgoal):
 1. \<exists>m. closed m (Forall p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m. closed m (Forall p)

goal (1 subgoal):
 1. \<And>x1 x2. \<exists>m. closed m (Pred x1 x2)
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma ex_closure: \<open>\<exists>m. closed 0 (put_unis m p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. closed 0 (put_unis m p)
[PROOF STEP]
by simp


[STATEMENT]
lemma remove_unis_sentence:
  assumes inf_params: \<open>infinite (- params p)\<close>
    and \<open>closed 0 (put_unis m p)\<close> \<open>[] \<turnstile> put_unis m p\<close>
  shows \<open>[] \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
obtain cs :: \<open>'a list\<close> where \<open>length cs = m\<close>
    and *: \<open>distinct cs\<close> and **: \<open>list_all (\<lambda>c. new c p) cs\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>cs. \<lbrakk>length cs = m; distinct cs; list_all (\<lambda>c. new c p) cs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms finite_compl finite_params fresh_constants inf_params
[PROOF STATE]
proof (prove)
using this:
infinite (- params p)
closed 0 (put_unis m p)
[] \<turnstile> put_unis m p
finite ?A \<Longrightarrow> finite (- ?A) = finite UNIV
finite (params ?p)
infinite UNIV \<Longrightarrow> \<exists>cs. length cs = ?m \<and> list_all (\<lambda>c. new c ?p) cs \<and> distinct cs
infinite (- params p)

goal (1 subgoal):
 1. (\<And>cs. \<lbrakk>length cs = m; distinct cs; list_all (\<lambda>c. new c p) cs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
length cs = m
distinct cs
list_all (\<lambda>c. new c p) cs

goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length cs = m
distinct cs
list_all (\<lambda>c. new c p) cs
[PROOF STEP]
have \<open>[] \<turnstile> consts_for_unis (put_unis (length cs) p) cs\<close>
[PROOF STATE]
proof (prove)
using this:
length cs = m
distinct cs
list_all (\<lambda>c. new c p) cs

goal (1 subgoal):
 1. [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs
[PROOF STEP]
using assms consts_for_unis
[PROOF STATE]
proof (prove)
using this:
length cs = m
distinct cs
list_all (\<lambda>c. new c p) cs
infinite (- params p)
closed 0 (put_unis m p)
[] \<turnstile> put_unis m p
[] \<turnstile> put_unis (length ?cs) ?p \<Longrightarrow> [] \<turnstile> consts_for_unis (put_unis (length ?cs) ?p) ?cs

goal (1 subgoal):
 1. [] \<turnstile> consts_for_unis (put_unis (length cs) p) cs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[] \<turnstile> consts_for_unis (put_unis (length cs) p) cs

goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<turnstile> consts_for_unis (put_unis (length cs) p) cs
[PROOF STEP]
have \<open>[] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> consts_for_unis (put_unis (length cs) p) cs

goal (1 subgoal):
 1. [] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs
[PROOF STEP]
using vars_for_consts inf_params
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> consts_for_unis (put_unis (length cs) p) cs
\<lbrakk>infinite (- params ?p); [] \<turnstile> ?p\<rbrakk> \<Longrightarrow> [] \<turnstile> vars_for_consts ?p ?xs
infinite (- params p)

goal (1 subgoal):
 1. [] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs

goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs

goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
have \<open>closed (length cs) p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closed (length cs) p
[PROOF STEP]
using assms \<open>length cs = m\<close>
[PROOF STATE]
proof (prove)
using this:
infinite (- params p)
closed 0 (put_unis m p)
[] \<turnstile> put_unis m p
length cs = m

goal (1 subgoal):
 1. closed (length cs) p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
closed (length cs) p

goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs
closed (length cs) p
[PROOF STEP]
show \<open>[] \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs
closed (length cs) p

goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
using vars_for_consts_for_unis * **
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> vars_for_consts (consts_for_unis (put_unis (length cs) p) cs) cs
closed (length cs) p
\<lbrakk>closed (length ?cs) ?p; list_all (\<lambda>c. new c ?p) ?cs; distinct ?cs\<rbrakk> \<Longrightarrow> vars_for_consts (consts_for_unis (put_unis (length ?cs) ?p) ?cs) ?cs = ?p
distinct cs
list_all (\<lambda>c. new c p) cs

goal (1 subgoal):
 1. [] \<turnstile> p
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
[] \<turnstile> p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem completeness:
  fixes p :: \<open>(nat, nat) form\<close>
  assumes \<open>\<forall>(e :: nat \<Rightarrow> nat hterm) f g. e, f, g, z \<Turnstile> p\<close>
  shows \<open>z \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
let ?p = \<open>put_imps p (rev z)\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
have *: \<open>\<forall>(e :: nat \<Rightarrow> nat hterm) f g. eval e f g ?p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e f g. eval e f g (put_imps p (rev z))
[PROOF STEP]
using assms semantics_put_imps
[PROOF STATE]
proof (prove)
using this:
\<forall>e f g. e,f,g,z \<Turnstile> p
(?e,?f,?g,?z \<Turnstile> ?p) = eval ?e ?f ?g (put_imps ?p ?z)

goal (1 subgoal):
 1. \<forall>e f g. eval e f g (put_imps p (rev z))
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
\<forall>e f g. list_all (eval e f g) z \<longrightarrow> eval e f g p
(list_all (eval ?e ?f ?g) ?z \<longrightarrow> eval ?e ?f ?g ?p) = eval ?e ?f ?g (put_imps ?p ?z)

goal (1 subgoal):
 1. \<forall>e f g. eval e f g (put_imps p (rev z))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>e f g. eval e f g (put_imps p (rev z))

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
obtain m where **: \<open>closed 0 (put_unis m ?p)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. closed 0 (put_unis m (put_imps p (rev z))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ex_closure
[PROOF STATE]
proof (prove)
using this:
\<exists>m. closed 0 (put_unis m ?p)

goal (1 subgoal):
 1. (\<And>m. closed 0 (put_unis m (put_imps p (rev z))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closed 0 (put_unis m (put_imps p (rev z)))

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
closed 0 (put_unis m (put_imps p (rev z)))

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
have \<open>list_all (closed 0) []\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (closed 0) []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_all (closed 0) []

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
list_all (closed 0) []

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
have \<open>\<forall>(e :: nat \<Rightarrow> nat hterm) f g. e, f, g, [] \<Turnstile> put_unis m ?p\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>e f g. e,f,g,[] \<Turnstile> put_unis m (put_imps p (rev z))
[PROOF STEP]
using * valid_put_unis
[PROOF STATE]
proof (prove)
using this:
\<forall>e f g. eval e f g (put_imps p (rev z))
\<forall>e f g. eval e f g ?p \<Longrightarrow> eval ?e ?f ?g (put_unis ?m ?p)

goal (1 subgoal):
 1. \<forall>e f g. e,f,g,[] \<Turnstile> put_unis m (put_imps p (rev z))
[PROOF STEP]
unfolding model_def
[PROOF STATE]
proof (prove)
using this:
\<forall>e f g. eval e f g (put_imps p (rev z))
\<forall>e f g. eval e f g ?p \<Longrightarrow> eval ?e ?f ?g (put_unis ?m ?p)

goal (1 subgoal):
 1. \<forall>e f g. list_all (eval e f g) [] \<longrightarrow> eval e f g (put_unis m (put_imps p (rev z)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>e f g. e,f,g,[] \<Turnstile> put_unis m (put_imps p (rev z))

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
closed 0 (put_unis m (put_imps p (rev z)))
list_all (closed 0) []
\<forall>e f g. e,f,g,[] \<Turnstile> put_unis m (put_imps p (rev z))
[PROOF STEP]
have \<open>[] \<turnstile> put_unis m ?p\<close>
[PROOF STATE]
proof (prove)
using this:
closed 0 (put_unis m (put_imps p (rev z)))
list_all (closed 0) []
\<forall>e f g. e,f,g,[] \<Turnstile> put_unis m (put_imps p (rev z))

goal (1 subgoal):
 1. [] \<turnstile> put_unis m (put_imps p (rev z))
[PROOF STEP]
using natded_complete
[PROOF STATE]
proof (prove)
using this:
closed 0 (put_unis m (put_imps p (rev z)))
list_all (closed 0) []
\<forall>e f g. e,f,g,[] \<Turnstile> put_unis m (put_imps p (rev z))
\<lbrakk>closed 0 ?p; list_all (closed 0) ?ps; \<forall>e f g. e,f,g,?ps \<Turnstile> ?p\<rbrakk> \<Longrightarrow> ?ps \<turnstile> ?p

goal (1 subgoal):
 1. [] \<turnstile> put_unis m (put_imps p (rev z))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
[] \<turnstile> put_unis m (put_imps p (rev z))

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<turnstile> put_unis m (put_imps p (rev z))
[PROOF STEP]
have \<open>[] \<turnstile> ?p\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> put_unis m (put_imps p (rev z))

goal (1 subgoal):
 1. [] \<turnstile> put_imps p (rev z)
[PROOF STEP]
using ** remove_unis_sentence
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> put_unis m (put_imps p (rev z))
closed 0 (put_unis m (put_imps p (rev z)))
\<lbrakk>infinite (- params ?p); closed 0 (put_unis ?m ?p); [] \<turnstile> put_unis ?m ?p\<rbrakk> \<Longrightarrow> [] \<turnstile> ?p

goal (1 subgoal):
 1. [] \<turnstile> put_imps p (rev z)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
[] \<turnstile> put_imps p (rev z)

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[] \<turnstile> put_imps p (rev z)
[PROOF STEP]
show \<open>z \<turnstile> p\<close>
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> put_imps p (rev z)

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
using remove_imps
[PROOF STATE]
proof (prove)
using this:
[] \<turnstile> put_imps p (rev z)
\<lbrakk>infinite (- params ?p); ?z' \<turnstile> put_imps ?p ?z\<rbrakk> \<Longrightarrow> rev ?z @ ?z' \<turnstile> ?p

goal (1 subgoal):
 1. z \<turnstile> p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
z \<turnstile> p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_Hermite_reduce_above:
  fixes A::"'a::{unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
  assumes "n<nrows A"
  shows "matrix_to_iarray (Hermite_reduce_above A n i j res)
  = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (to_nat i) (to_nat j) res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n < nrows A

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A 0 i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < nrows A

goal (2 subgoals):
 1. \<And>A. 0 < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A 0 i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
 2. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 < nrows A

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above A 0 i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_reduce_above A 0 i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) 0 (mod_type_class.to_nat i) (mod_type_class.to_nat j) res

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
n < nrows ?A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above ?A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray ?A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
Suc n < nrows A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
have n: "n<nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < nrows A
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc n < nrows A

goal (1 subgoal):
 1. n < nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc n < CARD('rows)

goal (1 subgoal):
 1. n < CARD('rows)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n < nrows A

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
obtain a::'rows where n_tna: "n = to_nat a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. n = mod_type_class.to_nat a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc.prems Suc_lessD nrows_def to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
n = mod_type_class.to_nat a

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. n < nrows A \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res; Suc n < nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
unfolding Hermite_reduce_above.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (let i' = mod_type_class.from_nat n; Aij = A $ i $ j; Ai'j = A $ i' $ j in Hermite_reduce_above (row_add A i' i ((res Aij Ai'j - Ai'j) div Aij)) n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
unfolding Hermite_reduce_above_iarrays.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (let i' = mod_type_class.from_nat n; Aij = A $ i $ j; Ai'j = A $ i' $ j in Hermite_reduce_above (row_add A i' i ((res Aij Ai'j - Ai'j) div Aij)) n i j res) = (let i' = n; Aij = matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j; Ai'j = matrix_to_iarray A !! i' !! mod_type_class.to_nat j in Hermite_reduce_above_iarrays (row_add_iarray (matrix_to_iarray A) i' (mod_type_class.to_nat i) ((res Aij Ai'j - Ai'j) div Aij)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res)
[PROOF STEP]
unfolding Let_def sub_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above (row_add A (mod_type_class.from_nat n) i ((res (A $ i $ j) (A $ mod_type_class.from_nat n $ j) - A $ mod_type_class.from_nat n $ j) div A $ i $ j)) n i j res) = Hermite_reduce_above_iarrays (row_add_iarray (matrix_to_iarray A) n (mod_type_class.to_nat i) ((res (matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j) (matrix_to_iarray A !! n !! mod_type_class.to_nat j) - matrix_to_iarray A !! n !! mod_type_class.to_nat j) div matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j)) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
unfolding n_tna
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above (row_add A (mod_type_class.from_nat (mod_type_class.to_nat a)) i ((res (A $ i $ j) (A $ mod_type_class.from_nat (mod_type_class.to_nat a) $ j) - A $ mod_type_class.from_nat (mod_type_class.to_nat a) $ j) div A $ i $ j)) (mod_type_class.to_nat a) i j res) = Hermite_reduce_above_iarrays (row_add_iarray (matrix_to_iarray A) (mod_type_class.to_nat a) (mod_type_class.to_nat i) ((res (matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j) (matrix_to_iarray A !! mod_type_class.to_nat a !! mod_type_class.to_nat j) - matrix_to_iarray A !! mod_type_class.to_nat a !! mod_type_class.to_nat j) div matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j)) (mod_type_class.to_nat a) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
unfolding matrix_to_iarray_row_add[symmetric] from_nat_to_nat_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above (row_add A a i ((res (A $ i $ j) (A $ a $ j) - A $ a $ j) div A $ i $ j)) (mod_type_class.to_nat a) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray (row_add A a i ((res (matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j) (matrix_to_iarray A !! mod_type_class.to_nat a !! mod_type_class.to_nat j) - matrix_to_iarray A !! mod_type_class.to_nat a !! mod_type_class.to_nat j) div matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat j))) (mod_type_class.to_nat a) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
unfolding matrix_to_iarray_nth
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above (row_add A a i ((res (A $ i $ j) (A $ a $ j) - A $ a $ j) div A $ i $ j)) (mod_type_class.to_nat a) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray (row_add A a i ((res (A $ i $ j) (A $ a $ j) - A $ a $ j) div A $ i $ j))) (mod_type_class.to_nat a) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
unfolding n_tna[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_reduce_above (row_add A a i ((res (A $ i $ j) (A $ a $ j) - A $ a $ j) div A $ i $ j)) n i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray (row_add A a i ((res (A $ i $ j) (A $ a $ j) - A $ a $ j) div A $ i $ j))) n (mod_type_class.to_nat i) (mod_type_class.to_nat j) res
[PROOF STEP]
by (rule Suc.hyps, auto simp add: nrows_def n[unfolded nrows_def])
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_reduce_above A (Suc n) i j res) = Hermite_reduce_above_iarrays (matrix_to_iarray A) (Suc n) (mod_type_class.to_nat i) (mod_type_class.to_nat j) res

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_Hermite_of_row_i[code_unfold]:
  fixes A::"'a::{unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
  shows "matrix_to_iarray (Hermite_of_row_i ass res A i)
  = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (to_nat i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
have zero_rw: "is_zero_iarray (matrix_to_iarray A !! to_nat i) = is_zero_row i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) = is_zero_row i A
[PROOF STEP]
by (simp add: is_zero_iarray_eq_iff is_zero_row_eq_row_zero vec_to_iarray_row')
[PROOF STATE]
proof (state)
this:
is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) = is_zero_row i A

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
proof (cases "is_zero_row i A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
 2. \<not> is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
is_zero_row i A

goal (2 subgoals):
 1. is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
 2. \<not> is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zero_row i A

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
unfolding Hermite_of_row_i_def Hermite_of_row_i_iarray_def Let_def zero_rw
[PROOF STATE]
proof (prove)
using this:
is_zero_row i A

goal (1 subgoal):
 1. matrix_to_iarray (if is_zero_row i A then A else Hermite_reduce_above (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)))) (mod_type_class.to_nat i) i (LEAST n. A $ i $ n \<noteq> (0::'a)) res) = (if is_zero_row i A then matrix_to_iarray A else Hermite_reduce_above_iarrays (mult_row_iarray (matrix_to_iarray A) (mod_type_class.to_nat i) (ass (matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) div matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i))) (mod_type_class.to_nat i) (mod_type_class.to_nat i) (least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) res)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)

goal (1 subgoal):
 1. \<not> is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row i A

goal (1 subgoal):
 1. \<not> is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
have Ain: "A $ i $ (LEAST n. A $ i $ n \<noteq> 0) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i A

goal (1 subgoal):
 1. A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by (metis (mono_tags, lifting) LeastI is_zero_row_def')
[PROOF STATE]
proof (state)
this:
A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<not> is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
have l: "least_non_zero_position_of_vector (matrix_to_iarray A !! to_nat i) = to_nat (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
have least_rw: " (LEAST n. A $ i $ n \<noteq> 0 \<and> 0 \<le> n) =  (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
by (rule Least_equality, auto simp add: least_mod_type Ain Least_le)
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n) = (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
have v_rw: "\<not> vector_all_zero_from_index (to_nat (0::'cols), vec_to_iarray (A $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (A $ i))
[PROOF STEP]
using False least_mod_type
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i A
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. \<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (A $ i))
[PROOF STEP]
unfolding vector_all_zero_from_index_eq[of 0 "A$i", symmetric] is_zero_row_def'
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. A $ i $ j = (0::'a))
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. \<not> (\<forall>m\<ge>0::'cols. A $ i $ m = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> vector_all_zero_from_index (mod_type_class.to_nat (0::'cols), vec_to_iarray (A $ i))

goal (1 subgoal):
 1. least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
using vec_to_iarray_least_non_zero_position_of_vector_from_index[OF v_rw]
[PROOF STATE]
proof (prove)
using this:
least_non_zero_position_of_vector_from_index (vec_to_iarray (A $ i)) (mod_type_class.to_nat (0::'cols)) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a) \<and> (0::'cols) \<le> n)

goal (1 subgoal):
 1. least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding least_rw least_non_zero_position_of_vector_def to_nat_0 vec_matrix
[PROOF STATE]
proof (prove)
using this:
least_non_zero_position_of_vector_from_index (matrix_to_iarray A !! mod_type_class.to_nat i) 0 = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. least_non_zero_position_of_vector_from_index (matrix_to_iarray A !! mod_type_class.to_nat i) 0 = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i) = mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> is_zero_row i A \<Longrightarrow> matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)
[PROOF STEP]
unfolding Hermite_of_row_i_def Hermite_of_row_i_iarray_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (if is_zero_row i A then A else Hermite_reduce_above (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)))) (mod_type_class.to_nat i) i (LEAST n. A $ i $ n \<noteq> (0::'a)) res) = (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then matrix_to_iarray A else Hermite_reduce_above_iarrays (mult_row_iarray (matrix_to_iarray A) (mod_type_class.to_nat i) (ass (matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) div matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i))) (mod_type_class.to_nat i) (mod_type_class.to_nat i) (least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) res)
[PROOF STEP]
unfolding zero_rw[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then A else Hermite_reduce_above (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)))) (mod_type_class.to_nat i) i (LEAST n. A $ i $ n \<noteq> (0::'a)) res) = (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then matrix_to_iarray A else Hermite_reduce_above_iarrays (mult_row_iarray (matrix_to_iarray A) (mod_type_class.to_nat i) (ass (matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) div matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i))) (mod_type_class.to_nat i) (mod_type_class.to_nat i) (least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) res)
[PROOF STEP]
unfolding matrix_to_iarray_mult_row[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then A else Hermite_reduce_above (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)))) (mod_type_class.to_nat i) i (LEAST n. A $ i $ n \<noteq> (0::'a)) res) = (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then matrix_to_iarray A else Hermite_reduce_above_iarrays (matrix_to_iarray (mult_row A i (ass (matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) div matrix_to_iarray A !! mod_type_class.to_nat i !! least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)))) (mod_type_class.to_nat i) (mod_type_class.to_nat i) (least_non_zero_position_of_vector (matrix_to_iarray A !! mod_type_class.to_nat i)) res)
[PROOF STEP]
unfolding l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then A else Hermite_reduce_above (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)))) (mod_type_class.to_nat i) i (LEAST n. A $ i $ n \<noteq> (0::'a)) res) = (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then matrix_to_iarray A else Hermite_reduce_above_iarrays (matrix_to_iarray (mult_row A i (ass (matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))) div matrix_to_iarray A !! mod_type_class.to_nat i !! mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))))) (mod_type_class.to_nat i) (mod_type_class.to_nat i) (mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))) res)
[PROOF STEP]
unfolding matrix_to_iarray_nth
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then A else Hermite_reduce_above (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a)))) (mod_type_class.to_nat i) i (LEAST n. A $ i $ n \<noteq> (0::'a)) res) = (if is_zero_iarray (matrix_to_iarray A !! mod_type_class.to_nat i) then matrix_to_iarray A else Hermite_reduce_above_iarrays (matrix_to_iarray (mult_row A i (ass (A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))) div A $ i $ (LEAST n. A $ i $ n \<noteq> (0::'a))))) (mod_type_class.to_nat i) (mod_type_class.to_nat i) (mod_type_class.to_nat (LEAST n. A $ i $ n \<noteq> (0::'a))) res)
[PROOF STEP]
by (auto, rule matrix_to_iarray_Hermite_reduce_above, simp add: nrows_def to_nat_less_card)
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_row_i ass res A i) = Hermite_of_row_i_iarray ass res (matrix_to_iarray A) (mod_type_class.to_nat i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_Hermite_of_upt_row_i:
  fixes A::"'a::{unique_euclidean_ring}^'cols::{mod_type}^'rows::{mod_type}"
  assumes i: "i\<le>nrows A"
  shows "matrix_to_iarray (Hermite_of_upt_row_i A i ass res)
  = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i \<le> nrows A

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res
[PROOF STEP]
proof (induct i arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. 0 \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A 0 ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) 0 ass res
 2. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 \<le> nrows A

goal (2 subgoals):
 1. \<And>A. 0 \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A 0 ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) 0 ass res
 2. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> nrows A

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_upt_row_i A 0 ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) 0 ass res
[PROOF STEP]
by (simp add: Hermite_of_upt_row_i_def Hermite_of_upt_row_i_iarrays_def)
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_upt_row_i A 0 ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) 0 ass res

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
i \<le> nrows ?A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i ?A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray ?A) i ass res
Suc i \<le> nrows A

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
have i: "i<nrows A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < nrows A
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
Suc i \<le> nrows A

goal (1 subgoal):
 1. i < nrows A
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
Suc i \<le> CARD('rows)

goal (1 subgoal):
 1. i < CARD('rows)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < nrows A

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
have "matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res)
    = matrix_to_iarray (Hermite_of_row_i ass res (Hermite_of_upt_row_i A i ass res) (from_nat i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = matrix_to_iarray (Hermite_of_row_i ass res (Hermite_of_upt_row_i A i ass res) (mod_type_class.from_nat i))
[PROOF STEP]
unfolding Hermite_of_upt_row_i_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (foldl (Hermite_of_row_i ass res) A (map mod_type_class.from_nat [0..<Suc i])) = matrix_to_iarray (Hermite_of_row_i ass res (foldl (Hermite_of_row_i ass res) A (map mod_type_class.from_nat [0..<i])) (mod_type_class.from_nat i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = matrix_to_iarray (Hermite_of_row_i ass res (Hermite_of_upt_row_i A i ass res) (mod_type_class.from_nat i))

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = matrix_to_iarray (Hermite_of_row_i ass res (Hermite_of_upt_row_i A i ass res) (mod_type_class.from_nat i))

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
have "... = (Hermite_of_row_i_iarray ass res
    (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (to_nat (from_nat i::'rows)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_row_i ass res (Hermite_of_upt_row_i A i ass res) (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i))
[PROOF STEP]
unfolding matrix_to_iarray_Hermite_of_row_i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_row_i ass res (Hermite_of_upt_row_i A i ass res) (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i))

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_row_i ass res (Hermite_of_upt_row_i A i ass res) (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i))

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
have "... = (Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i
[PROOF STEP]
using to_nat_from_nat_id[OF i[unfolded nrows_def]]
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat (mod_type_class.from_nat i) = i

goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) (mod_type_class.to_nat (mod_type_class.from_nat i)) = Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
have "... = (Hermite_of_row_i_iarray ass res
    (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i = Hermite_of_row_i_iarray ass res (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i
[PROOF STEP]
using Suc.hyps i
[PROOF STATE]
proof (prove)
using this:
i \<le> nrows ?A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i ?A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray ?A) i ass res
i < nrows A

goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i = Hermite_of_row_i_iarray ass res (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
using this:
i \<le> CARD('rows) \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i ?A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray ?A) i ass res
i < CARD('rows)

goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i = Hermite_of_row_i_iarray ass res (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i = Hermite_of_row_i_iarray ass res (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i_iarray ass res (matrix_to_iarray (Hermite_of_upt_row_i A i ass res)) i = Hermite_of_row_i_iarray ass res (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
have "... =  Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
unfolding Hermite_of_upt_row_i_iarrays_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_row_i_iarray ass res (foldl (Hermite_of_row_i_iarray ass res) (matrix_to_iarray A) [0..<i]) i = foldl (Hermite_of_row_i_iarray ass res) (matrix_to_iarray A) [0..<Suc i]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Hermite_of_row_i_iarray ass res (Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res) i = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res

goal (1 subgoal):
 1. \<And>i A. \<lbrakk>\<And>A. i \<le> nrows A \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A i ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) i ass res; Suc i \<le> nrows A\<rbrakk> \<Longrightarrow> matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of_upt_row_i A (Suc i) ass res) = Hermite_of_upt_row_i_iarrays (matrix_to_iarray A) (Suc i) ass res

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matrix_to_iarray_Hermite_of[code_unfold]:
  shows "matrix_to_iarray (Hermite_of A ass res bezout)
  = Hermite_of_iarrays (matrix_to_iarray A) ass res bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of A ass res bezout) = Hermite_of_iarrays (matrix_to_iarray A) ass res bezout
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of A ass res bezout) = Hermite_of_iarrays (matrix_to_iarray A) ass res bezout
[PROOF STEP]
have n: "nrows A \<le> nrows (echelon_form_of A bezout)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nrows A \<le> nrows (echelon_form_of A bezout)
[PROOF STEP]
unfolding nrows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('c) \<le> CARD('c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nrows A \<le> nrows (echelon_form_of A bezout)

goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of A ass res bezout) = Hermite_of_iarrays (matrix_to_iarray A) ass res bezout
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of A ass res bezout) = Hermite_of_iarrays (matrix_to_iarray A) ass res bezout
[PROOF STEP]
unfolding Hermite_of_def Hermite_of_iarrays_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matrix_to_iarray (Hermite_of_upt_row_i (echelon_form_of A bezout) (nrows A) ass res) = Hermite_of_upt_row_i_iarrays (echelon_form_of_iarrays (matrix_to_iarray A) bezout) (nrows_iarray (matrix_to_iarray A)) ass res
[PROOF STEP]
unfolding matrix_to_iarray_Hermite_of_upt_row_i[OF n]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_upt_row_i_iarrays (matrix_to_iarray (echelon_form_of A bezout)) (nrows A) ass res = Hermite_of_upt_row_i_iarrays (echelon_form_of_iarrays (matrix_to_iarray A) bezout) (nrows_iarray (matrix_to_iarray A)) ass res
[PROOF STEP]
unfolding matrix_to_iarray_echelon_form_of
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_upt_row_i_iarrays (echelon_form_of_iarrays (matrix_to_iarray A) bezout) (nrows A) ass res = Hermite_of_upt_row_i_iarrays (echelon_form_of_iarrays (matrix_to_iarray A) bezout) (nrows_iarray (matrix_to_iarray A)) ass res
[PROOF STEP]
unfolding matrix_to_iarray_nrows
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Hermite_of_upt_row_i_iarrays (echelon_form_of_iarrays (matrix_to_iarray A) bezout) (nrows_iarray (matrix_to_iarray A)) ass res = Hermite_of_upt_row_i_iarrays (echelon_form_of_iarrays (matrix_to_iarray A) bezout) (nrows_iarray (matrix_to_iarray A)) ass res
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
matrix_to_iarray (Hermite_of A ass res bezout) = Hermite_of_iarrays (matrix_to_iarray A) ass res bezout

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Set_bind_insert[simp]:
  "Set.bind (insert a A) B = B a \<union> (Set.bind A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set.bind (insert a A) B = B a \<union> Set.bind A B
[PROOF STEP]
by (auto simp: Set.bind_def)


[STATEMENT]
lemma option_bind_invE[elim]:
  "\<lbrakk> Option.bind f g = None; \<And>a. \<lbrakk> f = Some a; g a = None \<rbrakk> \<Longrightarrow> Q; f = None \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
  "\<lbrakk> Option.bind f g = Some x; \<And>a. \<lbrakk> f = Some a; g a = Some x \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>Option.bind f g = None; \<And>a. \<lbrakk>f = Some a; g a = None\<rbrakk> \<Longrightarrow> Q; f = None \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q) &&& (\<lbrakk>Option.bind f g = Some x; \<And>a. \<lbrakk>f = Some a; g a = Some x\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q)
[PROOF STEP]
by (case_tac [!] f) simp_all


[STATEMENT]
lemma colours_distinct[dest]:
  "black r s \<Longrightarrow> \<not>grey r s"
  "black r s \<Longrightarrow> \<not>white r s"
  "grey r s  \<Longrightarrow> \<not>black r s"
  "white r s \<Longrightarrow> \<not>black r s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((black r s \<Longrightarrow> \<not> grey r s) &&& (black r s \<Longrightarrow> \<not> white r s)) &&& (grey r s \<Longrightarrow> \<not> black r s) &&& (white r s \<Longrightarrow> \<not> black r s)
[PROOF STEP]
by (auto simp: black_def white_def obj_at_def split: option.splits)