text:
(*  Title:      HOL/Algebra/Algebraic_Closure.thy
    Author:     Paulo Emílio de Vilhena

With contributions by Martin Baillon.
*)

theory Algebraic_Closure
  imports Indexed_Polynomials Polynomial_Divisibility Pred_Zorn Finite_Extensions

begin

section \<open>Algebraic Closure\<close>

subsection \<open>Definitions\<close>

inductive iso_incl :: "'a ring \<Rightarrow> 'a ring \<Rightarrow> bool" (infixl "\<lesssim>" 65) for A B
  where iso_inclI [intro]: "id \<in> ring_hom A B \<Longrightarrow> iso_incl A B"

definition law_restrict :: "('a, 'b) ring_scheme \<Rightarrow> 'a ring"
  where "law_restrict R \<equiv> (ring.truncate R)
           \<lparr> mult := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<otimes>\<^bsub>R\<^esub> b),
              add := (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<oplus>\<^bsub>R\<^esub> b) \<rparr>"

definition (in ring) \<sigma> :: "'a list \<Rightarrow> (('a list multiset) \<Rightarrow> 'a) list"
  where "\<sigma> P = map indexed_const P"

definition (in ring) extensions :: "(('a list multiset) \<Rightarrow> 'a) ring set"
  where "extensions \<equiv> { L \<comment> \<open>such that\<close>.
           \<comment> \<open>i\<close>   (field L) \<and>
           \<comment> \<open>ii\<close>  (indexed_const \<in> ring_hom R L) \<and>
           \<comment> \<open>iii\<close> (\<forall>\<P> \<in> carrier L. carrier_coeff \<P>) \<and>
           \<comment> \<open>iv\<close>  (\<forall>\<P> \<in> carrier L. \<forall>P \<in> carrier (poly_ring R).
                       \<not> index_free \<P> P \<longrightarrow> \<X>\<^bsub>P\<^esub> \<in> carrier L \<and> (ring.eval L) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>L\<^esub>) }"

abbreviation (in ring) restrict_extensions :: "(('a list multiset) \<Rightarrow> 'a) ring set" ("\<S>")
  where "\<S> \<equiv> law_restrict ` extensions"

subsection \<open>Basic Properties\<close>

(* ========== *)
lemma (in field) is_ring: "ring R"
  using ring_axioms .
(* ========== *)

lemma law_restrict_carrier: "carrier (law_restrict R) = carrier R"
  by (simp add: law_restrict_def ring.defs)

lemma law_restrict_one: "one (law_restrict R) = one R"
  by (simp add: law_restrict_def ring.defs)

lemma law_restrict_zero: "zero (law_restrict R) = zero R"
  by (simp add: law_restrict_def ring.defs)

lemma law_restrict_mult: "monoid.mult (law_restrict R) = (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<otimes>\<^bsub>R\<^esub> b)"
  by (simp add: law_restrict_def ring.defs)

lemma law_restrict_add: "add (law_restrict R) = (\<lambda>a \<in> carrier R. \<lambda>b \<in> carrier R. a \<oplus>\<^bsub>R\<^esub> b)"
  by (simp add: law_restrict_def ring.defs)

lemma (in ring) law_restrict_is_ring: "ring (law_restrict R)"
  by (unfold_locales) (auto simp add: law_restrict_def Units_def ring.defs,
      simp_all add: a_assoc a_comm m_assoc l_distr r_distr a_lcomm)

lemma (in field) law_restrict_is_field: "field (law_restrict R)"
proof -
  have "comm_monoid_axioms (law_restrict R)"
    using m_comm unfolding comm_monoid_axioms_def law_restrict_carrier law_restrict_mult by auto
  then interpret L: cring "law_restrict R"
    using cring.intro law_restrict_is_ring comm_monoid.intro ring.is_monoid by auto
  have "Units R = Units (law_restrict R)"
    unfolding Units_def law_restrict_carrier law_restrict_mult law_restrict_one by auto
  thus ?thesis
    using L.cring_fieldI unfolding field_Units law_restrict_carrier law_restrict_zero by simp
qed

lemma law_restrict_iso_imp_eq:
  assumes "id \<in> ring_iso (law_restrict A) (law_restrict B)" and "ring A" and "ring B"
  shows "law_restrict A = law_restrict B"
proof -
  have "carrier A = carrier B"
    using ring_iso_memE(5)[OF assms(1)] unfolding bij_betw_def law_restrict_def by (simp add: ring.defs)
  hence mult: "a \<otimes>\<^bsub>law_restrict A\<^esub> b = a \<otimes>\<^bsub>law_restrict B\<^esub> b"
    and add:  "a \<oplus>\<^bsub>law_restrict A\<^esub> b = a \<oplus>\<^bsub>law_restrict B\<^esub> b" for a b
    using ring_iso_memE(2-3)[OF assms(1)] unfolding law_restrict_def by (auto simp add: ring.defs)
  have "monoid.mult (law_restrict A) = monoid.mult (law_restrict B)"
    using mult by auto
  moreover have "add (law_restrict A) = add (law_restrict B)"
    using add by auto
  moreover from \<open>carrier A = carrier B\<close> have "carrier (law_restrict A) = carrier (law_restrict B)"
    unfolding law_restrict_def by (simp add: ring.defs)
  moreover have "\<zero>\<^bsub>law_restrict A\<^esub> = \<zero>\<^bsub>law_restrict B\<^esub>"
    using ring_hom_zero[OF _ assms(2-3)[THEN ring.law_restrict_is_ring]] assms(1)
    unfolding ring_iso_def by auto
  moreover have "\<one>\<^bsub>law_restrict A\<^esub> = \<one>\<^bsub>law_restrict B\<^esub>"
    using ring_iso_memE(4)[OF assms(1)] by simp
  ultimately show ?thesis by simp
qed

lemma law_restrict_hom: "h \<in> ring_hom A B \<longleftrightarrow> h \<in> ring_hom (law_restrict A) (law_restrict B)"
proof
  assume "h \<in> ring_hom A B" thus "h \<in> ring_hom (law_restrict A) (law_restrict B)"
    by (auto intro!: ring_hom_memI dest: ring_hom_memE simp: law_restrict_def ring.defs)
next
  assume h: "h \<in> ring_hom (law_restrict A) (law_restrict B)" show "h \<in> ring_hom A B"
    using ring_hom_memE[OF h] by (auto intro!: ring_hom_memI simp: law_restrict_def ring.defs)
qed

lemma iso_incl_hom: "A \<lesssim> B \<longleftrightarrow> (law_restrict A) \<lesssim> (law_restrict B)"
  using law_restrict_hom iso_incl.simps by blast

subsection \<open>Partial Order\<close>

lemma iso_incl_backwards:
  assumes "A \<lesssim> B" shows "id \<in> ring_hom A B"
  using assms by cases

lemma iso_incl_antisym_aux:
  assumes "A \<lesssim> B" and "B \<lesssim> A" shows "id \<in> ring_iso A B"
proof -
  have hom: "id \<in> ring_hom A B" "id \<in> ring_hom B A"
    using assms(1-2)[THEN iso_incl_backwards] by auto
  thus ?thesis
    using hom[THEN ring_hom_memE(1)] by (auto simp add: ring_iso_def bij_betw_def inj_on_def)
qed

lemma iso_incl_refl: "A \<lesssim> A"
  by (rule iso_inclI[OF ring_hom_memI], auto)

lemma iso_incl_trans:
  assumes "A \<lesssim> B" and "B \<lesssim> C" shows "A \<lesssim> C"
  using ring_hom_trans[OF assms[THEN iso_incl_backwards]] by auto

lemma (in ring) iso_incl_antisym:
  assumes "A \<in> \<S>" "B \<in> \<S>" and "A \<lesssim> B" "B \<lesssim> A" shows "A = B"
proof -
  obtain A' B' :: "('a list multiset \<Rightarrow> 'a) ring"
    where A: "A = law_restrict A'" "ring A'" and B: "B = law_restrict B'" "ring B'"
    using assms(1-2) field.is_ring by (auto simp add: extensions_def)
  thus ?thesis
    using law_restrict_iso_imp_eq iso_incl_antisym_aux[OF assms(3-4)] by simp
qed

lemma (in ring) iso_incl_partial_order: "partial_order_on \<S> (rel_of (\<lesssim>) \<S>)"
  using iso_incl_refl iso_incl_trans iso_incl_antisym by (rule partial_order_on_rel_ofI)

lemma iso_inclE:
  assumes "ring A" and "ring B" and "A \<lesssim> B" shows "ring_hom_ring A B id"
  using iso_incl_backwards[OF assms(3)] ring_hom_ring.intro[OF assms(1-2)]
  unfolding symmetric[OF ring_hom_ring_axioms_def] by simp

lemma iso_incl_imp_same_eval:
  assumes "ring A" and "ring B" and "A \<lesssim> B" and "a \<in> carrier A" and "set p \<subseteq> carrier A"
  shows "(ring.eval A) p a = (ring.eval B) p a"
  using ring_hom_ring.eval_hom'[OF iso_inclE[OF assms(1-3)] assms(4-5)] by simp

subsection \<open>Extensions Non Empty\<close>

lemma (in ring) indexed_const_is_inj: "inj indexed_const"
  unfolding indexed_const_def by (rule inj_onI, metis)

lemma (in ring) indexed_const_inj_on: "inj_on indexed_const (carrier R)"
  unfolding indexed_const_def by (rule inj_onI, metis)

lemma (in field) extensions_non_empty: "\<S> \<noteq> {}"
proof -
  have "image_ring indexed_const R \<in> extensions"
  proof (auto simp add: extensions_def)
    show "field (image_ring indexed_const R)"
      using inj_imp_image_ring_is_field[OF indexed_const_inj_on] .
  next
    show "indexed_const \<in> ring_hom R (image_ring indexed_const R)"
      using inj_imp_image_ring_iso[OF indexed_const_inj_on] unfolding ring_iso_def by auto
  next
    fix \<P> :: "('a list multiset) \<Rightarrow> 'a" and P
    assume "\<P> \<in> carrier (image_ring indexed_const R)"
    then obtain k where "k \<in> carrier R" and "\<P> = indexed_const k"
      unfolding image_ring_carrier by blast
    hence "index_free \<P> P" for P
      unfolding index_free_def indexed_const_def by auto
    thus "\<not> index_free \<P> P \<Longrightarrow> \<X>\<^bsub>P\<^esub> \<in> carrier (image_ring indexed_const R)"
     and "\<not> index_free \<P> P \<Longrightarrow> ring.eval (image_ring indexed_const R) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>image_ring indexed_const R\<^esub>"
      by auto
    from \<open>k \<in> carrier R\<close> and \<open>\<P> = indexed_const k\<close> show "carrier_coeff \<P>"
      unfolding indexed_const_def carrier_coeff_def by auto
  qed
  thus ?thesis
    by blast
qed

subsection \<open>Chains\<close>

definition union_ring :: "(('a, 'c) ring_scheme) set \<Rightarrow> 'a ring"
  where "union_ring C =
           \<lparr> carrier = (\<Union>(carrier ` C)),
         monoid.mult = (\<lambda>a b. (monoid.mult (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b)),
                 one = one (SOME R. R \<in> C),
                zero = zero (SOME R. R \<in> C),
                 add = (\<lambda>a b. (add (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b)) \<rparr>"

lemma union_ring_carrier: "carrier (union_ring C) = (\<Union>(carrier ` C))"
  unfolding union_ring_def by simp

context
  fixes C :: "'a ring set"
  assumes field_chain: "\<And>R. R \<in> C \<Longrightarrow> field R" and chain: "\<And>R S. \<lbrakk> R \<in> C; S \<in> C \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
begin

lemma ring_chain: "R \<in> C \<Longrightarrow> ring R"
  using field.is_ring[OF field_chain] by blast

lemma same_one_same_zero:
  assumes "R \<in> C" shows "\<one>\<^bsub>union_ring C\<^esub> = \<one>\<^bsub>R\<^esub>" and "\<zero>\<^bsub>union_ring C\<^esub> = \<zero>\<^bsub>R\<^esub>"
proof -
  have "\<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>" if "R \<in> C" and "S \<in> C" for R S
    using ring_hom_one[of id] chain[OF that] unfolding iso_incl.simps by auto
  moreover have "\<zero>\<^bsub>R\<^esub> = \<zero>\<^bsub>S\<^esub>" if "R \<in> C" and "S \<in> C" for R S
    using chain[OF that] ring_hom_zero[OF _ ring_chain ring_chain] that unfolding iso_incl.simps by auto
  ultimately have "one (SOME R. R \<in> C) = \<one>\<^bsub>R\<^esub>" and "zero (SOME R. R \<in> C) = \<zero>\<^bsub>R\<^esub>"
    using assms by (metis (mono_tags) someI)+
  thus "\<one>\<^bsub>union_ring C\<^esub> = \<one>\<^bsub>R\<^esub>" and "\<zero>\<^bsub>union_ring C\<^esub> = \<zero>\<^bsub>R\<^esub>"
    unfolding union_ring_def by auto
qed

lemma same_laws:
  assumes "R \<in> C" and "a \<in> carrier R" and "b \<in> carrier R"
  shows "a \<otimes>\<^bsub>union_ring C\<^esub> b = a \<otimes>\<^bsub>R\<^esub> b" and "a \<oplus>\<^bsub>union_ring C\<^esub> b = a \<oplus>\<^bsub>R\<^esub> b"
proof -
  have "a \<otimes>\<^bsub>R\<^esub> b = a \<otimes>\<^bsub>S\<^esub> b"
    if "R \<in> C" "a \<in> carrier R" "b \<in> carrier R" and "S \<in> C" "a \<in> carrier S" "b \<in> carrier S" for R S
    using ring_hom_memE(2)[of id R S] ring_hom_memE(2)[of id S R] that chain[OF that(1,4)]
    unfolding iso_incl.simps by auto
  moreover have "a \<oplus>\<^bsub>R\<^esub> b = a \<oplus>\<^bsub>S\<^esub> b"
    if "R \<in> C" "a \<in> carrier R" "b \<in> carrier R" and "S \<in> C" "a \<in> carrier S" "b \<in> carrier S" for R S
    using ring_hom_memE(3)[of id R S] ring_hom_memE(3)[of id S R] that chain[OF that(1,4)]
    unfolding iso_incl.simps by auto
  ultimately
  have "monoid.mult (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b = a \<otimes>\<^bsub>R\<^esub> b"
   and         "add (SOME R. R \<in> C \<and> a \<in> carrier R \<and> b \<in> carrier R) a b = a \<oplus>\<^bsub>R\<^esub> b"
    using assms by (metis (mono_tags, lifting) someI)+
  thus "a \<otimes>\<^bsub>union_ring C\<^esub> b = a \<otimes>\<^bsub>R\<^esub> b" and "a \<oplus>\<^bsub>union_ring C\<^esub> b = a \<oplus>\<^bsub>R\<^esub> b"
    unfolding union_ring_def by auto
qed

lemma exists_superset_carrier:
  assumes "finite S" and "S \<noteq> {}" and "S \<subseteq> carrier (union_ring C)"
  shows "\<exists>R \<in> C. S \<subseteq> carrier R"
  using assms
proof (induction, simp)
  case (insert s S)
  obtain R where R: "s \<in> carrier R" "R \<in> C"
    using insert(5) unfolding union_ring_def by auto
  show ?case
  proof (cases)
    assume "S = {}" thus ?thesis
      using R by blast
  next
    assume "S \<noteq> {}"
    then obtain T where T: "S \<subseteq> carrier T" "T \<in> C"
      using insert(3,5) by blast
    have "carrier R \<subseteq> carrier T \<or> carrier T \<subseteq> carrier R"
      using ring_hom_memE(1)[of id R] ring_hom_memE(1)[of id T] chain[OF R(2) T(2)]
      unfolding iso_incl.simps by auto
    thus ?thesis
      using R T by auto
  qed
qed

lemma union_ring_is_monoid:
  assumes "C \<noteq> {}" shows "comm_monoid (union_ring C)"
proof
  fix a b c
  assume "a \<in> carrier (union_ring C)" "b \<in> carrier (union_ring C)" "c \<in> carrier (union_ring C)"
  then obtain R where R: "R \<in> C" "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
    using exists_superset_carrier[of "{ a, b, c }"] by auto
  then interpret field R
    using field_chain by simp

  show "a \<otimes>\<^bsub>union_ring C\<^esub> b \<in> carrier (union_ring C)"
    using R(1-3) unfolding same_laws(1)[OF R(1-3)] unfolding union_ring_def by auto
  show "(a \<otimes>\<^bsub>union_ring C\<^esub> b) \<otimes>\<^bsub>union_ring C\<^esub> c = a \<otimes>\<^bsub>union_ring C\<^esub> (b \<otimes>\<^bsub>union_ring C\<^esub> c)"
   and "a \<otimes>\<^bsub>union_ring C\<^esub> b = b \<otimes>\<^bsub>union_ring C\<^esub> a"
   and "\<one>\<^bsub>union_ring C\<^esub> \<otimes>\<^bsub>union_ring C\<^esub> a = a"
   and "a \<otimes>\<^bsub>union_ring C\<^esub> \<one>\<^bsub>union_ring C\<^esub> = a"
    using same_one_same_zero[OF R(1)] same_laws(1)[OF R(1)] R(2-4) m_assoc m_comm by auto
next
  show "\<one>\<^bsub>union_ring C\<^esub> \<in> carrier (union_ring C)"
    using ring.ring_simprules(6)[OF ring_chain] assms same_one_same_zero(1)
    unfolding union_ring_carrier by auto
qed

lemma union_ring_is_abelian_group:
  assumes "C \<noteq> {}" shows "cring (union_ring C)"
proof (rule cringI[OF abelian_groupI union_ring_is_monoid[OF assms]])
  fix a b c
  assume "a \<in> carrier (union_ring C)" "b \<in> carrier (union_ring C)" "c \<in> carrier (union_ring C)"
  then obtain R where R: "R \<in> C" "a \<in> carrier R" "b \<in> carrier R" "c \<in> carrier R"
    using exists_superset_carrier[of "{ a, b, c }"] by auto
  then interpret field R
    using field_chain by simp

  show "a \<oplus>\<^bsub>union_ring C\<^esub> b \<in> carrier (union_ring C)"
    using R(1-3) unfolding same_laws(2)[OF R(1-3)] unfolding union_ring_def by auto
  show "(a \<oplus>\<^bsub>union_ring C\<^esub> b) \<otimes>\<^bsub>union_ring C\<^esub> c = (a \<otimes>\<^bsub>union_ring C\<^esub> c) \<oplus>\<^bsub>union_ring C\<^esub> (b \<otimes>\<^bsub>union_ring C\<^esub> c)"
   and "(a \<oplus>\<^bsub>union_ring C\<^esub> b) \<oplus>\<^bsub>union_ring C\<^esub> c = a \<oplus>\<^bsub>union_ring C\<^esub> (b \<oplus>\<^bsub>union_ring C\<^esub> c)"
   and "a \<oplus>\<^bsub>union_ring C\<^esub> b = b \<oplus>\<^bsub>union_ring C\<^esub> a"
   and "\<zero>\<^bsub>union_ring C\<^esub> \<oplus>\<^bsub>union_ring C\<^esub> a = a"
    using same_one_same_zero[OF R(1)] same_laws[OF R(1)] R(2-4) l_distr a_assoc a_comm by auto
  have "\<exists>a' \<in> carrier R. a' \<oplus>\<^bsub>union_ring C\<^esub> a = \<zero>\<^bsub>union_ring C\<^esub>"
    using same_laws(2)[OF R(1)] R(2) same_one_same_zero[OF R(1)] by simp
  with \<open>R \<in> C\<close> show "\<exists>y \<in> carrier (union_ring C). y \<oplus>\<^bsub>union_ring C\<^esub> a = \<zero>\<^bsub>union_ring C\<^esub>"
    unfolding union_ring_carrier by auto
next
  show "\<zero>\<^bsub>union_ring C\<^esub> \<in> carrier (union_ring C)"
    using ring.ring_simprules(2)[OF ring_chain] assms same_one_same_zero(2)
    unfolding union_ring_carrier by auto
qed

lemma union_ring_is_field :
  assumes "C \<noteq> {}" shows "field (union_ring C)"
proof (rule cring.cring_fieldI[OF union_ring_is_abelian_group[OF assms]])
  have "carrier (union_ring C) - { \<zero>\<^bsub>union_ring C\<^esub> } \<subseteq> Units (union_ring C)"
  proof
    fix a assume "a \<in> carrier (union_ring C) - { \<zero>\<^bsub>union_ring C\<^esub> }"
    hence "a \<in> carrier (union_ring C)" and "a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>"
      by auto
    then obtain R where R: "R \<in> C" "a \<in> carrier R"
      using exists_superset_carrier[of "{ a }"] by auto
    then interpret field R
      using field_chain by simp

    from \<open>a \<in> carrier R\<close> and \<open>a \<noteq> \<zero>\<^bsub>union_ring C\<^esub>\<close> have "a \<in> Units R"
      unfolding same_one_same_zero[OF R(1)] field_Units by auto
    hence "\<exists>a' \<in> carrier R. a' \<otimes>\<^bsub>union_ring C\<^esub> a = \<one>\<^bsub>union_ring C\<^esub> \<and> a \<otimes>\<^bsub>union_ring C\<^esub> a' = \<one>\<^bsub>union_ring C\<^esub>"
      using same_laws[OF R(1)] same_one_same_zero[OF R(1)] R(2) unfolding Units_def by auto
    with \<open>R \<in> C\<close> and \<open>a \<in> carrier (union_ring C)\<close> show "a \<in> Units (union_ring C)"
      unfolding Units_def union_ring_carrier by auto
  qed
  moreover have "\<zero>\<^bsub>union_ring C\<^esub> \<notin> Units (union_ring C)"
  proof (rule ccontr)
    assume "\<not> \<zero>\<^bsub>union_ring C\<^esub> \<notin> Units (union_ring C)"
    then obtain a where a: "a \<in> carrier (union_ring C)" "a \<otimes>\<^bsub>union_ring C\<^esub> \<zero>\<^bsub>union_ring C\<^esub> = \<one>\<^bsub>union_ring C\<^esub>"
      unfolding Units_def by auto
    then obtain R where R: "R \<in> C" "a \<in> carrier R"
      using exists_superset_carrier[of "{ a }"] by auto
    then interpret field R
      using field_chain by simp
    have "\<one>\<^bsub>R\<^esub> = \<zero>\<^bsub>R\<^esub>"
      using a R same_laws(1)[OF R(1)] same_one_same_zero[OF R(1)] by auto
    thus False
      using one_not_zero by simp
  qed
  hence "Units (union_ring C) \<subseteq> carrier (union_ring C) - { \<zero>\<^bsub>union_ring C\<^esub> }"
    unfolding Units_def by auto
  ultimately show "Units (union_ring C) = carrier (union_ring C) - { \<zero>\<^bsub>union_ring C\<^esub> }"
    by simp
qed

lemma union_ring_is_upper_bound:
  assumes "R \<in> C" shows "R \<lesssim> union_ring C"
  using ring_hom_memI[of R id "union_ring C"] same_laws[of R] same_one_same_zero[of R] assms
  unfolding union_ring_carrier by auto

end

subsection \<open>Zorn\<close>

lemma (in ring) exists_core_chain:
  assumes "C \<in> Chains (rel_of (\<lesssim>) \<S>)" obtains C' where "C' \<subseteq> extensions" and "C = law_restrict ` C'"
  using Chains_rel_of[OF assms] by (meson subset_image_iff)

lemma (in ring) core_chain_is_chain:
  assumes "law_restrict ` C \<in> Chains (rel_of (\<lesssim>) \<S>)" shows "\<And>R S. \<lbrakk> R \<in> C; S \<in> C \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
proof -
  fix R S assume "R \<in> C" and "S \<in> C" thus "R \<lesssim> S \<or> S \<lesssim> R"
    using assms(1) unfolding iso_incl_hom[of R] iso_incl_hom[of S] Chains_def by auto
qed

lemma (in field) exists_maximal_extension:
  shows "\<exists>M \<in> \<S>. \<forall>L \<in> \<S>. M \<lesssim> L \<longrightarrow> L = M"
proof (rule predicate_Zorn[OF iso_incl_partial_order])
  show "\<forall>C \<in> Chains (rel_of (\<lesssim>) \<S>). \<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
  proof
    fix C assume C: "C \<in> Chains (rel_of (\<lesssim>) \<S>)"
    show "\<exists>L \<in> \<S>. \<forall>R \<in> C. R \<lesssim> L"
    proof (cases)
      assume "C = {}" thus ?thesis
        using extensions_non_empty by auto
    next
      assume "C \<noteq> {}"
      from \<open>C \<in> Chains (rel_of (\<lesssim>) \<S>)\<close>
      obtain C' where C': "C' \<subseteq> extensions" "C = law_restrict ` C'"
        using exists_core_chain by auto
      with \<open>C \<noteq> {}\<close> obtain S where S: "S \<in> C'" and "C' \<noteq> {}"
        by auto

      have core_chain: "\<And>R. R \<in> C' \<Longrightarrow> field R" "\<And>R S. \<lbrakk> R \<in> C'; S \<in> C' \<rbrakk> \<Longrightarrow> R \<lesssim> S \<or> S \<lesssim> R"
        using core_chain_is_chain[of C'] C' C unfolding extensions_def by auto
      from \<open>C' \<noteq> {}\<close> interpret Union: field "union_ring C'"
          using union_ring_is_field[OF core_chain] C'(1) by blast

      have "union_ring C' \<in> extensions"
      proof (auto simp add: extensions_def)
        show "field (union_ring C')"
          using Union.field_axioms .
      next
        from \<open>S \<in> C'\<close> have "indexed_const \<in> ring_hom R S"
          using C'(1) unfolding extensions_def by auto
        thus "indexed_const \<in> ring_hom R (union_ring C')"
          using ring_hom_trans[of _ R S id] union_ring_is_upper_bound[OF core_chain S]
          unfolding iso_incl.simps by auto
      next
        show "a \<in> carrier (union_ring C') \<Longrightarrow> carrier_coeff a" for a
          using C'(1) unfolding union_ring_carrier extensions_def by auto
      next
        fix \<P> P
        assume "\<P> \<in> carrier (union_ring C')" and P: "P \<in> carrier (poly_ring R)" "\<not> index_free \<P> P"
        from \<open>\<P> \<in> carrier (union_ring C')\<close> obtain T where T: "T \<in> C'" "\<P> \<in> carrier T"
          using exists_superset_carrier[of C' "{ \<P> }"] core_chain by auto
        hence "\<X>\<^bsub>P\<^esub> \<in> carrier T" and "(ring.eval T) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>T\<^esub>"
          and field: "field T" and hom: "indexed_const \<in> ring_hom R T"
          using P C'(1) unfolding extensions_def by auto
        with \<open>T \<in> C'\<close> show "\<X>\<^bsub>P\<^esub> \<in> carrier (union_ring C')"
          unfolding union_ring_carrier by auto
        have "set P \<subseteq> carrier R"
          using P(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
        hence "set (\<sigma> P) \<subseteq> carrier T"
          using ring_hom_memE(1)[OF hom] unfolding \<sigma>_def by (induct P) (auto)
        with \<open>\<X>\<^bsub>P\<^esub> \<in> carrier T\<close> and \<open>(ring.eval T) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>T\<^esub>\<close>
        show "(ring.eval (union_ring C')) (\<sigma> P) \<X>\<^bsub>P\<^esub> = \<zero>\<^bsub>union_ring C'\<^esub>"
          using iso_incl_imp_same_eval[OF field.is_ring[OF field] Union.is_ring
                union_ring_is_upper_bound[OF core_chain T(1)]] same_one_same_zero(2)[OF core_chain T(1)]
          by auto
      qed
      moreover have "R \<lesssim> law_restrict (union_ring C')" if "R \<in> C" for R
        using that union_ring_is_upper_bound[OF core_chain] iso_incl_hom unfolding C' by auto
      ultimately show ?thesis
        by blast
    qed
  qed
qed

subsection \<open>Existence of roots\<close>

lemma polynomial_hom:
  assumes "h \<in> ring_hom R S" and "field R" and "field S"
  shows "p \<in> carrier (poly_ring R) \<Longrightarrow> (map h p) \<in> carrier (poly_ring S)"
proof -
  assume "p \<in> carrier (poly_ring R)"
  interpret ring_hom_ring R S h
    using ring_hom_ringI2[OF assms(2-3)[THEN field.is_ring] assms(1)] .

  from \<open>p \<in> carrier (poly_ring R)\<close> have "set p \<subseteq> carrier R" and lc: "p \<noteq> [] \<Longrightarrow> lead_coeff p \<noteq> \<zero>\<^bsub>R\<^esub>"
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence "set (map h p) \<subseteq> carrier S"
    by (induct p) (auto)
  moreover have "h a = \<zero>\<^bsub>S\<^esub> \<Longrightarrow> a = \<zero>\<^bsub>R\<^esub>" if "a \<in> carrier R" for a
    using non_trivial_field_hom_is_inj[OF assms(1-3)] that unfolding inj_on_def by simp
  with \<open>set p \<subseteq> carrier R\<close> have "lead_coeff (map h p) \<noteq> \<zero>\<^bsub>S\<^esub>" if "p \<noteq> []"
    using lc[OF that] that by (cases p) (auto)
  ultimately show ?thesis
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
qed

lemma (in ring_hom_ring) subfield_polynomial_hom:
  assumes "subfield K R" and "\<one>\<^bsub>S\<^esub> \<noteq> \<zero>\<^bsub>S\<^esub>"
  shows "p \<in> carrier (K[X]\<^bsub>R\<^esub>) \<Longrightarrow> (map h p) \<in> carrier ((h ` K)[X]\<^bsub>S\<^esub>)"
proof -
  assume "p \<in> carrier (K[X]\<^bsub>R\<^esub>)"
  hence "p \<in> carrier (poly_ring (R \<lparr> carrier := K \<rparr>))"
    using R.univ_poly_consistent[OF subfieldE(1)[OF assms(1)]] by simp
  moreover have "h \<in> ring_hom (R \<lparr> carrier := K \<rparr>) (S \<lparr> carrier := h ` K \<rparr>)"
    using hom_mult subfieldE(3)[OF assms(1)] unfolding ring_hom_def subset_iff by auto
  moreover have "field (R \<lparr> carrier := K \<rparr>)" and "field (S \<lparr> carrier := (h ` K) \<rparr>)"
    using R.subfield_iff(2)[OF assms(1)] S.subfield_iff(2)[OF img_is_subfield(2)[OF assms]] by simp+
  ultimately have "(map h p) \<in> carrier (poly_ring (S \<lparr> carrier := h ` K \<rparr>))"
    using polynomial_hom[of h "R \<lparr> carrier := K \<rparr>" "S \<lparr> carrier := h ` K \<rparr>"] by auto
  thus ?thesis
    using S.univ_poly_consistent[OF subfieldE(1)[OF img_is_subfield(2)[OF assms]]] by simp
qed

lemma (in field) exists_root:
  assumes "M \<in> extensions" and "\<And>L. \<lbrakk> L \<in> extensions; M \<lesssim> L \<rbrakk> \<Longrightarrow> law_restrict L = law_restrict M"
    and "P \<in> carrier (poly_ring R)" and "degree P > 0"
  shows "\<exists>x \<in> carrier M. (ring.eval M) (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>"
proof (rule ccontr)
  from \<open>M \<in> extensions\<close> interpret M: field M + Hom: ring_hom_ring R M "indexed_const"
    using ring_hom_ringI2[OF ring_axioms field.is_ring] unfolding extensions_def by auto
  interpret UP: principal_domain "poly_ring M"
    using M.univ_poly_is_principal[OF M.carrier_is_subfield] .

  assume no_roots: "\<not> (\<exists>x \<in> carrier M. M.eval (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>)"
  have "(\<sigma> P) \<in> carrier (poly_ring M)"
    using polynomial_hom[OF Hom.homh field_axioms M.field_axioms assms(3)] unfolding \<sigma>_def by simp
  moreover have "(\<sigma> P) \<notin> Units (poly_ring M)" and "(\<sigma> P) \<noteq> \<zero>\<^bsub>poly_ring M\<^esub>"
    using assms(4) unfolding M.univ_poly_carrier_units \<sigma>_def univ_poly_zero by auto
  ultimately obtain Q
    where Q: "Q \<in> carrier (poly_ring M)" "pirreducible\<^bsub>M\<^esub> (carrier M) Q" "Q pdivides\<^bsub>M\<^esub> (\<sigma> P)"
    using UP.exists_irreducible_divisor[of "\<sigma> P"] unfolding pdivides_def by blast

  have hyps:
    \<comment> \<open>i\<close>   "field M"
    \<comment> \<open>ii\<close>  "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> carrier_coeff \<P>"
    \<comment> \<open>iii\<close> "\<And>\<P>. \<P> \<in> carrier M \<Longrightarrow> index_free \<P> P"
    \<comment> \<open>iv\<close>  "\<zero>\<^bsub>M\<^esub> = indexed_const \<zero>"
    using assms(1,3) no_roots unfolding extensions_def by auto
  have degree_gt: "degree Q > 1"
  proof (rule ccontr)
    assume "\<not> degree Q > 1" hence "degree Q = 1"
      using M.pirreducible_degree[OF M.carrier_is_subfield Q(1-2)] by simp
    then obtain x where "x \<in> carrier M" and "M.eval Q x = \<zero>\<^bsub>M\<^esub>"
      using M.degree_one_root[OF M.carrier_is_subfield Q(1)] M.add.inv_closed by blast
    hence "M.eval (\<sigma> P) x = \<zero>\<^bsub>M\<^esub>"
      using M.pdivides_imp_root_sharing[OF Q(1,3)] by simp
    with \<open>x \<in> carrier M\<close> show False
      using no_roots by simp
  qed

  define image_poly where "image_poly = image_ring (eval_pmod M P Q) (poly_ring M)"
  with \<open>degree Q > 1\<close> have "M \<lesssim> image_poly"
    using image_poly_iso_incl[OF hyps Q(1)] by auto
  moreover have is_field: "field image_poly"
    using image_poly_is_field[OF hyps Q(1-2)] unfolding image_poly_def by simp
  moreover have "image_poly \<in> extensions"
  proof (auto simp add: extensions_def is_field)
    fix \<P> assume "\<P> \<in> carrier image_poly"
    then obtain R where \<P>: "\<P> = eval_pmod M P Q R" and "R \<in> carrier (poly_ring M)"
      unfolding image_poly_def image_ring_carrier by auto
    hence "M.pmod R Q \<in> carrier (poly_ring M)"
      using M.long_division_closed(2)[OF M.carrier_is_subfield _ Q(1)] by simp
    hence "list_all carrier_coeff (M.pmod R Q)"
      using hyps(2) unfolding sym[OF univ_poly_carrier] list_all_iff polynomial_def by auto
    thus "carrier_coeff \<P>"
      using indexed_eval_in_carrier[of "M.pmod R Q"] unfolding \<P> by simp
  next
    from \<open>M \<lesssim> image_poly\<close> show "indexed_const \<in> ring_hom R image_poly"
      using ring_hom_trans[OF Hom.homh, of id] unfolding iso_incl.simps by simp
  next
    from \<open>M \<lesssim> image_poly\<close> interpret Id: ring_hom_ring M image_poly id
      using iso_inclE[OF M.ring_axioms field.is_ring[OF is_field]] by simp

    fix \<P> S
    assume A: "\<P> \<in> carrier image_poly" "\<not> index_free \<P> S" "S \<in> carrier (poly_ring R)"
    have "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly \<and> Id.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
    proof (cases)
      assume "P \<noteq> S"
      then obtain Q' where "Q' \<in> carrier M" and "\<not> index_free Q' S"
        using A(1) image_poly_index_free[OF hyps Q(1) _ A(2)] unfolding image_poly_def by auto
      hence "\<X>\<^bsub>S\<^esub> \<in> carrier M" and "M.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>M\<^esub>"
        using assms(1) A(3) unfolding extensions_def by auto
      moreover have "\<sigma> S \<in> carrier (poly_ring M)"
        using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \<sigma>_def .
      ultimately show ?thesis
        using Id.eval_hom[OF M.carrier_is_subring] Id.hom_closed Id.hom_zero by auto
    next
      assume "\<not> P \<noteq> S" hence S: "P = S"
        by simp
      have poly_hom: "R \<in> carrier (poly_ring image_poly)" if "R \<in> carrier (poly_ring M)" for R
        using polynomial_hom[OF Id.homh M.field_axioms is_field that] by simp
      have "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly"
        using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def S by simp
      moreover have "Id.eval Q \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
        using image_poly_eval_indexed_var[OF hyps Hom.homh Q(1) degree_gt Q(2)] unfolding image_poly_def S by simp
      moreover have "Q pdivides\<^bsub>image_poly\<^esub> (\<sigma> S)"
      proof -
        obtain R where R: "R \<in> carrier (poly_ring M)" "\<sigma> S = Q \<otimes>\<^bsub>poly_ring M\<^esub> R"
          using Q(3) unfolding S pdivides_def by auto
        moreover have "set Q \<subseteq> carrier M" and "set R \<subseteq> carrier M"
          using Q(1) R(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
        ultimately have "Id.normalize (\<sigma> S) = Q \<otimes>\<^bsub>poly_ring image_poly\<^esub> R"
          using Id.poly_mult_hom'[of Q R] unfolding univ_poly_mult by simp
        moreover have "\<sigma> S \<in> carrier (poly_ring M)"
          using polynomial_hom[OF Hom.homh field_axioms M.field_axioms A(3)] unfolding \<sigma>_def .
        hence "\<sigma> S \<in> carrier (poly_ring image_poly)"
          using polynomial_hom[OF Id.homh M.field_axioms is_field] by simp
        hence "Id.normalize (\<sigma> S) = \<sigma> S"
          using Id.normalize_polynomial unfolding sym[OF univ_poly_carrier] by simp
        ultimately show ?thesis
          using poly_hom[OF Q(1)] poly_hom[OF R(1)]
          unfolding pdivides_def factor_def univ_poly_mult by auto
      qed
      moreover have "Q \<in> carrier (poly_ring (image_poly))"
        using poly_hom[OF Q(1)] by simp
      ultimately show ?thesis
        using domain.pdivides_imp_root_sharing[OF field.axioms(1)[OF is_field], of Q] by auto
    qed
    thus "\<X>\<^bsub>S\<^esub> \<in> carrier image_poly" and "Id.eval (\<sigma> S) \<X>\<^bsub>S\<^esub> = \<zero>\<^bsub>image_poly\<^esub>"
      by auto
  qed
  ultimately have "law_restrict M = law_restrict image_poly"
    using assms(2) by simp
  hence "carrier M = carrier image_poly"
    unfolding law_restrict_def by (simp add:ring.defs)
  moreover have "\<X>\<^bsub>P\<^esub> \<in> carrier image_poly"
    using eval_pmod_var(2)[OF hyps Hom.homh Q(1) degree_gt] unfolding image_poly_def by simp
  moreover have "\<X>\<^bsub>P\<^esub> \<notin> carrier M"
    using indexed_var_not_index_free[of P] hyps(3) by blast
  ultimately show False by simp
qed

lemma (in field) exists_extension_with_roots:
  shows "\<exists>L \<in> extensions. \<forall>P \<in> carrier (poly_ring R).
    degree P > 0 \<longrightarrow> (\<exists>x \<in> carrier L. (ring.eval L) (\<sigma> P) x = \<zero>\<^bsub>L\<^esub>)"
proof -
  obtain M where "M \<in> extensions" and "\<forall>L \<in> extensions. M \<lesssim> L \<longrightarrow> law_restrict L = law_restrict M"
    using exists_maximal_extension iso_incl_hom by blast
  thus ?thesis
    using exists_root[of M] by auto
qed

subsection \<open>Existence of Algebraic Closure\<close>

locale algebraic_closure = field L + subfield K L for L (structure) and K +
  assumes algebraic_extension: "x \<in> carrier L \<Longrightarrow> (algebraic over K) x"
    and roots_over_subfield: "\<lbrakk> P \<in> carrier (K[X]); degree P > 0 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier L. eval P x = \<zero>\<^bsub>L\<^esub>"

locale algebraically_closed = field L for L (structure) +
  assumes roots_over_carrier: "\<lbrakk> P \<in> carrier (poly_ring L); degree P > 0 \<rbrakk> \<Longrightarrow> \<exists>x \<in> carrier L. eval P x = \<zero>\<^bsub>L\<^esub>"

definition (in field) closure :: "(('a list) multiset \<Rightarrow> 'a) ring" ("\<Omega>")
  where "closure = (SOME L \<comment> \<open>such that\<close>.
           \<comment> \<open>i\<close>  algebraic_closure L (indexed_const ` (carrier R)) \<and>
           \<comment> \<open>ii\<close> indexed_const \<in> ring_hom R L)"

lemma algebraic_hom:
  assumes "h \<in> ring_hom R S" and "field R" and "field S" and "subfield K R" and "x \<in> carrier R"
  shows "((ring.algebraic R) over K) x \<Longrightarrow> ((ring.algebraic S) over (h ` K)) (h x)"
proof -
  interpret Hom: ring_hom_ring R S h
    using ring_hom_ringI2[OF assms(2-3)[THEN field.is_ring] assms(1)] .
  assume "(Hom.R.algebraic over K) x"
  then obtain p where p: "p \<in> carrier (K[X]\<^bsub>R\<^esub>)" and "p \<noteq> []" and eval: "Hom.R.eval p x = \<zero>\<^bsub>R\<^esub>"
    using domain.algebraicE[OF field.axioms(1) subfieldE(1), of R K x] assms(2,4-5) by auto
  hence "(map h p) \<in> carrier ((h ` K)[X]\<^bsub>S\<^esub>)" and "(map h p) \<noteq> []"
    using Hom.subfield_polynomial_hom[OF assms(4) one_not_zero[OF assms(3)]] by auto
  moreover have "Hom.S.eval (map h p) (h x) = \<zero>\<^bsub>S\<^esub>"
    using Hom.eval_hom[OF subfieldE(1)[OF assms(4)] assms(5) p] unfolding eval by simp
  ultimately show ?thesis
    using Hom.S.non_trivial_ker_imp_algebraic[of "h ` K" "h x"] unfolding a_kernel_def' by auto
qed

lemma (in field) exists_closure:
  obtains L :: "(('a list multiset) \<Rightarrow> 'a) ring"
  where "algebraic_closure L (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R L"
proof -
  obtain L where "L \<in> extensions"
    and roots: "\<And>P. \<lbrakk> P \<in> carrier (poly_ring R); degree P > 0 \<rbrakk> \<Longrightarrow>
                      \<exists>x \<in> carrier L. (ring.eval L) (\<sigma> P) x = \<zero>\<^bsub>L\<^esub>"
    using exists_extension_with_roots by auto

  let ?K = "indexed_const ` (carrier R)"
  let ?set_of_algs = "{ x \<in> carrier L. ((ring.algebraic L) over ?K) x }"
  let ?M = "L \<lparr> carrier := ?set_of_algs \<rparr>"

  from \<open>L \<in> extensions\<close>
  have L: "field L" and  hom: "ring_hom_ring R L indexed_const"
    using ring_hom_ringI2[OF ring_axioms field.is_ring] unfolding extensions_def by auto
  have "subfield ?K L"
    using ring_hom_ring.img_is_subfield(2)[OF hom carrier_is_subfield
          domain.one_not_zero[OF field.axioms(1)[OF L]]] by auto
  hence set_of_algs: "subfield ?set_of_algs L"
    using field.subfield_of_algebraics[OF L, of ?K] by simp
  have M: "field ?M"
    using ring.subfield_iff(2)[OF field.is_ring[OF L] set_of_algs] by simp

  interpret Id: ring_hom_ring ?M L id
    using ring_hom_ringI[OF field.is_ring[OF M] field.is_ring[OF L]] by auto

  have is_subfield: "subfield ?K ?M"
  proof (intro ring.subfield_iff(1)[OF field.is_ring[OF M]])
    have "L \<lparr> carrier := ?K \<rparr> = ?M \<lparr> carrier := ?K \<rparr>"
      by simp
    moreover from \<open>subfield ?K L\<close> have "field (L \<lparr> carrier := ?K \<rparr>)"
      using ring.subfield_iff(2)[OF field.is_ring[OF L]] by simp
    ultimately show "field (?M \<lparr> carrier := ?K \<rparr>)"
      by simp
  next
    show "?K \<subseteq> carrier ?M"
    proof
      fix x :: "('a list multiset) \<Rightarrow> 'a"
      assume "x \<in> ?K"
      hence "x \<in> carrier L"
        using ring_hom_memE(1)[OF ring_hom_ring.homh[OF hom]] by auto
      moreover from \<open>subfield ?K L\<close> and \<open>x \<in> ?K\<close> have "(Id.S.algebraic over ?K) x"
        using domain.algebraic_self[OF field.axioms(1)[OF L] subfieldE(1)] by auto
      ultimately show "x \<in> carrier ?M"
        by auto
    qed
  qed

  have "algebraic_closure ?M ?K"
  proof (intro algebraic_closure.intro[OF M is_subfield])
    have "(Id.R.algebraic over ?K) x" if "x \<in> carrier ?M" for x
      using that Id.S.algebraic_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
    moreover have "\<exists>x \<in> carrier ?M. Id.R.eval P x = \<zero>\<^bsub>?M\<^esub>"
      if "P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)" and "degree P > 0" for P
    proof -
      from \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> have "P \<in> carrier (?K[X]\<^bsub>L\<^esub>)"
        unfolding Id.S.univ_poly_consistent[OF subfieldE(1)[OF set_of_algs]] .
      hence "set P \<subseteq> ?K"
        unfolding sym[OF univ_poly_carrier] polynomial_def by auto
      hence "\<exists>Q. set Q \<subseteq> carrier R \<and> P = \<sigma> Q"
      proof (induct P, simp add: \<sigma>_def)
        case (Cons p P)
        then obtain q Q where "q \<in> carrier R" "set Q \<subseteq> carrier R" and "\<sigma> Q = P""indexed_const q = p"
          unfolding \<sigma>_def by auto
        hence "set (q # Q) \<subseteq> carrier R" and "\<sigma> (q # Q) = (p # P)"
          unfolding \<sigma>_def by auto
        thus ?case
          by metis
      qed
      then obtain Q where "set Q \<subseteq> carrier R" and "\<sigma> Q = P"
        by auto
      moreover have "lead_coeff Q \<noteq> \<zero>"
      proof (rule ccontr)
        assume "\<not> lead_coeff Q \<noteq> \<zero>" then have "lead_coeff Q = \<zero>"
          by simp
        with \<open>\<sigma> Q = P\<close> and \<open>degree P > 0\<close> have "lead_coeff P = indexed_const \<zero>"
          unfolding \<sigma>_def degree_def lead_coeff_def
          by (metis diff_0_eq_0 length_map less_irrefl_nat list.map_sel(1) list.size(3))
        hence "lead_coeff P = \<zero>\<^bsub>L\<^esub>"
          using ring_hom_zero[OF ring_hom_ring.homh ring_hom_ring.axioms(1-2)] hom by auto
        with \<open>degree P > 0\<close> have "\<not> P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)"
          unfolding sym[OF univ_poly_carrier] polynomial_def by auto
        with \<open>P \<in> carrier (?K[X]\<^bsub>?M\<^esub>)\<close> show False
          by simp
      qed
      ultimately have "Q \<in> carrier (poly_ring R)"
        unfolding sym[OF univ_poly_carrier] polynomial_def by auto
      moreover from \<open>degree P > 0\<close> and \<open>\<sigma> Q = P\<close> have "degree Q > 0"
        unfolding \<sigma>_def by auto
      ultimately obtain x where "x \<in> carrier L" and "Id.S.eval P x = \<zero>\<^bsub>L\<^esub>"
        using roots[of Q] unfolding \<open>\<sigma> Q = P\<close> by auto
      hence "Id.R.eval P x = \<zero>\<^bsub>?M\<^esub>"
        unfolding Id.S.eval_consistent[OF subfieldE(1)[OF set_of_algs]] by simp
      moreover from \<open>degree P > 0\<close> have "P \<noteq> []"
        by auto
      with \<open>P \<in> carrier (?K[X]\<^bsub>L\<^esub>)\<close> and \<open>Id.S.eval P x = \<zero>\<^bsub>L\<^esub>\<close> have "(Id.S.algebraic over ?K) x"
        using Id.S.non_trivial_ker_imp_algebraic[of ?K x] unfolding a_kernel_def' by auto
      with \<open>x \<in> carrier L\<close> have "x \<in> carrier ?M"
        by auto
      ultimately show ?thesis
        by auto
    qed
    ultimately show "algebraic_closure_axioms ?M ?K"
      unfolding algebraic_closure_axioms_def by auto
  qed
  moreover have "indexed_const \<in> ring_hom R ?M"
    using ring_hom_ring.homh[OF hom] subfieldE(3)[OF is_subfield]
    unfolding subset_iff ring_hom_def by auto
  ultimately show thesis
    using that by auto
qed

lemma (in field) closureE:
  shows "algebraic_closure \<Omega> (indexed_const ` (carrier R))" and "indexed_const \<in> ring_hom R \<Omega>"
  using exists_closure unfolding closure_def
  by (metis (mono_tags, lifting) someI2)+

sublocale algebraic_closure \<subseteq> algebraically_closed
proof
  fix P assume in_carrier: "P \<in> carrier (poly_ring L)" and gt_zero: "degree P > 0"
  define A where "A = finite_extension K P"

  from \<open>P \<in> carrier (poly_ring L)\<close> have "set P \<subseteq> carrier L"
    by (simp add: polynomial_incl univ_poly_carrier)
  hence A: "subfield A L" and P: "P \<in> carrier (A[X])"
    using finite_extension_mem[OF subfieldE(1)[OF subfield_axioms], of P] in_carrier
          algebraic_extension finite_extension_is_subfield[OF subfield_axioms, of P]
    unfolding sym[OF A_def] sym[OF univ_poly_carrier] polynomial_def by auto
  from \<open>set P \<subseteq> carrier L\<close> have incl: "K \<subseteq> A"
    using finite_extension_incl[OF subfieldE(3)[OF subfield_axioms]] unfolding A_def by simp

  interpret UP_K: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF subfield_axioms]] .
  interpret UP_A: domain "A[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF A]] .
  interpret Rupt: ring "Rupt A P"
    unfolding rupture_def using ideal.quotient_is_ring[OF UP_A.cgenideal_ideal[OF P]] .
  interpret Hom: ring_hom_ring "L \<lparr> carrier := A \<rparr>" "Rupt A P" "rupture_surj A P \<circ> poly_of_const"
    using ring_hom_ringI2[OF subring_is_ring[OF subfieldE(1)] Rupt.ring_axioms
          rupture_surj_norm_is_hom[OF subfieldE(1) P]] A by simp
  let ?h = "rupture_surj A P \<circ> poly_of_const"

  have h_simp: "rupture_surj A P ` poly_of_const ` E = ?h ` E" for E
    by auto
  hence aux_lemmas:
    "subfield (rupture_surj A P ` poly_of_const ` K) (Rupt A P)"
    "subfield (rupture_surj A P ` poly_of_const ` A) (Rupt A P)"
    using Hom.img_is_subfield(2)[OF _ rupture_one_not_zero[OF A P gt_zero]]
          ring.subfield_iff(1)[OF subring_is_ring[OF subfieldE(1)[OF A]]]
          subfield_iff(2)[OF subfield_axioms] subfield_iff(2)[OF A] incl
    by auto

  have "carrier (K[X]) \<subseteq> carrier (A[X])"
    using subsetI[of "carrier (K[X])" "carrier (A[X])"] incl
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence "id \<in> ring_hom (K[X]) (A[X])"
    unfolding ring_hom_def unfolding univ_poly_mult univ_poly_add univ_poly_one by (simp add: subsetD)
  hence "rupture_surj A P \<in> ring_hom (K[X]) (Rupt A P)"
    using ring_hom_trans[OF _ rupture_surj_hom(1)[OF subfieldE(1)[OF A] P], of id] by simp
  then interpret Hom': ring_hom_ring "K[X]" "Rupt A P" "rupture_surj A P"
    using ring_hom_ringI2[OF UP_K.ring_axioms Rupt.ring_axioms] by simp

  from \<open>id \<in> ring_hom (K[X]) (A[X])\<close> have Id: "ring_hom_ring (K[X]) (A[X]) id"
    using ring_hom_ringI2[OF UP_K.ring_axioms UP_A.ring_axioms] by simp
  hence "subalgebra (poly_of_const ` K) (carrier (K[X])) (A[X])"
    using ring_hom_ring.img_is_subalgebra[OF Id _ UP_K.carrier_is_subalgebra[OF subfieldE(3)]]
          univ_poly_subfield_of_consts[OF subfield_axioms] by auto

  moreover from \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "poly_of_const ` K \<subseteq> carrier (A[X])"
    using subfieldE(3)[OF univ_poly_subfield_of_consts[OF subfield_axioms]] by simp

  ultimately
  have "subalgebra (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X])) (Rupt A P)"
    using ring_hom_ring.img_is_subalgebra[OF rupture_surj_hom(2)[OF subfieldE(1)[OF A] P]] by simp

  moreover have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (carrier (Rupt A P))"
  proof (intro Rupt.telescopic_base_dim(1)[where
            ?K = "rupture_surj A P ` poly_of_const ` K" and
            ?F = "rupture_surj A P ` poly_of_const ` A" and
            ?E = "carrier (Rupt A P)", OF aux_lemmas])
    show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` A) (carrier (Rupt A P))"
      using Rupt.finite_dimensionI[OF rupture_dimension[OF A P gt_zero]] .
  next
    let ?h = "rupture_surj A P \<circ> poly_of_const"

    from \<open>set P \<subseteq> carrier L\<close> have "finite_dimension K A"
      using finite_extension_finite_dimension(1)[OF subfield_axioms, of P] algebraic_extension
      unfolding A_def by auto
    then obtain Us where Us: "set Us \<subseteq> carrier L" "A = Span K Us"
      using exists_base subfield_axioms by blast
    hence "?h ` A = Rupt.Span (?h ` K) (map ?h Us)"
      using Hom.Span_hom[of K Us] incl Span_base_incl[OF subfield_axioms, of Us]
      unfolding Span_consistent[OF subfieldE(1)[OF A]] by simp
    moreover have "set (map ?h Us) \<subseteq> carrier (Rupt A P)"
      using Span_base_incl[OF subfield_axioms Us(1)] ring_hom_memE(1)[OF Hom.homh]
      unfolding sym[OF Us(2)] by auto
    ultimately
    show "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` poly_of_const ` A)"
      using Rupt.Span_finite_dimension[OF aux_lemmas(1)] unfolding h_simp by simp
  qed

  moreover have "rupture_surj A P ` carrier (A[X]) = carrier (Rupt A P)"
    unfolding rupture_def FactRing_def A_RCOSETS_def' by auto
  with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "rupture_surj A P ` carrier (K[X]) \<subseteq> carrier (Rupt A P)"
    by auto

  ultimately
  have "Rupt.finite_dimension (rupture_surj A P ` poly_of_const ` K) (rupture_surj A P ` carrier (K[X]))"
    using Rupt.subalbegra_incl_imp_finite_dimension[OF aux_lemmas(1)] by simp

  hence "\<not> inj_on (rupture_surj A P) (carrier (K[X]))"
    using Hom'.infinite_dimension_hom[OF _ rupture_one_not_zero[OF A P gt_zero] _
          UP_K.carrier_is_subalgebra[OF subfieldE(3)] univ_poly_infinite_dimension[OF subfield_axioms]]
          univ_poly_subfield_of_consts[OF subfield_axioms]
    by auto
  then obtain Q where "Q \<in> carrier (K[X])" and "Q \<noteq> []" and "rupture_surj A P Q = \<zero>\<^bsub>Rupt A P\<^esub>"
    using Hom'.trivial_ker_imp_inj Hom'.hom_zero unfolding a_kernel_def' univ_poly_zero by blast
  with \<open>carrier (K[X]) \<subseteq> carrier (A[X])\<close> have "Q \<in> PIdl\<^bsub>A[X]\<^esub> P"
    using ideal.rcos_const_imp_mem[OF UP_A.cgenideal_ideal[OF P]]
    unfolding rupture_def FactRing_def by auto
  then obtain R where "R \<in> carrier (A[X])" and "Q = R \<otimes>\<^bsub>A[X]\<^esub> P"
    unfolding cgenideal_def by blast
qed

end

author: DeVilhena-Paulo


text:
theory deMorgan3
  imports Main
begin

lemma deMorgan3: "(\<not>p \<or> \<not>q) \<longrightarrow> \<not>(p \<and> q)"
	apply (rule impI)
	apply (erule disjE)
	 apply (rule notI)
	 apply (erule notE)
	 apply (erule conjE)
	 apply assumption
	apply (rule notI)
	apply (erule notE)
	apply (erule conjE)
	apply assumption
	done
end

author: snigdhakalathur


text:
(*  Author:     Tobias Nipkow, 2007  *)

theory QEpres
imports PresArith
begin

subsection\<open>DNF-based quantifier elimination\<close>

(* all hd-coeffs are nonzero! *)
definition
"hd_coeffs1 as =
 (let m = zlcms(map hd_coeff as)
  in Dvd m 0 [1] # map (hd_coeff1 m) as)"

lemma I_hd_coeffs1:
assumes 0: "\<forall>a\<in>set as. hd_coeff a \<noteq> 0" shows
  "(\<exists>x. \<forall>a \<in> set(hd_coeffs1 as). I\<^sub>Z a (x#xs)) =
   (\<exists>x. \<forall>a \<in> set as. I\<^sub>Z a (x#xs))" (is "?B = ?A")
proof -
  let ?m = "zlcms(map hd_coeff as)"
  have "?m>0" using 0 by(simp add:zlcms_pos)
  have "?A = (\<exists>x. \<forall>a \<in> set as. I\<^sub>Z (hd_coeff1 ?m a) (?m*x#xs))"
    by (simp add:I_hd_coeff1_mult_a[OF \<open>?m>0\<close>] dvd_zlcms 0)
  also have "\<dots> = (\<exists>x. ?m dvd x+0 \<and> (\<forall>a \<in> set as. I\<^sub>Z (hd_coeff1 ?m a) (x#xs)))"
    by(rule unity_coeff_ex[THEN meta_eq_to_obj_eq])
  finally show ?thesis by(simp add:hd_coeffs1_def)
qed

abbreviation "is_dvd a \<equiv> case a of Le _ _ \<Rightarrow> False | _ \<Rightarrow> True"

definition
"qe_pres\<^sub>1 as =
 (let ds = filter is_dvd as; (d::int) = zlcms(map divisor ds); ls = lbounds as
  in if ls = []
     then Disj [0..d - 1] (\<lambda>n. list_conj(map (Atom \<circ> asubst n []) ds))
     else
     Disj ls (\<lambda>(li,lks).
       Disj [0..d - 1] (\<lambda>n.
         list_conj(map (Atom \<circ> asubst (li + n) (-lks)) as))))"
text\<open>\noindent Note the optimization in the case @{prop"ls = []"}: only the
divisibility atoms are tested, not the inequalities. This complicates
the proof.\<close>

lemma I_cyclic:
assumes "is_dvd a" and "hd_coeff a = 1" and "i mod divisor a = j mod divisor a"
shows "I\<^sub>Z a (i#e) = I\<^sub>Z a (j#e)"
proof (cases a)
  case (Dvd d l ks)
  with \<open>hd_coeff a = 1\<close> obtain ks' where [simp]: "ks = 1#ks'"
    by(simp split:list.splits)
  have "(l + (i + \<langle>ks',e\<rangle>)) mod d = (l + (j + \<langle>ks',e\<rangle>)) mod d" (is "?l=?r")
  proof -
    have "?l = (l mod d + (i + \<langle>ks',e\<rangle>) mod d) mod d"
      by (simp add: mod_add_eq)
    also have "(i + \<langle>ks',e\<rangle>) mod d = (i mod d + \<langle>ks',e\<rangle> mod d) mod d"
      by (simp add: mod_add_eq)
    also have "i mod d = j mod d"
      using \<open>i mod divisor a = j mod divisor a\<close> Dvd by simp
    also have "(j mod d + \<langle>ks',e\<rangle> mod d) mod d = (j + \<langle>ks',e\<rangle>) mod d"
      by(rule mod_add_eq)
    also have "(l mod d + (j + \<langle>ks',e\<rangle>) mod d) mod d = ?r"
      by(rule mod_add_eq)
    finally show ?thesis .
  qed
  thus ?thesis using Dvd by (simp add:dvd_eq_mod_eq_0)
next
  case (NDvd d l ks)
  with \<open>hd_coeff a = 1\<close> obtain ks' where [simp]: "ks = 1#ks'"
    by(simp split:list.splits)
  have "(l + (i + \<langle>ks',e\<rangle>)) mod d = (l + (j + \<langle>ks',e\<rangle>)) mod d" (is "?l=?r")
  proof -
    have "?l = (l mod d + (i + \<langle>ks',e\<rangle>) mod d) mod d"
      by (simp add: mod_add_eq)
    also have "(i + \<langle>ks',e\<rangle>) mod d = (i mod d + \<langle>ks',e\<rangle> mod d) mod d"
      by (simp add: mod_add_eq)
    also have "i mod d = j mod d"
      using \<open>i mod divisor a = j mod divisor a\<close> NDvd by simp
    also have "(j mod d + \<langle>ks',e\<rangle> mod d) mod d = (j + \<langle>ks',e\<rangle>) mod d"
      by(rule mod_add_eq)
    also have "(l mod d + (j + \<langle>ks',e\<rangle>) mod d) mod d = ?r"
      by(rule mod_add_eq)
    finally show ?thesis .
  qed
  thus ?thesis using NDvd by (simp add:dvd_eq_mod_eq_0)
next
  case Le thus ?thesis using \<open>is_dvd a\<close> by simp
qed

lemma I_qe_pres\<^sub>1:
assumes norm: "\<forall>a \<in> set as. divisor a \<noteq> 0"
and hd: "\<forall>a \<in> set as. hd_coeff_is1 a"
shows "Z.I (qe_pres\<^sub>1 as) xs = (\<exists>x. \<forall>a\<in> set as. I\<^sub>Z a (x#xs))"
proof -
  let ?lbs = "lbounds as"
  let ?ds = "filter is_dvd as"
  let ?lcm = "zlcms(map divisor ?ds)"
  let ?Ds = "{a \<in> set as. is_dvd a}"
  let ?Us = "{a \<in> set as. case a of Le _ (k#_) \<Rightarrow> k < 0 | _ \<Rightarrow> False}"
  let ?Ls = "{a \<in> set as. case a of Le _ (k#_) \<Rightarrow> k > 0 | _ \<Rightarrow> False}"
  have as: "set as = ?Ds \<union> ?Ls \<union> ?Us" (is "_ = ?S")
  proof -
    { fix x assume "x \<in> set as"
      hence "x \<in> ?S" using hd by (cases x rule: atom.exhaust)(auto split:list.splits) }
    moreover
    { fix x assume "x \<in> ?S"
      hence "x \<in> set as" by auto }
    ultimately show ?thesis by blast
  qed
  have 1: "\<forall>a \<in> ?Ds. hd_coeff a = 1" using hd by(fastforce split:atom.splits)
  show ?thesis  (is "?QE = (\<exists>x. ?P x)")
  proof
    assume "?QE"
    { assume "?lbs = []"
      with \<open>?QE\<close> obtain n where "n < ?lcm" and
        A: "\<forall>a \<in> ?Ds. I\<^sub>Z a (n#xs)" using 1
        by(auto simp:IZ_asubst qe_pres\<^sub>1_def)
      have "?Ls = {}" using \<open>?lbs = []\<close> set_lbounds[of as]
        by (auto simp add:filter_empty_conv split:atom.split list.split)
      have "\<exists>x. ?P x"
      proof cases
        assume "?Us = {}"
        with \<open>?Ls = {}\<close> have "set as = ?Ds" using as by(simp (no_asm_use))blast
        hence "?P n" using A by auto
        thus ?thesis ..
      next
        assume "?Us \<noteq> {}"
        let ?M = "{\<langle>tl ks, xs\<rangle> - i|ks i. Le i ks \<in> ?Us}" let ?m = "Min ?M"
        have "finite ?M"
        proof -
          have "finite ( (\<lambda>Le i ks \<Rightarrow> \<langle>tl ks, xs\<rangle> - i) `
                         {a\<in>set as. \<exists>i k ks. k<0 \<and> a = Le i (k#ks)} )"
            (is "finite ?B")
            by simp
          also have "?B = ?M" using hd
            by(fastforce simp:image_def neq_Nil_conv split:atom.splits list.splits)
          finally show ?thesis by auto
        qed
        have "?M \<noteq> {}"
        proof -
          from \<open>?Us \<noteq> {}\<close> obtain i k ks where "Le i (k#ks) \<in> ?Us \<and> k<0"
            by (fastforce split:atom.splits list.splits)
          thus ?thesis by auto
        qed
        let ?k = "(n - ?m) div ?lcm + 1" let ?x = "n - ?k * ?lcm"
        have "\<forall>a \<in> ?Ds. I\<^sub>Z a (?x # xs)"
        proof (intro allI ballI)
          fix a assume "a \<in> ?Ds"
          let ?d = "divisor a"
          have 2: "?d dvd ?lcm" using \<open>a \<in> ?Ds\<close> by(simp add:dvd_zlcms)
          have "?x mod ?d = n mod ?d" (is "?l = ?r")
          proof -
            have "?l = (?r - ((?k * ?lcm) mod ?d)) mod ?d"
              by (simp add: mod_diff_eq)
            also have "(?k * ?lcm) mod ?d = 0"
              by(simp add: dvd_eq_mod_eq_0[symmetric] dvd_mult[OF 2])
            finally show ?thesis by simp
          qed
          thus "I\<^sub>Z a (?x#xs)" using A I_cyclic[of a n ?x] \<open>a \<in> ?Ds\<close> 1 by auto
        qed
        moreover
        have "\<forall>a\<in> ?Us. I\<^sub>Z a (?x#xs)"
        proof
          fix a assume "a \<in> ?Us"
          then obtain l ks where [simp]: "a = Le l (-1#ks)" using hd
            by(fastforce split:atom.splits list.splits)
          have "?m \<le> \<langle>ks,xs\<rangle> - l"
            using Min_le_iff[OF \<open>finite ?M\<close> \<open>?M \<noteq> {}\<close>] \<open>a \<in> ?Us\<close> by fastforce
          moreover have "(n - ?m) mod ?lcm < ?lcm"
            by(simp add: pos_mod_bound[OF zlcms_pos] norm)
          ultimately show "I\<^sub>Z a (?x#xs)"
            by(simp add:minus_mod_eq_mult_div [symmetric] algebra_simps)
        qed
        moreover
        have "set as = ?Ds \<union> ?Us" using as \<open>?Ls = {}\<close>
          by (simp (no_asm_use)) blast
        ultimately have "?P(?x)" by auto
        thus ?thesis ..
      qed }
    moreover
    { assume "?lbs \<noteq> []"
      with \<open>?QE\<close> obtain il ksl m
        where "\<forall>a\<in>set as. I\<^sub>Z (asubst (il + m) ksl a) xs"
        by(auto simp:qe_pres\<^sub>1_def)
      hence "?P(il + m + \<langle>ksl,xs\<rangle>)" by(simp add:IZ_asubst)
      hence "\<exists>x. ?P x" .. }
    ultimately show "\<exists>x. ?P x" by blast
  next
    assume "\<exists>x. ?P x" then obtain x where x: "?P x" ..
    show ?QE
    proof cases
      assume "?lbs = []"
      moreover
      have "\<exists>x. 0 \<le> x \<and> x < ?lcm \<and> (\<forall>a \<in> ?Ds. I\<^sub>Z a (x # xs))"
        (is "\<exists>x. ?P x")
      proof
        { fix a assume "a \<in> ?Ds"
          hence "I\<^sub>Z a ((x mod ?lcm) # xs) = I\<^sub>Z a (x # xs)" using 1
            by (fastforce del:iffI intro: I_cyclic
                simp: mod_mod_cancel dvd_zlcms) }
        thus "?P(x mod ?lcm)" using x norm by(simp add: zlcms_pos)
      qed
      ultimately show ?thesis by (auto simp:qe_pres\<^sub>1_def IZ_asubst)
    next
      assume "?lbs \<noteq> []"
      let ?L = "{i - \<langle>ks,xs\<rangle> |ks i. (i,ks) \<in> set(lbounds as)}"
      let ?lm = "Max ?L"
      let ?n = "(x - ?lm) mod ?lcm"
      have "finite ?L"
      proof -
        have "finite((\<lambda>(i,ks). i-\<langle>ks,xs\<rangle>) ` set(lbounds as) )" (is "finite ?B")
          by simp
        also have "?B = ?L" by auto
        finally show ?thesis by auto
      qed
      moreover have "?L \<noteq> {}" using \<open>?lbs \<noteq> []\<close>
        by(fastforce simp:neq_Nil_conv)
      ultimately have "?lm \<in> ?L" by(rule Max_in)
      then obtain li lks where "(li,lks)\<in> set ?lbs" and lm: "?lm = li-\<langle>lks,xs\<rangle>"
        by blast
      moreover
      have n: "0 \<le> ?n \<and> ?n < ?lcm" using norm by(simp add:zlcms_pos)
      moreover
      { fix a assume "a \<in> set as"
        with x have "I\<^sub>Z a (x # xs)" by blast
        have "I\<^sub>Z a ((li + ?n - \<langle>lks,xs\<rangle>) # xs)"
        proof -
          { assume "a \<in> ?Ls"
            then obtain i ks where [simp]: "a = Le i (1#ks)" using hd
              by(fastforce split:atom.splits list.splits)
            from \<open>a \<in> ?Ls\<close> have "i-\<langle>ks,xs\<rangle> \<in> ?L" by(fastforce simp:set_lbounds)
            hence "i-\<langle>ks,xs\<rangle> \<le> li - \<langle>lks,xs\<rangle>"
              using lm[symmetric] \<open>finite ?L\<close> \<open>?L \<noteq> {}\<close> by auto
            hence ?thesis using n by simp }
          moreover
          { assume "a \<in> ?Us"
            then obtain i ks where [simp]: "a = Le i (-1#ks)" using hd
              by(fastforce split:atom.splits list.splits)
            have "Le li (1#lks) \<in> set as" using \<open>(li,lks) \<in> set ?lbs\<close> hd
              by(auto simp:set_lbounds)
            hence "li - \<langle>lks,xs\<rangle> \<le> x" using x by auto
            hence "(x - ?lm) mod ?lcm \<le> x - ?lm"
              using lm by(simp add: zmod_le_nonneg_dividend)
            hence ?thesis using \<open>I\<^sub>Z a (x # xs)\<close> lm by auto }
          moreover
          { assume "a \<in> ?Ds"
            have ?thesis
            proof(rule I_cyclic[THEN iffD2, OF _ _ _ \<open>I\<^sub>Z a (x # xs)\<close>])
              show "is_dvd a" using \<open>a \<in> ?Ds\<close> by simp
              show "hd_coeff a = 1" using \<open>a \<in> ?Ds\<close> hd
                by(fastforce split:atom.splits list.splits)
              have "li + (x-?lm) mod ?lcm - \<langle>lks,xs\<rangle> = ?lm + (x-?lm) mod ?lcm"
                using lm by arith
              hence "(li + (x-?lm) mod ?lcm - \<langle>lks,xs\<rangle>) mod divisor a =
                     (?lm + (x-?lm) mod ?lcm) mod divisor a" by (simp only:)
              also have "\<dots> =
        (?lm mod divisor a + (x-?lm) mod ?lcm mod divisor a) mod divisor a"
                by (simp add: mod_add_eq)
              also have
        "\<dots> = (?lm mod divisor a + (x-?lm) mod divisor a) mod divisor a"
                using \<open>is_dvd a\<close> \<open>a\<in> set as\<close>
                by(simp add: mod_mod_cancel dvd_zlcms)
              also have "\<dots> = (?lm + (x-?lm)) mod divisor a"
                by(rule mod_add_eq)
              also have "\<dots> = x mod divisor a" by simp
              finally
              show "(li + ?n - \<langle>lks,xs\<rangle>) mod divisor a = x mod divisor a"
                using norm by(auto simp: zlcms_pos)
            qed }
          ultimately show ?thesis using \<open>a \<in> set as\<close> as by blast
        qed
      }
      ultimately show ?thesis using \<open>?lbs \<noteq> []\<close>
        by (simp (no_asm_simp) add:qe_pres\<^sub>1_def IZ_asubst split_def)
           (force simp del:int_nat_eq)
    qed
  qed
qed

lemma  divisors_hd_coeffs1:
assumes div0: "\<forall>a\<in>set as. divisor a \<noteq> 0" and hd0: "\<forall>a\<in>set as. hd_coeff a \<noteq> 0"
and a: "a\<in>set (hd_coeffs1 as)" shows "divisor a \<noteq> 0"
proof -
  let ?m = "zlcms(map hd_coeff as)"
  from a have "a = Dvd ?m 0 [1] \<or> (\<exists>b \<in> set as. a = hd_coeff1 ?m b)"
    (is "?A \<or> ?B")
    by(auto simp:hd_coeffs1_def)
  thus ?thesis
  proof
    assume ?A thus ?thesis using hd0 by(auto)
  next
    assume ?B
    then obtain b where "b \<in> set as" and [simp]: "a = hd_coeff1 ?m b" ..
    hence b: "hd_coeff b \<noteq> 0" "divisor b \<noteq> 0" using div0 hd0 by auto
    show ?thesis
    proof (cases b)
      case (Le i ks) thus ?thesis using b by(auto split:list.splits)
    next
      case [simp]: (Dvd d i ks)
      then obtain k ks' where [simp]: "ks = k#ks'" using b
        by(auto split:list.splits)
      have k: "k \<in> set(map hd_coeff as)" using \<open>b \<in> set as\<close> by force
      have "zlcms (map hd_coeff as) div k \<noteq> 0"
        using b hd0 dvd_zlcms[OF k]
        by(auto simp add:dvd_def)
      thus ?thesis using b by (simp)
    next
      case [simp]: (NDvd d i ks)
      then obtain k ks' where [simp]: "ks = k#ks'" using b
        by(auto split:list.splits)
      have k: "k \<in> set(map hd_coeff as)" using \<open>b \<in> set as\<close> by force
      have "zlcms (map hd_coeff as) div k \<noteq> 0"
        using b hd0 dvd_zlcms[OF k]
        by(auto simp add:dvd_def)
      thus ?thesis using b by (simp)
    qed
  qed
qed

lemma hd_coeff_is1_hd_coeffs1:
assumes hd0: "\<forall>a\<in>set as. hd_coeff a \<noteq> 0"
and a: "a\<in>set (hd_coeffs1 as)" shows "hd_coeff_is1 a"
proof -
  let ?m = "zlcms(map hd_coeff as)"
  from a have "a = Dvd ?m 0 [1] \<or> (\<exists>b \<in> set as. a = hd_coeff1 ?m b)"
    (is "?A \<or> ?B")
    by(auto simp:hd_coeffs1_def)
  thus ?thesis
  proof
    assume ?A thus ?thesis using hd0 by simp
  next
    assume ?B
    then obtain b where "b \<in> set as" and [simp]: "a = hd_coeff1 ?m b" ..
    hence b: "hd_coeff b \<noteq> 0" using hd0 by auto
    show ?thesis using b
      by (cases b) (auto simp: sgn_if split:list.splits)
  qed
qed

lemma I_qe_pres\<^sub>1_o:
 "\<lbrakk> \<forall>a \<in> set as. divisor a \<noteq> 0; \<forall>a\<in>set as. hd_coeff a \<noteq> 0 \<rbrakk> \<Longrightarrow>
  Z.I ((qe_pres\<^sub>1 \<circ> hd_coeffs1) as) e = (\<exists>x. \<forall>a\<in> set as. I\<^sub>Z a (x#e))"
apply(simp)
apply(subst I_qe_pres\<^sub>1)
  apply(simp add: divisors_hd_coeffs1)
 apply(simp add: hd_coeff_is1_hd_coeffs1)
using I_hd_coeffs1 apply(simp)
done

definition "qe_pres = Z.lift_dnf_qe (qe_pres\<^sub>1 \<circ> hd_coeffs1)"

lemma qfree_qe_pres_o: "qfree ((qe_pres\<^sub>1 \<circ> hd_coeffs1) as)"
by(auto simp:qe_pres\<^sub>1_def intro!:qfree_list_disj)

lemma normal_qe_pres\<^sub>1_o:
  "\<forall>a \<in> set as. hd_coeff a \<noteq> 0 \<and> divisor a \<noteq> 0 \<Longrightarrow>
   Z.normal ((qe_pres\<^sub>1 \<circ> hd_coeffs1) as)"
  supply image_cong_simp [cong del]
apply(auto simp:qe_pres\<^sub>1_def Z.normal_def
   dest!:atoms_list_disjE atoms_list_conjE)

apply(simp add: hd_coeffs1_def)
 apply(erule disjE) apply fastforce
apply (clarsimp)
apply(case_tac xa)
  apply(rename_tac list) apply(case_tac list) apply fastforce apply (simp split:if_split_asm)
 apply(rename_tac list) apply(case_tac list) apply fastforce
 apply (simp split:if_split_asm) apply fastforce
 apply(erule disjE) prefer 2 apply fastforce
 apply(simp add:zdiv_eq_0_iff)
 apply(subgoal_tac "a \<in> set(map hd_coeff as)")
  prefer 2 apply force
 apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
  prefer 2 apply simp
 apply (metis elem_le_zlcms linorder_not_le zlcms_pos)
apply(rename_tac list) apply(case_tac list) apply fastforce
apply (simp split:if_split_asm) apply fastforce
apply(simp add:zdiv_eq_0_iff)
apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
 prefer 2 apply simp
apply(subgoal_tac "a \<in> set(map hd_coeff as)")
 prefer 2 apply force
apply(erule disjE)
 apply (metis elem_le_zlcms linorder_not_le)
apply(erule disjE)
 apply (metis linorder_not_le zlcms_pos)
apply fastforce

apply(simp add: hd_coeffs1_def)
 apply(erule disjE) apply fastforce
apply (clarsimp)
apply(case_tac xa)
  apply(rename_tac list) apply(case_tac list) apply fastforce apply (simp split:if_split_asm)
 apply(rename_tac list) apply(case_tac list) apply fastforce
 apply (simp split:if_split_asm) apply fastforce
 apply(erule disjE) prefer 2 apply fastforce
 apply(simp add:zdiv_eq_0_iff)
 apply(subgoal_tac "a \<in> set(map hd_coeff as)")
  prefer 2 apply force
 apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
  prefer 2 apply simp
 apply (metis elem_le_zlcms linorder_not_le zlcms_pos)
apply(rename_tac list) apply(case_tac list) apply fastforce
apply (simp split:if_split_asm) apply fastforce
apply(simp add:zdiv_eq_0_iff)
apply(subgoal_tac "\<forall>i\<in> set(map hd_coeff as). i \<noteq> 0")
 prefer 2 apply simp
apply(subgoal_tac "a \<in> set(map hd_coeff as)")
 prefer 2 apply force
apply(erule disjE)
 apply (metis elem_le_zlcms linorder_not_le)
apply(erule disjE)
 apply (metis linorder_not_le zlcms_pos)
apply fastforce
done

theorem I_pres_qe: "Z.normal \<phi> \<Longrightarrow>  Z.I (qe_pres \<phi>) xs = Z.I \<phi> xs"
by(simp add:qe_pres_def Z.I_lift_dnf_qe_anormal I_qe_pres\<^sub>1_o qfree_qe_pres_o normal_qe_pres\<^sub>1_o del:o_apply)

theorem qfree_pres_qe: "qfree (qe_pres f)"
by(simp add:qe_pres_def Z.qfree_lift_dnf_qe qfree_qe_pres_o del:o_apply)

end

repo: PSL


text:
theory Asymptotics_Test
  imports Asymptotics_Recurrences
begin

(* Some test functions *)

definition f :: "nat \<Rightarrow> nat" where "f x = 4 * x + 1"
lemma f_bound [asym_bound]: "f \<in> \<Theta>(\<lambda>n. real n)" unfolding f_def by auto2

definition flog :: "nat \<Rightarrow> nat" where "flog x = nat \<lceil>log 2 x\<rceil>"
lemma flog_bound [asym_bound]: "flog \<in> \<Theta>(\<lambda>n. ln n)"
  unfolding flog_def using abcd_lnx[of 0 1 1 0] by auto

definition g :: "nat \<Rightarrow> nat" where "g x = 5"
lemma g_bound [asym_bound]: "g \<in> \<Theta>(\<lambda>n. 1)" unfolding g_def by auto2

fun f_prod :: "nat \<times> nat \<Rightarrow> nat" where
  "f_prod (n,m) = n * m"

lemma f_prod_asym [asym_bound]: "f_prod \<in> \<Theta>\<^sub>2(\<lambda>x. real (fst x * snd x))"
  apply (subst surjective_pairing) unfolding f_prod.simps by auto2

fun f_sum :: "nat \<times> nat \<Rightarrow> nat" where
  "f_sum (n,m) = n + m"

lemma f_sum_asym [asym_bound]: "f_sum \<in> \<Theta>\<^sub>2(\<lambda>x. real (fst x) + real (snd x))"
  apply (subst surjective_pairing) unfolding f_sum.simps by auto2

lemma "(\<lambda>x::nat. real 1) \<in> \<Theta>(\<lambda>n. 1::real)" by auto2

lemma "(\<lambda>x. real (f (5 * x))) \<in> \<Theta>(\<lambda>n. real n)" by auto2

lemma "(\<lambda>n. f (n + 1) + n * flog (2 * n) + 3 * n * flog (n div 3)) \<in> \<Theta>(\<lambda>n. n * ln n)" by auto2

(* Examples of f applied to constants *)
declare f_def [rewrite]
lemma "(\<lambda>x::nat. real (f 5)) \<in> \<Theta>(\<lambda>n. 1::real)" by auto2

(* how to incorporate 1D into 2D *)

lemma "(\<lambda>(n,m). f (5*m)) \<in> \<Theta>\<^sub>2(\<lambda>(n::nat,m). real m)" by auto2

lemma "(\<lambda>(n,m). f (5*n)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). real n)" by auto2

lemma "(\<lambda>x. real (fst x * snd x + 2)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real (n * m))" by auto2

lemma "(\<lambda>x. real (fst x * fst x + 2)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). real (n^2))" by auto2

lemma "(\<lambda>x. real (fst x * fst x + snd x)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). real (n^2) + real m)" by auto2

lemma "(\<lambda>(n,m). f_prod (n+1,m+1) + 1) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real n * real m)" by auto2

lemma "(\<lambda>(n,m). f_sum (n+1,m+1)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real n + real m)" by auto2

lemma "(\<lambda>(n,m). f_prod (n+1,m+1) + f_sum (n+1,m+1) + 1) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real n * real m)" by auto2

lemma "(\<lambda>(n,m). f n + flog m + n * m + f_prod (n div 3,m+1)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real n * real m)" by auto2

lemma "(\<lambda>(n,m). 1 + f n + flog m + f_sum (n+1, m+1)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real n + real m)" by auto2

lemma "(\<lambda>(n,m). (1 + f n) * m * flog m) \<in> \<Theta>\<^sub>2(\<lambda>(n::nat,m). n * m * ln m)" by auto2

lemma "(\<lambda>(n,m). (1 + f n) * m * flog m) \<in> \<Theta>\<^sub>2(\<lambda>(n::nat,m::nat). n * m * ln m)" by auto2

lemma "(\<lambda>(n,m). (f m + f n) * m) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real (m^2) + real n * real m)" by auto2

lemma "(\<lambda>(n,m). m * (f m + f n)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real (m^2) + real n * real m)" by auto2

lemma "(\<lambda>(n,m). (f m + n) * (m + f n)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m). real (m^2) + real n * real m + real (n^2))" by auto2

lemma "(\<lambda>x. real ((fst x * fst x + fst x) * snd x)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). real (n^2) * real m)" by auto2

lemma "(\<lambda>(n,m). real ((n * n + n) * m)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). real (n^2) * real m)" by auto2

lemma "(\<lambda>(n,m). real (f m + n)) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). real (m + n))" by auto2

lemma "(\<lambda>(n,m). f m * m + n) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). m^2 + n)" by auto2

lemma "(\<lambda>(n,m). f m * m + m * n + n * f n) \<in> \<Theta>\<^sub>2(\<lambda>(n,m::nat). m^2 + m * n + n^2)" by auto2

(* Examples of f or f_sum applied to constants *)
declare f_sum.simps [rewrite]

lemma "(\<lambda>x. real (f 1)) \<in> \<Theta>\<^sub>2(\<lambda>(n::nat,m::nat). 1)"
  apply (subst surjective_pairing) by auto2

lemma "(\<lambda>x. real (f_sum (5,3))) \<in> \<Theta>\<^sub>2(\<lambda>(n::nat,m::nat). 1)"
  apply (subst surjective_pairing) by auto2

ML_file "landau_util_test.ML"

hide_const f g flog f_prod f_sum

end

author: bzhan


text:
section\<open>Word Upto\<close>
theory Word_Upto
imports Main
  "../../IP_Addresses/Hs_Compat"
  "../../Word_Lib/Word_Lemmas"
begin

text\<open>Enumerate a range of machine words.\<close>

text\<open>enumerate from the back (inefficient)\<close>
function word_upto :: "'a word \<Rightarrow> 'a word \<Rightarrow> ('a::len0) word list" where
"word_upto a b = (if a = b then [a] else word_upto a (b - 1) @ [b])"
by pat_completeness auto

(*by the way: does not terminate practically if b < a; will terminate after it
  reaches the word wrap-around!*)

termination word_upto
apply(relation "measure (unat \<circ> uncurry (op -) \<circ> prod.swap)")
 apply(rule wf_measure; fail)
apply(simp)
apply(subgoal_tac "unat (b - a - 1) < unat (b - a)")
 apply(simp add: diff_right_commute; fail)
apply(rule measure_unat)
apply auto
done

declare word_upto.simps[simp del]

text\<open>enumerate from the front (more inefficient)\<close>
function word_upto' :: "'a word \<Rightarrow> 'a word \<Rightarrow> ('a::len0) word list" where
"word_upto' a b = (if a = b then [a] else a # word_upto' (a + 1) b)"
by pat_completeness auto

termination word_upto'
apply(relation "measure (\<lambda> (a, b). unat (b - a))")
 apply(rule wf_measure; fail)
apply(simp)
apply(subgoal_tac "unat (b - a - 1) < unat (b - a)")
 apply (simp add: diff_diff_add; fail)
apply(rule measure_unat)
apply auto
done

declare word_upto'.simps[simp del]

lemma word_upto_cons_front[code]:
 "word_upto a b = word_upto' a b"
 proof(induction a b rule:word_upto'.induct)
 case (1 a b)
   have hlp1: "a \<noteq> b \<Longrightarrow> a # word_upto (a + 1) b = word_upto a b"
   apply(induction a b rule:word_upto.induct)
   apply simp
   apply(subst(1) word_upto.simps)
   apply(simp)
   apply safe
    apply(subst(1) word_upto.simps)
    apply (simp)
    apply(subst(1) word_upto.simps)
    apply (simp; fail)
   apply(case_tac "a \<noteq> b - 1")
    apply(simp)
    apply (metis Cons_eq_appendI word_upto.simps)
   apply(simp)
   done

   from 1[symmetric] show ?case
     apply(cases "a = b")
      subgoal
      apply(subst word_upto.simps)
      apply(subst word_upto'.simps)
      by(simp)
     apply(subst word_upto'.simps)
     by(simp add: hlp1)
 qed

(* Most of the lemmas I show about word_upto hold without a \<le> b,
   but I don't need that right now and it's giving me a headache *)

lemma word_upto_set_eq: "a \<le> b \<Longrightarrow> x \<in> set (word_upto a b) \<longleftrightarrow> a \<le> x \<and> x \<le> b"
proof
  show "a \<le> b \<Longrightarrow> x \<in> set (word_upto a b) \<Longrightarrow> a \<le> x \<and> x \<le> b"
    apply(induction a b rule: word_upto.induct)
    apply(case_tac "a = b")
     apply(subst(asm) word_upto.simps)
     apply(simp; fail)
    apply(subst(asm) word_upto.simps)
    apply(simp)
    apply(erule disjE)
     apply(simp; fail)
    proof(goal_cases)
     case (1 a b)
     from 1(2-3) have "b \<noteq> 0" by force
     from 1(2,3) have "a \<le> b - 1" by (metis \<open>b \<noteq> 0\<close> eq_iff le_step_down_nat unat_arith_simps(1) unat_minus_one)
     from 1(1)[OF this 1(4)] show ?case by (metis dual_order.trans 1(2,3) less_imp_le measure_unat word_le_0_iff word_le_nat_alt)
    qed
next
  show "a \<le> x \<and> x \<le> b \<Longrightarrow> x \<in> set (word_upto a b)"
    apply(induction a b rule: word_upto.induct)
    apply(case_tac "a = b")
     apply(subst word_upto.simps)
     apply(simp; force)
    apply(subst word_upto.simps)
    apply(simp)
    apply(case_tac "x = b")
     apply(simp;fail)
    proof(goal_cases)
       case (1 a b)
       from 1(2-4) have "b \<noteq> 0" by force
       from 1(2,4) have "x \<le> b - 1" by (metis `b \<noteq> 0` dual_order.antisym le_step_down_nat unat_minus_one word_le_nat_alt)
       from 1(1) this show ?case by simp
    qed
qed

lemma word_upto_distinct_hlp: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> b \<notin> set (word_upto a (b - 1))"
   apply(rule ccontr, unfold not_not)
   apply(subgoal_tac "a \<le> b - 1")
    apply(drule iffD1[OF word_upto_set_eq[of a "b -1" b]])
     apply(simp add: word_upto.simps; fail)
    apply(subgoal_tac "b \<noteq> 0")
     apply(meson leD measure_unat word_le_nat_alt)
    apply(blast intro: iffD1[OF word_le_0_iff])
   apply(metis antisym_conv le_step_down_nat unat_minus_one word_le_0_iff word_le_nat_alt)
done

lemma distinct_word_upto: "a \<le> b \<Longrightarrow> distinct (word_upto a b)"
apply(induction a b rule: word_upto.induct)
apply(case_tac "a = b")
 apply(subst word_upto.simps)
 apply(simp; force)
apply(subst word_upto.simps)
apply(case_tac "a \<le> b - 1")
 apply(simp)
 apply(rule word_upto_distinct_hlp; simp; fail)
apply(simp)
apply(rule ccontr)
apply(metis le_step_down_nat less_le not_le unat_minus_one word_le_nat_alt word_not_simps(1))
done

lemma word_upto_eq_upto: "s \<le> e \<Longrightarrow> e \<le> unat (max_word :: 'l word) \<Longrightarrow>
       word_upto ((of_nat :: nat \<Rightarrow> ('l :: len) word) s) (of_nat e) = map of_nat (upt s (Suc e))"
proof(induction e)
  let ?mwon = "of_nat :: nat \<Rightarrow> 'l word"
  let ?mmw = "max_word :: 'l word"
  case (Suc e)
  show ?case
  proof(cases "?mwon s = ?mwon (Suc e)")
    case True
    have "s = Suc e" using le_unat_uoi Suc.prems True by metis
    with True show ?thesis by(subst word_upto.simps) (simp)
  next
    case False
    hence le: "s \<le> e" using le_SucE Suc.prems by blast
    have lm: "e \<le> unat ?mmw" using Suc.prems by simp
    have sucm: "(of_nat :: nat \<Rightarrow> ('l :: len) word) (Suc e) - 1 = of_nat e" using Suc.prems(2) by simp
    note mIH = Suc.IH[OF le lm]
    show ?thesis by(subst word_upto.simps) (simp add: False[simplified] Suc.prems mIH sucm)
  qed
qed(simp add: word_upto.simps)

lemma word_upto_alt: "(a :: ('l :: len) word) \<le> b \<Longrightarrow>
  word_upto a b = map of_nat (upt (unat a) (Suc (unat b)))"
proof -
   let ?mmw = "max_word :: 'l word"
   assume le: "a \<le> b"
   hence nle: "unat a \<le> unat b" by(unat_arith)
   have lem: "unat b \<le> unat ?mmw" by (simp add: word_unat_less_le)
   note word_upto_eq_upto[OF nle lem, unfolded word_unat.Rep_inverse]
   thus "word_upto a b = map of_nat [unat a..<Suc (unat b)]" .
qed

lemma word_upto_upt:
  "word_upto a b = (if a \<le> b then map of_nat (upt (unat a) (Suc (unat b))) else word_upto a b)"
  using word_upto_alt by metis

lemma sorted_word_upto:
   fixes a b :: "('l :: len) word"
   assumes "a \<le> b"
   shows "sorted (word_upto a b)"
using assms
proof(induction b)
  fix b
  assume le_prem: "a \<le> 1 + b"
  assume nmax_prem: "1 + b \<noteq> 0"
  assume IH: "a \<le> b \<Longrightarrow> sorted (word_upto a b)"
  show "sorted (word_upto a (1 + b))"
  proof(cases "a = 1 + b")
    case True thus ?thesis by(simp add: word_upto.simps)
  next
    case False
    have fprem: "a \<le> b" using le_prem False by (metis add.commute antisym_conv1 plus_one_helper)
    note mIH = IH[OF this]
    show ?thesis by(subst word_upto.simps)
                   (simp add: fprem lt1_neq0 nmax_prem word_le_plus_either word_upto_set_eq False sorted_append mIH)
    qed
qed(simp add: word_upto.simps)

end

author: diekmann


text:
theory Submission
  imports Defs
begin

fun bound :: "com \<Rightarrow> nat" where
"bound SKIP = 0" |
"bound (Assign x a) = 1" |
"bound (Seq c\<^sub>1 c\<^sub>2) = bound c\<^sub>1 + bound c\<^sub>2 + 1" |
"bound (If b c\<^sub>1 c\<^sub>2) = max (bound c\<^sub>1) (bound c\<^sub>2) + 1" |
"bound (While b c) = 0" (* assuming by the assignment this doesn't matter *)

lemma bound_decr: "while_free c \<Longrightarrow> (c, s) \<rightarrow> (c', s') \<Longrightarrow> bound c' < bound c"
by(induction c arbitrary: c' s s' rule: while_free.induct, auto)

end

author: MaximilianAnzinger


text:
(*  Title:       An example submission to the Archive of Formal Proofs
    Author:      Gerwin Klein <kleing at cse.unsw.edu.au>, 2004
    Maintainer:  Gerwin Klein <kleing at cse.unsw.edu.au>
*)

header "An Example Submission"

theory Submission
  imports Main
begin

text {*
  This is an example submission to the Archive of Formal Proofs.

  The scope of the archive encompasses examples, textbook-style
  proofs, libraries and larger scientific developments.
*}

section "Format of a submission"

text {*
  Submission should be by email to \texttt{afp-submit at in.tum.de} and contain
  the following:
  \begin{itemize}
  \item Title, authors, and abstract.
  The abstract should be in plain text or plain html (no images/styles).
  \item A short name that will become the directory name of the
  submission.
  \item The Isabelle theories: a tar.gz file with the theory files,
  a ROOT file, and a document directory.
  The theories should work with the current release of Isabelle.
  Each theory file should include a header comment like the one
  in this theory.
  \item A statement whether you would like to release your submission
  under the BSD or the LGPL license.
  \end{itemize}

  The submission of the example you are reading is at
  @{url "http://afp.sf.net/release/afp-Example-Submission-current.tar.gz"}.
*}

section "Proof styles"

text {*
  We accept proofs in \isakeyword{apply}-script style like the
  following.
*}

lemma true: "True"
  apply blast
  done

text {*
  We encourage structured proofs with comments and
  explanations. The Isabelle document preparation tools support
  antiquotations like @{thm true}, normal {\LaTeX} commands and BibTeX
  citations. See \cite{LNCS2283} and the Isabelle documentation for
  more information.
*}
lemma very_true: "True"
proof -
  -- "a very roundabout way"
  fix P have "P \<longrightarrow> True" by blast
  -- "to show @{term True}"
  thus True by blast
qed

section "The anatomy of a submission"

text {*
  The directory structure of this example submission is the following
\begin{verbatim}
Example-Submission/
    document/
        root.tex
        root.bib
    config
    ROOT
    Submission.thy
\end{verbatim}

The document directory contains the {\LaTeX} master file
\texttt{root.tex} and the bibliography \texttt{root.bib}.
The {\LaTeX} part of your
submission should contain title, abstract, author, and any
further documentation
you wish to provide.

The file \texttt{config} contains maintenance information. This is
optional. If you do not submit one, we will create one for you.

\texttt{ROOT} controls which theories should be loaded. If you have
one main theory that depends on all the others, you only need to
include this one. You can also use the \texttt{ROOT} file to control the
order in which theories are read.

The file \texttt{Submission.thy} is the Isabelle theory containing
this text. A usual submission has more than one theory file. You can
devise your own subdirectory structure if you have more theories and
one directory becomes too crowded. You can also build on existing articles
in the AFP by importing them. For example, if you build on theory W in
the article MiniML, the way to import it is:

\begin{verbatim}
theory My_Theory
  imports "../MiniML/W"
begin
\end{verbatim}

To build on a theory that is in the Isabelle distribtion, but not in
one of the standard images like HOL, use something like the following:

\begin{verbatim}
theory My_Theory
  imports "~~/src/HOL/Number_Theory/Number_Theory"
begin
\end{verbatim}
*}

end

author: Josh-Tilles

repo: AFP

save_path: github-repos/isabelle/Josh-Tilles-AFP


text:
theory Test_Embed_Data2
imports
  Lazy_Case.Lazy_Case
  "../Preproc/Embed"
  "../Preproc/Eval_Instances"
  "Pairing_Heap.Pairing_Heap_Tree"
begin

declare List.Ball_set[code_unfold]

lemma [code_unfold]: "(\<forall>x \<in> set_tree l. P x) \<longleftrightarrow> list_all P (inorder l)"
  by (induction l) auto

declassify valid:
  Pairing_Heap_Tree.link
  Pairing_Heap_Tree.pass\<^sub>1
  Pairing_Heap_Tree.pass\<^sub>2
  Pairing_Heap_Tree.merge_pairs
  Pairing_Heap_Tree.is_root
  Pairing_Heap_Tree.pheap

thm valid

derive evaluate
  Tree.tree
  Orderings_ord__dict
  Orderings_preorder__dict
  Orderings_order__dict
  Orderings_linorder__dict
  HOL_equal__dict

experiment begin

embed (eval) test1 is
  Pairing__Heap__Tree_link
  Pairing__Heap__Tree_pass\<^sub>1
  Pairing__Heap__Tree_pass\<^sub>2
  Pairing__Heap__Tree_merge__pairs
  Pairing__Heap__Tree_pheap
  .

end

end


text:
(* Title: Unary Modalities
   Author: Brijesh Dongol, Victor Gomes, Ian J Hayes, Georg Struth
   Maintainer: Victor Gomes <victor.gomes@cl.cam.ac.uk>
               Georg Struth <g.struth@sheffield.ac.uk>
*)

section \<open>Unary Modalities\<close>

theory Unary_Modalities
  imports Binary_Modalities
begin

text \<open>Unary modalites arise as specialisations of the binary ones; and as generalisations of the
standard (multi-)modal operators from predicates to functions into complete lattices. They are interesting, for instance,
in combination with partial semigroups or monoids, for modelling the Halpern-Shoham modalities in interval logics. \<close>

subsection \<open>Forward and Backward Diamonds\<close>

definition fdia :: "('a \<times> 'b) set \<Rightarrow> ('b \<Rightarrow> 'c::complete_lattice) \<Rightarrow> 'a \<Rightarrow> 'c" ("( |_\<rangle> _ _)" [61,81] 82) where
  "( |R\<rangle> f x) = \<Squnion>{f y|y. (x,y) \<in> R}"

definition bdia :: "('a \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'c::complete_lattice) \<Rightarrow> 'b \<Rightarrow> 'c" ("( \<langle>_| _ _)" [61,81] 82)where
  "(\<langle>R| f y) = \<Squnion>{f x |x. (x,y) \<in> R}"

definition c1 :: "'a \<Rightarrow> 'b::unital_quantale" where
  "c1 x = 1"

text \<open>The relationship with binary modalities is as follows.\<close>

lemma bdia_bmod_comp: "(\<langle>R| f x) = \<otimes> (\<lambda>y x z. (x,y) \<in> R) f c1 x"
  by (simp add: bdia_def bmod_comp_def c1_def)

lemma bmod_fdia_comp: "\<otimes> R f g x = |{(x,(y,z)) |x y z. R x y z}\<rangle> (\<lambda>(x,y). (f x) \<cdot> (g y)) x"
  by (simp add: fdia_def bmod_comp_def)

lemma bmod_fdia_comp_var:
  "\<otimes> R f g x = |{(x,(y,z)) |x y z. R x y z}\<rangle> (\<lambda>(x,y). (\<lambda>(v,w).(v \<cdot> w)) (f x,g y)) x"
  by (simp add: fdia_def bmod_comp_def)

lemma fdia_im: "( |R\<rangle> f x) = \<Squnion>(f ` R `` {x})"
  apply (simp add: fdia_def)
  apply (rule antisym)
  apply (intro Sup_least, clarsimp simp: SUP_upper)
  by (intro SUP_least Sup_upper, force)

lemma fdia_un_rel: "fdia (R \<union> S) = fdia R \<squnion> fdia S"
  apply (simp add: fun_eq_iff)
  by (clarsimp simp: fun_eq_iff fdia_im SUP_union Un_Image)

lemma fdia_Un_rel: "( |\<Union>\<R>\<rangle> f x) = \<Squnion>{|R\<rangle> f x |R. R \<in> \<R>}"
  apply (simp add: fdia_im)
  apply (rule antisym)
  apply (intro SUP_least, safe)
  apply (rule Sup_upper2, force)
  apply (rule SUP_upper, simp)
  apply (rule Sup_least)
  by (clarsimp simp: Image_mono SUP_subset_mono Sup_upper)

lemma fdia_sup_fun: "fdia R (f \<squnion> g) = fdia R f \<squnion> fdia R g"
  by (simp add: fun_eq_iff fdia_im complete_lattice_class.SUP_sup_distrib)

lemma fdia_Sup_fun: "( |R\<rangle> (\<Squnion>\<F>) x) = \<Squnion>{|R\<rangle> f x |f. f \<in> \<F>} "
  apply (simp add: fdia_im)
  apply (rule antisym)
  apply (rule SUP_least)+
  apply (rule Sup_upper2, force)
  apply (rule SUP_upper, simp)
  apply (rule Sup_least, safe)
  apply (rule SUP_least)
  by (simp add: SUP_upper2)

lemma fdia_seq: "fdia (R ; S) f x  = fdia R (fdia S f) x"
  by (simp add: fdia_im relcomp_Image, metis Image_eq_UN SUP_UNION)

lemma fdia_Id [simp]: "( |Id\<rangle> f x) = f x"
  by (simp add: fdia_def)

subsection \<open>Forward and Backward Boxes\<close>

definition fbox :: "('a \<times> 'b) set \<Rightarrow> ('b \<Rightarrow> 'c::complete_lattice) \<Rightarrow> 'a \<Rightarrow> 'c" ("|_] _ _" [61,81] 82) where
  "( |R] f x) = \<Sqinter>{f y|y. (x,y) \<in> R}"

definition bbox :: "('a \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> 'c::complete_lattice) \<Rightarrow> 'b \<Rightarrow> 'c" ("[_| _ _" [61,81] 82)where
  "([R| f y) = \<Sqinter>{f x |x. (x,y) \<in> R}"

subsection \<open>Symmetries and Dualities\<close>

lemma fdia_fbox_demorgan: "( |R\<rangle> (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - |R] (\<lambda>y. -f y) x"
  apply (simp add: fbox_def fdia_def)
  apply (rule antisym)
   apply (rule Sup_least)
   apply (simp add: Inf_lower compl_le_swap1)
  apply (simp add: uminus_Inf)
  apply (rule SUP_least; intro Sup_upper)
  by auto

lemma fbox_fdia_demorgan: "( |R] (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - |R\<rangle> (\<lambda>y. -f y) x"
  apply (simp add: fbox_def fdia_def)
  apply (rule antisym)
   apply (simp add: uminus_Sup)
   apply (rule INF_greatest; rule Inf_lower)
   apply auto[1]
  apply (rule Inf_greatest)
  by (simp add: Sup_upper compl_le_swap2)

lemma bdia_bbox_demorgan: "(\<langle>R| (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - [R| (\<lambda>y. -f y) x"
  apply (simp add: bbox_def bdia_def)
  apply (rule antisym)
   apply (rule Sup_least)
   apply (simp add: Inf_lower compl_le_swap1)
  apply (simp add: uminus_Inf)
  apply (rule SUP_least; intro Sup_upper)
  by auto

lemma bbox_bdia_demorgan: "( [R| (f::'b \<Rightarrow> 'c::complete_boolean_algebra) x) = - \<langle>R| (\<lambda>y. -f y) x"
  apply (simp add: bbox_def bdia_def)
  apply (rule antisym)
   apply (simp add: uminus_Sup)
   apply (rule INF_greatest; rule Inf_lower)
   apply auto[1]
  apply (rule Inf_greatest)
  by (simp add: Sup_upper compl_le_swap2)

lemma fdia_bdia_conv: "( |R\<rangle> f x) = \<langle>converse R| f x"
  by (simp add: fdia_def bdia_def)

lemma fbox_bbox_conv: "( |R] f x) = [converse R| f x"
  by (simp add: fbox_def bbox_def)

lemma fdia_bbox_galois: "(\<forall>x. ( |R\<rangle> f x) \<le> g x) \<longleftrightarrow> (\<forall>x. f x \<le> [R| g x)"
  apply (standard, simp_all add: fdia_def bbox_def)
   apply safe
   apply (rule Inf_greatest)
   apply (force simp: Sup_le_iff)
  apply (rule Sup_least)
  by (force simp: le_Inf_iff)