text:
(*
   Title: The pi-calculus
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Weak_Early_Bisim_Pres
  imports Strong_Early_Bisim_Pres Weak_Early_Sim_Pres Weak_Early_Bisim_SC Weak_Early_Bisim
begin

(************ Preservation rules ************)

lemma tauPres:
  fixes P :: pi
  and   Q :: pi

  assumes "P \<approx> Q"

  shows "\<tau>.(P) \<approx> \<tau>.(Q)"
proof -
  let ?X = "{(\<tau>.(P), \<tau>.(Q)) | P Q. P \<approx> Q}"
  from \<open>P \<approx> Q\<close> have "(\<tau>.(P), \<tau>.(Q)) \<in> ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    thus ?case
      by(force intro: Weak_Early_Sim_Pres.tauPres)
  next
    case(cSym P Q)
    thus ?case by(force dest: Weak_Early_Bisim.symetric simp add: pi.inject)
  qed
qed

lemma outputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<approx> Q"

  shows "a{b}.P \<approx> a{b}.Q"
proof -
  let ?X = "{(a{b}.(P), a{b}.(Q)) | P Q a b. P \<approx> Q}"
  from \<open>P \<approx> Q\<close> have "(a{b}.(P), a{b}.(Q)) \<in> ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    thus ?case
      by(force intro: Weak_Early_Sim_Pres.outputPres)
  next
    case(cSym P Q)
    thus ?case by(force dest: Weak_Early_Bisim.symetric simp add: pi.inject)
  qed
qed

lemma inputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   x :: name

  assumes PSimQ: "\<forall>y. P[x::=y] \<approx> Q[x::=y]"

  shows "a<x>.P \<approx> a<x>.Q"
proof -
  let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. \<forall>y. P[x::=y] \<approx> Q[x::=y]}"
  {
    fix axP axQ p
    assume "(axP, axQ) \<in> ?X"
    then obtain a x P Q where A: "\<forall>y. P[x::=y] \<approx> Q[x::=y]" and B: "axP = a<x>.P" and C: "axQ = a<x>.Q"
      by auto
    have "\<And>y. ((p::name prm) \<bullet> P)[(p \<bullet> x)::=y] \<approx> (p \<bullet> Q)[(p \<bullet> x)::=y]"
    proof -
      fix y
      from A have "P[x::=(rev p \<bullet> y)] \<approx> Q[x::=(rev p \<bullet> y)]"
        by blast
      hence "(p \<bullet> (P[x::=(rev p \<bullet> y)])) \<approx> p \<bullet> (Q[x::=(rev p \<bullet> y)])"
        by(rule eqvts)
      thus "(p \<bullet> P)[(p \<bullet> x)::=y] \<approx> (p \<bullet> Q)[(p \<bullet> x)::=y]"
        by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst])
    qed
    hence "((p::name prm) \<bullet> axP, p \<bullet> axQ) \<in> ?X" using B C
      by auto
  }
  hence "eqvt ?X" by(simp add: eqvt_def)

  from PSimQ have "(a<x>.P, a<x>.Q) \<in> ?X" by auto
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim P Q)
    thus ?case using \<open>eqvt ?X\<close>
      by(force intro: Weak_Early_Sim_Pres.inputPres)
  next
    case(cSym P Q)
    thus ?case
      by(blast dest: weakBisimE)
  qed
qed

  shows "<\<nu>x>P \<approx> <\<nu>x>Q"
proof -
  let ?X = "{(<\<nu>x>P, <\<nu>x>Q) | x P Q. P \<approx> Q}"
  from \<open>P \<approx> Q\<close> have "(<\<nu>x>P, <\<nu>x>Q) \<in> ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim xP xQ)
    {
      fix P Q x
      assume "P \<approx> Q"
      hence "P \<leadsto><weakBisim> Q" by(rule weakBisimE)
      moreover have "\<And>P Q x. P \<approx> Q \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> ?X \<union> weakBisim" by blast
      moreover have "weakBisim \<subseteq> ?X \<union> weakBisim" by blast
      moreover have "eqvt weakBisim" by simp
      moreover have "eqvt (?X \<union> weakBisim)"
        by(auto simp add: eqvt_def dest: Weak_Early_Bisim.eqvtI)+
      ultimately have "<\<nu>x>P \<leadsto><(?X \<union> weakBisim)> <\<nu>x>Q"
        by(rule Weak_Early_Sim_Pres.resPres)
    }
    with \<open>(xP, xQ) \<in> ?X\<close> show ?case by blast
  next
    case(cSym xP xQ)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

  assumes "P \<approx> Q"

  shows "[a\<frown>b]P \<approx> [a\<frown>b]Q"
proof -
  let ?X = "{([a\<frown>b]P, [a\<frown>b]Q) | a b P Q. P \<approx> Q}"
  from \<open>P \<approx> Q\<close> have "([a\<frown>b]P, [a\<frown>b]Q) \<in> ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim abP abQ)
    {
      fix P Q a b
      assume "P \<approx> Q"
      hence "P \<leadsto><weakBisim> Q" by(rule weakBisimE)
      moreover have "weakBisim \<subseteq> (?X \<union> weakBisim)" by blast
      moreover have "\<And>P Q a. P \<approx> Q \<Longrightarrow> [a\<frown>a]P \<approx> Q"
        by (metis (full_types) strongBisimWeakBisim Strong_Early_Bisim_SC.matchId Weak_Early_Bisim.transitive)
      ultimately have"[a\<frown>b]P \<leadsto><(?X \<union> weakBisim)> [a\<frown>b]Q"
        by(rule Weak_Early_Sim_Pres.matchPres)
    }
    with \<open>(abP, abQ) \<in> ?X\<close> show ?case by blast
  next
    case(cSym abP abQ)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

lemma mismatchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<approx> Q"

  shows "[a\<noteq>b]P \<approx> [a\<noteq>b]Q"
proof -
  let ?X = "{([a\<noteq>b]P, [a\<noteq>b]Q)| a b P Q. P \<approx> Q}"
  from \<open>P \<approx> Q\<close> have "([a\<noteq>b]P, [a\<noteq>b]Q) \<in> ?X" by blast
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSim abP abQ)
    {
      fix P Q a b
      assume "P \<approx> Q"
      hence "P \<leadsto><weakBisim> Q" by(rule weakBisimE)
      moreover have "weakBisim \<subseteq> (?X \<union> weakBisim)" by blast
      moreover have "\<And>P Q a b. \<lbrakk>P \<approx> Q; a \<noteq> b\<rbrakk> \<Longrightarrow> [a\<noteq>b]P \<approx> Q"
        by (metis (full_types) strongBisimWeakBisim Strong_Early_Bisim_SC.mismatchId Weak_Early_Bisim.transitive)
      ultimately have "[a\<noteq>b]P \<leadsto><(?X \<union> weakBisim)> [a\<noteq>b]Q"
        by(rule Weak_Early_Sim_Pres.mismatchPres)
    }
    with \<open>(abP, abQ) \<in> ?X\<close> show ?case by blast
  next
    case(cSym abP abQ)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

lemma parPres:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes "P \<approx> Q"

  shows "P \<parallel> R \<approx> Q \<parallel> R"
proof -
  let ?X = "{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) | lst P R Q. P \<approx> Q}"
  have BC: "\<And>P Q. P \<parallel> Q = resChain [] (P \<parallel> Q)" by auto
  from \<open>P \<approx> Q\<close> have "(P \<parallel> R, Q \<parallel> R) \<in> ?X" by(blast intro: BC)
  thus ?thesis
  proof(coinduct rule: weakBisimCoinduct)
    case(cSym PR QR)
    {
      fix P Q R lst
      assume "P \<approx> Q"
      moreover hence "P \<leadsto><weakBisim> Q" by(rule weakBisimE)
      moreover have "\<And>P Q R. P \<approx> Q \<Longrightarrow> (P \<parallel> R, Q \<parallel> R) \<in> ?X" using BC
        by blast
      moreover {
        fix PR QR x
        assume "(PR, QR) \<in> ?X"
        then obtain lst P Q R where "P \<approx> Q" and A: "PR = resChain lst (P \<parallel> R)" and B: "QR = resChain lst (Q \<parallel> R)"
          by auto
        from A have "<\<nu>x>PR = resChain (x#lst) (P \<parallel> R)" by auto
        moreover from B have "<\<nu>x>QR = resChain (x#lst) (Q \<parallel> R)" by auto
        ultimately have "(<\<nu>x>PR, <\<nu>x>QR) \<in> ?X" using \<open>P \<approx> Q\<close>
          by blast
      }
      note Res = this
      ultimately have "P \<parallel> R \<leadsto><?X> Q \<parallel> R"
        by(rule_tac Weak_Early_Sim_Pres.parPres)
      moreover have "eqvt ?X"
        by(auto simp add: eqvt_def) (blast intro: eqvts)
      ultimately have "resChain lst (P \<parallel> R) \<leadsto><?X> resChain lst (Q \<parallel> R)" using Res
        by(rule_tac Weak_Early_Sim_Pres.resChainI)
      hence "resChain lst (P \<parallel> R) \<leadsto><(?X \<union> weakBisim)> resChain lst (Q \<parallel> R)"
        by(force intro: Weak_Early_Sim.monotonic)
    }
    with \<open>(PR, QR) \<in> ?X\<close> show "PR \<leadsto><(?X \<union> weakBisim)> QR"
      by blast
  next
    case(cSym PR QR)
    thus ?case by(blast dest: Weak_Early_Bisim.symetric)
  qed
qed

  assumes PBisimQ: "P \<approx> Q"

  shows "!P \<approx> !Q"
proof -
  let ?X = "(bangRel weakBisim)"
  let ?Y = "Strong_Early_Bisim.bisim O (bangRel weakBisim) O Strong_Early_Bisim.bisim"

  from Weak_Early_Bisim.eqvt Strong_Early_Bisim.eqvt have eqvtY: "eqvt ?Y" by(blast intro: eqvtBangRel)
  have XsubY: "?X \<subseteq> ?Y" by(auto intro: Strong_Early_Bisim.reflexive)

  have RelStay: "\<And>P Q. (P \<parallel> !P, Q) \<in> ?Y \<Longrightarrow> (!P, Q) \<in> ?Y"
  proof(auto)
    fix P Q R T
    assume PBisimQ: "P \<parallel> !P \<sim>\<^sub>e Q"
       and QBRR: "(Q, R) \<in> bangRel weakBisim"
       and RBisimT: "R \<sim>\<^sub>e T"
    have "!P \<sim>\<^sub>e Q"
    proof -
      have "!P \<sim>\<^sub>e P \<parallel> !P" by(rule Strong_Early_Bisim_SC.bangSC)
      thus ?thesis using PBisimQ by(rule Strong_Early_Bisim.transitive)
    qed
    with QBRR RBisimT show "(!P, T) \<in> ?Y" by blast
  qed

  have ParCompose: "\<And>P Q R T. \<lbrakk>P \<approx> Q; (R, T) \<in> ?Y\<rbrakk> \<Longrightarrow> (P \<parallel> R, Q \<parallel> T) \<in> ?Y"
  proof -
    fix P Q R T
    assume PBisimQ: "P \<approx> Q"
       and RYT:     "(R, T) \<in> ?Y"
    thus "(P \<parallel> R, Q \<parallel> T) \<in> ?Y"
    proof(auto)
      fix T' R'
      assume T'BisimT: "T' \<sim>\<^sub>e T" and RBisimR': "R \<sim>\<^sub>e R'"
         and R'BRT': "(R', T') \<in> bangRel weakBisim"
      have "P \<parallel> R \<sim>\<^sub>e P \<parallel> R'"
      proof -
        from RBisimR' have "R \<parallel> P \<sim>\<^sub>e R' \<parallel> P" by(rule Strong_Early_Bisim_Pres.parPres)
        moreover have "P \<parallel> R \<sim>\<^sub>e R \<parallel> P" and "R' \<parallel> P \<sim>\<^sub>e P \<parallel> R'" by(rule Strong_Early_Bisim_SC.parSym)+
        ultimately show ?thesis by(blast intro: Strong_Early_Bisim.transitive)
      qed
      moreover from PBisimQ R'BRT' have "(P \<parallel> R', Q \<parallel> T') \<in> bangRel weakBisim" by(rule BRPar)
      moreover have "Q \<parallel> T' \<sim>\<^sub>e Q \<parallel> T"
      proof -
        from T'BisimT have "T' \<parallel> Q \<sim>\<^sub>e T \<parallel> Q" by(rule Strong_Early_Bisim_Pres.parPres)
        moreover have "Q \<parallel> T' \<sim>\<^sub>e T' \<parallel> Q" and "T \<parallel> Q \<sim>\<^sub>e Q \<parallel> T" by(rule Strong_Early_Bisim_SC.parSym)+
        ultimately show ?thesis by(blast intro: Strong_Early_Bisim.transitive)
      qed
      ultimately show ?thesis by blast
    qed
  qed

  have ResCong: "\<And>P Q x. (P, Q) \<in> ?Y \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> ?Y"
    by(auto intro: BRRes Strong_Early_Bisim_Pres.resPres transitive)

  have Sim: "\<And>P Q. (P, Q) \<in> ?X \<Longrightarrow> P \<leadsto><?Y> Q"
  proof -
    fix P Q
    assume "(P, Q) \<in> ?X"
    thus "P \<leadsto><?Y> Q"
    proof(induct)
      case(BRBang P Q)
      have "P \<approx> Q" by fact
      moreover hence "P \<leadsto><weakBisim> Q" by(blast dest: weakBisimE)
      moreover have "\<And>P Q. P \<approx> Q \<Longrightarrow> P \<leadsto><weakBisim> Q" by(blast dest: weakBisimE)
      moreover from Strong_Early_Bisim.eqvt Weak_Early_Bisim.eqvt have "eqvt ?Y" by(blast intro: eqvtBangRel)

      ultimately show "!P \<leadsto><?Y> !Q" using ParCompose ResCong RelStay XsubY
        by(rule_tac Weak_Early_Sim_Pres.bangPres, simp_all)
    next
      case(BRPar P Q R T)
      have PBiSimQ: "P \<approx> Q" by fact
      moreover have RBangRelT: "(R, T) \<in> ?X" by fact
      have RSimT: "R \<leadsto><?Y> T" by fact
      moreover from PBiSimQ  have "P \<leadsto><weakBisim> Q" by(blast dest: weakBisimE)
      moreover from RBangRelT have "(R, T) \<in> ?Y" by(blast intro: Strong_Early_Bisim.reflexive)
      ultimately show "P \<parallel> R \<leadsto><?Y> Q \<parallel> T" using ParCompose ResCong eqvt eqvtY
        by(rule_tac Weak_Early_Sim_Pres.parCompose)
    next
      case(BRRes P Q x)
      have "P \<leadsto><?Y> Q" by fact
      thus "<\<nu>x>P \<leadsto><?Y> <\<nu>x>Q" using ResCong eqvtY XsubY
        by(rule_tac Weak_Early_Sim_Pres.resPres, simp_all)
    qed
  qed

  from PBisimQ have "(!P, !Q) \<in> ?X" by(rule BRBang)
  moreover from Weak_Early_Bisim.eqvt have "eqvt (bangRel weakBisim)" by(rule eqvtBangRel)
  ultimately show ?thesis
    apply(coinduct rule: Weak_Early_Bisim.transitive_coinduct_weak)
    apply(blast intro: Sim)
    by(blast dest: bangRelSymetric Weak_Early_Bisim.symetric intro: Strong_Early_Bisim.reflexive)
qed

end


text:
(*
    Title:      Gauss_Jordan_PA_IArrays.thy
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
*)

header{*Obtaining explicitly the invertible matrix which transforms a matrix to its reduced row echelon form over nested iarrays*}

theory Gauss_Jordan_PA_IArrays
imports
  Gauss_Jordan_PA
  Gauss_Jordan_IArrays
begin

subsection{*Definitions*}

definition "Gauss_Jordan_in_ij_iarrays_PA A' i j =
(let  P = fst A'; A = snd A'; n = least_non_zero_position_of_vector_from_index (column_iarray j A) i; interchange_A = interchange_rows_iarray A i n;
 interchange_P = interchange_rows_iarray P i n; P' = mult_row_iarray interchange_P i (1 / interchange_A !! i !! j)
 in (IArray.of_fun (\<lambda>s. if s = i then P' !! s else row_add_iarray P' s i (- interchange_A !! s !! j) !! s) (nrows_iarray A), Gauss_Jordan_in_ij_iarrays A i j))"

definition Gauss_Jordan_column_k_iarrays_PA :: "('a::{field} iarray iarray \<times> nat \<times> 'a::{field} iarray iarray) => nat => ('a iarray iarray \<times> nat \<times> 'a iarray iarray)"
  where "Gauss_Jordan_column_k_iarrays_PA A' k=(let P = fst A'; i = fst (snd A'); A = snd (snd A') in
  if (vector_all_zero_from_index (i, (column_iarray k A))) \<or> i = (nrows_iarray A) then (P,i,A) else let Gauss = Gauss_Jordan_in_ij_iarrays_PA (P, A) i k
    in (fst Gauss, i + 1, snd Gauss))"

definition Gauss_Jordan_upt_k_iarrays_PA :: "'a::{field} iarray iarray => nat => ('a::{field} iarray iarray \<times> 'a iarray iarray)"
  where "Gauss_Jordan_upt_k_iarrays_PA A k = (let foldl = foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray A), 0, A) [0..<Suc k] in (fst foldl, snd (snd foldl)))"

definition Gauss_Jordan_iarrays_PA :: "'a::{field} iarray iarray => ('a iarray iarray  \<times> 'a iarray iarray)"
  where "Gauss_Jordan_iarrays_PA A = Gauss_Jordan_upt_k_iarrays_PA A (ncols_iarray A - 1)"

subsection{*Proofs*}

subsubsection{*Properties of @{term "Gauss_Jordan_in_ij_iarrays_PA"}*}

lemma Gauss_Jordan_in_ij_iarrays_PA_def'[code]:
"Gauss_Jordan_in_ij_iarrays_PA A' i j =
(let  P = fst A'; A = snd A'; n = least_non_zero_position_of_vector_from_index (column_iarray j A) i;
  interchange_A = interchange_rows_iarray A i n; A' = mult_row_iarray interchange_A i (1 / interchange_A !! i !! j);
  interchange_P = interchange_rows_iarray P i n; P' = mult_row_iarray interchange_P i (1 / interchange_A !! i !! j)
 in (IArray.of_fun (\<lambda>s. if s = i then P' !! s else row_add_iarray P' s i (- interchange_A !! s !! j) !! s) (nrows_iarray A),
    (IArray.of_fun (\<lambda>s. if s = i then A' !! s else row_add_iarray A' s i (- interchange_A !! s !! j) !! s) (nrows_iarray A))))"
unfolding Gauss_Jordan_in_ij_iarrays_PA_def Gauss_Jordan_in_ij_iarrays_def Let_def ..

lemma snd_Gauss_Jordan_in_ij_iarrays_PA:
 shows "snd (Gauss_Jordan_in_ij_iarrays_PA (P, A) i j) = Gauss_Jordan_in_ij_iarrays A i j"
unfolding Gauss_Jordan_in_ij_iarrays_PA_def Gauss_Jordan_in_ij_iarrays_def Let_def snd_conv ..

lemma matrix_to_iarray_snd_Gauss_Jordan_in_ij_iarrays_PA:
 assumes "\<not> vector_all_zero_from_index (to_nat i, vec_to_iarray (column j A))"
 shows "matrix_to_iarray (snd (Gauss_Jordan_in_ij_PA (P,A) i j)) = snd (Gauss_Jordan_in_ij_iarrays_PA (matrix_to_iarray P,matrix_to_iarray A) (to_nat i) (to_nat j))"
by (metis assms matrix_to_iarray_Gauss_Jordan_in_ij snd_Gauss_Jordan_in_ij_PA_eq snd_Gauss_Jordan_in_ij_iarrays_PA)

lemma matrix_to_iarray_fst_Gauss_Jordan_in_ij_iarrays_PA:
 assumes not_all_zero: "\<not> vector_all_zero_from_index (to_nat i, vec_to_iarray (column j A))"
 shows "matrix_to_iarray (fst (Gauss_Jordan_in_ij_PA (P,A) i j)) = fst (Gauss_Jordan_in_ij_iarrays_PA (matrix_to_iarray P,matrix_to_iarray A) (to_nat i) (to_nat j))"
proof (unfold Gauss_Jordan_in_ij_PA_def Gauss_Jordan_in_ij_iarrays_PA_def Let_def fst_conv snd_conv, rule matrix_to_iarray_eq_of_fun, auto simp del: length_def sub_def)
show "vec_to_iarray (mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j) $ i) =
    mult_row_iarray (interchange_rows_iarray (matrix_to_iarray P) (to_nat i)
       (least_non_zero_position_of_vector_from_index (column_iarray (to_nat j) (matrix_to_iarray A)) (to_nat i))) (to_nat i)
     (1 / interchange_rows_iarray (matrix_to_iarray A) (to_nat i)
           (least_non_zero_position_of_vector_from_index (column_iarray (to_nat j) (matrix_to_iarray A)) (to_nat i)) !! to_nat i !! to_nat j) !! to_nat i"
    unfolding vec_to_iarray_column[symmetric]
    unfolding vec_to_iarray_least_non_zero_position_of_vector_from_index'[OF not_all_zero]
    unfolding matrix_to_iarray_interchange_rows[symmetric]
    unfolding matrix_to_iarray_mult_row[symmetric]
    unfolding matrix_to_iarray_nth
    unfolding interchange_rows_i
    unfolding vec_matrix ..
next
fix ia
show "vec_to_iarray (row_add (mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / A $ (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ j)) ia i
            (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ ia $ j) $ ia) =
         row_add_iarray (mult_row_iarray (interchange_rows_iarray (matrix_to_iarray P) (to_nat i)
              (least_non_zero_position_of_vector_from_index (column_iarray (to_nat j) (matrix_to_iarray A)) (to_nat i))) (to_nat i)
            (1 / interchange_rows_iarray (matrix_to_iarray A) (to_nat i)
                  (least_non_zero_position_of_vector_from_index (column_iarray (to_nat j) (matrix_to_iarray A)) (to_nat i)) !!
                 to_nat i !! to_nat j)) (to_nat ia) (to_nat i)
          (- interchange_rows_iarray (matrix_to_iarray A) (to_nat i)
              (least_non_zero_position_of_vector_from_index (column_iarray (to_nat j) (matrix_to_iarray A)) (to_nat i)) !!
             to_nat ia !! to_nat j) !! to_nat ia"
    unfolding vec_to_iarray_column[symmetric]
    unfolding vec_to_iarray_least_non_zero_position_of_vector_from_index'[OF not_all_zero]
    unfolding matrix_to_iarray_interchange_rows[symmetric]
    unfolding matrix_to_iarray_mult_row[symmetric]
    unfolding matrix_to_iarray_nth
    unfolding interchange_rows_i
    unfolding matrix_to_iarray_row_add[symmetric]
    unfolding vec_matrix ..
next
show "nrows_iarray (matrix_to_iarray A) = IArray.length (matrix_to_iarray
       (\<chi> s. if s = i then mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ i $ j) $ s
             else row_add (mult_row (interchange_rows P i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n)) i (1 / interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ i $ j)) s i
             (- interchange_rows A i (LEAST n. A $ n $ j \<noteq> 0 \<and> i \<le> n) $ s $ j) $ s))"
unfolding length_eq_card_rows nrows_eq_card_rows ..
qed

subsubsection{*Properties about @{term "Gauss_Jordan_column_k_iarrays_PA"}*}

lemma matrix_to_iarray_fst_Gauss_Jordan_column_k_PA:
assumes i: "i\<le>nrows A" and k: "k<ncols A"
shows "matrix_to_iarray (fst (Gauss_Jordan_column_k_PA (P,i,A) k)) = fst (Gauss_Jordan_column_k_iarrays_PA (matrix_to_iarray P, i, matrix_to_iarray A) k)"
proof (cases "i<nrows A")
case True
show ?thesis
unfolding Gauss_Jordan_column_k_PA_def Gauss_Jordan_column_k_iarrays_PA_def Let_def
unfolding snd_conv fst_conv
unfolding matrix_vector_all_zero_from_index
unfolding to_nat_from_nat_id[OF True[unfolded nrows_def]]
unfolding matrix_to_iarray_nrows
using matrix_to_iarray_fst_Gauss_Jordan_in_ij_iarrays_PA[of "from_nat i" "from_nat k" A P]
using matrix_to_iarray_snd_Gauss_Jordan_in_ij_iarrays_PA[of "from_nat i" "from_nat k" A  P]
unfolding to_nat_from_nat_id[OF True[unfolded nrows_def]]
unfolding to_nat_from_nat_id[OF k[unfolded ncols_def]]
unfolding vec_to_iarray_column'[OF k] by auto
next
case False
hence i_eq_nrows:"i=nrows A" using i by simp
thus ?thesis
unfolding Gauss_Jordan_column_k_PA_def Gauss_Jordan_column_k_iarrays_PA_def Let_def
unfolding snd_conv fst_conv unfolding matrix_to_iarray_nrows by fastforce
qed

lemma matrix_to_iarray_snd_Gauss_Jordan_column_k_PA:
assumes i: "i\<le>nrows A" and k: "k<ncols A"
shows "(fst (snd (Gauss_Jordan_column_k_PA (P,i,A) k))) = fst (snd (Gauss_Jordan_column_k_iarrays_PA (matrix_to_iarray P, i, matrix_to_iarray A) k))"
using matrix_to_iarray_Gauss_Jordan_column_k_1[OF k i]
unfolding Gauss_Jordan_column_k_def Gauss_Jordan_column_k_iarrays_def
unfolding Gauss_Jordan_column_k_PA_def Gauss_Jordan_column_k_iarrays_PA_def snd_conv fst_conv Let_def
unfolding snd_Gauss_Jordan_in_ij_iarrays_PA
unfolding snd_if_conv
unfolding snd_Gauss_Jordan_in_ij_PA_eq
by fastforce

lemma matrix_to_iarray_third_Gauss_Jordan_column_k_PA:
assumes i: "i\<le>nrows A" and k: "k<ncols A"
shows "matrix_to_iarray (snd (snd (Gauss_Jordan_column_k_PA (P,i,A) k))) = snd (snd (Gauss_Jordan_column_k_iarrays_PA (matrix_to_iarray P, i, matrix_to_iarray A) k))"
using matrix_to_iarray_Gauss_Jordan_column_k_2[OF k i]
unfolding Gauss_Jordan_column_k_def Gauss_Jordan_column_k_iarrays_def
unfolding Gauss_Jordan_column_k_PA_def Gauss_Jordan_column_k_iarrays_PA_def snd_conv fst_conv Let_def
unfolding snd_Gauss_Jordan_in_ij_iarrays_PA
unfolding snd_if_conv snd_Gauss_Jordan_in_ij_PA_eq by fast

subsubsection{*Properties about @{term "Gauss_Jordan_upt_k_iarrays_PA"}*}

lemma
assumes "k<ncols A"
shows matrix_to_iarray_fst_Gauss_Jordan_upt_k_PA: "matrix_to_iarray (fst (Gauss_Jordan_upt_k_PA A k)) = fst (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) k)"
and matrix_to_iarray_snd_Gauss_Jordan_upt_k_PA: "matrix_to_iarray (snd (Gauss_Jordan_upt_k_PA A k)) = (snd (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) k))"
and "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) =
    fst (snd (foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray (matrix_to_iarray A)), 0, matrix_to_iarray A) [0..<Suc k]))"
and "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) \<le> nrows A"
using assms
proof (induct k)
assume zero_less_ncols: "0 < ncols A"
show " matrix_to_iarray (fst (Gauss_Jordan_upt_k_PA A 0)) = fst (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) 0)"
unfolding Gauss_Jordan_upt_k_PA_def Gauss_Jordan_upt_k_iarrays_PA_def Let_def fst_conv apply auto
unfolding nrows_eq_card_rows unfolding matrix_to_iarray_mat[symmetric]
by (rule matrix_to_iarray_fst_Gauss_Jordan_column_k_PA, auto simp add: zero_less_ncols)
show "matrix_to_iarray (snd (Gauss_Jordan_upt_k_PA A 0)) = snd (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) 0)"
unfolding Gauss_Jordan_upt_k_PA_def Gauss_Jordan_upt_k_iarrays_PA_def Let_def fst_conv snd_conv apply auto
unfolding nrows_eq_card_rows unfolding matrix_to_iarray_mat[symmetric]
by (rule matrix_to_iarray_third_Gauss_Jordan_column_k_PA, auto simp add: zero_less_ncols)
show "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc 0])) =
    fst (snd (foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray (matrix_to_iarray A)), 0, matrix_to_iarray A) [0..<Suc 0]))"
apply simp unfolding nrows_eq_card_rows unfolding matrix_to_iarray_mat[symmetric]
by (rule matrix_to_iarray_snd_Gauss_Jordan_column_k_PA, auto simp add: zero_less_ncols)
show "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc 0])) \<le> nrows A"
by (simp add: fst_snd_Gauss_Jordan_column_k_PA_eq fst_Gauss_Jordan_column_k)
next
fix k assume "(k < ncols A \<Longrightarrow> matrix_to_iarray (fst (Gauss_Jordan_upt_k_PA A k)) = fst (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) k))"
and "(k < ncols A \<Longrightarrow> matrix_to_iarray (snd (Gauss_Jordan_upt_k_PA A k)) = snd (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) k))"
and "(k < ncols A \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) =
         fst (snd (foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray (matrix_to_iarray A)), 0, matrix_to_iarray A) [0..<Suc k])))"
and "(k < ncols A \<Longrightarrow> fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) \<le> nrows A)"
and Suc_k: "Suc k < ncols A"
hence hyp1: "matrix_to_iarray (fst (Gauss_Jordan_upt_k_PA A k)) = fst (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) k)"
and hyp2: "matrix_to_iarray (snd (Gauss_Jordan_upt_k_PA A k)) = snd (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) k)"
and hyp3: "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) =
         fst (snd (foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray (matrix_to_iarray A)), 0, matrix_to_iarray A) [0..<Suc k]))"
and hyp4: "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])) \<le> nrows A"
by linarith+

have suc_rw: "[0..<Suc (Suc k)] = [0..<Suc k] @ [Suc k]" by simp
def A'=="(foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k])"
def B=="(foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray (matrix_to_iarray A)), 0, matrix_to_iarray A) [0..<Suc k])"
have A'_eq: "A' = (fst A', fst (snd A'), snd (snd A'))" by auto

have fst_A': "matrix_to_iarray (fst A') = fst B" unfolding A'_def B_def by (rule hyp1[unfolded Gauss_Jordan_upt_k_PA_def Gauss_Jordan_upt_k_iarrays_PA_def Let_def fst_conv])
have fst_snd_A': "fst (snd A') = fst (snd B)" unfolding A'_def B_def by (rule hyp3[unfolded Gauss_Jordan_upt_k_PA_def Gauss_Jordan_upt_k_iarrays_PA_def ])
have snd_snd_A': "matrix_to_iarray (snd (snd A')) = (snd (snd B))"
unfolding A'_def B_def
by (rule hyp2[unfolded Gauss_Jordan_upt_k_PA_def Gauss_Jordan_upt_k_iarrays_PA_def Let_def fst_conv snd_conv])

show "matrix_to_iarray (fst (Gauss_Jordan_upt_k_PA A (Suc k))) = fst (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) (Suc k))"
proof -
have "matrix_to_iarray (fst (Gauss_Jordan_upt_k_PA A (Suc k))) = matrix_to_iarray (fst (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc (Suc k)]))"
unfolding Gauss_Jordan_upt_k_PA_def Let_def fst_conv ..
also have "... = matrix_to_iarray (fst (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]) (Suc k)))"
unfolding suc_rw foldl_append unfolding List.foldl.simps ..
also have "... = matrix_to_iarray (fst (Gauss_Jordan_column_k_PA (fst A',fst (snd A'), snd (snd A')) (Suc k)))" unfolding A'_def by simp
also have "... = fst (Gauss_Jordan_column_k_iarrays_PA (matrix_to_iarray (fst A'), fst (snd A'), matrix_to_iarray (snd (snd A'))) (Suc k))"
proof (rule matrix_to_iarray_fst_Gauss_Jordan_column_k_PA)
 show "fst (snd A') \<le> nrows (snd (snd A'))" using hyp4 unfolding nrows_def A'_def .
 show  "Suc k < ncols (snd (snd A'))" using Suc_k unfolding ncols_def .
qed
also have "... =  fst (Gauss_Jordan_column_k_iarrays_PA (fst B, fst (snd B), snd (snd B)) (Suc k))"
unfolding fst_A' fst_snd_A' snd_snd_A' ..
also have "... = fst (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) (Suc k))"
unfolding Gauss_Jordan_upt_k_iarrays_PA_def Let_def fst_conv
unfolding suc_rw foldl_append unfolding List.foldl.simps B_def by fastforce
finally show ?thesis .
qed

show "matrix_to_iarray (snd (Gauss_Jordan_upt_k_PA A (Suc k))) = snd (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) (Suc k))"
proof -
  have "matrix_to_iarray (snd (Gauss_Jordan_upt_k_PA A (Suc k))) =  matrix_to_iarray (snd (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc (Suc k)])))"
  unfolding Gauss_Jordan_upt_k_PA_def Let_def snd_conv ..
also have "... =  matrix_to_iarray (snd (snd (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]) (Suc k))))"
unfolding suc_rw foldl_append unfolding List.foldl.simps ..
also have "... = matrix_to_iarray (snd (snd (Gauss_Jordan_column_k_PA (fst A',fst (snd A'), snd (snd A')) (Suc k))))" unfolding A'_def by simp
also have "... =  snd (snd (Gauss_Jordan_column_k_iarrays_PA (matrix_to_iarray (fst A'), fst (snd A'), matrix_to_iarray (snd (snd A'))) (Suc k)))"
proof (rule matrix_to_iarray_third_Gauss_Jordan_column_k_PA)
 show "fst (snd A') \<le> nrows (snd (snd A'))" using hyp4 unfolding nrows_def A'_def .
 show  "Suc k < ncols (snd (snd A'))" using Suc_k unfolding ncols_def .
qed
also have "... = snd (snd (Gauss_Jordan_column_k_iarrays_PA (fst B, fst (snd B), snd (snd B)) (Suc k)))"
unfolding fst_A' fst_snd_A' snd_snd_A' ..
also have "... = snd (Gauss_Jordan_upt_k_iarrays_PA (matrix_to_iarray A) (Suc k))"
unfolding Gauss_Jordan_upt_k_iarrays_PA_def Let_def fst_conv
unfolding suc_rw foldl_append unfolding List.foldl.simps B_def by fastforce
finally show ?thesis .
qed

show "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc (Suc k)])) =
        fst (snd (foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray (matrix_to_iarray A)), 0, matrix_to_iarray A) [0..<Suc (Suc k)]))"
proof -
have "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc (Suc k)])) =
  fst (snd (Gauss_Jordan_column_k_PA (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc k]) (Suc k)))"
unfolding suc_rw foldl_append unfolding List.foldl.simps ..
also have "... = fst (snd (Gauss_Jordan_column_k_PA (fst A',fst (snd A'), snd (snd A')) (Suc k)))"
unfolding A'_def by simp
also have "... = fst (snd (Gauss_Jordan_column_k_iarrays_PA (matrix_to_iarray (fst A'),fst (snd A'), matrix_to_iarray (snd (snd A'))) (Suc k)))"
proof (rule matrix_to_iarray_snd_Gauss_Jordan_column_k_PA)
 show "fst (snd A') \<le> nrows (snd (snd A'))" using hyp4 unfolding nrows_def A'_def .
 show "Suc k < ncols (snd (snd A'))" using Suc_k unfolding ncols_def .
qed
also have  "\<dots> = fst (snd (Gauss_Jordan_column_k_iarrays_PA (fst B,fst (snd B), snd (snd B)) (Suc k)))"
unfolding fst_A' fst_snd_A' snd_snd_A' ..
also have "... = fst (snd (foldl Gauss_Jordan_column_k_iarrays_PA (mat_iarray 1 (nrows_iarray (matrix_to_iarray A)), 0, matrix_to_iarray A) [0..<Suc (Suc k)]))"
unfolding B_def unfolding nrows_eq_card_rows unfolding matrix_to_iarray_mat[symmetric] by auto
finally show ?thesis .
qed
show "fst (snd (foldl Gauss_Jordan_column_k_PA (mat 1, 0, A) [0..<Suc (Suc k)])) \<le> nrows A"
by (metis snd_foldl_Gauss_Jordan_column_k_eq Suc_k fst_foldl_Gauss_Jordan_column_k_less)
qed

subsubsection{*Properties about @{term "Gauss_Jordan_iarrays_PA"}*}

lemma matrix_to_iarray_fst_Gauss_Jordan_PA:
shows "matrix_to_iarray (fst (Gauss_Jordan_PA A)) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))"
unfolding Gauss_Jordan_PA_def Gauss_Jordan_iarrays_PA_def using matrix_to_iarray_fst_Gauss_Jordan_upt_k_PA
by (metis One_nat_def Suc_eq_plus1_left add_diff_inverse diff_le_self less_Suc0 matrix_to_iarray_ncols n_not_Suc_n nat_neq_iff ncols_not_0 not_le)

lemma matrix_to_iarray_snd_Gauss_Jordan_PA:
shows "matrix_to_iarray (snd (Gauss_Jordan_PA A)) = snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A))"
unfolding Gauss_Jordan_PA_def Gauss_Jordan_iarrays_PA_def using matrix_to_iarray_snd_Gauss_Jordan_upt_k_PA
by (metis One_nat_def Suc_eq_plus1_left add_diff_inverse diff_le_self less_Suc0 matrix_to_iarray_ncols n_not_Suc_n nat_neq_iff ncols_not_0 not_le)

lemma Gauss_Jordan_iarrays_PA_mult:
fixes A::"'a::{field}^'cols::{mod_type}^'rows::{mod_type}"
shows "snd (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) = fst (Gauss_Jordan_iarrays_PA (matrix_to_iarray A)) **i (matrix_to_iarray A)"
proof -
have "snd (Gauss_Jordan_PA A) = fst (Gauss_Jordan_PA A) ** A" using fst_Gauss_Jordan_PA[of A] ..
hence "matrix_to_iarray (snd (Gauss_Jordan_PA A)) = matrix_to_iarray (fst (Gauss_Jordan_PA A) ** A)" by simp
thus ?thesis unfolding matrix_to_iarray_snd_Gauss_Jordan_PA matrix_to_iarray_matrix_matrix_mult matrix_to_iarray_fst_Gauss_Jordan_PA .
qed

lemma snd_snd_Gauss_Jordan_column_k_iarrays_PA_eq:
shows "snd (snd (Gauss_Jordan_column_k_iarrays_PA (P,i,A) k)) = snd (Gauss_Jordan_column_k_iarrays (i,A) k)"
unfolding Gauss_Jordan_column_k_iarrays_PA_def Gauss_Jordan_column_k_iarrays_def unfolding Let_def snd_conv fst_conv unfolding snd_Gauss_Jordan_in_ij_iarrays_PA by auto

lemma fst_snd_Gauss_Jordan_column_k_iarrays_PA_eq:
shows "fst (snd (Gauss_Jordan_column_k_iarrays_PA (P,i,A) k)) = fst (Gauss_Jordan_column_k_iarrays (i,A) k)"
unfolding Gauss_Jordan_column_k_iarrays_PA_def Gauss_Jordan_column_k_iarrays_def unfolding Let_def snd_conv fst_conv by auto

lemma foldl_Gauss_Jordan_column_k_iarrays_eq:
"snd (foldl Gauss_Jordan_column_k_iarrays_PA (B, 0, A) [0..<k]) = foldl Gauss_Jordan_column_k_iarrays (0, A) [0..<k]"
proof (induct k)
case 0
show ?case by simp
case (Suc k)
have suc_rw: "[0..<Suc k] = [0..<k] @ [k]" by simp
show ?case
unfolding suc_rw foldl_append unfolding List.foldl.simps
by (metis Suc.hyps fst_snd_Gauss_Jordan_column_k_iarrays_PA_eq snd_snd_Gauss_Jordan_column_k_iarrays_PA_eq surjective_pairing)
qed

lemma snd_Gauss_Jordan_upt_k_iarrays_PA:
shows "snd (Gauss_Jordan_upt_k_iarrays_PA A k) = (Gauss_Jordan_upt_k_iarrays A k)"
unfolding Gauss_Jordan_upt_k_iarrays_PA_def Gauss_Jordan_upt_k_iarrays_def Let_def
using foldl_Gauss_Jordan_column_k_iarrays_eq[of "mat_iarray 1 (nrows_iarray A)" A "Suc k"] by simp

lemma snd_Gauss_Jordan_iarrays_PA_eq: "snd (Gauss_Jordan_iarrays_PA A) = Gauss_Jordan_iarrays A"
unfolding Gauss_Jordan_iarrays_def Gauss_Jordan_iarrays_PA_def
using snd_Gauss_Jordan_upt_k_iarrays_PA by auto

end

author: Josh-Tilles

repo: AFP

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


text:
section \<open>Soundness Theorems\<close>

theory Wasm_Soundness imports Main Wasm_Properties begin

theorem preservation:
  assumes "\<turnstile>_i s;vs;es : ts"
          "\<lparr>s;vs;es\<rparr> \<leadsto>_i \<lparr>s';vs';es'\<rparr>"
  shows "\<turnstile>_i s';vs';es' : ts"
proof -
  obtain \<S> where "store_typing s \<S>" "\<S>\<bullet>None \<tturnstile>_i vs;es : ts"
    using assms(1) config_typing.simps
    by blast
  hence "store_typing s' \<S>" "\<S>\<bullet>None \<tturnstile>_i vs';es' : ts"
    using assms(2) store_preserved types_preserved_e
    by simp_all
  thus ?thesis
    using config_typing.intros
    by blast
qed

theorem progress:
  assumes "\<turnstile>_i s;vs;es : ts"
  shows "const_list es \<or> es = [Trap] \<or> (\<exists>a s' vs' es'. \<lparr>s;vs;es\<rparr> \<leadsto>_i \<lparr>s';vs';es'\<rparr>)"
proof -
  obtain \<S> where "store_typing s \<S>" "\<S>\<bullet>None \<tturnstile>_i vs;es : ts"
    using assms config_typing.simps
    by blast
  thus ?thesis
    using progress_e3
    by blast
qed

end

repo: PSL


text:
theory InstanceTerms
imports NonFreeAnimation
begin

(*Binding terms with freshness and substitution (another "must" since it further tests parameter conditions): *)

type_synonym var = nat

(*
datatype terms = Var "var" | App "terms" "terms" | Lm "var" "terms" | Subst ""terms" "terms" "var"

Note: changed Subst argument order to get order  external inputs -> internal inputs -> output
notation X[ Y / y] for Subst X Y y  or  (subst y := Y in X)

with fresh : var => term => bool
where
   (Var x) [X / x] = X

  x ~= y ==>  (Var x) [Y / y] = Var x

  (App X Y) [Z / z] = App (X [Z / z]) (Y [Z / z])

 [|x ~= y; fresh x Y|] ==>  (Lm  x X) [Y / y] = Lm x (X [Y / y])

  x ~= y ==> fresh x (Var y)

  [|fresh x Y; fresh x Z|] ==> fresh x (App Y Z)

  fresh x (Lm x X)

  fresh x Y ==> fresh x (Lm y Y)

  [|y ~= x; fresh y X|] ==> Lm x X = Lm y (X [(Var y) / x])
*)

locale results =
  fixes var :: tyco
    and terms_name :: tyco
    and Var_name :: oper
    and App_name :: oper
    and Lam_name :: oper
    and Subst_name :: oper
    and fresh_name :: rel
    and neq :: pcond
begin

lemma [ffact]: "terms_name tycohaskind IntType" ..
lemma [ffact]: "var tycohaskind ExtType" ..
lemma [ffact]: "var tyinterpr TYPE(var)" ..
lemma [ffact]: "decl_tyvars () []" ..

lemma [ffact]: "Var_name operhasty (var =T=> terms_name)" ..
lemma [ffact]: "App_name operhasty (terms_name =T=> terms_name =T=> terms_name)" ..
lemma [ffact]: "Lam_name operhasty (var =T=> terms_name =T=> terms_name)" ..
  (* we need to switch the argument order to adhere to  external inputs -> internal inputs -> output *)
lemma [ffact]: "Subst_name operhasty (terms_name =T=> terms_name =T=> var =T=> terms_name)" ..

abbreviation
  subst_abbrev ("subst _ := _ in _" [100,100,100] 60)
where
  "(subst x := t2 in t1) == Subst_name $ t1 $ t2 $ x"

lemma [ffact]: "fresh_name relhasty (var =T=> terms_name =T=> bool)" ..
lemma [ffact]: "neq pcondhasty (var =T=> var =T=> bool)" ..
lemma [ffact]: "neq pcondinterpr (% (x :: var) y. x ~= y)" ..

definition "subst_clause1_name = (0::nat)"
definition "subst_clause2_name = (0::nat)"
definition "subst_clause3_name = (0::nat)"
definition "subst_clause4_name = (0::nat)"
definition "subst_clause5_name = (0::nat)"
definition "fresh_clause1_name = (0::nat)"
definition "fresh_clause2_name = (0::nat)"
definition "fresh_clause3_name = (0::nat)"
definition "fresh_clause4_name = (0::nat)"

(*
  (Var x) [X / x] = X
  x ~= y ==>  (Var x) [Y / y] = Var x
  (App X Y) [Z / z] = App (X [Z / z]) (Y [Z / z])
  [|x ~= y; fresh x Y|] ==>  (Lm x X) [Y / y] = Lm x (X [Y / y])
  [|y ~= x; fresh y X|] ==> Lm x X = Lm y (X [(Var y) / x]) *)
lemma [ffact]: "decl_hcl subst_clause1_name (QUANT x:var. QUANT X:terms_name.
   subst x := X in (Var_name $ x) === X)" ..
lemma [ffact]: "decl_hcl subst_clause2_name (QUANT x:var. QUANT y:var. QUANT Y:terms_name.
  neq $ x $ y --->
    subst y := Y in (Var_name $ x) === Var_name $ x)" ..
lemma [ffact]: "decl_hcl subst_clause3_name (QUANT z : var. QUANT X : terms_name. QUANT Y : terms_name. QUANT Z : terms_name.
  subst z := Z in (App_name $ X $ Y) === App_name $ (subst z := Z in X) $ (subst z := Z in Y))" ..
lemma [ffact]: "decl_hcl subst_clause4_name (QUANT x:var. QUANT y:var. QUANT X:terms_name. QUANT Y:terms_name.
  neq $ x $ y ---> fresh_name $ x $ Y --->
    subst y := Y in (Lam_name $ x $ X) === Lam_name $ x $ (subst y := Y in X))" ..
lemma [ffact]: "decl_hcl subst_clause5_name (QUANT x:var. QUANT y:var. QUANT X:terms_name.
  neq $ y $ x ---> fresh_name $ y $ X --->
    Lam_name $ x $ X === Lam_name $ y $ (subst x := (Var_name $ y) in X))" ..

(*  x ~= y ==> fresh x (Var y)
  [|fresh x Y; fresh x Z|] ==> fresh x (App Y Z)
  fresh x (Lm x X)
  fresh x Y ==> fresh x (Lm y Y) *)
lemma [ffact]: "decl_hcl fresh_clause1_name (QUANT x:var. QUANT y:var. QUANT X:terms_name.
  neq $ x $ y ---> fresh_name $ x $ (Var_name $ y))" ..
lemma [ffact]: "decl_hcl fresh_clause2_name (QUANT x:var. QUANT Y:terms_name. QUANT Z:terms_name.
  fresh_name $ x $ Y ---> fresh_name $ x $ Z ---> fresh_name $ x $ (App_name $ Y $ Z))" ..
lemma [ffact]: "decl_hcl fresh_clause3_name (QUANT x:var. QUANT X:terms_name.
  fresh_name $ x $ (Lam_name $ x $ X))" ..
lemma [ffact]: "decl_hcl fresh_clause4_name (QUANT x:var. QUANT y:var. QUANT Y:terms_name.
  fresh_name $ x $ Y ---> fresh_name $ x $ (Lam_name $ y $ Y))" ..

ML {*
 Toplevel.profiling := 0
*}

local_setup {* MetaRec.run_expl_frules *}

end

thm results.fresh_clause2
thm results.subst_clause4

locale algebra_results = results  var terms_name Var_name App_name Lam_name Subst_name fresh_name neq
    for var :: tyco
    and terms_name :: tyco
    and Var_name :: oper
    and App_name :: oper
    and Lam_name :: oper
    and Subst_name :: oper
    and fresh_name :: rel
    and neq :: pcond
begin

definition
  myiter_name where
  "myiter_name = (0::nat)"

definition freshint where
  "freshint == (% (x :: var) (y :: nat). True)"

lemma [ffact]: "decl_iter_name terms_name myiter_name" ..

lemma [ffact]: "terms_name alginterpr TYPE(nat)" ..
lemma [ffact]: "Var_name operalginterpr (% (x::var). 0::nat)" ..
lemma [ffact]: "App_name operalginterpr (% (X :: nat) Y. X + Y)" ..
lemma [ffact]: "Lam_name operalginterpr (% (x::var) X ::nat. X + 1)" ..
  (* wrong of course! just testing *)
lemma [ffact]: "Subst_name operalginterpr (% (X::nat) Y (x::var). X * Y)" ..
lemma [ffact]: "fresh_name relalginterpr freshint" ..

  (* assume everything! just testing *)
lemma [ffact]: "proven_hcl True" by (simp add: proven_hcl_def)
lemma [MR]: "proven_hcl P" by sorry2

local_setup {* MetaRec.run_expl_frules *}

end

thm algebra_results.iter_op_clauses0
thm algebra_results.iter_rel_clauses0

end

author: metaforcy

repo: nonfree-data


text:
(*  Title:      HOL/Proofs/Extraction/Util.thy
    Author:     Stefan Berghofer, TU Muenchen
*)

section \<open>Auxiliary lemmas used in program extraction examples\<close>

theory Util
imports Main
begin

text \<open>Decidability of equality on natural numbers.\<close>

lemma nat_eq_dec: "\<And>n::nat. m = n \<or> m \<noteq> n"
  apply (induct m)
  apply (case_tac n)
  apply (case_tac [3] n)
  apply (simp only: nat.simps, iprover?)+
  done

text \<open>
  Well-founded induction on natural numbers, derived using the standard
  structural induction rule.
\<close>

lemma nat_wf_ind:
  assumes R: "\<And>x::nat. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
  shows "P z"
proof (rule R)
  show "\<And>y. y < z \<Longrightarrow> P y"
  proof (induct z)
    case 0
    then show ?case by simp
  next
    case (Suc n y)
    from nat_eq_dec show ?case
    proof
      assume ny: "n = y"
      have "P n"
        by (rule R) (rule Suc)
      with ny show ?case by simp
    next
      assume "n \<noteq> y"
      with Suc have "y < n" by simp
      then show ?case by (rule Suc)
    qed
  qed
qed

text \<open>Bounded search for a natural number satisfying a decidable predicate.\<close>

lemma search:
  assumes dec: "\<And>x::nat. P x \<or> \<not> P x"
  shows "(\<exists>x<y. P x) \<or> \<not> (\<exists>x<y. P x)"
proof (induct y)
  case 0
  show ?case by simp
next
  case (Suc z)
  then show ?case
  proof
    assume "\<exists>x<z. P x"
    then obtain x where le: "x < z" and P: "P x" by iprover
    from le have "x < Suc z" by simp
    with P show ?case by iprover
  next
    assume nex: "\<not> (\<exists>x<z. P x)"
    from dec show ?case
    proof
      assume P: "P z"
      have "z < Suc z" by simp
      with P show ?thesis by iprover
    next
      assume nP: "\<not> P z"
      have "\<not> (\<exists>x<Suc z. P x)"
      proof
        assume "\<exists>x<Suc z. P x"
        then obtain x where le: "x < Suc z" and P: "P x" by iprover
        have "x < z"
        proof (cases "x = z")
          case True
          with nP and P show ?thesis by simp
        next
          case False
          with le show ?thesis by simp
        qed
        with P have "\<exists>x<z. P x" by iprover
        with nex show False ..
      qed
      then show ?case by iprover
    qed
  qed
qed

end

repo: isabelle


text:
(* This Isabelle theory is produced using the TIP tool offered at the following website:
     https://github.com/tip-org/tools
   This file was originally provided as part of TIP benchmark at the following website:
     https://github.com/tip-org/benchmarks
   Yutaka Nagashima at CIIRC, CTU changed the TIP output theory file slightly
   to make it compatible with Isabelle2017.*)
  theory TIP_int_mul_assoc
imports "../../Test_Base"
begin

datatype Sign = Pos | Neg

datatype Nat = Z | S "Nat"

datatype Integer = P "Nat" | N "Nat"

fun toInteger :: "Sign => Nat => Integer" where
"toInteger (Pos) y = P y"
| "toInteger (Neg) (Z) = P Z"
| "toInteger (Neg) (S z) = N z"

fun sign :: "Integer => Sign" where
"sign (P y) = Pos"
| "sign (N z) = Neg"

fun pred :: "Nat => Nat" where
"pred (S y) = y"

fun plus :: "Nat => Nat => Nat" where
"plus (Z) y = y"
| "plus (S z) y = S (plus z y)"

fun times2 :: "Nat => Nat => Nat" where
"times2 (Z) y = Z"
| "times2 (S z) y = plus y (times2 z y)"

fun opposite :: "Sign => Sign" where
"opposite (Pos) = Neg"
| "opposite (Neg) = Pos"

fun timesSign :: "Sign => Sign => Sign" where
"timesSign (Pos) y = y"
| "timesSign (Neg) y = opposite y"

fun absVal :: "Integer => Nat" where
"absVal (P n) = n"
| "absVal (N m) = plus (S Z) m"

fun times :: "Integer => Integer => Integer" where
"times x y =
   toInteger
     (timesSign (sign x) (sign y)) (times2 (absVal x) (absVal y))"

theorem property0 :
  "((times x (times y z)) = (times (times x y) z))"
  oops

end


text:
(*  Title: thys/Rec_Ex.thy
    Author: Franz Regensburger (FABR) 03/2022
 *)

section \<open>Examples for Recursive Functions based on Rec\_def\<close>

theory Rec_Ex
  imports Rec_Def
begin

definition plus_2 :: "recf"
  where
    "plus_2 = (Cn 1 s [s])"

lemma "rec_exec plus_2 [0] = Suc (Suc 0)"
  unfolding plus_2_def
proof -
  have "rec_exec (Cn 1 s [s]) [0] = rec_exec s (map (\<lambda> a. rec_exec a [0]) [s])"
    by auto
  also have "... = rec_exec s [Suc 0]"
    by auto
  also have "... = Suc (Suc 0)"
    by auto
  finally show "rec_exec (Cn 1 s [s]) [0] = Suc (Suc 0)" .
qed

lemma "rec_exec plus_2 [2] = 4"
  unfolding plus_2_def
 by auto

lemma "rec_exec plus_2 [0] = 2"
  unfolding plus_2_def
 by auto

text \<open>The arity parameter given to the constructors of recursive functions
is not checked during execution by the interpreter.

See the next example where we
run @{term "pls_2"} with two arguments instead of only one.
\<close>

lemma "rec_exec plus_2 [2,3] = 4"
  unfolding plus_2_def
 by auto

lemma "rec_exec plus_2 [2,3] = 4"
  unfolding plus_2_def
 by auto

text \<open>What is the purpose of the arity parameter?

   The argument 1 of the constructors, which is supposed to be the arity,
   is completely ignored by @{term "rec_exec"}.
   However, for proofing termination, we need a correct arity specification.
\<close>

lemma "terminate plus_2 [2]"
  unfolding plus_2_def
proof (rule Rec_Def.terminate.termi_cn)
  show "terminate s (map (\<lambda>g. rec_exec g [2]) [s])"
  proof -
    have "(map (\<lambda>g. rec_exec g [2]) [s]) = [rec_exec s [2]]" by auto
    then show ?thesis using termi_s by auto
  qed
next
  show "\<forall>g\<in>set [s]. terminate g [2]" by (auto simp add: termi_s)
next
 (*  1. length [2] = 8
    ahh: we need the correct arity for proving the predicate termination
 *)
  show "length [2] = 1" by auto
qed

lemma "terminate plus_2 [2]"
  unfolding plus_2_def
  by (rule Rec_Def.terminate.termi_cn) (auto simp add: termi_s)

text \<open>If we try to proof termination of a run with superfluous arguments, we are stuck.
We need the correct arity for proving the predicate termination.\<close>

lemma "terminate plus_2 [2,3]"
  unfolding plus_2_def
proof (rule Rec_Def.terminate.termi_cn)
  show "terminate s (map (\<lambda>g. rec_exec g [2, 3]) [s])"
    by (auto simp add: termi_s)
next
  show "\<forall>g\<in>set [s]. terminate g [2, 3]"
  proof
    fix g
    assume "g \<in> set [s]"
    then show "terminate g [2, 3]"
    proof -
      have "terminate s [2, 3]"
        (* this, we cannot prove based on the inductive definition of s *)
        oops

end

author: isabelle-prover

repo: mirror-afp-devel


text:
(* This Isabelle theory is produced using the TIP tool offered at the following website:
     https://github.com/tip-org/tools
   This file was originally provided as part of TIP benchmark at the following website:
     https://github.com/tip-org/benchmarks
   Yutaka Nagashima at CIIRC, CTU changed the TIP output theory file slightly
   to make it compatible with Isabelle2017.*)
  theory TIP_list_nat_elem
imports "../../Test_Base"
begin

datatype 'a list = nil2 | cons2 "'a" "'a list"

datatype Nat = Z | S "Nat"

fun x :: "'a list => Nat => 'a" where
"x (cons2 z2 x2) (Z) = z2"
| "x (cons2 z2 x2) (S x3) = x x2 x3"

fun elem :: "'a => 'a list => bool" where
"elem y (nil2) = False"
| "elem y (cons2 z2 xs) = ((z2 = y) | (elem y xs))"

theorem property0 :
  "((elem y xs) ==> (? (z :: Nat) . (y = (x xs z))))"
  oops

end


text:
theory Inherence
  imports PossibleWorlds Chains
begin

text_raw \<open>\Copy{locale:inherence-sig}{\<close>
locale inherence_sig =
    possible_worlds_alt_sig where \<W> = \<W>
  for \<W> :: \<open>'e set set\<close> +
  fixes
    inheresIn :: \<open>'e \<Rightarrow> 'e \<Rightarrow> bool\<close> (infix \<open>\<triangleleft>\<close> 75)
text_raw \<open>}\<close>

sublocale inherence_sig \<subseteq> inh: binary_relation \<open>(\<triangleleft>)\<close> .

record 'e inherence_model =
  im_\<W> :: \<open>'e set set\<close>
  im_inheresIn :: \<open>'e \<Rightarrow> 'e \<Rightarrow> bool\<close>

text_raw \<open>\Copy{locale:inherence-base}{\<close>
locale inherence_base =
  inherence_sig +
  possible_worlds_alt +
  assumes
    inherence_imp_ed: \<open>x \<triangleleft> y \<Longrightarrow> ed x y\<close> and
    moment_non_migration: \<open>\<lbrakk> x \<triangleleft> y ; x \<triangleleft> z \<rbrakk> \<Longrightarrow> y = z\<close>
text_raw \<open>}\<close>

text_raw \<open>\Copy{locale:inherence-original}{\<close>
locale inherence_original =
  inherence_base +
  assumes
    inherence_scope: \<open>x \<triangleleft> y \<Longrightarrow> x \<in> \<E> \<and> y \<in> \<E>\<close> and
    inherence_irrefl: \<open>\<not> x \<triangleleft> x\<close> and
    inherence_asymm: \<open>x \<triangleleft> y \<Longrightarrow> \<not> y \<triangleleft> x\<close> and
    inherence_antitrgansitive: "\<lbrakk> x \<triangleleft> y ; y \<triangleleft> z \<rbrakk> \<Longrightarrow> \<not> x \<triangleleft> z"
text_raw \<open>}\<close>

context inherence_base
begin

lemma inherence_scope: \<open>x \<triangleleft> y \<Longrightarrow> x \<in> \<E> \<and> y \<in> \<E>\<close>
  using ed_scope inherence_imp_ed by blast

lemma asymm_imp_irrefl:
  assumes \<open>\<And>x y. x \<triangleleft> y \<Longrightarrow> \<not> y \<triangleleft> x\<close>
  shows \<open>\<And>x. \<not> x \<triangleleft> x\<close>
  using assms by metis

lemma asymm_imp_antitrgansitivity:
  assumes \<open>\<And>x y. x \<triangleleft> y \<Longrightarrow> \<not> y \<triangleleft> x\<close> \<open>x \<triangleleft> y\<close> \<open>y \<triangleleft> z\<close>
  shows \<open>\<not> x \<triangleleft> z\<close>
proof
  assume \<open>x \<triangleleft> z\<close>
  then have \<open>y = z\<close> using moment_non_migration assms(2) by blast
  then have \<open>z \<triangleleft> z\<close> using assms(3) by blast
  then show False using assms(1) asymm_imp_irrefl by simp
qed

end

text_raw \<open>\Copy{locale:inherence-simplified}{\<close>
locale inherence_simplified =
  inherence_base +
  assumes
    inherence_asymm: \<open>x \<triangleleft> y \<Longrightarrow> \<not> y \<triangleleft> x\<close>
text_raw \<open>}\<close>

sublocale inherence_simplified \<subseteq> inherence_original
proof (unfold_locales)
  show inherence_scope: \<open>\<And>x y. x \<triangleleft> y \<Longrightarrow> x \<in> \<E> \<and> y \<in> \<E>\<close>
    using ed_scope inherence_imp_ed by blast
  show inherence_irrefl: \<open>\<And>x. \<not> x \<triangleleft> x\<close>
    using asymm_imp_irrefl inherence_asymm by metis
  show  \<open>\<And>x y. x \<triangleleft> y \<Longrightarrow> \<not> y \<triangleleft> x\<close>
    using inherence_asymm by metis
  show \<open>\<And>x y z. x \<triangleleft> y \<Longrightarrow> y \<triangleleft> z \<Longrightarrow> \<not> x \<triangleleft> z\<close>
    using inherence_asymm asymm_imp_antitrgansitivity by metis
qed

lemma inherence_original_eq_simplified:
  \<open>inherence_original = inherence_simplified\<close>
proof (intro ext iffI)
  fix \<W> :: \<open>'e set set\<close> and
      inheresIn :: \<open>'e \<Rightarrow> 'e \<Rightarrow> bool\<close> (infix \<open>\<triangleleft>\<close> 75)
  assume \<open>inherence_original \<W> (\<triangleleft>)\<close>
  then interpret inherence_original \<W> \<open>(\<triangleleft>)\<close> .
  show \<open>inherence_simplified \<W> (\<triangleleft>)\<close>
    apply (unfold_locales)
    using inherence_asymm .
next
  fix \<W> :: \<open>'e set set\<close> and
      inheresIn :: \<open>'e \<Rightarrow> 'e \<Rightarrow> bool\<close> (infix \<open>\<triangleleft>\<close> 75)
  assume \<open>inherence_simplified \<W> (\<triangleleft>)\<close>
  then interpret inherence_simplified \<W> \<open>(\<triangleleft>)\<close> .
  show \<open>inherence_original \<W> (\<triangleleft>)\<close>
    by intro_locales
qed

text_raw \<open>\Copy{lemma:inherence-original-eq-simplified}{%\<close>
text \<open>@{thm inherence_original_eq_simplified}\<close>
text_raw \<open>}\<close>

context inherence_sig
begin

text_raw \<open>\Copy{def:inherence-symbols}{\<close>
definition \<open>\<M> \<equiv> { x | x y . inheresIn x y }\<close>

definition \<open>\<S> \<equiv> { x . x \<in> \<E> \<and> (\<forall>y. \<not> inheresIn x y) }\<close>

definition \<open>bearerOf s m \<equiv> (\<triangleleft>)\<inverse>\<inverse>\<close>

definition \<open>ultimate_bearer_of s m \<equiv> s \<in> \<S> \<and> m \<in> \<E> \<and> (\<triangleleft>)\<^sup>*\<^sup>* m s\<close>

definition \<open>order_of x n \<equiv> x \<in> \<E> \<and> (\<exists>s \<in> \<S>. ((\<triangleleft>)^^n) x s)\<close>
text_raw \<open>}\<close>

definition \<open>has_ultimate_bearer_problem \<equiv> \<exists>x \<in> \<M>. \<nexists>y. ultimate_bearer_of y x\<close>

definition \<open>has_order_problem \<equiv> \<exists>x \<in> \<M>. \<nexists>n. order_of x n\<close>

end

context inherence_sig
begin

lemma \<M>_I[intro]: \<open>x \<triangleleft> y \<Longrightarrow> x \<in> \<M>\<close>
  by (auto simp: \<M>_def)

lemma \<M>_E[elim]:
  assumes \<open>x \<in> \<M>\<close>
  obtains y where \<open>x \<triangleleft> y\<close>
  using assms by (auto simp: \<M>_def)

lemma \<S>_I[intro!]:
  assumes \<open>x \<in> \<E>\<close> \<open>\<forall>y. \<not> x \<triangleleft> y\<close>
  shows \<open>x \<in> \<S>\<close>
  using assms by (auto simp: \<S>_def)

lemma \<S>_E[elim]:
  assumes \<open>x \<in> \<S>\<close>
  obtains \<open>x \<in> \<E>\<close> \<open>\<And>y. x \<triangleleft> y \<Longrightarrow> False\<close>
  using assms by (auto simp: \<S>_def)

lemma \<E>_cases[cases set]:
  assumes \<open>x \<in> \<E>\<close>
  obtains (substantial) \<open>x \<in> \<S>\<close> |
          (moment) \<open>x \<in> \<M>\<close>
  using assms by auto

lemma \<M>_\<S>_disj[dest!]:
  assumes \<open>x \<in> \<M>\<close> \<open>x \<in> \<S>\<close>
  shows False
  using assms \<M>_E by auto

lemma ultimate_bearer_of_I1:
  assumes \<open>s \<in> \<S>\<close> \<open>m \<in> \<E>\<close> \<open>(\<triangleleft>)\<^sup>*\<^sup>* m s\<close>
  shows \<open>ultimate_bearer_of s m\<close>
  using assms by (auto simp: ultimate_bearer_of_def)

lemma ultimate_bearer_of_E[elim!]:
  assumes \<open>ultimate_bearer_of s m\<close>
  obtains \<open>s \<in> \<S>\<close> \<open>m \<in> \<E>\<close> \<open>(\<triangleleft>)\<^sup>*\<^sup>* m s\<close>
  using assms by (auto simp: ultimate_bearer_of_def)

lemma order_of_I1:
  assumes \<open>x \<in> \<E>\<close> \<open>s \<in> \<S>\<close> \<open>((\<triangleleft>)^^n) x s\<close>
  shows \<open>order_of x n\<close>
  using assms by (auto simp: order_of_def)

lemma order_of_E[elim]:
  assumes \<open>order_of x n\<close>
  obtains s where \<open>x \<in> \<E>\<close> \<open>s \<in> \<S>\<close> \<open>((\<triangleleft>)^^n) x s\<close>
  using assms by (auto simp: order_of_def)

lemma has_ultimate_bearer_problem_I1:
  assumes \<open>x \<in> \<M>\<close> \<open>\<forall>y. \<not> ultimate_bearer_of y x\<close>
  shows \<open>has_ultimate_bearer_problem\<close>
  using assms apply (simp add: has_ultimate_bearer_problem_def)
  by (intro bexI[of _ x] ; simp)

lemma has_ultimate_bearer_problem_E[elim!]:
  assumes \<open>has_ultimate_bearer_problem\<close>
  obtains x where \<open>x \<in> \<M>\<close> \<open>\<forall>y. \<not> ultimate_bearer_of y x\<close>
  using assms apply (simp add: has_ultimate_bearer_problem_def Bex_def)
  by metis

lemma has_order_problem_I1:
  assumes \<open>x \<in> \<M>\<close> \<open>\<forall>n. \<not> order_of x n\<close>
  shows \<open>has_order_problem\<close>
  using assms apply (simp add: has_order_problem_def)
  by (intro bexI[of _ x] ; simp)

lemma has_order_problem_E[elim!]:
  assumes \<open>has_order_problem\<close>
  obtains x where \<open>x \<in> \<M>\<close> \<open>\<forall>n. \<not> order_of x n\<close>
  using assms apply (simp add: has_order_problem_def Bex_def)
  by metis

end

context inherence_base
begin

lemma \<M>_are_\<E>[dest]: \<open>x \<in> \<M> \<Longrightarrow> x \<in> \<E>\<close>
  using inherence_scope
  by (auto simp: \<M>_def)

lemma ultimate_bearer_of_I[intro!]:
  assumes \<open>s \<in> \<S>\<close> \<open>(\<triangleleft>)\<^sup>*\<^sup>* m s\<close>
  shows \<open>ultimate_bearer_of s m\<close>
proof -
  have s_E[simp]: \<open>s \<in> \<E>\<close> using \<open>s \<in> \<S>\<close> by blast
  have m_E[simp]: \<open>m \<in> \<E>\<close>
  proof (cases \<open>m = s\<close>)
    case True
    then show ?thesis using \<open>s \<in> \<E>\<close> by simp
  next
    case False
    then have \<open>(\<triangleleft>)\<^sup>+\<^sup>+ m s\<close>
      using assms by (meson rtranclpD)
    then show ?thesis
      using inherence_scope
      by (meson tranclpD)
  qed
  show ?thesis
    using assms by (intro ultimate_bearer_of_I1 ; simp)
qed

lemma order_of_I[intro]:
  assumes \<open>s \<in> \<S>\<close> \<open>((\<triangleleft>)^^n) x s\<close>
  shows \<open>order_of x n\<close>
proof -
  have s_E[simp]: \<open>s \<in> \<E>\<close> using \<open>s \<in> \<S>\<close> by blast
  have m_E[simp]: \<open>x \<in> \<E>\<close>
  proof (cases \<open>x = s\<close>)
    case True
    then show ?thesis using \<open>s \<in> \<E>\<close> by simp
  next
    case False
    then have \<open>(\<triangleleft>)\<^sup>+\<^sup>+ x s\<close>
      using assms
      by (meson relpowp_imp_rtranclp rtranclpD)
    then show ?thesis
      using inherence_scope
      by (meson tranclpD)
  qed
  show ?thesis
    by (intro order_of_I1[of _ s] assms ; simp)
qed

lemma has_ultimate_bearer_problem_I[intro]:
  assumes \<open>x \<in> \<E>\<close> \<open>\<forall>y. \<not> ultimate_bearer_of y x\<close>
  shows \<open>has_ultimate_bearer_problem\<close>
proof -
  have \<open>x \<notin> \<S>\<close> using assms(2) ultimate_bearer_of_I by auto
  then have \<open>x \<in> \<M>\<close> using assms(1) by blast
  then show ?thesis
    using assms has_ultimate_bearer_problem_I1 by metis
qed

lemma has_order_problem_I[intro]:
  assumes \<open>x \<in> \<E>\<close> \<open>\<forall>n. \<not> order_of x n\<close>
  shows \<open>has_order_problem\<close>
proof -
  have \<open>x \<notin> \<S>\<close> using assms(2) order_of_I[of x 0] by auto
  then have \<open>x \<in> \<M>\<close> using assms(1) by blast
  then show ?thesis
    using assms has_order_problem_I1 by metis
qed

end

sublocale inherence_simplified \<subseteq> inh: single_valued_range_relation \<open>(\<triangleleft>)\<close>
  apply (unfold_locales)
  using moment_non_migration by metis

context inherence_simplified
begin

lemma ultimate_bearer_iff_ub: \<open>ultimate_bearer_of s m \<longleftrightarrow> m \<in> \<E> \<and> inh.is_upper_bound_of s m\<close>
  apply (auto)
  by (metis \<E>_I inherence_scope rtranclp.cases)

lemma ub_iff_ultimate_bearer:
        \<open>inh.is_upper_bound_of s m \<longleftrightarrow>
         ultimate_bearer_of s m \<or> (m \<notin> \<E> \<and> s = m)\<close>
  apply (auto)
  subgoal for w by (metis \<E>_I inherence_scope rtranclp.cases)
  subgoal by (metis inherence_scope rtranclp.cases)
  by (metis inherence_scope)

lemma order_of_iff_upper_order_of:
  \<open>order_of x n \<longleftrightarrow> x \<in> \<E> \<and> inh.is_upper_order_of n x\<close>
  apply (auto ; (elim order_of_E inh.is_upper_order_of_E)?)
  subgoal using order_of_I by auto
  by (metis \<E>_I inherence_scope inherence_sig.\<S>_I
            order_of_I relpowp_imp_rtranclp rtranclp.cases)

lemma upper_order_of_iff_order_of:
  \<open>inh.is_upper_order_of n x \<longleftrightarrow> order_of x n \<or> (x \<notin> \<E> \<and> n = 0)\<close>
  apply (auto)
  subgoal by (simp add: \<E>_I order_of_iff_upper_order_of)
  subgoal by (metis inh.is_upper_order_of_def inherence_scope
                    order_of_iff_upper_order_of relpowp_E2)
  subgoal by (simp add: order_of_iff_upper_order_of)
  using inh.is_upper_order_of_def inherence_scope by auto

lemma ultimate_bearer_order_ex_iff:
  \<open>(\<exists>y. ultimate_bearer_of y x) \<longleftrightarrow> (\<exists>n. order_of x n)\<close>
proof (intro iffI ; elim exE ultimate_bearer_of_E order_of_E)
  show \<open>\<exists>n. order_of x n\<close> if as: \<open>y \<in> \<S>\<close> \<open>x \<in> \<E>\<close> \<open>(\<triangleleft>)\<^sup>*\<^sup>* x y\<close> for x y
    by (meson order_of_I1 rtranclp_imp_relpowp that)
  show \<open>\<exists>y. ultimate_bearer_of y x\<close> if as: \<open>x \<in> \<E>\<close> \<open>s \<in> \<S>\<close> \<open>((\<triangleleft>) ^^ n) x s\<close> for n s
    by (meson relpowp_imp_rtranclp that(2) that(3) ultimate_bearer_of_I)
qed

lemma all_if_not_ex: \<open>(\<forall>x. \<not> P x) \<longleftrightarrow> \<not>(\<exists>x. P x)\<close>  by blast

lemma ultimate_bearer_prob_imp_order_prob:
  \<open>has_ultimate_bearer_problem \<longleftrightarrow> has_order_problem\<close>
  by (simp add: has_ultimate_bearer_problem_def has_order_problem_def ;
         simp only: all_if_not_ex ultimate_bearer_order_ex_iff)

lemma \<open>x \<in> \<M> \<Longrightarrow> \<exists>y. ultimate_bearer_of y x\<close>
  nitpick[expect=genuine]
  oops

end

definition
  \<open>inherence_simplified_model \<Gamma> =
    inherence_simplified (im_\<W> \<Gamma>) (im_inheresIn \<Gamma>) \<close>

context
begin

definition \<open>prob_model_1 \<equiv> \<lparr>
    im_\<W> = { \<emptyset>, {0,1,2} },
    im_inheresIn = (\<lambda>x y. x < 3 \<and> y < 3 \<and> (y = Suc x \<or> x = 2 \<and> y = 0))
  \<rparr>\<close>

abbreviation pm1_worlds (\<open>\<W>\<close>) where \<open>\<W> \<equiv> im_\<W> prob_model_1\<close>

abbreviation inheresIn (infix \<open>\<triangleleft>\<close> 75)
  where \<open>(\<triangleleft>) \<equiv> im_inheresIn prob_model_1\<close>

interpretation  inherence_sig \<open>\<W>\<close> \<open>(\<triangleleft>)\<close> .

lemma prob_model_is_inherence_simplified_model:
  \<open>inherence_simplified_model prob_model_1\<close>
  apply (simp only: inherence_simplified_model_def)
  apply (unfold_locales ; (simp add: ed_def)? ; (simp add: existsIn_def \<E>_def)?
                        ; (simp add: prob_model_1_def)?)
  subgoal for x y
    by (cases x ; cases y ; simp)
  subgoal for x y z
    by (cases x ; cases y ; cases z ; simp)
  subgoal for x y
    by (cases x ; cases y ; simp)
  done

interpretation inherence_simplified \<W> \<open>(\<triangleleft>)\<close>
  using prob_model_is_inherence_simplified_model
  by (simp add: inherence_simplified_model_def)

lemma prob_model_1_has_ultimate_bearer_problem:
  \<open>has_ultimate_bearer_problem\<close>
proof -
  have \<open>\<S> = \<emptyset>\<close>
  proof (rule ccontr)
    assume \<open>\<S> \<noteq> \<emptyset>\<close>
    then obtain x where \<open>x \<in> \<S>\<close> by blast
    then obtain A: \<open>x \<in> \<E>\<close> \<open>\<And>y. \<not> x \<triangleleft> y\<close> by blast
    then show False
      apply (cases x ; simp add: \<S>_def \<M>_def \<E>_def
              ; simp add: prob_model_1_def possible_worlds_alt_sig.\<E>_def)
      subgoal by (elim disjE ; simp ; presburger)
      by presburger
  qed
  show ?thesis
  proof (intro has_ultimate_bearer_problem_I[of 0])
    show \<open>0 \<in> \<E>\<close> by (simp only: \<E>_def ; simp add: prob_model_1_def)
    show \<open>\<forall>y. \<not> ultimate_bearer_of y 0\<close>
    proof (intro allI notI)
      fix y
      assume \<open>ultimate_bearer_of y 0\<close>
      then obtain \<open>y \<in> \<S>\<close> by blast
      then show False using \<open>\<S> = \<emptyset>\<close> by auto
    qed
  qed
qed

no_notation pm1_worlds (\<open>\<W>\<close>)

no_notation inheresIn (infix \<open>\<triangleleft>\<close> 75)

end

text_raw \<open>\Copy{locale:inherence-with-ultimate-bearers}{%\<close>
locale inherence_with_ultimate_bearers =
  inherence_simplified +
assumes
  ultimate_bearers_ex:
  \<open>x \<in> \<M> \<Longrightarrow> \<exists>y. ultimate_bearer_of y x\<close>
text_raw \<open>}\<close>

lemma (in inherence_with_ultimate_bearers)
    \<open>\<not> has_ultimate_bearer_problem\<close>
  using has_ultimate_bearer_problem_E ultimate_bearers_ex by metis

text_raw \<open>\Copy{locale:inherence-acyclic}{%\<close>
locale inherence_acyclic =
  inherence_simplified +
 assumes
  acyclic_inherence: \<open>\<not> ((\<triangleleft>)\<^sup>+\<^sup>+) x x\<close>
text_raw \<open>}\<close>

sublocale inherence_with_ultimate_bearers \<subseteq>
  inh: single_valued_range_upper_bounded_relation \<open>(\<triangleleft>)\<close>
  apply (unfold_locales)
proof -
  fix x
  show \<open>\<exists>y. inh.is_upper_bound_of y x\<close> (is \<open>\<exists>x. ?P x\<close>)
  proof (cases \<open>x \<in> \<M>\<close>)
    assume \<open>x \<notin> \<M>\<close>
    then have \<open>\<not> x \<triangleleft> y\<close> for y by auto
    then show \<open>\<exists>x. ?P x\<close> by blast
  next
    assume \<open>x \<in> \<M>\<close>
    then obtain y where \<open>ultimate_bearer_of y x\<close>
      using ultimate_bearers_ex by metis
    then show \<open>\<exists>x. ?P x\<close>
      by blast
  qed
qed

sublocale inherence_with_ultimate_bearers \<subseteq> inherence_acyclic
  apply (unfold_locales)
  by (simp add: inh.acyclic)

lemma prob_model_1_not_acyclic:
  \<open>\<not> inherence_acyclic (im_\<W> prob_model_1) (im_inheresIn prob_model_1)\<close>
proof -
  have A: \<open>im_inheresIn prob_model_1 0 1\<close>
          \<open>im_inheresIn prob_model_1 1 2\<close>
          \<open>im_inheresIn prob_model_1 2 0\<close>
    by (simp_all add: prob_model_1_def)
  then have B: \<open>(im_inheresIn prob_model_1)\<^sup>+\<^sup>+ 0 0\<close>
    by auto
  show ?thesis
  proof
    assume \<open>inherence_acyclic (im_\<W> prob_model_1)
                         (im_inheresIn prob_model_1)\<close>
    then interpret inherence_acyclic
          \<open>im_\<W> prob_model_1\<close> \<open>im_inheresIn prob_model_1\<close> by simp
    show False
      using B acyclic_inherence by metis
  qed
qed

context
begin

definition \<open>
  prob_model_2 \<equiv> \<lparr>
    im_\<W> = { \<emptyset>, UNIV :: nat set},
    im_inheresIn = (\<lambda>x y. y = Suc x)
    \<rparr>\<close>

private abbreviation pm2_worlds (\<open>\<W>\<close>) where \<open>\<W> \<equiv> im_\<W> prob_model_2\<close>

private abbreviation pm2_inheresIn (infix \<open>\<triangleleft>\<close> 75)
  where \<open>(\<triangleleft>) \<equiv> im_inheresIn prob_model_2\<close>

interpretation inherence_sig \<W> \<open>(\<triangleleft>)\<close> .

interpretation possible_worlds_alt \<W>
    by (unfold_locales ; simp add: prob_model_2_def)

interpretation inherence_original
    \<open>\<W>\<close> \<open>(\<triangleleft>)\<close>
  by (unfold_locales ; (simp add: ed_def existsIn_def)?
           ; (simp add: \<E>_def)? ; (simp add: prob_model_2_def))

lemma prob_model_2_is_inherence_acyclic[simp]:
  \<open>inherence_acyclic \<W> (\<triangleleft>)\<close>
proof -
  show ?thesis
    apply (unfold_locales ; auto simp: prob_model_2_def)
    using less_nat_rel by force
qed

interpretation inherence_acyclic \<W> \<open>(\<triangleleft>)\<close> by simp

lemma prob_model_2_has_ultimate_bearer_problem:
    \<open>has_ultimate_bearer_problem\<close>
proof (intro has_ultimate_bearer_problem_I[of 0] allI)
  show \<open>0 \<in> \<E>\<close>
    by (simp only: \<E>_def ; simp add: prob_model_2_def)
  show \<open>\<not> ultimate_bearer_of y 0\<close> for y
  proof
    assume \<open>ultimate_bearer_of y 0\<close>
    then obtain \<open>y \<in> \<S>\<close> \<open>0 \<in> \<E>\<close> \<open>((\<triangleleft>))\<^sup>*\<^sup>* 0 y\<close>
      using ultimate_bearer_of_def[of y 0] by metis
    have \<open>y \<triangleleft> Suc y\<close>
      by (simp add: prob_model_2_def)
    then have \<open>y \<in> \<M>\<close> by blast
    then show False using \<open>y \<in> \<S>\<close> by blast
  qed
qed

no_notation pm2_worlds (\<open>\<W>\<close>)

no_notation pm2_inheresIn (infix \<open>\<triangleleft>\<close> 75)

end

text_raw \<open>\Copy{locale:inherence-no-infinite-chains}{\<close>
locale inherence_no_infinite_chains =
  inherence_acyclic +
assumes
  no_infinite_up_chains:
    \<open>\<lbrakk> x \<in> X ; \<forall>y \<in> X. (\<triangleleft>)\<^sup>*\<^sup>* x y ;
      \<forall>x \<in> X. \<forall>y \<in> X. (\<triangleleft>)\<^sup>*\<^sup>* x y \<or> (\<triangleleft>)\<^sup>*\<^sup>* y x \<rbrakk> \<Longrightarrow> finite X\<close>
text_raw \<open>}\<close>

sublocale inherence_no_infinite_chains \<subseteq>
  inh: single_valued_range_acyclic_finite_lb_chains_relation \<open>(\<triangleleft>)\<close>
proof -
  have fin_lb_chain: \<open>finite X\<close> if \<open>lb_chain (\<triangleleft>) X\<close> for X
  proof -
    interpret P: lb_chain \<open>(\<triangleleft>)\<close> X using that .
    obtain x where x: \<open>x \<in> X\<close> \<open>\<And>y. y \<in> X \<Longrightarrow> (\<triangleleft>)\<^sup>*\<^sup>* x y\<close>
      using P.lb_exists by blast
    have R1: \<open>\<forall>y \<in> X.(\<triangleleft>)\<^sup>*\<^sup>* x y\<close> using x by auto
    have R2: \<open>\<forall>x \<in> X. \<forall>y \<in> X. (\<triangleleft>)\<^sup>*\<^sup>* x y \<or> (\<triangleleft>)\<^sup>*\<^sup>* y x\<close>
      using P.R_connected by blast
    show \<open>finite X\<close> using no_infinite_up_chains R1 R2 \<open>x \<in> X\<close> by metis
  qed

  show \<open>single_valued_range_acyclic_finite_lb_chains_relation (\<triangleleft>)\<close>
    by (unfold_locales ; simp add: moment_non_migration acyclic_inherence fin_lb_chain)
qed

theorem inherence_acyclic_no_infinite_chains_eq_no_ultimate_bearers:
 \<open>inherence_no_infinite_chains = inherence_with_ultimate_bearers\<close>
proof (intro ext iffI)
  fix \<W> :: \<open>'e set set\<close> and inheresIn (infix \<open>\<triangleleft>\<close> 75)
  assume \<open>inherence_no_infinite_chains \<W> (\<triangleleft>)\<close>
  then interpret inherence_no_infinite_chains \<W> \<open>(\<triangleleft>)\<close> .
  interpret inh: single_valued_range_upper_bounded_relation \<open>(\<triangleleft>)\<close>
    apply (simp only: single_valued_range_acyclic_finite_lb_chains_relation_ub[symmetric])
    by (intro_locales)
  show \<open>inherence_with_ultimate_bearers \<W> (\<triangleleft>)\<close>
  proof (unfold_locales)
    fix x
    assume \<open>x \<in> \<M>\<close>
    then obtain y where \<open>(\<triangleleft>)\<^sup>*\<^sup>* x y\<close> \<open>\<And>z. \<not> y \<triangleleft> z\<close>
      using inh.upper_bounded inh.is_upper_bound_of_E by metis
    then have \<open>y \<in> \<E>\<close> using \<open>x \<in> \<M>\<close>
      by (metis local.\<M>_E local.inherence_scope rtranclp.cases)
    then have \<open>y \<in> \<S>\<close> using \<S>_I \<open>\<And>z. \<not> y \<triangleleft> z\<close> by blast
    have \<open>x \<in> \<E>\<close> using  \<open>x \<in> \<M>\<close> \<M>_E inherence_scope by metis
    have \<open>ultimate_bearer_of y x\<close>
      by (intro ultimate_bearer_of_I \<open>x \<in> \<E>\<close> \<open>(\<triangleleft>)\<^sup>*\<^sup>* x y\<close> \<open>y \<in> \<S>\<close>)
    then show \<open>\<exists>y. local.ultimate_bearer_of y x\<close> by metis
  qed
next
  fix \<W> :: \<open>'e set set\<close> and inheresIn (infix \<open>\<triangleleft>\<close> 75)
  assume \<open>inherence_with_ultimate_bearers \<W> (\<triangleleft>)\<close>
  then interpret inherence_with_ultimate_bearers \<W> \<open>(\<triangleleft>)\<close> .
  interpret inh: single_valued_range_upper_bounded_relation \<open>(\<triangleleft>)\<close>
    by unfold_locales
  interpret inh: single_valued_range_acyclic_finite_lb_chains_relation \<open>(\<triangleleft>)\<close>
    apply (simp only: single_valued_range_acyclic_finite_lb_chains_relation_ub)
    by intro_locales
  show \<open>inherence_no_infinite_chains \<W> (\<triangleleft>)\<close>
  proof (unfold_locales)
    show \<open>finite X\<close>
        if as: \<open>x \<in> X\<close> \<open>\<forall>y\<in>X. (\<triangleleft>)\<^sup>*\<^sup>* x y\<close>
               \<open>\<forall>x\<in>X. \<forall>y\<in>X. (\<triangleleft>)\<^sup>*\<^sup>* x y \<or> (\<triangleleft>)\<^sup>*\<^sup>* y x\<close>
             for x X
      apply (intro inh.finite_lb_chains ; unfold_locales)
      using as by auto
  qed
qed

text_raw \<open>\Copy{locale:inherence-noetherian}{\<close>
locale inherence_noetherian =
  inherence_base  +
    assumes
    inherence_is_noetherian: \<open>wfP ((\<triangleleft>)\<inverse>\<inverse>)\<close>
text_raw \<open>}\<close>

context inherence_base
begin
text_raw \<open>\Copy{def:wfP-eq-minimal-bearer-of}{%\<close> text \<open>@{thm wfP_eq_minimal[of \<open>(\<triangleleft>)\<inverse>\<inverse>\<close>,simplified]}\<close> text_raw \<open>}\<close>
end

sublocale inherence_noetherian \<subseteq>
   inh: single_valued_range_noetherian_relation \<open>(\<triangleleft>)\<close>
  using moment_non_migration inherence_is_noetherian
    by (unfold_locales ; metis)

theorem noethereian_inherence_eq_inherence_with_ultimate_bearers:
  \<open>inherence_noetherian = inherence_with_ultimate_bearers\<close>
proof (intro ext iffI)
  fix \<W> :: \<open>'e set set\<close> and inheresIn (infix \<open>\<triangleleft>\<close> 75)
  assume \<open>inherence_noetherian \<W> (\<triangleleft>)\<close>
  then interpret inherence_noetherian \<W> \<open>(\<triangleleft>)\<close> .
  interpret inh: single_valued_range_noetherian_relation \<open>(\<triangleleft>)\<close>
    by intro_locales
  interpret inh: single_valued_range_upper_bounded_relation \<open>(\<triangleleft>)\<close>
    using single_valued_range_ub_eq_noetherian
    by auto
  show \<open>inherence_with_ultimate_bearers \<W> (\<triangleleft>)\<close>
  proof (unfold_locales)
    show asymm: \<open>\<not> y \<triangleleft> x\<close> if \<open>x \<triangleleft> y\<close> for x y
      by (meson inh.acyclic r_into_rtranclp rtranclp_into_tranclp1 that)
    show \<open>\<exists>y. ultimate_bearer_of y x\<close> if \<open>x \<in> \<M>\<close> for x
      by (metis \<M>_are_\<E> \<open>\<And>y x. x \<triangleleft> y \<Longrightarrow> \<not> y \<triangleleft> x\<close>
          inh.all_unique_upper_order inherence_base_axioms
          inherence_simplified.order_of_iff_upper_order_of
          inherence_simplified.ultimate_bearer_order_ex_iff
          inherence_simplified_axioms.intro inherence_simplified_def
          that)
  qed
next
  fix \<W> :: \<open>'e set set\<close> and inheresIn (infix \<open>\<triangleleft>\<close> 75)
  assume \<open>inherence_with_ultimate_bearers \<W> (\<triangleleft>)\<close>
  then interpret inherence_with_ultimate_bearers \<W> \<open>(\<triangleleft>)\<close> .
  interpret inh: single_valued_range_upper_bounded_relation \<open>(\<triangleleft>)\<close>
    by (unfold_locales)
  show \<open>inherence_noetherian \<W> (\<triangleleft>)\<close>
    apply (unfold_locales)
    by (simp add: inh.noetherian)
qed

context inherence_noetherian
begin

text_raw \<open>\Copy{lemma:noetherian-induct}{\<close>
text \<open>@{thm inherence_is_noetherian[THEN wfP_induct,of P z,simplified]}\<close>
text_raw \<open>}\<close>
end

end

author: joaoraf


text:
theory Sum
imports Main Complex_Main
begin

primrec sum :: "nat list => nat" where
"sum [] = 0"|
"sum (x#l) = x + sum l"

primrec sum_till :: "nat \<Rightarrow> nat" where
 "sum_till 0 = 0"|
 "sum_till (Suc k) = sum_till (k) + Suc(k)"

lemma sum_2_list [simp]: "sum (l1 @ l2) = sum l1 + sum l2"
  apply(induct l1)
  apply(auto)
  done

theorem sum_rev_list: "sum (rev l) = sum l"
  apply (induct l)
  apply (auto simp: sum_2_list)
  done

theorem sum_formula: "sum_till n = n*(n+1) div 2"
  apply (induct n)
  apply (auto)
  done

theorem sum_n: "(\<Sum>i::nat=0..n. i) = n*(n+1::nat) div 2" (is "?P n")
proof(induct n)
  case 0
  show ?case by simp
  case Suc
  fix n assume "?P n"
  thus "?P(Suc n)" by simp
qed

theorem sum_of_squares:
  "(\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1) div 6"
(is "?P n")
proof (induct n)
  case 0
  show ?case by simp
  case Suc
  fix n assume "?P n"
  thus "?P(Suc n)" by (simp add: add_mult_distrib add_mult_distrib2)
qed

theorem sum_of_naturals:
  "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
  (is "?P n" is "?S n = _")
proof (induct n)
  show "?P 0" by simp
next
  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)"
    by simp
  assume "?P n"
  also have "\<dots> + 2 * (n + 1) = (n + 1) * (n + 2)"
    by simp
  finally show "?P (Suc n)"
    by simp
qed

end

repo: Isabelle-Simulink


text:
theory hw3_sol
imports Main
begin

lemma p4: "(\<forall> x. \<forall> y. P(x) \<longrightarrow> Q(y)) \<longrightarrow> ((\<exists> x. P(x)) \<longrightarrow>  (\<forall> y. Q(y)))"
  apply (rule impI)
  apply (rule impI)
  apply (rule allI)
  apply (erule exE)
  apply (erule_tac x = "x" in allE)
  apply (erule_tac x = "y" in allE)
  by (erule impE)

lemma p5: "(\<forall> x. \<forall> y. P(x) \<and> P(y)) \<longrightarrow> ((\<forall> x. P(x)) \<and>  (\<forall> y. P(y)))"
  apply (rule impI)
  apply (rule conjI)
  apply (rule allI)
  apply (erule_tac x = "x" in allE)
  apply (erule allE)
  apply (erule conjE)
  apply assumption
  apply (rule allI)
  apply (erule_tac x = "y" in allE)
  apply (erule allE)
  by (erule conjE)

end

author: YunyiZheng

repo: mpref

save_path: github-repos/isabelle/YunyiZheng-mpref