text:
(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section \<open>Cardinality of Set Partitions\<close>

theory Card_Partitions
imports
  "HOL-Library.Stirling"
  Set_Partition
  Injectivity_Solver
begin

lemma set_partition_on_insert_with_fixed_card_eq:
  assumes "finite A"
  assumes "a \<notin> A"
  shows "{P. partition_on (insert a A) P \<and> card P = Suc k} = (do {
     P <- {P. partition_on A P \<and> card P = Suc k};
     p <- P;
     {insert (insert a p) (P - {p})}
  })
  \<union> (do {
    P <- {P. partition_on A P \<and> card P = k};
    {insert {a} P}
  })" (is "?S = ?T")
proof
  show "?S \<subseteq> ?T"
  proof
    fix P
    assume "P \<in> {P. partition_on (insert a A) P \<and> card P = Suc k}"
    from this have "partition_on (insert a A) P" and "card P = Suc k" by auto
    show "P \<in> ?T"
    proof cases
      assume "{a} \<in> P"
      have "partition_on A (P - {{a}})"
        using \<open>{a} \<in> P\<close> \<open>partition_on (insert a A) P\<close>[THEN partition_on_Diff, of "{{a}}"] \<open>a \<notin> A\<close>
        by auto
      moreover from \<open>{a} \<in> P\<close> \<open>card P = Suc k\<close> have "card (P - {{a}}) = k"
        by (subst card_Diff_singleton) (auto intro: card_ge_0_finite)
      moreover from \<open>{a} \<in> P\<close> have "P = insert {a} (P - {{a}})" by auto
      ultimately have "P \<in> {P. partition_on A P \<and> card P = k} \<bind> (\<lambda>P. {insert {a} P})"
        by auto
      from this show ?thesis by auto
    next
      assume "{a} \<notin> P"
      let ?p' = "(THE X. a \<in> X \<and> X \<in> P)"
      let ?p = "(THE X. a \<in> X \<and> X \<in> P) - {a}"
      let ?P' = "insert ?p (P - {?p'})"
      from \<open>partition_on (insert a A) P\<close> have "a \<in> (THE X. a \<in> X \<and> X \<in> P)"
        using partition_on_in_the_unique_part by fastforce
      from \<open>partition_on (insert a A) P\<close> have "(THE X. a \<in> X \<and> X \<in> P) \<in> P"
        using partition_on_the_part_mem by fastforce
      from this \<open>partition_on (insert a A) P\<close> have "(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P"
        using partition_subset_imp_notin \<open>a \<in> (THE X. a \<in> X \<and> X \<in> P)\<close> by blast
      have "(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}"
        using \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close> \<open>{a} \<notin> P\<close> by auto
      from \<open>partition_on (insert a A) P\<close> have "(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A"
        using \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close> partition_onD1 by fastforce
      note facts_on_the_part_of = \<open>a \<in> (THE X. a \<in> X \<and> X \<in> P)\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close>
        \<open>(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) \<noteq> {a}\<close>
        \<open>(THE X. a \<in> X \<and> X \<in> P) \<subseteq> insert a A\<close>
      from \<open>partition_on (insert a A) P\<close> \<open>finite A\<close> have "finite P"
        by (meson finite.insertI finite_elements)
      from \<open>partition_on (insert a A) P\<close> \<open>a \<notin> A\<close> have "partition_on (A - ?p) (P - {?p'})"
        using facts_on_the_part_of by (auto intro: partition_on_remove_singleton)
      from this have "partition_on A ?P'"
        using facts_on_the_part_of by (auto intro: partition_on_insert simp add: disjnt_iff)
      moreover have "card ?P' = Suc k"
      proof -
        from \<open>card P = Suc k\<close> have "card (P - {THE X. a \<in> X \<and> X \<in> P}) = k"
          using \<open>finite P\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) \<in> P\<close> by simp
        from this show ?thesis
          using \<open>finite P\<close> \<open>(THE X. a \<in> X \<and> X \<in> P) - {a} \<notin> P\<close> by (simp add: card_insert_if)
      qed
      moreover have "?p \<in> ?P'" by auto
      moreover have "P = insert (insert a ?p) (?P' - {?p})"
        using facts_on_the_part_of by (auto simp add: insert_absorb)
      ultimately have "P \<in> {P. partition_on A P \<and> card P = Suc k} \<bind> (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})}))"
        by auto
      then show ?thesis by auto
    qed
  qed
next
  show "?T \<subseteq> ?S"
  proof
    fix P
    assume "P \<in> ?T" (is "_ \<in> ?subexpr1 \<union> ?subexpr2")
    from this show "P \<in> ?S"
    proof
      assume "P \<in> ?subexpr1"
      from this obtain p P' where "P = insert (insert a p) (P' - {p})"
        and "partition_on A P'" and "card P' = Suc k" and "p \<in> P'"  by auto
      from \<open>p \<in> P'\<close> \<open>partition_on A P'\<close> have "partition_on (A - p) (P' - {p})"
        by (simp add: partition_on_remove_singleton)
      from \<open>partition_on A P'\<close> \<open>finite A\<close> have "finite P"
        using \<open>P = _\<close> finite_elements by auto
      from \<open>partition_on A P'\<close> \<open>a \<notin> A\<close> have "insert a p \<notin> P' - {p}"
        using partition_onD1 by fastforce
      from \<open>P = _\<close> this \<open>card P' = Suc k\<close> \<open>finite P\<close> \<open>p \<in> P'\<close>
      have "card P = Suc k" by auto
      moreover have "partition_on (insert a A) P"
        using \<open>partition_on (A - p) (P' - {p})\<close> \<open>a \<notin> A\<close> \<open>p \<in> P'\<close> \<open>partition_on A P'\<close> \<open>P = _\<close>
        by (auto intro!: partition_on_insert dest: partition_onD1 simp add: disjnt_iff)
      ultimately show "P \<in> ?S" by auto
    next
      assume "P \<in> ?subexpr2"
      from this obtain P' where "P = insert {a} P'" and "partition_on A P'" and "card P' = k" by auto
      from \<open>partition_on A P'\<close> \<open>finite A\<close> have "finite P"
        using \<open>P = insert {a} P'\<close> finite_elements by auto
      from \<open>partition_on A P'\<close> \<open>a \<notin> A\<close> have "{a} \<notin> P'"
        using partition_onD1 by fastforce
      from \<open>P = insert {a} P'\<close> \<open>card P' = k\<close> this \<open>finite P\<close> have "card P = Suc k" by auto
      moreover from \<open>partition_on A P'\<close> \<open>a \<notin> A\<close> have "partition_on (insert a A) P"
        using \<open>P = insert {a} P'\<close> by (simp add: partition_on_insert_singleton)
      ultimately show "P \<in> ?S" by auto
    qed
  qed
qed

lemma injectivity_subexpr2:
  assumes "a \<notin> A"
  assumes "insert {a} P = insert {a} P'"
  assumes "(partition_on A P \<and> card P = k') \<and> partition_on A P' \<and> card P' = k'"
  shows "P = P'"
proof -
  from assms(1, 3) have "{a} \<notin> P" and "{a} \<notin> P'"
    using partition_onD1 by auto
  from \<open>{a} \<notin> P\<close> have "P = insert {a} P - {{a}}" by simp
  also from \<open>insert {a} P = insert {a} P'\<close> have "\<dots> = insert {a} P' - {{a}}" by simp
  also from \<open>{a} \<notin> P'\<close> have "\<dots> = P'" by simp
  finally show ?thesis .
qed

theorem card_partition_on:
  assumes "finite A"
  shows "card {P. partition_on A P \<and> card P = k} = Stirling (card A) k"
using assms
proof (induct A arbitrary: k)
  case empty
    have eq: "{P. P = {} \<and> card P = 0} = {{}}" by auto
    show ?case by (cases k) (auto simp add: partition_on_empty eq)
next
  case (insert a A)
  from this show ?case
  proof (cases k)
    case 0
    from insert(1) have empty: "{P. partition_on (insert a A) P \<and> card P = 0} = {}"
      unfolding partition_on_def by (auto simp add: card_eq_0_iff finite_UnionD)
    from 0 insert show ?thesis by (auto simp add: empty)
  next
    case (Suc k')
    let ?subexpr1 = "do {
      P <- {P. partition_on A P \<and> card P = Suc k'};
      p <- P;
      {insert (insert a p) (P - {p})}
    }"
    let ?subexpr2 = "do {
      P <- {P. partition_on A P \<and> card P = k'};
      {insert {a} P}
    }"
    let ?expr = "?subexpr1 \<union> ?subexpr2"
    have "card {P. partition_on (insert a A) P \<and> card P = k} = card ?expr"
      using \<open>finite A\<close> \<open>a \<notin> A\<close> \<open>k = Suc k'\<close> by (simp add: set_partition_on_insert_with_fixed_card_eq)
    also have "card ?expr = Stirling (card A) k' + Stirling (card A) (Suc k') * Suc k'"
    proof -
      have "finite ?subexpr1 \<and> card ?subexpr1 = Stirling (card A) (Suc k') * Suc k'"
      proof -
        from \<open>finite A\<close> have "finite {P. partition_on A P \<and> card P = Suc k'}"
          by (simp add: finitely_many_partition_on)
        moreover have "\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))"
          using finite_elements \<open>finite A\<close> finite_bind
          by (metis (no_types, lifting) finite.emptyI finite_insert mem_Collect_eq)
        moreover have "disjoint_family_on (\<lambda>P. P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) {P. partition_on A P \<and> card P = Suc k'}"
          by (injectivity_solver rule: injectivity_subexpr1(1)[OF \<open>a \<notin> A\<close>])
        moreover have "card (P \<bind> (\<lambda>p. {insert (insert a p) (P - {p})})) = Suc k'"
          if "P \<in> {P. partition_on A P \<and> card P = Suc k'}" for P
        proof -
          from that \<open>finite A\<close> have "finite P"
            using finite_elements by blast
          moreover have "inj_on (\<lambda>p. insert (insert a p) (P - {p})) P"
            using that injectivity_subexpr1(2)[OF \<open>a \<notin> A\<close>] by (simp add: inj_onI)
          moreover from that have "card P = Suc k'" by simp
          ultimately show ?thesis by (simp add: card_bind_singleton)
        qed
        ultimately have "card ?subexpr1 = card {P. partition_on A P \<and> card P = Suc k'} * Suc k'"
          by (subst card_bind_constant) simp+
        from this have "card ?subexpr1 = Stirling (card A) (Suc k') * Suc k'"
          using insert.hyps(3) by simp
        moreover have "finite ?subexpr1"
          using \<open>finite {P. partition_on A P \<and> card P = Suc k'}\<close>
          \<open>\<forall>X\<in>{P. partition_on A P \<and> card P = Suc k'}. finite (X \<bind> (\<lambda>p. {insert (insert a p) (X - {p})}))\<close>
          by (auto intro: finite_bind)
        ultimately show ?thesis by blast
      qed
      moreover have "finite ?subexpr2 \<and> card ?subexpr2 = Stirling (card A) k'"
      proof -
        from \<open>finite A\<close> have "finite {P. partition_on A P \<and> card P = k'}"
          by (simp add: finitely_many_partition_on)
        moreover have " inj_on (insert {a}) {P. partition_on A P \<and> card P = k'}"
          using injectivity_subexpr2[OF \<open>a \<notin> A\<close>] by (simp add: inj_on_def)
        ultimately have "card ?subexpr2 = card {P. partition_on A P \<and> card P = k'}"
          by (simp add: card_bind_singleton)
        also have "\<dots> = Stirling (card A) k'"
          using insert.hyps(3) .
        finally have "card ?subexpr2 = Stirling (card A) k'" .
        moreover have "finite ?subexpr2"
          by (simp add: \<open>finite {P. partition_on A P \<and> card P = k'}\<close> finite_bind)
        ultimately show ?thesis by blast
      qed
      moreover have "?subexpr1 \<inter> ?subexpr2 = {}"
      proof -
        have "\<forall>P\<in>?subexpr1. {a} \<notin> P"
          using insert.hyps(2) by (force elim!: partition_onE)
        moreover have "\<forall>P\<in>?subexpr2. {a} \<in> P" by auto
        ultimately show "?subexpr1 \<inter> ?subexpr2 = {}" by blast
      qed
      ultimately show ?thesis
        by (simp add: card_Un_disjoint)
    qed
    also have "\<dots> = Stirling (card (insert a A)) k"
      using insert(1, 2) \<open>k = Suc k'\<close> by simp
    finally show ?thesis .
  qed
qed

theorem card_partition_on_at_most_size:
  assumes "finite A"
  shows "card {P. partition_on A P \<and> card P \<le> k} = (\<Sum>j\<le>k. Stirling (card A) j)"
proof -
  have "card {P. partition_on A P \<and> card P \<le> k} = card (\<Union>j\<le>k. {P. partition_on A P \<and> card P = j})"
    by (rule arg_cong[where f="card"]) auto
  also have "\<dots> = (\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j})"
    by (subst card_UN_disjoint) (auto simp add: \<open>finite A\<close> finitely_many_partition_on)
  also have "(\<Sum>j\<le>k. card {P. partition_on A P \<and> card P = j}) = (\<Sum>j\<le>k. Stirling (card A) j)"
    using \<open>finite A\<close> by (simp add: card_partition_on)
  finally show ?thesis .
qed

theorem partition_on_size1:
  assumes "finite A"
  shows "{P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} = {(\<lambda>a. {a}) ` A}"
proof
  show "{P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} \<subseteq> {(\<lambda>a. {a}) ` A}"
  proof
    fix P
    assume P: "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
    have "P = (\<lambda>a. {a}) ` A"
    proof
      show "P \<subseteq> (\<lambda>a. {a}) ` A"
      proof
        fix X
        assume "X \<in> P"
        from P this obtain x where "X = {x}"
           by (auto simp add: card_Suc_eq)
        from this \<open>X \<in> P\<close> have "x \<in> A"
          using P unfolding partition_on_def by blast
        from this \<open>X = {x}\<close> show "X \<in>(\<lambda>a. {a}) ` A" by auto
      qed
    next
      show "(\<lambda>a. {a}) ` A \<subseteq> P"
      proof
        fix X
        assume "X \<in> (\<lambda>a. {a}) ` A"
        from this obtain x where X: "X = {x}" "x \<in> A" by auto
        have "\<Union>P = A"
          using P unfolding partition_on_def by blast
        from this \<open>x \<in> A\<close> obtain X' where "x \<in> X'" and "X' \<in> P"
          using UnionE by blast
        from \<open>X' \<in> P\<close> have "card X' = 1"
          using P unfolding partition_on_def by auto
        from this \<open>x \<in> X'\<close> have "X' = {x}"
          using card_1_singletonE by blast
        from this X(1) \<open>X' \<in> P\<close> show "X \<in> P" by auto
      qed
    qed
    from this show "P \<in> {(\<lambda>a. {a}) ` A}" by auto
  qed
next
  show "{(\<lambda>a. {a}) ` A} \<subseteq> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
  proof
    fix P
    assume "P \<in> {(\<lambda>a. {a}) ` A}"
    from this have P: "P = (\<lambda>a. {a}) ` A" by auto
    from this have "partition_on A P" by (auto intro: partition_onI)
    from P this show "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}" by auto
  qed
qed

theorem card_partition_on_size1:
  assumes "finite A"
  shows "card {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)} = 1"
using assms partition_on_size1 by fastforce

lemma card_partition_on_size1_eq_1:
  assumes "finite A"
  assumes "card A \<le> k"
  shows "card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 1"
proof -
  {
    fix P
    assume "partition_on A P" "\<forall>X\<in>P. card X = 1"
    from this have "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}" by simp
    from this have "P \<in> {(\<lambda>a. {a}) ` A}"
      using partition_on_size1 \<open>finite A\<close> by auto
    from this have "P = (\<lambda>a. {a}) ` A" by auto
    moreover from this have "card P = card A"
      by (auto intro: card_image)
  }
  from this have "{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}"
    using \<open>card A \<le> k\<close> by auto
  from this show ?thesis
    using \<open>finite A\<close> by (simp only: card_partition_on_size1)
qed

lemma card_partition_on_size1_eq_0:
  assumes "finite A"
  assumes "k < card A"
  shows "card {P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = 0"
proof -
  {
    fix P
    assume "partition_on A P" "\<forall>X\<in>P. card X = 1"
    from this have "P \<in> {P. partition_on A P \<and> (\<forall>X\<in>P. card X = 1)}" by simp
    from this have "P \<in> {(\<lambda>a. {a}) ` A}"
      using partition_on_size1 \<open>finite A\<close> by auto
    from this have "P = (\<lambda>a. {a}) ` A" by auto
    from this have "card P = card A"
      by (auto intro: card_image)
  }
  from this assms(2) have "{P. partition_on A P \<and> card P \<le> k \<and> (\<forall>X\<in>P. card X = 1)} = {}"
    using Collect_empty_eq leD by fastforce
  from this show ?thesis by (simp only: card_empty)
qed

end

repo: PSL


text:
(*
   Title: The Calculus of Communicating Systems
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Strong_Sim_SC
  imports Strong_Sim
begin

lemma resNilLeft:
  fixes x :: name

  shows "\<lparr>\<nu>x\<rparr>\<zero> \<leadsto>[Rel] \<zero>"
by(auto simp add: simulation_def)

lemma resNilRight:
  fixes x :: name

  shows "\<zero> \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>\<zero>"
by(auto simp add: simulation_def elim: resCases)

lemma test[simp]:
  fixes x :: name
  and   P :: ccs

  shows "x \<sharp> [x].P"
by(auto simp add: abs_fresh)

lemma scopeExtSumLeft:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x \<sharp> P"
  and     C1: "\<And>y R. y \<sharp> R \<Longrightarrow> (\<lparr>\<nu>y\<rparr>R, R) \<in> Rel"
  and     "Id \<subseteq> Rel"

  shows "\<lparr>\<nu>x\<rparr>(P \<oplus> Q) \<leadsto>[Rel] P \<oplus> \<lparr>\<nu>x\<rparr>Q"
using assms
apply(auto simp add: simulation_def)
by(elim sumCases resCases) (blast intro: Res Sum1 Sum2 C1 dest: freshDerivative)+

lemma scopeExtSumRight:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x \<sharp> P"
  and     C1: "\<And>y R. y \<sharp> R \<Longrightarrow> (R, \<lparr>\<nu>y\<rparr>R) \<in> Rel"
  and     "Id \<subseteq> Rel"

  shows "P \<oplus> \<lparr>\<nu>x\<rparr>Q \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>(P \<oplus> Q)"
using assms
apply(auto simp add: simulation_def)
by(elim sumCases resCases) (blast intro: Res Sum1 Sum2 C1 dest: freshDerivative)+

lemma scopeExtLeft:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x \<sharp> P"
  and     C1: "\<And>y R T. y \<sharp> R \<Longrightarrow> (\<lparr>\<nu>y\<rparr>(R \<parallel> T), R \<parallel> \<lparr>\<nu>y\<rparr>T) \<in> Rel"

  shows "\<lparr>\<nu>x\<rparr>(P \<parallel> Q) \<leadsto>[Rel] P \<parallel> \<lparr>\<nu>x\<rparr>Q"
using assms
by(fastforce elim: parCases resCases intro: Res C1 Par1 Par2 Comm dest: freshDerivative simp add: simulation_def)

lemma scopeExtRight:
  fixes x :: name
  and   P :: ccs
  and   Q :: ccs

  assumes "x \<sharp> P"
  and     C1: "\<And>y R T. y \<sharp> R \<Longrightarrow> (R \<parallel> \<lparr>\<nu>y\<rparr>T, \<lparr>\<nu>y\<rparr>(R \<parallel> T)) \<in> Rel"

  shows "P \<parallel> \<lparr>\<nu>x\<rparr>Q \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>(P \<parallel> Q)"
using assms
by(fastforce elim: parCases resCases intro: Res C1 Par1 Par2 Comm dest: freshDerivative simp add: simulation_def)

  assumes "Id \<subseteq> Rel"

  shows "P \<oplus> Q \<leadsto>[Rel] Q \<oplus> P"
using assms
by(force simp add: simulation_def elim: sumCases intro: Sum1 Sum2)

lemma sumAssocLeft:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "Id \<subseteq> Rel"

  shows "(P \<oplus> Q) \<oplus> R \<leadsto>[Rel] P \<oplus> (Q \<oplus> R)"
using assms
by(force simp add: simulation_def elim: sumCases intro: Sum1 Sum2)

lemma sumAssocRight:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes "Id \<subseteq> Rel"

  shows " P \<oplus> (Q \<oplus> R) \<leadsto>[Rel] (P \<oplus> Q) \<oplus> R"
using assms
by(intro simI, elim sumCases) (blast intro: Sum1 Sum2)+

lemma sumIdLeft:
  fixes P   :: ccs
  and   Rel :: "(ccs \<times> ccs) set"

  assumes "Id \<subseteq> Rel"

  shows "P \<oplus> \<zero> \<leadsto>[Rel] P"
using assms
by(auto simp add: simulation_def intro: Sum1)

lemma sumIdRight:
  fixes P   :: ccs
  and   Rel :: "(ccs \<times> ccs) set"

  assumes "Id \<subseteq> Rel"

  shows "P \<leadsto>[Rel] P \<oplus> \<zero>"
using assms
by(fastforce simp add: simulation_def elim: sumCases)

lemma parComm:
  fixes P :: ccs
  and   Q :: ccs

  assumes C1: "\<And>R T. (R \<parallel> T, T \<parallel> R) \<in> Rel"

  shows "P \<parallel> Q \<leadsto>[Rel] Q \<parallel> P"
by(fastforce simp add: simulation_def elim: parCases intro: Par1 Par2 Comm C1)

lemma parAssocLeft:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes C1: "\<And>S T U. ((S \<parallel> T) \<parallel> U, S \<parallel> (T \<parallel> U)) \<in> Rel"

  shows "(P \<parallel> Q) \<parallel> R \<leadsto>[Rel] P \<parallel> (Q \<parallel> R)"
by(fastforce simp add: simulation_def elim: parCases intro: Par1 Par2 Comm C1)

lemma parAssocRight:
  fixes P :: ccs
  and   Q :: ccs
  and   R :: ccs

  assumes C1: "\<And>S T U. (S \<parallel> (T \<parallel> U), (S \<parallel> T) \<parallel> U) \<in> Rel"

  shows "P \<parallel> (Q \<parallel> R) \<leadsto>[Rel] (P \<parallel> Q) \<parallel> R"
by(fastforce simp add: simulation_def elim: parCases intro: Par1 Par2 Comm C1)

lemma parIdLeft:
  fixes P   :: ccs
  and   Rel :: "(ccs \<times> ccs) set"

  assumes "\<And>Q. (Q \<parallel> \<zero>, Q) \<in> Rel"

  shows "P \<parallel> \<zero> \<leadsto>[Rel] P"
using assms
by(auto simp add: simulation_def intro: Par1)

lemma parIdRight:
  fixes P   :: ccs
  and   Rel :: "(ccs \<times> ccs) set"

  assumes "\<And>Q. (Q, Q \<parallel> \<zero>) \<in> Rel"

  shows "P \<leadsto>[Rel] P \<parallel> \<zero>"
using assms
by(fastforce simp add: simulation_def elim: parCases)

declare fresh_atm[simp]

lemma resActLeft:
  fixes x :: name
  and   \<alpha> :: act
  and   P :: ccs

  assumes "x \<sharp> \<alpha>"
  and     "Id \<subseteq> Rel"

  shows "\<lparr>\<nu>x\<rparr>(\<alpha>.(P)) \<leadsto>[Rel] (\<alpha>.(\<lparr>\<nu>x\<rparr>P))"
using assms
by(fastforce simp add: simulation_def elim: actCases intro: Res Action)

lemma resActRight:
  fixes x :: name
  and   \<alpha> :: act
  and   P :: ccs

  assumes "x \<sharp> \<alpha>"
  and     "Id \<subseteq> Rel"

  shows "\<alpha>.(\<lparr>\<nu>x\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>x\<rparr>(\<alpha>.(P))"
using assms
by(fastforce simp add: simulation_def elim: resCases actCases intro: Action)

lemma resComm:
  fixes x :: name
  and   y :: name
  and   P :: ccs

  assumes "\<And>Q. (\<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>Q), \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>Q)) \<in> Rel"

  shows "\<lparr>\<nu>x\<rparr>(\<lparr>\<nu>y\<rparr>P) \<leadsto>[Rel] \<lparr>\<nu>y\<rparr>(\<lparr>\<nu>x\<rparr>P)"
using assms
by(fastforce simp add: simulation_def elim: resCases intro: Res)

inductive_cases bangCases[simplified ccs.distinct act.distinct]: "!P \<longmapsto>\<alpha> \<prec> P'"

lemma bangUnfoldLeft:
  fixes P :: ccs

  assumes "Id \<subseteq> Rel"

  shows "P \<parallel> !P \<leadsto>[Rel] !P"
using assms
by(fastforce simp add: simulation_def ccs.inject elim: bangCases)

lemma bangUnfoldRight:
  fixes P :: ccs

  assumes "Id \<subseteq> Rel"

  shows "!P \<leadsto>[Rel] P \<parallel> !P"
using assms
by(fastforce simp add: simulation_def ccs.inject intro: Bang)

end


(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

theory ArchSchedule_AI
imports Schedule_AI
begin

context Arch begin global_naming ARM_HYP

named_theorems Schedule_AI_asms

lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]:
  "valid invs (do_machine_op (mapM (\<lambda>p. storeWord p 0) S)) (\<lambda>_. invs)"
  apply (simp add: dom_mapM ef_storeWord)
  apply (rule mapM_UNIV_wp)
  apply (simp add: do_machine_op_def split_def)
  apply wp
  apply (clarsimp simp: invs_def valid_state_def cur_tcb_def
                        valid_machine_state_def)
  apply (rule conjI)
   apply(erule use_valid[OF _ storeWord_valid_irq_states], simp)
  apply (erule use_valid)
   apply (simp add: storeWord_def word_rsplit_0)
   apply wp
  apply (clarsimp simp: word_bits_conv)
  done

crunch device_state_inv[wp]: clearExMonitor "\<lambda>ms. P (device_state ms)"

lemma clearExMonitor_invs [wp]:
  "\<lbrace>invs\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. invs\<rbrace>"
  apply (wp dmo_invs)
  apply (clarsimp simp: clearExMonitor_def machine_op_lift_def
                        machine_rest_lift_def in_monad select_f_def)
  done

global_naming Arch

lemma arch_stt_invs [wp,Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>"
  apply (wpsimp simp: arch_switch_to_thread_def)
  by (rule sym_refs_VCPU_hyp_live; fastforce)

lemma arch_stt_tcb [wp,Schedule_AI_asms]:
  "\<lbrace>tcb_at t'\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. tcb_at t'\<rbrace>"
  by (wpsimp simp: arch_switch_to_thread_def wp: tcb_at_typ_at)

lemma arch_stt_runnable[Schedule_AI_asms]:
  "\<lbrace>st_tcb_at runnable t\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>r. st_tcb_at runnable t\<rbrace>"
  by (wpsimp simp: arch_switch_to_thread_def)

lemma idle_strg:
  "thread = idle_thread s \<and> invs s \<Longrightarrow> invs (s\<lparr>cur_thread := thread\<rparr>)"
  by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def
                     pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def)

lemma set_vcpu_ct[wp]:
  "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> set_vcpu v v' \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
  by (wpsimp simp: set_vcpu_def wp: get_object_wp)

crunches
  vcpu_update, vgic_update, vgic_update_lr, vcpu_restore_reg_range, vcpu_save_reg_range,
  vcpu_enable, vcpu_disable, vcpu_save, vcpu_restore, vcpu_switch, vcpu_save
  for it[wp]: "\<lambda>s. P (idle_thread s)"
  and ct[wp]: "\<lambda>s. P (cur_thread s)"
  (wp: mapM_x_wp mapM_wp subset_refl)

lemma arch_stit_invs[wp, Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. invs\<rbrace>"
  by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def)

lemma arch_stit_tcb_at[wp]:
  "\<lbrace>tcb_at t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. tcb_at t\<rbrace>"
  apply (simp add: arch_switch_to_idle_thread_def )
  apply (wp tcb_at_typ_at)
  done

crunches set_vm_root
  for ct[wp]: "\<lambda>s. P (cur_thread s)"
  and it[wp]: "\<lambda>s. P (idle_thread s)"
  (simp: crunch_simps wp: hoare_drop_imps)

lemma arch_stit_activatable[wp, Schedule_AI_asms]:
  "\<lbrace>ct_in_state activatable\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>"
  apply (clarsimp simp: arch_switch_to_idle_thread_def)
  apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift)
  done

lemma stit_invs [wp,Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. invs\<rbrace>"
  apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def)
  apply (wpsimp|strengthen idle_strg)+
  done

lemma stit_activatable[Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>"
  apply (simp add: switch_to_idle_thread_def arch_switch_to_idle_thread_def)
  apply (wp | simp add: ct_in_state_def)+
  apply (clarsimp simp: invs_def valid_state_def cur_tcb_def valid_idle_def
                 elim!: pred_tcb_weaken_strongerE)
  done

lemma stt_invs [wp,Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>"
  apply (simp add: switch_to_thread_def)
  apply wp
     apply (simp add: trans_state_update[symmetric] del: trans_state_update)
    apply (rule_tac Q="\<lambda>_. invs and tcb_at t'" in hoare_strengthen_post, wp)
    apply (clarsimp simp: invs_def valid_state_def valid_idle_def
                          valid_irq_node_def valid_machine_state_def)
    apply (fastforce simp: cur_tcb_def obj_at_def
                     elim: valid_pspace_eqI ifunsafe_pspaceI)
   apply wp+
  apply clarsimp
  apply (simp add: is_tcb_def)
  done
end

interpretation Schedule_AI_U?: Schedule_AI_U
  proof goal_cases
  interpret Arch .
  case 1 show ?case
  by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?)
  qed

interpretation Schedule_AI?: Schedule_AI
  proof goal_cases
  interpret Arch .
  case 1 show ?case
  by (intro_locales; (unfold_locales; fact Schedule_AI_asms)?)
  qed

end


text:
(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

theory PageTableDuplicates
imports Syscall_R
begin

context begin interpretation Arch . (*FIXME: arch_split*)

lemma doMachineOp_ksPSpace_inv[wp]:
  "\<lbrace>\<lambda>s. P (ksPSpace s)\<rbrace> doMachineOp f \<lbrace>\<lambda>ya s. P (ksPSpace s)\<rbrace>"
  by (simp add:doMachineOp_def split_def | wp)+

lemma foldr_data_map_insert[simp]:
  "foldr (\<lambda>addr map a. if a = addr then Some b else map a) = foldr (\<lambda>addr. data_map_insert addr b)"
  apply (rule ext)+
  apply (simp add:data_map_insert_def[abs_def] fun_upd_def)
  done

crunch arch_inv[wp]: resetUntypedCap "\<lambda>s. P (ksArchState s)"
  (simp: crunch_simps
     wp: hoare_drop_imps hoare_unless_wp mapME_x_inv_wp
         preemptionPoint_inv)

lemma mapM_x_mapM_valid:
  "\<lbrace> P \<rbrace> mapM_x f xs \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>mapM f xs \<lbrace>\<lambda>r. Q\<rbrace>"
  apply (simp add:NonDetMonadLemmaBucket.mapM_x_mapM)
  apply (clarsimp simp:valid_def return_def bind_def)
  apply (drule spec)
  apply (erule impE)
   apply simp
  apply (drule(1) bspec)
  apply fastforce
  done

declare withoutPreemption_lift [wp del]

crunch valid_cap'[wp]:
  isFinalCapability "\<lambda>s. valid_cap' cap s"
  (wp: crunch_wps filterM_preserved simp: crunch_simps unless_def)

end

end

author: NICTA


text:
(* Author: Tobias Nipkow *)

theory Def_Init_Small
imports Star Def_Init_Exp Def_Init
begin

subsection "Initialization-Sensitive Small Step Semantics"

inductive
  small_step :: "(com \<times> state) \<Rightarrow> (com \<times> state) \<Rightarrow> bool" (infix "\<rightarrow>" 55)
where
Assign:  "aval a s = Some i \<Longrightarrow> (x ::= a, s) \<rightarrow> (SKIP, s(x := Some i))" |

Seq1:   "(SKIP;;c,s) \<rightarrow> (c,s)" |
Seq2:   "(c\<^sub>1,s) \<rightarrow> (c\<^sub>1',s') \<Longrightarrow> (c\<^sub>1;;c\<^sub>2,s) \<rightarrow> (c\<^sub>1';;c\<^sub>2,s')" |

IfTrue:  "bval b s = Some True \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>1,s)" |
IfFalse: "bval b s = Some False \<Longrightarrow> (IF b THEN c\<^sub>1 ELSE c\<^sub>2,s) \<rightarrow> (c\<^sub>2,s)" |

While:   "(WHILE b DO c,s) \<rightarrow> (IF b THEN c;; WHILE b DO c ELSE SKIP,s)"

lemmas small_step_induct = small_step.induct[split_format(complete)]

abbreviation small_steps :: "com * state \<Rightarrow> com * state \<Rightarrow> bool" (infix "\<rightarrow>*" 55)
where "x \<rightarrow>* y == star small_step x y"

subsection "Soundness wrt Small Steps"

theorem progress:
  "D (dom s) c A' \<Longrightarrow> c \<noteq> SKIP \<Longrightarrow> \<exists>cs'. (c,s) \<rightarrow> cs'"
proof (induction c arbitrary: s A')
  case Assign thus ?case by auto (metis aval_Some small_step.Assign)
next
  case (If b c1 c2)
  then obtain bv where "bval b s = Some bv" by (auto dest!:bval_Some)
  then show ?case
    by(cases bv)(auto intro: small_step.IfTrue small_step.IfFalse)
qed (fastforce intro: small_step.intros)+

lemma D_mono:  "D A c M \<Longrightarrow> A \<subseteq> A' \<Longrightarrow> \<exists>M'. D A' c M' & M <= M'"
proof (induction c arbitrary: A A' M)
  case Seq thus ?case by auto (metis D.intros(3))
next
  case (If b c1 c2)
  then obtain M1 M2 where "vars b \<subseteq> A" "D A c1 M1" "D A c2 M2" "M = M1 \<inter> M2"
    by auto
  with If.IH \<open>A \<subseteq> A'\<close> obtain M1' M2'
    where "D A' c1 M1'" "D A' c2 M2'" and "M1 \<subseteq> M1'" "M2 \<subseteq> M2'" by metis
  hence "D A' (IF b THEN c1 ELSE c2) (M1' \<inter> M2')" and "M \<subseteq> M1' \<inter> M2'"
    using \<open>vars b \<subseteq> A\<close> \<open>A \<subseteq> A'\<close> \<open>M = M1 \<inter> M2\<close> by(fastforce intro: D.intros)+
  thus ?case by metis
next
  case While thus ?case by auto (metis D.intros(5) subset_trans)
qed (auto intro: D.intros)

theorem D_preservation:
  "(c,s) \<rightarrow> (c',s') \<Longrightarrow> D (dom s) c A \<Longrightarrow> \<exists>A'. D (dom s') c' A' & A <= A'"
proof (induction arbitrary: A rule: small_step_induct)
  case (While b c s)
  then obtain A' where A': "vars b \<subseteq> dom s" "A = dom s" "D (dom s) c A'" by blast
  then obtain A'' where "D A' c A''" by (metis D_incr D_mono)
  with A' have "D (dom s) (IF b THEN c;; WHILE b DO c ELSE SKIP) (dom s)"
    by (metis D.If[OF \<open>vars b \<subseteq> dom s\<close> D.Seq[OF \<open>D (dom s) c A'\<close> D.While[OF _ \<open>D A' c A''\<close>]] D.Skip] D_incr Int_absorb1 subset_trans)
  thus ?case by (metis D_incr \<open>A = dom s\<close>)
next
  case Seq2 thus ?case by auto (metis D_mono D.intros(3))
qed (auto intro: D.intros)

theorem D_sound:
  "(c,s) \<rightarrow>* (c',s') \<Longrightarrow> D (dom s) c A'
   \<Longrightarrow> (\<exists>cs''. (c',s') \<rightarrow> cs'') \<or> c' = SKIP"
apply(induction arbitrary: A' rule:star_induct)
apply (metis progress)
by (metis D_preservation)

end

repo: isabelle


(*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 *)

(*
Utilities for the machine level which are not machine-dependent.
*)

chapter "Machine Accessor Functions"

theory MiscMachine_A
imports Machine_A "ExecSpec.MachineExports"
begin

context begin interpretation Arch .

requalify_types
  user_context
  user_monad
  register
  data
  obj_ref
  asid_high_len
  asid_high_index
  asid_low_len
  asid_low_index
  asid_len
  asid_rep_len
  asid
  cap_ref
  length_type
  vspace_ref

requalify_consts
  nat_to_cref
  msg_info_register
  msg_registers
  cap_register
  badge_register
  frame_registers
  gp_registers
  exception_message
  syscall_message
  new_context
  slot_bits
  oref_to_data
  data_to_oref
  vref_to_data
  data_to_vref
  nat_to_len
  data_to_nat
  data_to_16
  data_to_cptr
  combine_ntfn_badges

end

(* Needs to be done here after plain type names are exported *)
translations
  (type) "'a user_monad" <= (type) "user_context \<Rightarrow> ('a \<times> user_context) set \<times> bool"

definition
  asid_high_bits :: nat
where
  "asid_high_bits \<equiv> LENGTH(asid_high_len)"

definition
  asid_low_bits :: nat
where
  "asid_low_bits \<equiv> LENGTH(asid_low_len)"

definition
  asid_bits :: nat
where
  "asid_bits \<equiv> LENGTH(asid_len)"

lemmas asid_bits_defs =
  asid_bits_def asid_high_bits_def asid_low_bits_def

(* Sanity checks. *)
lemma asid_bits_len_checks:
  "asid_bits = asid_high_bits + asid_low_bits"
  "asid_bits \<le> LENGTH(asid_rep_len)"
  unfolding asid_bits_defs by auto

definition ipa_size :: nat where
  "ipa_size \<equiv> if config_ARM_PA_SIZE_BITS_40 then 40 else 44"

end


text:
(*  Title:      HOL/BNF_Composition.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Jan van Brügge, TU Muenchen
    Copyright   2012, 2013, 2014, 2022

Composition of bounded natural functors.
*)

section \<open>Composition of Bounded Natural Functors\<close>

theory BNF_Composition
imports BNF_Def
begin

lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X"
  by simp

lemma empty_natural: "(\<lambda>_. {}) \<circ> f = image g \<circ> (\<lambda>_. {})"
  by (rule ext) simp

lemma Cinfinite_gt_empty: "Cinfinite r \<Longrightarrow> |{}| <o r"
  by (simp add: cinfinite_def finite_ordLess_infinite card_of_ordIso_finite Field_card_of card_of_well_order_on emptyI card_order_on_well_order_on)

lemma Union_natural: "Union \<circ> image (image f) = image f \<circ> Union"
  by (rule ext) (auto simp only: comp_apply)

lemma in_Union_o_assoc: "x \<in> (Union \<circ> gset \<circ> gmap) A \<Longrightarrow> x \<in> (Union \<circ> (gset \<circ> gmap)) A"
  by (unfold comp_assoc)

lemma regularCard_UNION_bound:
  assumes "Cinfinite r" "regularCard r" and "|I| <o r" "\<And>i. i \<in> I \<Longrightarrow> |A i| <o r"
  shows "|\<Union>i\<in>I. A i| <o r"
  using assms cinfinite_def regularCard_stable stable_UNION by blast

lemma comp_single_set_bd_strict:
  assumes fbd: "Cinfinite fbd" "regularCard fbd" and
    gbd: "Cinfinite gbd" "regularCard gbd" and
    fset_bd: "\<And>x. |fset x| <o fbd" and
    gset_bd: "\<And>x. |gset x| <o gbd"
  shows "|\<Union>(fset ` gset x)| <o gbd *c fbd"
proof (cases "fbd <o gbd")
  case True
  then have "|fset x| <o gbd" for x using fset_bd ordLess_transitive by blast
  then have "|\<Union>(fset ` gset x)| <o gbd" using regularCard_UNION_bound[OF gbd gset_bd] by blast
  then have "|\<Union> (fset ` gset x)| <o fbd *c gbd"
    using ordLess_ordLeq_trans ordLeq_cprod2 gbd(1) fbd(1) cinfinite_not_czero by blast
  then show ?thesis using ordLess_ordIso_trans cprod_com by blast
next
  case False
  have "Well_order fbd" "Well_order gbd" using fbd(1) gbd(1) card_order_on_well_order_on by auto
  then have "gbd \<le>o fbd" using not_ordLess_iff_ordLeq False by blast
  then have "|gset x| <o fbd" for x using gset_bd ordLess_ordLeq_trans by blast
  then have "|\<Union>(fset ` gset x)| <o fbd" using regularCard_UNION_bound[OF fbd] fset_bd by blast
  then show ?thesis using ordLess_ordLeq_trans ordLeq_cprod2 gbd(1) fbd(1) cinfinite_not_czero by blast
qed

lemma comp_single_set_bd:
  assumes fbd_Card_order: "Card_order fbd" and
    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
    gset_bd: "\<And>x. |gset x| \<le>o gbd"
  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
  apply simp
  apply (rule ordLeq_transitive)
  apply (rule card_of_UNION_Sigma)
  apply (subst SIGMA_CSUM)
  apply (rule ordLeq_transitive)
  apply (rule card_of_Csum_Times')
  apply (rule fbd_Card_order)
  apply (rule ballI)
  apply (rule fset_bd)
  apply (rule ordLeq_transitive)
  apply (rule cprod_mono1)
  apply (rule gset_bd)
  apply (rule ordIso_imp_ordLeq)
  apply (rule ordIso_refl)
  apply (rule Card_order_cprod)
  done

lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
  apply (erule ordIso_transitive)
  apply (frule csum_absorb2')
  apply (erule ordLeq_refl)
  by simp

lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
  apply (erule ordIso_transitive)
  apply (rule cprod_infinite)
  by simp

lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
  by simp

lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
  by simp

lemma image_o_collect: "collect ((\<lambda>f. image g \<circ> f) ` F) = image g \<circ> collect F"
  by (rule ext) (auto simp add: collect_def)

lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
  by blast

lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
  by blast

lemma comp_set_bd_Union_o_collect: "|\<Union>(\<Union>((\<lambda>f. f x) ` X))| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
  by (unfold comp_apply collect_def) simp

lemma comp_set_bd_Union_o_collect_strict: "|\<Union>(\<Union>((\<lambda>f. f x) ` X))| <o hbd \<Longrightarrow> |(Union \<circ> collect X) x| <o hbd"
  by (unfold comp_apply collect_def) simp

lemma Collect_inj: "Collect P = Collect Q \<Longrightarrow> P = Q"
  by blast

lemma Grp_fst_snd: "(Grp (Collect (case_prod R)) fst)\<inverse>\<inverse> OO Grp (Collect (case_prod R)) snd = R"
  unfolding Grp_def fun_eq_iff relcompp.simps by auto

lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)\<inverse>\<inverse> OO Grp A g = (Grp B f)\<inverse>\<inverse> OO Grp B g"
  by (rule arg_cong)

lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
  vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
  unfolding vimage2p_def by auto

lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f \<circ> M \<circ> g) x = (f \<circ> N \<circ> h) x"
  by auto

lemma type_copy_set_bd: "(\<And>y. |S y| <o bd) \<Longrightarrow> |(S \<circ> Rep) x| <o bd"
  by auto

lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
  by simp

lemma Ball_comp_iff: "(\<lambda>x. Ball (A x) f) \<circ> g = (\<lambda>x. Ball ((A \<circ> g) x) f)"
  unfolding o_def by auto

lemma conj_comp_iff: "(\<lambda>x. P x \<and> Q x) \<circ> g = (\<lambda>x. (P \<circ> g) x \<and> (Q \<circ> g) x)"
  unfolding o_def by auto

context
  fixes Rep Abs
  assumes type_copy: "type_definition Rep Abs UNIV"
begin

lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs \<circ> M \<circ> Rep = id"
  using type_definition.Rep_inverse[OF type_copy] by auto

lemma type_copy_map_comp0: "M = M1 \<circ> M2 \<Longrightarrow> f \<circ> M \<circ> g = (f \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> g)"
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto

lemma type_copy_set_map0: "S \<circ> M = image f \<circ> S' \<Longrightarrow> (S \<circ> Rep) \<circ> (Abs \<circ> M \<circ> g) = image f \<circ> (S' \<circ> g)"
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)

lemma type_copy_wit: "x \<in> (S \<circ> Rep) (Abs y) \<Longrightarrow> x \<in> S y"
  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto

lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
    Grp (Collect (\<lambda>x. P (f x))) (Abs \<circ> h \<circ> f)"
  unfolding vimage2p_def Grp_def fun_eq_iff
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   type_definition.Rep_inverse[OF type_copy] dest: sym)

lemma type_copy_vimage2p_Grp_Abs:
  "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep \<circ> h \<circ> g)"
  unfolding vimage2p_def Grp_def fun_eq_iff
  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   type_definition.Rep_inverse[OF type_copy] dest: sym)

lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
proof safe
  fix b assume "F b"
  show "\<exists>b'. F (Rep b')"
  proof (rule exI)
    from \<open>F b\<close> show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
  qed
qed blast

lemma vimage2p_relcompp_converse:
  "vimage2p f g (R\<inverse>\<inverse> OO S) = (vimage2p Rep f R)\<inverse>\<inverse> OO vimage2p Rep g S"
  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
  by (auto simp: type_copy_ex_RepI)

end

bnf DEADID: 'a
  map: "id :: 'a \<Rightarrow> 'a"
  bd: natLeq
  rel: "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
  by (auto simp add: natLeq_card_order natLeq_cinfinite regularCard_natLeq)

definition id_bnf :: "'a \<Rightarrow> 'a" where
  "id_bnf \<equiv> (\<lambda>x. x)"

lemma id_bnf_apply: "id_bnf x = x"
  unfolding id_bnf_def by simp

bnf ID: 'a
  map: "id_bnf :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
  sets: "\<lambda>x. {x}"
  bd: natLeq
  rel: "id_bnf :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
  pred: "id_bnf :: ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
  unfolding id_bnf_def
  apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite regularCard_natLeq)
  apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
  apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
  done

lemma type_definition_id_bnf_UNIV: "type_definition id_bnf id_bnf UNIV"
  unfolding id_bnf_def by unfold_locales auto

ML_file \<open>Tools/BNF/bnf_comp_tactics.ML\<close>
ML_file \<open>Tools/BNF/bnf_comp.ML\<close>

hide_fact
  DEADID.inj_map DEADID.inj_map_strong DEADID.map_comp DEADID.map_cong DEADID.map_cong0
  DEADID.map_cong_simp DEADID.map_id DEADID.map_id0 DEADID.map_ident DEADID.map_transfer
  DEADID.rel_Grp DEADID.rel_compp DEADID.rel_compp_Grp DEADID.rel_conversep DEADID.rel_eq
  DEADID.rel_flip DEADID.rel_map DEADID.rel_mono DEADID.rel_transfer
  ID.inj_map ID.inj_map_strong ID.map_comp ID.map_cong ID.map_cong0 ID.map_cong_simp ID.map_id
  ID.map_id0 ID.map_ident ID.map_transfer ID.rel_Grp ID.rel_compp ID.rel_compp_Grp ID.rel_conversep
  ID.rel_eq ID.rel_flip ID.rel_map ID.rel_mono ID.rel_transfer ID.set_map ID.set_transfer

end


text:
theory chapter5_exercises_test
imports Main sexpression_print
begin

(*
Exercise 5.1. Give a readable, structured proof of the following lemma:
*)

thm allE (* \<lbrakk>\<forall>x. ?P x; ?P ?x \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R *)
thm exE (* \<lbrakk>\<exists>x. ?P x; \<And>x. ?P x \<Longrightarrow> ?Q\<rbrakk> \<Longrightarrow> ?Q *)
lemma exercise5p1_apply:
"\<lbrakk> \<forall>x y. T x y \<or> T y x;(\<forall>x y. A x y \<and> A y x \<longrightarrow> x = y);(\<forall>x y. T x y \<longrightarrow> A x y); A x y\<rbrakk> \<Longrightarrow> T x y"
  by metis

thm HOL.mp (* \<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q *)
thm conjE (* \<lbrakk>?P \<and> ?Q; \<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R *)
lemma exercise5p1:
  assumes T: "\<forall>x y. T x y \<or> T y x"
    and   A: "\<forall>x y. A x y \<and> A y x \<longrightarrow> x = y"
    and   TA: "\<forall>x y. T x y \<longrightarrow> A x y"
    and   "A x y"
  shows "T x y"
proof -
  have T2: "T x y \<or> T y x" using T by simp
  print_state
  ML_val "List.map to_sexpr_untyped (Thm.prems_of (#goal @{Isar.goal}))"
  have exercise5p1 sorry
qed

end

repo: isabelle-gym


text:
(*    Title:              SatSolverVerification/SatSolverCode.thy
      Author:             Filip Maric
      Maintainer:         Filip Maric <filip at matf.bg.ac.yu>
*)

header{* Functional implementation of a SAT solver with Two Watch literal propagation. *}
theory SatSolverCode
imports SatSolverVerification "~~/src/HOL/Library/Code_Target_Numeral"
begin

(******************************************************************************)
subsection{* Specification *}
(******************************************************************************)

lemma [code_unfold]:
  fixes literal :: Literal and clause :: Clause
  shows "literal el clause = List.member clause literal"
  by (auto simp add: member_def)

datatype ExtendedBool = TRUE | FALSE | UNDEF

record State =
  -- {* Satisfiability flag: UNDEF, TRUE or FALSE *}
"getSATFlag" :: ExtendedBool
  -- {* Formula *}
"getF"       :: Formula
  -- {* Assertion Trail *}
"getM"       :: LiteralTrail
  -- {* Conflict flag *}
"getConflictFlag"   :: bool   -- {* raised iff M falsifies F *}
  -- {* Conflict clause index *}
"getConflictClause" :: nat    -- {* corresponding clause from F is false in M *}
  -- {* Unit propagation queue *}
"getQ" :: "Literal list"
  -- {* Unit propagation graph *}
"getReason" :: "Literal \<Rightarrow> nat option" -- {* index of a clause that is a reason for propagation of a literal *}
  -- {* Two-watch literal scheme *}
  -- {* clause indices instead of clauses are used *}
"getWatch1" :: "nat \<Rightarrow> Literal option"  -- {* First watch of a clause *}
"getWatch2" :: "nat \<Rightarrow> Literal option"  -- {* Second watch of a clause *}
"getWatchList" :: "Literal \<Rightarrow> nat list" -- {* Watch list of a given literal *}
  -- {* Conflict analysis data structures *}
"getC"   :: Clause             -- {* Conflict analysis clause - always false in M *}
"getCl"  :: Literal            -- {* Last asserted literal in (opposite getC) *}
"getCll" :: Literal            -- {* Second last asserted literal in (opposite getC) *}
"getCn"  :: nat                -- {* Number of literals of (opposite getC) on the (currentLevel M) *}

definition
setWatch1 :: "nat \<Rightarrow> Literal \<Rightarrow> State \<Rightarrow> State"
where
"setWatch1 clause literal state =
    state\<lparr> getWatch1 := (getWatch1 state)(clause := Some literal),
           getWatchList := (getWatchList state)(literal := clause # (getWatchList state literal))
         \<rparr>
"
declare setWatch1_def[code_unfold]

definition
setWatch2 :: "nat \<Rightarrow> Literal \<Rightarrow> State \<Rightarrow> State"
where
"setWatch2 clause literal state =
    state\<lparr> getWatch2 := (getWatch2 state)(clause := Some literal),
           getWatchList := (getWatchList state)(literal := clause # (getWatchList state literal))
         \<rparr>
"
declare setWatch2_def[code_unfold]

definition
swapWatches :: "nat \<Rightarrow> State \<Rightarrow> State"
where
"swapWatches clause state ==
    state\<lparr> getWatch1 := (getWatch1 state)(clause := (getWatch2 state clause)),
           getWatch2 := (getWatch2 state)(clause := (getWatch1 state clause))
         \<rparr>
"
declare swapWatches_def[code_unfold]

primrec getNonWatchedUnfalsifiedLiteral :: "Clause \<Rightarrow> Literal \<Rightarrow> Literal \<Rightarrow> LiteralTrail \<Rightarrow> Literal option"
where
"getNonWatchedUnfalsifiedLiteral [] w1 w2 M = None" |
"getNonWatchedUnfalsifiedLiteral (literal # clause) w1 w2 M =
    (if literal \<noteq> w1 \<and>
        literal \<noteq> w2 \<and>
        \<not> (literalFalse literal (elements M)) then
            Some literal
     else
            getNonWatchedUnfalsifiedLiteral clause w1 w2 M
    )
"

definition
setReason :: "Literal \<Rightarrow> nat \<Rightarrow> State \<Rightarrow> State"
where
"setReason literal clause state =
    state\<lparr> getReason := (getReason state)(literal := Some clause) \<rparr>
"
declare setReason_def[code_unfold]

primrec notifyWatches_loop::"Literal \<Rightarrow> nat list \<Rightarrow> nat list \<Rightarrow> State \<Rightarrow> State"
where
"notifyWatches_loop literal [] newWl state = state\<lparr> getWatchList := (getWatchList state)(literal := newWl) \<rparr>" |
"notifyWatches_loop literal (clause # list') newWl state =
    (let state' = (if Some literal = (getWatch1 state clause) then
                       (swapWatches clause state)
                   else
                       state) in
    case (getWatch1 state' clause) of
        None \<Rightarrow> state
    |   Some w1 \<Rightarrow> (
    case (getWatch2 state' clause) of
        None \<Rightarrow> state
    |   Some w2 \<Rightarrow>
    (if (literalTrue w1 (elements (getM state'))) then
        notifyWatches_loop literal list' (clause # newWl) state'
     else
        (case (getNonWatchedUnfalsifiedLiteral (nth (getF state') clause) w1 w2 (getM state')) of
            Some l' \<Rightarrow>
                notifyWatches_loop literal list' newWl (setWatch2 clause l' state')
          | None \<Rightarrow>
                (if (literalFalse w1 (elements (getM state'))) then
                    let state'' = (state'\<lparr> getConflictFlag := True, getConflictClause := clause \<rparr>) in
                    notifyWatches_loop literal list' (clause # newWl) state''
                else
                    let state'' = state'\<lparr> getQ := (if w1 el (getQ state') then
                                                      (getQ state')
                                                  else
                                                      (getQ state') @ [w1]
                                                  )
                                        \<rparr> in
                   let state''' = (setReason w1 clause state'') in
                   notifyWatches_loop literal list' (clause # newWl) state'''
                )
        )
    )
    )
    )
"

definition
notifyWatches :: "Literal \<Rightarrow> State \<Rightarrow> State"
where
"notifyWatches literal state ==
    notifyWatches_loop literal (getWatchList state literal) [] state
"
declare notifyWatches_def[code_unfold]

definition
assertLiteral :: "Literal \<Rightarrow> bool \<Rightarrow> State \<Rightarrow> State"
where
"assertLiteral literal decision state ==
    let state' = (state\<lparr> getM := (getM state) @ [(literal, decision)] \<rparr>) in
    notifyWatches (opposite literal) state'
"

definition
applyUnitPropagate :: "State \<Rightarrow> State"
where
"applyUnitPropagate state =
    (let state' = (assertLiteral (hd (getQ state)) False state) in
    state'\<lparr> getQ := tl (getQ state')\<rparr>)
"

partial_function (tailrec)
exhaustiveUnitPropagate :: "State \<Rightarrow> State"
where
exhaustiveUnitPropagate_unfold[code]:
"exhaustiveUnitPropagate state =
    (if (getConflictFlag state) \<or> (getQ state) = [] then
        state
    else
        exhaustiveUnitPropagate (applyUnitPropagate state)
    )
"

inductive
exhaustiveUnitPropagate_dom :: "State \<Rightarrow> bool"
where
step: "(\<not> getConflictFlag state \<Longrightarrow> getQ state \<noteq> []
   \<Longrightarrow> exhaustiveUnitPropagate_dom (applyUnitPropagate state))
   \<Longrightarrow> exhaustiveUnitPropagate_dom state"

definition
addClause :: "Clause \<Rightarrow> State \<Rightarrow> State"
where
"addClause clause state =
    (let clause' = (remdups (removeFalseLiterals clause (elements (getM state)))) in
    (if (clauseTrue clause' (elements (getM state))) then
        state
    else (if clause'=[] then
        state\<lparr> getSATFlag := FALSE \<rparr>
    else (if (length clause' = 1) then
        let state' = (assertLiteral (hd clause') False state) in
        exhaustiveUnitPropagate state'
    else (if (clauseTautology clause') then
        state
    else
        let clauseIndex = length (getF state) in
        let state'   = state\<lparr> getF := (getF state) @ [clause']\<rparr> in
        let state''  = setWatch1 clauseIndex (nth clause' 0) state' in
        let state''' = setWatch2 clauseIndex (nth clause' 1) state'' in
        state'''
   )))
 ))"

definition
initialState :: "State"
where
"initialState =
    \<lparr> getSATFlag = UNDEF,
      getF = [],
      getM = [],
      getConflictFlag = False,
      getConflictClause = 0,
      getQ = [],
      getReason = \<lambda> l. None,
      getWatch1 = \<lambda> c. None,
      getWatch2 = \<lambda> c. None,
      getWatchList = \<lambda> l. [],
      getC = [],
      getCl = (Pos 0),
      getCll = (Pos 0),
      getCn = 0
    \<rparr>
"

primrec initialize :: "Formula \<Rightarrow> State \<Rightarrow> State"
where
"initialize [] state = state" |
"initialize (clause # formula) state = initialize formula (addClause clause state)"

definition
findLastAssertedLiteral :: "State \<Rightarrow> State"
where
"findLastAssertedLiteral state =
   state \<lparr> getCl := getLastAssertedLiteral (oppositeLiteralList (getC state)) (elements (getM state)) \<rparr>"

definition
countCurrentLevelLiterals :: "State \<Rightarrow> State"
where
"countCurrentLevelLiterals state =
   (let cl = currentLevel (getM state) in
        state \<lparr> getCn := length (filter (\<lambda> l. elementLevel (opposite l) (getM state) = cl) (getC state)) \<rparr>)"

definition setConflictAnalysisClause :: "Clause \<Rightarrow> State \<Rightarrow> State"
where
"setConflictAnalysisClause clause state =
  (let oppM0 = oppositeLiteralList (elements (prefixToLevel 0 (getM state))) in
   let state' = state (| getC := remdups (list_diff clause oppM0) |) in
     countCurrentLevelLiterals (findLastAssertedLiteral state')
  )"

definition
applyConflict :: "State \<Rightarrow> State"
where
"applyConflict state =
   (let conflictClause = (nth (getF state) (getConflictClause state)) in
    setConflictAnalysisClause conflictClause state)"

definition
applyExplain :: "Literal \<Rightarrow> State \<Rightarrow> State"
where
"applyExplain literal state =
    (case (getReason state literal) of
        None \<Rightarrow>
            state
    |   Some reason \<Rightarrow>
            let res = resolve (getC state) (nth (getF state) reason) (opposite literal) in
            setConflictAnalysisClause res state

    )
"

partial_function (tailrec)
applyExplainUIP :: "State \<Rightarrow> State"
where
applyExplainUIP_unfold:
"applyExplainUIP state =
    (if (getCn state = 1) then
         state
     else
         applyExplainUIP (applyExplain (getCl state) state)
    )
"

inductive
applyExplainUIP_dom :: "State \<Rightarrow> bool"
where
step:
"(getCn state \<noteq> 1
    \<Longrightarrow> applyExplainUIP_dom (applyExplain (getCl state) state))
  \<Longrightarrow> applyExplainUIP_dom state
"

definition
applyLearn :: "State \<Rightarrow> State"
where
"applyLearn state =
        (if getC state = [opposite (getCl state)] then
            state
         else
            let state' = state\<lparr> getF := (getF state) @ [getC state] \<rparr> in
            let l  = (getCl state) in
            let ll = (getLastAssertedLiteral (removeAll l (oppositeLiteralList (getC state))) (elements (getM state))) in
            let clauseIndex = length (getF state) in
            let state''  = setWatch1 clauseIndex (opposite l) state' in
            let state''' = setWatch2 clauseIndex (opposite ll) state'' in
            state'''\<lparr> getCll := ll \<rparr>
        )
"

definition
getBackjumpLevel :: "State \<Rightarrow> nat"
where
"getBackjumpLevel state ==
    (if getC state = [opposite (getCl state)] then
        0
     else
        elementLevel (getCll state) (getM state)
     )
"

definition
applyBackjump :: "State \<Rightarrow> State"
where
"applyBackjump state =
    (let l = (getCl state) in
     let level = getBackjumpLevel state in
     let state' = state\<lparr> getConflictFlag := False, getQ := [], getM := (prefixToLevel level (getM state))\<rparr> in
     let state'' = (if level > 0 then setReason (opposite l) (length (getF state) - 1) state' else state') in
     assertLiteral (opposite l) False state''
    )
"

axiomatization selectLiteral :: "State \<Rightarrow> Variable set \<Rightarrow> Literal"
where
selectLiteral_def:
"Vbl - vars (elements (getM state)) \<noteq> {} \<longrightarrow>
    var (selectLiteral state Vbl) \<in> (Vbl - vars (elements (getM state)))"

definition
applyDecide :: "State \<Rightarrow> Variable set \<Rightarrow> State"
where
"applyDecide state Vbl =
    assertLiteral (selectLiteral state Vbl) True state
"

definition
solve_loop_body :: "State \<Rightarrow> Variable set \<Rightarrow> State"
where
"solve_loop_body state Vbl =
    (let state' = exhaustiveUnitPropagate state in
    (if (getConflictFlag state') then
        (if (currentLevel (getM state')) = 0 then
            state'\<lparr> getSATFlag := FALSE \<rparr>
         else
            (applyBackjump
            (applyLearn
            (applyExplainUIP
            (applyConflict
                state'
            )
            )
            )
            )
         )
     else
        (if (vars (elements (getM state')) \<supseteq> Vbl) then
            state'\<lparr> getSATFlag := TRUE \<rparr>
         else
            applyDecide state' Vbl
        )
    )
    )
"

partial_function (tailrec)
solve_loop :: "State \<Rightarrow> Variable set \<Rightarrow> State"
where
solve_loop_unfold:
"solve_loop state Vbl =
    (if (getSATFlag state) \<noteq> UNDEF then
        state
     else
        let state' = solve_loop_body state Vbl in
        solve_loop state' Vbl
    )
"

inductive
solve_loop_dom :: "State \<Rightarrow> Variable set \<Rightarrow> bool"
where
step:
"(getSATFlag state = UNDEF
    \<Longrightarrow> solve_loop_dom (solve_loop_body state Vbl) Vbl)
  \<Longrightarrow> solve_loop_dom state Vbl"

definition solve::"Formula \<Rightarrow> ExtendedBool"
where
"solve F0 =
    (getSATFlag
        (solve_loop
            (initialize F0 initialState) (vars F0)
        )
    )
"

(*
code_modulename SML
  Nat Numbers
  Int Numbers
  Ring_and_Field Numbers

code_modulename OCaml
  Nat Numbers
  Int Numbers
  Ring_and_Field Numbers

export_code solve in OCaml file "code/solve.ML"
                  in SML file "code/solve.ocaml
                  in Haskell file "code/"
*)

(******************************************************************************)
(*      I N V A R I A N T S                                                   *)
(******************************************************************************)

definition
InvariantWatchListsContainOnlyClausesFromF :: "(Literal \<Rightarrow> nat list) \<Rightarrow> Formula \<Rightarrow> bool"
where
"InvariantWatchListsContainOnlyClausesFromF Wl F =
    (\<forall> (l::Literal) (c::nat). c \<in>  set (Wl l) \<longrightarrow> 0 \<le> c \<and> c < length F)
"

definition
InvariantWatchListsUniq :: "(Literal \<Rightarrow> nat list) \<Rightarrow> bool"
where
"InvariantWatchListsUniq Wl =
    (\<forall> l. uniq (Wl l))
"

definition
InvariantWatchListsCharacterization :: "(Literal \<Rightarrow> nat list) \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> bool"
where
"InvariantWatchListsCharacterization Wl w1 w2 =
    (\<forall> (c::nat) (l::Literal). c \<in> set (Wl l) = (Some l = (w1 c) \<or> Some l = (w2 c)))
"

definition
InvariantWatchesEl :: "Formula \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> bool"
where
"InvariantWatchesEl formula watch1 watch2 ==
    \<forall> (clause::nat). 0 \<le> clause \<and> clause < length formula \<longrightarrow>
        (\<exists> (w1::Literal) (w2::Literal). watch1 clause = Some w1 \<and> watch2 clause = Some w2 \<and>
             w1 el (nth formula clause) \<and> w2 el (nth formula clause))
"

definition
InvariantWatchesDiffer :: "Formula \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> bool"
where
"InvariantWatchesDiffer formula watch1 watch2 ==
    \<forall> (clause::nat). 0 \<le> clause \<and> clause < length formula \<longrightarrow> watch1 clause \<noteq> watch2 clause
"

definition
watchCharacterizationCondition::"Literal \<Rightarrow> Literal \<Rightarrow> LiteralTrail \<Rightarrow> Clause \<Rightarrow> bool"
where
"watchCharacterizationCondition w1 w2 M clause =
    (literalFalse w1 (elements M) \<longrightarrow>
        ( (\<exists> l. l el clause \<and> literalTrue l (elements M) \<and> elementLevel l M \<le> elementLevel (opposite w1) M) \<or>
          (\<forall> l. l el clause \<and> l \<noteq> w1 \<and> l \<noteq> w2 \<longrightarrow>
                literalFalse l (elements M) \<and> elementLevel (opposite l) M \<le> elementLevel (opposite w1) M)
          )
    )
"

definition
InvariantWatchCharacterization::"Formula \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> (nat \<Rightarrow> Literal option) \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantWatchCharacterization F watch1 watch2 M =
    (\<forall> c w1 w2. (0 \<le> c \<and> c < length F \<and> Some w1 = watch1 c \<and> Some w2 = watch2 c) \<longrightarrow>
          watchCharacterizationCondition w1 w2 M (nth F c) \<and>
          watchCharacterizationCondition w2 w1 M (nth F c)
    )
"

definition
InvariantQCharacterization :: "bool \<Rightarrow> Literal list \<Rightarrow> Formula \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantQCharacterization conflictFlag Q F M ==
   \<not> conflictFlag \<longrightarrow> (\<forall> (l::Literal). l el Q = (\<exists> (c::Clause). c el F \<and> isUnitClause c l (elements M)))
"

definition
InvariantUniqQ :: "Literal list \<Rightarrow> bool"
where
"InvariantUniqQ Q =
    uniq Q
"

definition
InvariantConflictFlagCharacterization :: "bool \<Rightarrow> Formula \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantConflictFlagCharacterization conflictFlag F M ==
    conflictFlag = formulaFalse F (elements M)
"

definition
InvariantNoDecisionsWhenConflict :: "Formula \<Rightarrow> LiteralTrail \<Rightarrow> nat \<Rightarrow> bool"
where
"InvariantNoDecisionsWhenConflict F M level=
    (\<forall> level'. level' < level \<longrightarrow>
              \<not> formulaFalse F (elements (prefixToLevel level' M))
    )
"

definition
InvariantNoDecisionsWhenUnit :: "Formula \<Rightarrow> LiteralTrail \<Rightarrow> nat \<Rightarrow> bool"
where
"InvariantNoDecisionsWhenUnit F M level =
    (\<forall> level'. level' < level \<longrightarrow>
              \<not> (\<exists> clause literal. clause el F \<and>
                                   isUnitClause clause literal (elements (prefixToLevel level' M)))
    )
"

definition InvariantEquivalentZL :: "Formula \<Rightarrow> LiteralTrail \<Rightarrow> Formula \<Rightarrow> bool"
where
"InvariantEquivalentZL F M F0 =
    equivalentFormulae (F @ val2form (elements (prefixToLevel 0 M))) F0
"

definition
InvariantGetReasonIsReason :: "(Literal \<Rightarrow> nat option) \<Rightarrow> Formula \<Rightarrow> LiteralTrail \<Rightarrow> Literal set \<Rightarrow> bool"
where
"InvariantGetReasonIsReason GetReason F M Q ==
     \<forall> literal. (literal el (elements M) \<and> \<not> literal el (decisions M) \<and> elementLevel literal M > 0 \<longrightarrow>
                   (\<exists> (reason::nat). (GetReason literal) = Some reason \<and> 0 \<le> reason \<and> reason < length F \<and>
                         isReason (nth F reason) literal (elements M)
                   )
                 ) \<and>
                (currentLevel M > 0 \<and> literal \<in> Q \<longrightarrow>
                   (\<exists> (reason::nat). (GetReason literal) = Some reason \<and> 0 \<le> reason \<and> reason < length F \<and>
                         (isUnitClause (nth F reason) literal (elements M) \<or> clauseFalse (nth F reason) (elements M))
                   )
                 )
"

definition
InvariantConflictClauseCharacterization :: "bool \<Rightarrow> nat \<Rightarrow> Formula \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantConflictClauseCharacterization conflictFlag conflictClause F M  ==
         conflictFlag \<longrightarrow> (conflictClause < length F \<and>
                           clauseFalse (nth F conflictClause) (elements M))"

definition
InvariantClCharacterization :: "Literal \<Rightarrow> Clause \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantClCharacterization Cl C M ==
  isLastAssertedLiteral Cl (oppositeLiteralList C) (elements M)"

definition
InvariantCllCharacterization :: "Literal \<Rightarrow> Literal \<Rightarrow> Clause \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantCllCharacterization Cl Cll C M ==
  set C \<noteq> {opposite Cl} \<longrightarrow>
      isLastAssertedLiteral Cll (removeAll Cl (oppositeLiteralList C)) (elements M)"

definition
InvariantClCurrentLevel :: "Literal \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantClCurrentLevel Cl M ==
  elementLevel Cl M = currentLevel M"

definition
InvariantCnCharacterization :: "nat \<Rightarrow> Clause \<Rightarrow> LiteralTrail \<Rightarrow> bool"
where
"InvariantCnCharacterization Cn C M ==
  Cn = length (filter (\<lambda> l. elementLevel (opposite l) M = currentLevel M) (remdups C))
"

definition
InvariantUniqC :: "Clause \<Rightarrow> bool"
where
"InvariantUniqC clause = uniq clause"

definition
InvariantVarsQ :: "Literal list \<Rightarrow> Formula \<Rightarrow> Variable set \<Rightarrow> bool"
where
"InvariantVarsQ Q F0 Vbl ==
  vars Q \<subseteq> vars F0 \<union> Vbl"

(******************************************************************************)

end

author: Josh-Tilles

repo: AFP

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


text:
(*<*)

(* Author: Kyndylan Nienhuis *)

theory InvokeCap

imports
  "UnpredictableBehaviour"
  "ExceptionFlag"
  "ExecutionStep"
begin

(*>*)
section \<open>Semantics of @{const InvokeCapability}}\<close>

definition SemanticsInvokePost where
  "SemanticsInvokePost codeCap dataCap capr scapr mem \<equiv>
   return (getSealed codeCap \<and>
           getSealed dataCap \<and>
           getTag codeCap \<and>
           getTag dataCap \<and>
           Permit_CCall (getPerms codeCap) \<and>
           Permit_CCall (getPerms dataCap) \<and>
           Permit_Execute (getPerms codeCap) \<and>
           \<not> Permit_Execute (getPerms dataCap) \<and>
           (getType codeCap = getType dataCap)) \<and>\<^sub>b
   (\<forall>\<^sub>bcd. read_state (getCAPR cd) =\<^sub>b
          return (if cd = 26
                  then setType (setSealed (dataCap, False), 0)
                  else capr cd)) \<and>\<^sub>b
   (\<forall>\<^sub>bcd. read_state (getSCAPR cd) =\<^sub>b return (scapr cd)) \<and>\<^sub>b
   (\<forall>\<^sub>ba. read_state (getMEM a) =\<^sub>b return (mem a))"

lemma Commute_SemanticsInvokePost [Commute_compositeI]:
  assumes "Commute (read_state getPCC) m"
  assumes "\<And>cd. Commute (read_state (getSCAPR cd)) m"
      and "\<And>cd. Commute (read_state (getCAPR cd)) m"
      and "\<And>a. Commute (read_state (getMEM a)) m"
  shows "Commute (SemanticsInvokePost codeCap dataCap capr scapr mem) m"
unfolding SemanticsInvokePost_def
by (Commute intro: assms)

lemma SemanticsInvoke_CCallFast:
  shows "HoareTriple ((return codeCap =\<^sub>b read_state (getCAPR cd)) \<and>\<^sub>b
                  (return dataCap =\<^sub>b read_state (getCAPR cd')) \<and>\<^sub>b
                  (return capr =\<^sub>b read_state (\<lambda>s cd. getCAPR cd s)) \<and>\<^sub>b
                  (return scapr =\<^sub>b read_state (\<lambda>s cd. getSCAPR cd s)) \<and>\<^sub>b
                  (return mem =\<^sub>b read_state (\<lambda>s a. getMEM a s)) \<and>\<^sub>b
                  (read_state getBranchTo =\<^sub>b return None) \<and>\<^sub>b
                  (read_state BranchToPCC =\<^sub>b return None) \<and>\<^sub>b
                  (return (v = (cd, cd'))))
                 (dfn'CCallFast v)
                 (\<lambda>_. read_state getExceptionSignalled \<or>\<^sub>b
                      read_state isUnpredictable \<or>\<^sub>b
                      (SemanticsInvokePost codeCap dataCap capr scapr mem \<and>\<^sub>b
                       (read_state BranchDelayPCC =\<^sub>b
                        return (Some (getOffset codeCap, setType (setSealed (codeCap, False), 0)))) \<and>\<^sub>b
                       (read_state getBranchDelay =\<^sub>b return None) \<and>\<^sub>b
                       (read_state getBranchTo =\<^sub>b return None) \<and>\<^sub>b
                       (read_state BranchToPCC =\<^sub>b return None)))"
unfolding dfn'CCallFast_alt_def SemanticsInvokePost_def
unfolding CheckBranch_alt_def
by (HoareTriple intro: nonExceptionCase_exceptions[THEN HoareTriple_post_weakening]) auto

lemma SemanticsInvoke_Run_aux:
  shows "HoareTriple ((return codeCap =\<^sub>b read_state (getCAPR cd)) \<and>\<^sub>b
                  (return dataCap =\<^sub>b read_state (getCAPR cd')) \<and>\<^sub>b
                  (return capr =\<^sub>b read_state (\<lambda>s cd. getCAPR cd s)) \<and>\<^sub>b
                  (return scapr =\<^sub>b read_state (\<lambda>s cd. getSCAPR cd s)) \<and>\<^sub>b
                  (return mem =\<^sub>b read_state (\<lambda>s a. getMEM a s)) \<and>\<^sub>b
                  (read_state getBranchTo =\<^sub>b return None) \<and>\<^sub>b
                  (read_state BranchToPCC =\<^sub>b return None) \<and>\<^sub>b
                  (return (case v of COP2 (CHERICOP2 (CCallFast (cs, cb))) \<Rightarrow> (cs = cd) \<and> (cb = cd')
                                   | _ \<Rightarrow> False)))
                 (Run v)
                 (\<lambda>_. read_state getExceptionSignalled \<or>\<^sub>b
                      read_state isUnpredictable \<or>\<^sub>b
                      (SemanticsInvokePost codeCap dataCap capr scapr mem \<and>\<^sub>b
                       (read_state BranchDelayPCC =\<^sub>b
                        return (Some (getOffset codeCap, setType (setSealed (codeCap, False), 0)))) \<and>\<^sub>b
                       (read_state getBranchDelay =\<^sub>b return None) \<and>\<^sub>b
                       (read_state getBranchTo =\<^sub>b return None) \<and>\<^sub>b
                       (read_state BranchToPCC =\<^sub>b return None)))"
unfolding Run_alt_def RunActions_def HoareTriple_def
using HoareTripleE[OF SemanticsInvoke_CCallFast]
by (auto simp: ValueAndStatePart_simp split: all_split)

lemmas SemanticsInvoke_Run =
  HoareTriple_weakest_pre_disj[OF SemanticsInvoke_Run_aux
                              UndefinedCase_Run]

lemma SemanticsInvoke_Fetch:
  fixes codeCap dataCap cd cd' capr scapr mem
  defines "p \<equiv> \<lambda>w. (return codeCap =\<^sub>b read_state (getCAPR cd)) \<and>\<^sub>b
                   (return dataCap =\<^sub>b read_state (getCAPR cd')) \<and>\<^sub>b
                   (return capr =\<^sub>b read_state (\<lambda>s cd. getCAPR cd s)) \<and>\<^sub>b
                   (return scapr =\<^sub>b read_state (\<lambda>s cd. getSCAPR cd s)) \<and>\<^sub>b
                   (return mem =\<^sub>b read_state (\<lambda>s a. getMEM a s)) \<and>\<^sub>b
                   (read_state getBranchTo =\<^sub>b return None) \<and>\<^sub>b
                   (read_state BranchToPCC =\<^sub>b return None) \<and>\<^sub>b
                   (return (case Decode w of COP2 (CHERICOP2 (CCallFast (cs, cb))) \<Rightarrow>
                                             (cs = cd) \<and> (cb = cd')
                                           | _ \<Rightarrow> False))"
  shows "HoareTriple (bind NextInstruction (case_option (return True) p))
                  Fetch
                  (\<lambda>b. case b of None \<Rightarrow> read_state getExceptionSignalled
                               | Some y \<Rightarrow> read_state isUnpredictable \<or>\<^sub>b p y)"
unfolding p_def
by (intro HoareTriple_Fetch[THEN HoareTriple_post_weakening]) Commute+

lemma SemanticsInvoke_TakeBranch:
  shows "HoareTriple (read_state getExceptionSignalled \<or>\<^sub>b
                  read_state isUnpredictable \<or>\<^sub>b
                  (SemanticsInvokePost codeCap dataCap capr scapr mem \<and>\<^sub>b
                   (read_state getBranchDelay =\<^sub>b return None) \<and>\<^sub>b
                   (read_state BranchDelayPCC =\<^sub>b
                    return (Some (getOffset codeCap, setType (setSealed (codeCap, False), 0)))) \<and>\<^sub>b
                   (read_state getBranchTo =\<^sub>b return None) \<and>\<^sub>b
                   (read_state BranchToPCC =\<^sub>b return None)))
                 TakeBranch
                 (\<lambda>_. read_state getExceptionSignalled \<or>\<^sub>b
                      read_state isUnpredictable \<or>\<^sub>b
                      (SemanticsInvokePost codeCap dataCap capr scapr mem \<and>\<^sub>b
                       bind (read_state getPCC)
                            (\<lambda>x. return (x = setType (setSealed (codeCap, False), 0))) \<and>\<^sub>b
                       (read_state getBranchDelay =\<^sub>b return None) \<and>\<^sub>b
                       (read_state BranchDelayPCC =\<^sub>b return None) \<and>\<^sub>b
                       bind (read_state getPC)
                            (\<lambda>x. return (x = getOffset codeCap))))"
unfolding TakeBranch_def SemanticsInvokePost_def
by HoareTriple (auto split: option.splits)

lemma SemanticsInvoke_NextWithGhostState:
  shows "HoareTriple ((return codeCap =\<^sub>b read_state (getCAPR cd)) \<and>\<^sub>b
                  (return dataCap =\<^sub>b read_state (getCAPR cd')) \<and>\<^sub>b
                  (return capr =\<^sub>b read_state (\<lambda>s cd. getCAPR cd s)) \<and>\<^sub>b
                  (return scapr =\<^sub>b read_state (\<lambda>s cd. getSCAPR cd s)) \<and>\<^sub>b
                  (return mem =\<^sub>b read_state (\<lambda>s a. getMEM a s)) \<and>\<^sub>b
                  (read_state getBranchTo =\<^sub>b return None) \<and>\<^sub>b
                  (read_state BranchToPCC =\<^sub>b return None) \<and>\<^sub>b
                  (read_state NextNonExceptionStep =\<^sub>b
                   return (SwitchDomain (InvokeCapability cd cd'))))
                 NextWithGhostState
                 (\<lambda>_. read_state getExceptionSignalled \<or>\<^sub>b
                      read_state isUnpredictable \<or>\<^sub>b
                      (SemanticsInvokePost codeCap dataCap capr scapr mem \<and>\<^sub>b
                       bind (read_state getPCC)
                            (\<lambda>x. return (x = setType (setSealed (codeCap, False), 0))) \<and>\<^sub>b
                       (read_state getBranchDelay =\<^sub>b return None) \<and>\<^sub>b
                       (read_state BranchDelayPCC =\<^sub>b return None) \<and>\<^sub>b
                       bind (read_state getPC)
                            (\<lambda>x. return (x = getOffset codeCap))))"
proof -
  note intros = SemanticsInvoke_TakeBranch[where codeCap=codeCap and dataCap=dataCap]
                SemanticsInvoke_Run[where codeCap=codeCap and dataCap=dataCap and
                                          cd=cd and cd'=cd']
                SemanticsInvoke_Fetch[where codeCap=codeCap and dataCap=dataCap and
                                            cd=cd and cd'=cd']
  show ?thesis
    unfolding NextWithGhostState_def
    unfolding NextNonExceptionStep_def DomainActions_def
    by (HoareTriple intro: intros[THEN HoareTriple_post_weakening])
       (auto split: option.splits elim!: CCallFastInstructionParam_Some)
qed

theorem SemanticsInvokeCap:
  fixes s cd cd'
  defines "CodeCap \<equiv> getCAPR cd s"
  defines "DataCap \<equiv> getCAPR cd' s"
  assumes valid: "getStateIsValid s"
      and suc: "(SwitchDomain (InvokeCapability cd cd'), s') \<in> SemanticsCheriMips s"
  shows "getSealed CodeCap"
    and "getSealed DataCap"
    and "getTag CodeCap"
    and "getTag DataCap"
    and "Permit_CCall (getPerms CodeCap)"
    and "Permit_CCall (getPerms DataCap)"
    and "Permit_Execute (getPerms CodeCap)"
    and "\<not> Permit_Execute (getPerms DataCap)"
    and "getType CodeCap = getType DataCap"
    and "getPC s' = getOffset CodeCap"
    and "getPCC s' = setType (setSealed (CodeCap, False), 0)"
    and "getBranchDelay s' = None"
    and "BranchDelayPCC s' = None"
    and "\<And>x. getCAPR x s' = (if x = 26 then setType (setSealed (DataCap, False), 0)
                             else getCAPR x s)"
    and "\<And>x. getSCAPR x s' = getSCAPR x s"
    and "\<And>x. getMEM x s' = getMEM x s"
using suc valid
using SemanticsInvoke_NextWithGhostState
         [where codeCap=CodeCap and dataCap=DataCap and cd=cd and cd'=cd' and
                capr="\<lambda>cd. getCAPR cd s" and scapr="\<lambda>cd. getSCAPR cd s" and
                mem="\<lambda>a. getMEM a s",
          THEN HoareTripleE[where s=s]]
unfolding CodeCap_def DataCap_def SemanticsInvokePost_def
unfolding SemanticsCheriMips_def Next_NextWithGhostState
unfolding StateIsValid_def GhostStateIsValid_def
by (auto simp: ValueAndStatePart_simp split: if_splits)

corollary InvokeCapInstantiation:
  assumes "(lbl, s') \<in> SemanticsCheriMips s"
  shows "InvokeCapProp s lbl s'"
unfolding InvokeCapProp_def
using assms SemanticsInvokeCap
by auto

(*<*)
end
(*>*)

author: CTSRD-CHERI


text:
(*  Title:      HOL/Auth/n_german_lemma_on_inv__58.thy
    Author:     Yongjian Li and Kaiqiang Duan, State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
    Copyright    2016 State Key Lab of Computer Science, Institute of Software, Chinese Academy of Sciences
*)

(*header{*The n_german Protocol Case Study*}*)

theory n_german_lemma_on_inv__58 imports n_german_base
begin
section{*All lemmas on causal relation between inv__58 and some rule r*}
lemma n_RecvInvAckVsinv__58:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_RecvInvAck  i)" and
a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_RecvInvAck  i" apply fastforce done
from a2 obtain p__Inv0 p__Inv2 where a2:"p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2" apply fastforce done
have "(i=p__Inv2)\<or>(i=p__Inv0)\<or>(i~=p__Inv0\<and>i~=p__Inv2)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv2)"
  have "((formEval (eqn (IVar (Ident ''ExGntd'')) (Const true)) s))\<or>((formEval (neg (eqn (IVar (Ident ''ExGntd'')) (Const true))) s))" by auto
  moreover {
    assume c1: "((formEval (eqn (IVar (Ident ''ExGntd'')) (Const true)) s))"
    have "?P1 s"
    proof(cut_tac a1 a2 b1 c1, auto) qed
    then have "invHoldForRule s f r (invariants N)" by auto
  }
  moreover {
    assume c1: "((formEval (neg (eqn (IVar (Ident ''ExGntd'')) (Const true))) s))"
    have "?P1 s"
    proof(cut_tac a1 a2 b1 c1, auto) qed
    then have "invHoldForRule s f r (invariants N)" by auto
  }
  ultimately have "invHoldForRule s f r (invariants N)" by satx
}
moreover {
  assume b1: "(i=p__Inv0)"
  have "((formEval (eqn (IVar (Ident ''ExGntd'')) (Const true)) s))\<or>((formEval (neg (eqn (IVar (Ident ''ExGntd'')) (Const true))) s))" by auto
  moreover {
    assume c1: "((formEval (eqn (IVar (Ident ''ExGntd'')) (Const true)) s))"
    have "?P1 s"
    proof(cut_tac a1 a2 b1 c1, auto) qed
    then have "invHoldForRule s f r (invariants N)" by auto
  }
  moreover {
    assume c1: "((formEval (neg (eqn (IVar (Ident ''ExGntd'')) (Const true))) s))"
    have "?P1 s"
    proof(cut_tac a1 a2 b1 c1, auto) qed
    then have "invHoldForRule s f r (invariants N)" by auto
  }
  ultimately have "invHoldForRule s f r (invariants N)" by satx
}
moreover {
  assume b1: "(i~=p__Inv0\<and>i~=p__Inv2)"
  have "((formEval (eqn (IVar (Ident ''ExGntd'')) (Const true)) s))\<or>((formEval (neg (eqn (IVar (Ident ''ExGntd'')) (Const true))) s))" by auto
  moreover {
    assume c1: "((formEval (eqn (IVar (Ident ''ExGntd'')) (Const true)) s))"
    have "?P1 s"
    proof(cut_tac a1 a2 b1 c1, auto) qed
    then have "invHoldForRule s f r (invariants N)" by auto
  }
  moreover {
    assume c1: "((formEval (neg (eqn (IVar (Ident ''ExGntd'')) (Const true))) s))"
    have "?P2 s"
    proof(cut_tac a1 a2 b1 c1, auto) qed
    then have "invHoldForRule s f r (invariants N)" by auto
  }
  ultimately have "invHoldForRule s f r (invariants N)" by satx
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_SendGntSVsinv__58:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_SendGntS  i)" and
a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_SendGntS  i" apply fastforce done
from a2 obtain p__Inv0 p__Inv2 where a2:"p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2" apply fastforce done
have "(i=p__Inv2)\<or>(i=p__Inv0)\<or>(i~=p__Inv0\<and>i~=p__Inv2)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv2)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv0)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv0\<and>i~=p__Inv2)"
  have "?P2 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_SendGntEVsinv__58:
assumes a1: "(\<exists> i. i\<le>N\<and>r=n_SendGntE N i)" and
a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
shows "invHoldForRule s f r (invariants N)" (is "?P1 s \<or> ?P2 s \<or> ?P3 s")
proof -
from a1 obtain i where a1:"i\<le>N\<and>r=n_SendGntE N i" apply fastforce done
from a2 obtain p__Inv0 p__Inv2 where a2:"p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2" apply fastforce done
have "(i=p__Inv2)\<or>(i=p__Inv0)\<or>(i~=p__Inv0\<and>i~=p__Inv2)" apply (cut_tac a1 a2, auto) done
moreover {
  assume b1: "(i=p__Inv2)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i=p__Inv0)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
moreover {
  assume b1: "(i~=p__Inv0\<and>i~=p__Inv2)"
  have "?P1 s"
  proof(cut_tac a1 a2 b1, auto) qed
  then have "invHoldForRule s f r (invariants N)" by auto
}
ultimately show "invHoldForRule s f r (invariants N)" by satx
qed

lemma n_SendReqE__part__1Vsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendReqE__part__1  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_StoreVsinv__58:
  assumes a1: "\<exists> i d. i\<le>N\<and>d\<le>N\<and>r=n_Store  i d" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_RecvGntSVsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_RecvGntS  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_RecvReqEVsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_RecvReqE N i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_RecvGntEVsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_RecvGntE  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendInvAckVsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendInvAck  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendInv__part__0Vsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendInv__part__0  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendReqE__part__0Vsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendReqE__part__0  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendInv__part__1Vsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendInv__part__1  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_SendReqSVsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_SendReqS  i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

lemma n_RecvReqSVsinv__58:
  assumes a1: "\<exists> i. i\<le>N\<and>r=n_RecvReqS N i" and
  a2: "(\<exists> p__Inv0 p__Inv2. p__Inv0\<le>N\<and>p__Inv2\<le>N\<and>p__Inv0~=p__Inv2\<and>f=inv__58  p__Inv0 p__Inv2)"
  shows "invHoldForRule s f r (invariants N)"
  apply (rule noEffectOnRule, cut_tac a1 a2, auto) done

end

author: hongjianjiang


text:
(* Author: Florian Haftmann, TU Muenchen *)

section \<open>A HOL random engine\<close>

theory Random
imports List Groups_List
begin

subsection \<open>Auxiliary functions\<close>

fun log :: "natural \<Rightarrow> natural \<Rightarrow> natural" where
  "log b i = (if b \<le> 1 \<or> i < b then 1 else 1 + log b (i div b))"

definition inc_shift :: "natural \<Rightarrow> natural \<Rightarrow> natural" where
  "inc_shift v k = (if v = k then 1 else k + 1)"

definition minus_shift :: "natural \<Rightarrow> natural \<Rightarrow> natural \<Rightarrow> natural" where
  "minus_shift r k l = (if k < l then r + k - l else k - l)"

subsection \<open>Random seeds\<close>

type_synonym seed = "natural \<times> natural"

primrec "next" :: "seed \<Rightarrow> natural \<times> seed" where
  "next (v, w) = (let
     k =  v div 53668;
     v' = minus_shift 2147483563 ((v mod 53668) * 40014) (k * 12211);
     l =  w div 52774;
     w' = minus_shift 2147483399 ((w mod 52774) * 40692) (l * 3791);
     z =  minus_shift 2147483562 v' (w' + 1) + 1
   in (z, (v', w')))"

definition split_seed :: "seed \<Rightarrow> seed \<times> seed" where
  "split_seed s = (let
     (v, w) = s;
     (v', w') = snd (next s);
     v'' = inc_shift 2147483562 v;
     w'' = inc_shift 2147483398 w
   in ((v'', w'), (v', w'')))"

subsection \<open>Base selectors\<close>

context
  includes state_combinator_syntax
begin

fun iterate :: "natural \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
  "iterate k f x = (if k = 0 then Pair x else f x \<circ>\<rightarrow> iterate (k - 1) f)"

definition range :: "natural \<Rightarrow> seed \<Rightarrow> natural \<times> seed" where
  "range k = iterate (log 2147483561 k)
      (\<lambda>l. next \<circ>\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
    \<circ>\<rightarrow> (\<lambda>v. Pair (v mod k))"

lemma range:
  "k > 0 \<Longrightarrow> fst (range k s) < k"
  by (simp add: range_def split_def less_natural_def del: log.simps iterate.simps)

definition select :: "'a list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
  "select xs = range (natural_of_nat (length xs))
    \<circ>\<rightarrow> (\<lambda>k. Pair (nth xs (nat_of_natural k)))"

lemma select:
  assumes "xs \<noteq> []"
  shows "fst (select xs s) \<in> set xs"
proof -
  from assms have "natural_of_nat (length xs) > 0" by (simp add: less_natural_def)
  with range have
    "fst (range (natural_of_nat (length xs)) s) < natural_of_nat (length xs)" by best
  then have
    "nat_of_natural (fst (range (natural_of_nat (length xs)) s)) < length xs" by (simp add: less_natural_def)
  then show ?thesis
    by (simp add: split_beta select_def)
qed

primrec pick :: "(natural \<times> 'a) list \<Rightarrow> natural \<Rightarrow> 'a" where
  "pick (x # xs) i = (if i < fst x then snd x else pick xs (i - fst x))"

lemma pick_member:
  "i < sum_list (map fst xs) \<Longrightarrow> pick xs i \<in> set (map snd xs)"
  by (induct xs arbitrary: i) (simp_all add: less_natural_def)

lemma pick_drop_zero:
  "pick (filter (\<lambda>(k, _). k > 0) xs) = pick xs"
  by (induct xs) (auto simp add: fun_eq_iff less_natural_def minus_natural_def)

lemma pick_same:
  "l < length xs \<Longrightarrow> Random.pick (map (Pair 1) xs) (natural_of_nat l) = nth xs l"
proof (induct xs arbitrary: l)
  case Nil then show ?case by simp
next
  case (Cons x xs) then show ?case by (cases l) (simp_all add: less_natural_def)
qed

definition select_weight :: "(natural \<times> 'a) list \<Rightarrow> seed \<Rightarrow> 'a \<times> seed" where
  "select_weight xs = range (sum_list (map fst xs))
   \<circ>\<rightarrow> (\<lambda>k. Pair (pick xs k))"

lemma select_weight_member:
  assumes "0 < sum_list (map fst xs)"
  shows "fst (select_weight xs s) \<in> set (map snd xs)"
proof -
  from range assms
    have "fst (range (sum_list (map fst xs)) s) < sum_list (map fst xs)" .
  with pick_member
    have "pick xs (fst (range (sum_list (map fst xs)) s)) \<in> set (map snd xs)" .
  then show ?thesis by (simp add: select_weight_def scomp_def split_def)
qed

lemma select_weight_cons_zero:
  "select_weight ((0, x) # xs) = select_weight xs"
  by (simp add: select_weight_def less_natural_def)

lemma select_weight_drop_zero:
  "select_weight (filter (\<lambda>(k, _). k > 0) xs) = select_weight xs"
proof -
  have "sum_list (map fst [(k, _)\<leftarrow>xs . 0 < k]) = sum_list (map fst xs)"
    by (induct xs) (auto simp add: less_natural_def natural_eq_iff)
  then show ?thesis by (simp only: select_weight_def pick_drop_zero)
qed

lemma select_weight_select:
  assumes "xs \<noteq> []"
  shows "select_weight (map (Pair 1) xs) = select xs"
proof -
  have less: "\<And>s. fst (range (natural_of_nat (length xs)) s) < natural_of_nat (length xs)"
    using assms by (intro range) (simp add: less_natural_def)
  moreover have "sum_list (map fst (map (Pair 1) xs)) = natural_of_nat (length xs)"
    by (induct xs) simp_all
  ultimately show ?thesis
    by (auto simp add: select_weight_def select_def scomp_def split_def
      fun_eq_iff pick_same [symmetric] less_natural_def)
qed

end

subsection \<open>\<open>ML\<close> interface\<close>

code_reflect Random_Engine
  functions range select select_weight

ML \<open>
structure Random_Engine =
struct

open Random_Engine;

type seed = Code_Numeral.natural * Code_Numeral.natural;

local

val seed = Unsynchronized.ref
  (let
    val now = Time.toMilliseconds (Time.now ());
    val (q, s1) = IntInf.divMod (now, 2147483562);
    val s2 = q mod 2147483398;
  in apply2 Code_Numeral.natural_of_integer (s1 + 1, s2 + 1) end);

in

fun next_seed () =
  let
    val (seed1, seed') = @{code split_seed} (! seed)
    val _ = seed := seed'
  in
    seed1
  end

fun run f =
  let
    val (x, seed') = f (! seed);
    val _ = seed := seed'
  in x end;

end;

end;
\<close>

hide_type (open) seed
hide_const (open) inc_shift minus_shift log "next" split_seed
  iterate range select pick select_weight
hide_fact (open) range_def

end

author: object-logics