text:
header {* The Second Monotonicity Calculus *}
theory Mcalc2
imports Mono
begin

subsection{* Extension policies *}

text{* Extension policy: copy, true or false extension: *}

datatype epol = Cext | Text | Fext

text{* Problem with infinite knowledge and predicate-extension policy: *}

locale ProblemIkPol = ProblemIk wtFsym wtPsym arOf resOf parOf \<Phi> infTp
for wtFsym :: "'fsym \<Rightarrow> bool" and wtPsym :: "'psym \<Rightarrow> bool"
and arOf :: "'fsym \<Rightarrow> 'tp list"
and resOf and parOf and \<Phi> and infTp
+ fixes (* the predicate-extension policy *) pol :: "'tp \<Rightarrow> 'psym \<Rightarrow> epol"
and (* guard of a variable occurring in a certain literal of a certain clause: *)
    grdOf ::
"('fsym, 'psym) cls \<Rightarrow> ('fsym, 'psym) lit \<Rightarrow> var \<Rightarrow> ('fsym, 'psym) lit"

context ProblemIkPol begin

subsection{* Naked variables *}

fun nv2T where
"nv2T (Var x) = {x}"
|
"nv2T (Fn f Tl) = {}"

fun nv2L where
"nv2L (Pos (Eq T1 T2)) = nv2T T1 \<union> nv2T T2"
|
"nv2L (Neg (Eq T1 T2)) = {}"
|
"nv2L (Pos (Pr p Tl)) = {x \<in> \<Union> set (map nv2T Tl) . pol (tpOfV x) p = Fext}"
|
"nv2L (Neg (Pr p Tl)) = {x \<in> \<Union> set (map nv2T Tl) . pol (tpOfV x) p = Text}"

definition "nv2C c \<equiv> \<Union> set (map nv2L c)"

lemma in_nv2T: "x \<in> nv2T T \<longleftrightarrow> T = Var x"
apply(cases T)
  apply (metis equals0D nv2T.simps singleton_iff)
  by simp

lemma nv2T_vars[simp]: "x \<in> nv2T T \<Longrightarrow> x \<in> vars T"
by (induct T, auto split: if_splits)

lemma nv2L_varsL[simp]:
assumes "x \<in> nv2L l" shows "x \<in> varsL l"
proof (cases l)
  case (Pos at)
  show ?thesis proof(cases at)
    case (Pr p Tl) thus ?thesis using assms unfolding Pos
    apply(cases "pol (tpOfV x) p", simp_all) by (metis nv2T_vars)
  qed(insert assms, unfold Pos, auto)
next
  case (Neg at)
  show ?thesis proof(cases at)
    case (Pr p Tl) thus ?thesis using assms unfolding Neg
    apply(cases "pol (tpOfV x) p", simp_all) by (metis nv2T_vars)
  qed(insert assms, unfold Neg, auto)
qed

lemma nv2C_varsC[simp]: "x \<in> nv2C c \<Longrightarrow> x \<in> varsC c"
unfolding varsC_def nv2C_def by (induct c, auto)

subsection{* The calculus *}

text{* The notion of a literal being a guard for a (typed) variable: *}

fun isGuard :: "var \<Rightarrow> ('fsym,'psym) lit \<Rightarrow> bool" where
"isGuard x (Pos (Eq T1 T2)) \<longleftrightarrow> False"
|
"isGuard x (Neg (Eq T1 T2)) \<longleftrightarrow>
 (T1 = Var x \<and> (\<exists> f Tl. T2 = Fn f Tl)) \<or>
 (T2 = Var x \<and> (\<exists> f Tl. T1 = Fn f Tl))"
|
"isGuard x (Pos (Pr p Tl)) \<longleftrightarrow> x \<in> \<Union> set (map nv2T Tl) \<and> pol (tpOfV x) p = Text"
|
"isGuard x (Neg (Pr p Tl)) \<longleftrightarrow> x \<in> \<Union> set (map nv2T Tl) \<and> pol (tpOfV x) p = Fext"

text{* The monotonicity calculus from the Classen et. al. paper, applied
to non-infinite types only: it checks that any variable in any literal of any clause
is indeed guarded by its guard: *}

inductive mcalc2 (infix "\<turnstile>2" 40) where
 [simp]: "infTp \<sigma> \<Longrightarrow> \<sigma> \<turnstile>2 c"
|[simp]: "(\<And> l x. \<lbrakk>l \<in> set c; x \<in> nv2L l; tpOfV x = \<sigma>\<rbrakk>
         \<Longrightarrow> isGuard x (grdOf c l x)) \<Longrightarrow> \<sigma> \<turnstile>2 c"

lemma mcalc2_iff:
"\<sigma> \<turnstile>2 c \<longleftrightarrow>
 infTp \<sigma> \<or> (\<forall> l x. l \<in> set c \<and> x \<in> nv2L l \<and> tpOfV x = \<sigma> \<longrightarrow> isGuard x (grdOf c l x))"
unfolding mcalc2.simps by auto

end (* context ProblemIk *)

locale ProblemIkPolMcalc2 = ProblemIkPol wtFsym wtPsym arOf resOf parOf \<Phi> infTp pol grdOf
for wtFsym :: "'fsym \<Rightarrow> bool" and wtPsym :: "'psym \<Rightarrow> bool"
and arOf :: "'fsym \<Rightarrow> 'tp list"
and resOf and parOf and \<Phi> and infTp and pol and grdOf
+ assumes
(* well-definednedd of the guard: *)
    grdOf: "\<And> c l x. \<lbrakk>c \<in> \<Phi>; l \<in> set c; x \<in> nv2L l; \<not> infTp (tpOfV x)\<rbrakk>
                     \<Longrightarrow> grdOf c l x \<in> set c"
and mcalc2: "\<And> \<sigma> c. c \<in> \<Phi> \<Longrightarrow> \<sigma> \<turnstile>2 c"
begin
lemma wtL_grdOf[simp]:
assumes "c \<in> \<Phi>" and "l \<in> set c" and "x \<in> nv2L l" and "\<not> infTp (tpOfV x)"
shows "wtL (grdOf c l x)"
using grdOf[OF assms] by (metis assms list_all_iff wtC_def wtPB_def wt_\<Phi>)
end

locale ModelIkPolMcalc2 =
ModelIk wtFsym wtPsym arOf resOf parOf \<Phi> infTp intT intF intP +
ProblemIkPolMcalc2 wtFsym wtPsym arOf resOf parOf \<Phi> infTp pol grdOf
for wtFsym :: "'fsym \<Rightarrow> bool" and wtPsym :: "'psym \<Rightarrow> bool"
and arOf :: "'fsym \<Rightarrow> 'tp list"
and resOf and parOf and \<Phi> and infTp pol and grdOf and intT and intF and intP

end

author: Josh-Tilles

repo: AFP

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


text:
section \<open>Prelude\<close>

theory Prelude
imports HOLCF
begin

default_sort type

(* allows to use lift_definition for continuous functions *)
setup_lifting type_definition_cfun

text \<open>SMT-Proofs are not allowed in the AFP, so don't generate them\<close>
sledgehammer_params [smt_proofs=false]

text \<open>Helpful lemmas to work with HOL and HOLCF's definitions.\<close>

lemma trivial[simp]: "(Not \<circ> Not) = id"
  by auto

text \<open>Convert a relation to a map (function with \<open>option\<close>al result).\<close>
definition rel2map ::   "('c * 'm) set \<Rightarrow> ('c \<rightharpoonup> 'm)"
where rel2map_def: "rel2map r \<equiv> \<lambda>x. (if x \<in> Domain r then Some (SOME a. (x,a) \<in> r) else None)"

text \<open>Domain of rel2map.\<close>

text \<open>Unwrapping an \<open>'a option\<close> value. Result for \<open>None\<close> is undefined.\<close>
definition unsome :: "'a option \<Rightarrow> 'a" where
"unsome x = (case x of Some y \<Rightarrow> y | None \<Rightarrow> undefined)"

text \<open>Unsome is the inverse of Some.\<close>
lemma [simp]: "unsome (Some x) = x"
by (simp add: unsome_def)

text \<open>For natural numbers j and k with @{term "j \<le> k"}, @{term "k - j"} is natural as well\<close>
lemma natl1: "(j::nat) \<le> k \<Longrightarrow> \<exists>i. j + i = k"
apply (simp add: atomize_imp)
apply (rule_tac x="j" in spec)
apply (induct_tac k, auto)
by (case_tac "x", auto)

text \<open>Commutation on natural numbers\<close>
lemma natl2: "(i::nat) + k = k + i"
by auto

text \<open>Removing successive duplicates from a list:\<close>
primrec lrcdups :: "'a list \<Rightarrow> 'a list"
where
  "lrcdups [] = []" |
  "lrcdups (x#xs) =
     (if xs = []
        then [x]
        else
          (if x = List.hd xs
             then lrcdups xs
             else (x#(lrcdups xs))))"

(* ----------------------------------------------------------------------- *)
section \<open>Some auxiliary HOLCF lemmas\<close>
(* ----------------------------------------------------------------------- *)

subsection \<open>cfun\<close>

text \<open>Introduction of continuity of \<open>f\<close> using monotonicity and lub on chains:\<close>
lemma contI2:
  "\<lbrakk>monofun (f::'a::cpo \<Rightarrow> 'b::cpo);
        (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i)))\<rbrakk> \<Longrightarrow> cont f"
apply (rule contI)
apply (rule is_lubI)
apply (rule ub_rangeI)
apply (rule monofunE [of f], assumption)
apply (rule is_ub_thelub, assumption)
apply (erule_tac x="Y" in allE, drule mp, assumption)
apply (rule_tac y="\<Squnion>i. f (Y i)" in below_trans, assumption)
apply (rule is_lub_thelub)
by (rule ch2ch_monofun [of f], assumption+)

text \<open>The higher-order function, which takes as input f and yields the result of
the application of on x, is a continous function.\<close>
lemma [simp]: "cont (\<lambda> f. f x)"
apply (rule contI)
apply (subst lub_fun, assumption)
apply (rule thelubE)
apply (rule ch2ch_fun, assumption)
by (rule refl)

text \<open>In a chain, every two elements are comparable\<close>
lemma chain_tord: "chain S \<Longrightarrow> S k \<sqsubseteq> S j \<or> S j \<sqsubseteq> S k"
apply (insert linear [of "j" "k"])
apply (erule disjE)
apply (rule disjI2)
apply (rule chain_mono,simp+)
apply (rule disjI1)
by (rule chain_mono,simp+)

text \<open>Every non-empty set contains an element\<close>
lemma neq_emptyD: "s \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> s"
by auto

(* below lemmata *)
lemma cont_pref_eq1I: assumes "(a \<sqsubseteq> b)"
  shows "f\<cdot>a \<sqsubseteq> f\<cdot>b"
  by (simp add: assms monofun_cfun_arg)

lemma cont_pref_eq2I:  assumes "(a \<sqsubseteq> b)"
  shows "f\<cdot>x\<cdot>a \<sqsubseteq> f\<cdot>x\<cdot>b"
  by (simp add: assms monofun_cfun_arg)

(* equality lemmata *)
lemma cfun_arg_eqI:  assumes "(a = b)"
  shows "f\<cdot>a = f\<cdot>b"
  by (simp add: assms)

(* ----------------------------------------------------------------------- *)
section \<open>More functions\<close>
(* ----------------------------------------------------------------------- *)

text \<open>This section introduces some more functions to work with lists.\<close>

text \<open>Range shifting on least upper bound of chains.\<close>
lemma less_lubl1:
  "\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); X \<sqsubseteq> (\<Squnion>k. Y (k + j))\<rbrakk> \<Longrightarrow> X \<sqsubseteq> (\<Squnion>k. Y k)"
by (subst lub_range_shift [THEN sym, of "Y" "j"], simp+)

text \<open>Another lemma on range shifting on least upper bound of chains.\<close>
lemma less_lubl2:
"\<lbrakk>chain (Y::nat \<Rightarrow> 'a::cpo); chain f; \<And>x. (\<Squnion>k. f k\<cdot>x) = x; \<And>n. f n\<cdot>x \<sqsubseteq> (f n\<cdot>(Lub Y))\<rbrakk> \<Longrightarrow> x \<sqsubseteq> Lub Y"
by (insert lub_mono [of "\<lambda>n. f n\<cdot>x" "\<lambda>n. f n\<cdot>(Lub Y)"], simp)

text \<open>Using the constructur Suc, show that n + 1 = 1 + n.\<close>
lemma Suc2plus: "Suc n = Suc 0 + n"
by simp

text \<open>Similar lemma as above, using the constructur Suc.\<close>
lemma Suc_def2: "Suc i = i + Suc 0"
by simp

text \<open>If a chain contains its least upper bound as an element, this element is the
  maximum of the chain\<close>
lemma max_in_chainI3: "\<lbrakk>chain (Y::nat\<Rightarrow>'a::cpo); Y i = Lub Y\<rbrakk> \<Longrightarrow> max_in_chain i Y"
apply (simp add: max_in_chain_def)
apply (rule allI, rule impI)
apply (rule po_eq_conv [THEN iffD2])
apply (rule conjI)
apply (drule sym, simp)
apply (rule chain_mono, assumption+)
by (rule is_ub_thelub)

text \<open>A chain which contains its maximum is finite\<close>
lemma finite_chainI: "\<lbrakk>chain Y; max_in_chain i Y\<rbrakk> \<Longrightarrow> finite_chain Y"
by (auto simp add: finite_chain_def)

text \<open>'zipping' two chains together also zips their least upper bounds\<close>
lemma lub_prod2: "\<lbrakk>chain (X::nat \<Rightarrow> 'a::cpo); chain (Y::nat \<Rightarrow> 'b::cpo)\<rbrakk> \<Longrightarrow>
                        (\<Squnion>k. (X k,Y k)) = (Lub X, Lub Y)"
by (subst lub_prod, simp+)

text \<open>The least upper bound of a chainelement in a chain
is the least upper bound of the chainelement plus another element\<close>
lemma lub_range_shift2: "chain Y \<Longrightarrow> (\<Squnion>i. Y i) = (\<Squnion>i. Y (i+j))"
  apply(simp add: lub_def)
  using is_lub_range_shift lub_def by fastforce

text\<open>The least upper bound of any finite chain is a member of the chain\<close>
lemma l42: "chain S \<Longrightarrow> finite_chain S \<Longrightarrow> \<exists>t. (\<Squnion> j. S j) = S t"
using lub_eqI lub_finch2 by auto

text\<open>The least upper bound of a monotone function applied on a finite chain is the
function applied to the least upper bound of the finite chain\<close>
lemma finite_chain_lub: fixes Y :: "nat \<Rightarrow> 'a ::cpo"
  assumes "finite_chain Y" and "chain Y" and "monofun f"
  shows "f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i))"
proof -
  obtain nn :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat" where
    f1: "Lub Y = Y (nn Y)"
    by (meson assms(1) assms(2) l42)
  then have "\<forall>n. f (Y n) \<sqsubseteq> f (Y (nn Y))"
    by (metis (no_types) assms(2) assms(3) is_ub_thelub monofun_def)
  then show ?thesis
    using f1 by (simp add: lub_chain_maxelem)
qed

(* If you like admissibility proofs you will love this one. Never again "contI" ! *)
(* Dieses Lemma wurde nach langer suche von Sebastian entdeckt. Möge er ewig leben *)
lemma adm2cont:
  fixes f:: "'a::cpo \<Rightarrow> 'b::cpo"
  assumes "monofun f" and "\<And>k. adm (\<lambda>Y. (f Y)\<sqsubseteq>k)"
  shows "cont f"
  apply(rule contI2)
   apply(auto simp add: assms)
proof -
  fix Y:: "nat \<Rightarrow> 'a"
  assume "chain Y"
  obtain k where k_def: "k=(\<Squnion>i. (f (Y i)))" by simp
      (* komischer zwischenschritt, aber anders schafft sledgi das nicht *)
  have "\<And>j. f (Y j) \<sqsubseteq> (\<Squnion>i. (f (Y i)))"
    using \<open>chain Y\<close> assms(1) below_lub ch2ch_monofun by blast
  hence "\<And>j. f (Y j) \<sqsubseteq> k" by(simp add: k_def)
  hence "f (\<Squnion>j. Y j) \<sqsubseteq> k"
    by (metis (no_types, lifting) \<open>chain Y\<close> adm_def assms(2))
  thus "f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i)) "
    using k_def by blast
qed

text \<open>Creating a list from iteration a function \<open>f\<close>
  \<open>n\<close>-times on a start value \<open>s\<close>.\<close>
primrec literate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list"
where
  literate_0:  "literate 0 f s = []" |
  literate_Suc:"literate (Suc n) f s = s#(literate n f (f s))"

text \<open>Iterative conversion of @{term literate} result to a set\<close>
lemma literate_Suc2:
  "set (literate (Suc n) f s) = {s} \<union> set (literate n f (f s))"
by auto

text \<open>A set of successive natural numbers can be split into the smallest
  number and the rest\<close>
lemma natl3: "{i. x \<le> i \<and> i < Suc n + x} = {x} \<union> {i. Suc x \<le> i \<and> i < Suc n + x}"
by auto

text \<open>Create set of natural numbers from k to n+k-1 by @{term literate}\<close>
lemma literatel1 [simp]:
  "set (literate n Suc k) = {i. k \<le> i \<and> i < (n + k)}"
apply (rule_tac x="k" in spec)
apply (induct_tac n, simp)
apply (subst literate_Suc2)
apply (rule allI)
apply (erule_tac x="Suc x" in allE)
by (subst natl3, simp)

text \<open>A list of length @{term n} contains at most @{term n} different elements\<close>
lemma card_set_list_le_length: "card (set x) \<le> length x"
apply (induct_tac x, simp+)
by (simp add: card_insert_if)

text \<open>@{term "literate n"} creates lists with length @{term n}\<close>
lemma [simp]: "length (literate n f k) = n"
apply (rule_tac x="k" in spec)
by (induct_tac n, simp+)

text \<open>Zipping and unzipping on lists\<close>
lemma [simp]: "map snd (map (Pair k) a) = a"
by (induct_tac a, simp+)

text \<open>For a list @{term x}, each element in @{term "set x"} appears at some position in
  @{term x}\<close>
lemma from_set_to_nth: "xa \<in> set x \<Longrightarrow> \<exists>k. x!k = xa \<and> k < length x"
apply (simp add: atomize_imp)
apply (induct_tac x, simp+)
apply (rule conjI, rule impI)
apply (rule_tac x="0" in exI, simp)
apply (rule impI, simp)
apply (erule exE)
by (rule_tac x="Suc k" in exI, simp)

text \<open>Replacing a filter on lists by a stronger filter\<close>
lemma filterl4: "\<lbrakk>\<And>x. Q x \<Longrightarrow> P x; filter P x = []\<rbrakk> \<Longrightarrow> filter Q x = []"
by (simp add: atomize_imp, induct_tac x, auto)

text \<open>Induction on lists from the right\<close>
lemma list_rinduct_lemma: "\<forall>y. length y = k \<and> (P [] \<and> (\<forall>x xs. P xs \<longrightarrow> P (xs @ [x]))) \<longrightarrow> P y"
apply (induct_tac k, simp)
apply (rule allI)
apply (rule impI)
apply (erule conjE)+
apply (erule_tac x="butlast y" in allE, auto)
apply (erule_tac x="last y" in allE)
apply (erule_tac x="butlast y" in allE, auto)
by (case_tac "y = []", auto)

(* ----------------------------------------------------------------------- *)
section \<open>Some more lemmas about sets\<close>
(* ----------------------------------------------------------------------- *)

text \<open>All subsets of a finite set are finite themselves\<close>
lemma finite_subset1: "finite Y \<Longrightarrow> (\<forall>X. X \<subseteq> Y \<longrightarrow> finite X)"
  by (simp add: finite_subset)

text \<open>Given an infinite and a finite set, the infinite one contains an element
  which is not in the finite one\<close>
lemma ex_new_if_finitel1:
  "\<lbrakk>finite Y; \<not> finite X\<rbrakk> \<Longrightarrow> \<exists>a. a \<in> X \<and> a \<notin> Y"
apply (rule ccontr, auto)
apply (subgoal_tac "X \<subseteq> Y")
by (frule_tac Y="Y" in finite_subset1, auto)

text \<open>Create a finite set with \<open>n\<close> distinct continuously
  numbered entries from set \<open>A\<close>.\<close>
primrec
  getinj:: "'a set \<Rightarrow> nat \<Rightarrow> (nat \<times> 'a) set"
where
  "getinj A 0 = {(0,SOME x. x \<in> A)}" |
  "getinj A (Suc n) = {(Suc n, SOME x. x \<in> A \<and> x \<notin> (snd ` (getinj A n)))} \<union> getinj A n"

text \<open>The result of @{term "getinj A n"} and its projections on the first or
  second attribute are finite\<close>

lemma finite_getinjs[simp]: "finite (getinj A n)"
by (induct_tac n, simp+)

lemma finite_snd_getinjs[simp]: "finite (snd ` (getinj A n))"
by (induct_tac n, simp+)

lemma finite_fst_getinjs[simp]: "finite (fst ` (getinj A n))"
by (induct_tac n, simp+)

text \<open>@{term "getinj A n"} only contains entries for numbers up to @{term n}\<close>
lemma getinjs_l1: "\<forall>k. n < k \<longrightarrow> (k, x) \<notin> getinj A n"
by (induct_tac n, simp+)

text \<open>...especially, it contains no entry for @{term "n+1"}\<close>
lemma [simp]: "(Suc n,x) \<notin> getinj A n"
by (insert getinjs_l1 [of n x A], auto)

text \<open>Projecting to the second component is an injective function on results
  of @{term getinj}\<close>
lemma card_getinj_

lemma inj_on_getinj: "\<not> finite A \<Longrightarrow> inj_on snd (getinj A n)"
by (rule eq_card_imp_inj_on, simp+)

text \<open>@{term "getinj X n"} maps @{term n} to something\<close>
lemma getinj_ex[simp]: "\<exists>a. (n,a) \<in> getinj X n"
by (induct_tac n, simp+)

text \<open>For a fixed set @{term "A"}, @{term "getinj A i"} is a chain\<close>
lemma getinj_chain:
  "\<lbrakk>\<not> finite A; (j, x) \<in> getinj A j; j \<le> k\<rbrakk> \<Longrightarrow> (j, x) \<in> getinj A k"
apply (simp add: atomize_imp)
apply (induct_tac k, auto)
by (case_tac "j = Suc n", auto)

lemma inter_union_id:"(x \<union> y) \<inter> x = x"
  by blast

(* ----------------------------------------------------------------------- *)
section \<open>updis\<close>
(* ----------------------------------------------------------------------- *)

text \<open>The @{term "updis"} command lifts an arbitrary type to a
  discrete pointed partial order.\<close>
abbreviation
  updis :: "'a \<Rightarrow> 'a discr u"
    where "updis \<equiv> (\<lambda>a. up\<cdot>(Discr a))"

definition upApply :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a discr u \<rightarrow> 'b discr u" where
"upApply f \<equiv> \<Lambda> a. (if a=\<bottom> then \<bottom> else updis (f (THE b. a = updis b)))"

definition upApply2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a discr\<^sub>\<bottom> \<rightarrow> 'b discr\<^sub>\<bottom> \<rightarrow> 'c discr\<^sub>\<bottom>" where
"upApply2 f \<equiv> \<Lambda> a b. (if a=\<bottom>\<or>b=\<bottom> then \<bottom> else updis (f (THE x. a = updis x) (THE x. b = updis x)))"

(* updis lemma *)
lemma updis_exists: assumes "x\<noteq>\<bottom>"
  obtains n where "updis n = x"
  by (metis Discr_undiscr Exh_Up assms)

(* upApply *)
lemma upapply_mono [simp]: "monofun (\<lambda> a. (if a=\<bottom> then \<bottom> else updis (f (THE b. a = updis b))))"
apply (rule monofunI, auto)
by (metis (full_types, hide_lams) discrete_cpo upE up_below)

lemma upapply_lub: assumes "chain Y"
  shows "((\<lambda> a. (if a=\<bottom> then \<bottom> else updis (f (THE b. a = updis b)))) (\<Squnion>i. Y i))
=(\<Squnion>i. (\<lambda> a. (if a=\<bottom> then \<bottom> else updis (f (THE b. a = updis b)))) (Y i))"
apply (rule finite_chain_lub)
by (simp_all add: assms chfin2finch)

lemma upapply_cont [simp]: "cont (\<lambda> a. (if a=\<bottom> then \<bottom> else updis (f (THE b. a = updis b))))"
using chfindom_monofun2cont upapply_mono by blast

lemma upapply_rep_eq [simp]: "upApply f\<cdot>(updis a) = updis (f a)"
by (simp add: upApply_def)

lemma upapply_insert: "upApply f\<cdot>a = (if a=\<bottom> then \<bottom> else updis (f (THE b. a = updis b)))"
by(simp add: upApply_def)

lemma upapply_strict [simp]: "upApply f\<cdot>\<bottom> = \<bottom>"
by(simp add: upApply_def)

lemma upapply_nbot [simp]: "x\<noteq>\<bottom> \<Longrightarrow> upApply f\<cdot>x\<noteq>\<bottom>"
by(simp add: upApply_def)

lemma upapply_up [simp]: assumes "x\<noteq>\<bottom>" obtains a where "up\<cdot>a = upApply f\<cdot>x"
by(simp add: upApply_def assms)

lemma chain_nbot: assumes "chain Y" and  "(\<Squnion>i. Y i) \<noteq>\<bottom>"
  obtains n::nat where "(\<And>i. ((Y (i+n)) \<noteq>\<bottom>))"
  by (metis assms(1) assms(2) bottomI le_add2 lub_eq_bottom_iff po_class.chain_mono)

lemma upapply2_mono [simp]:
  "monofun (\<lambda> b. (if a=\<bottom>\<or>b=\<bottom> then \<bottom> else updis (f (THE x. a = updis x) (THE x. b = updis x))))"
apply (rule monofunI, auto)
by (metis discrete_cpo upE up_below)

lemma upapply2_cont [simp]:
  "cont (\<lambda>b. if a = \<bottom> \<or> b = \<bottom> then \<bottom> else updis (f (THE x. a = updis x) (THE x. b = updis x)))"
by (simp add: chfindom_monofun2cont)

lemma upapply2_mono2 [simp]:
  "monofun (\<lambda>a. \<Lambda> b. if a = \<bottom> \<or> b = \<bottom> then \<bottom> else updis (f (THE x. a = updis x) (THE x. b = updis x)))"
apply (rule monofunI)
apply (subst cfun_belowI, auto)
by (metis discrete_cpo upE up_below)

lemma upapply2_cont2 [simp]:
  "cont (\<lambda>a. \<Lambda> b. if a = \<bottom> \<or> b = \<bottom> then \<bottom> else updis (f (THE x. a = updis x) (THE x. b = updis x)))"
by (simp add: chfindom_monofun2cont)

lemma upapply2_rep_eq [simp]: "upApply2 f\<cdot>(updis a)\<cdot>(updis b) = updis (f a b)"
by (simp add: upApply2_def)

lemma upapply2_insert:
  "upApply2 f\<cdot>a\<cdot>b = (if a=\<bottom>\<or>b=\<bottom> then \<bottom> else updis (f (THE x. a = updis x) (THE x. b = updis x)))"
by (simp add: upApply2_def)

lemma upapply2_strict [simp]: "upApply2 f\<cdot>\<bottom> = \<bottom>"
by(simp add: upApply2_def)

lemma upapply2_nbot [simp]: "x\<noteq>\<bottom> \<Longrightarrow> y\<noteq>\<bottom> \<Longrightarrow> upApply2 f\<cdot>x\<cdot>y\<noteq>\<bottom>"
by(simp add: upApply2_def)

lemma upapply2_up [simp]: assumes "x\<noteq>\<bottom>" and "y\<noteq>\<bottom>" obtains a where "up\<cdot>a = upApply2 f\<cdot>x\<cdot>y"
by(simp add: upApply2_def assms)

lemma cont2lub_lub_eq: assumes cont: "\<And>i. cont (\<lambda>x. F i x)"
  shows "chain Y\<longrightarrow>  (\<Squnion>i. F i (\<Squnion>i. Y i)) = (\<Squnion>i ia. F i (Y ia))"
proof -
  { assume "\<exists>a. (\<Squnion>n. F a (Y n)) \<noteq> F a (Lub Y)"
    have ?thesis
      by (simp add: cont cont2contlubE) }
  thus ?thesis
    by force
qed

lemma[simp]: "x \<sqsubseteq> y \<Longrightarrow> (\<Lambda> ya. f\<cdot>x\<cdot>ya) \<sqsubseteq> (\<Lambda> ya. f\<cdot>y\<cdot>ya)"
  by (simp add: cont_pref_eq1I eta_cfun)

lemma[simp]:"\<forall>Y. chain Y \<longrightarrow> (\<Lambda> y. f\<cdot>(\<Squnion>i. Y i)\<cdot>y) \<sqsubseteq> (\<Squnion>i. \<Lambda> y. f\<cdot>(Y i)\<cdot>y)"
  apply(simp add: contlub_cfun_fun contlub_cfun_arg,auto)
  apply(subst contlub_lambda,auto)
  by (simp add: cfun.lub_cfun cont_pref_eq1I)

lemma cont_lam2cont[simp]:"cont (\<lambda>x. \<Lambda> y. f\<cdot>x\<cdot>y)"
  by(rule contI2, rule monofunI, simp+)

section \<open>add lemmas to cont2cont\<close>

lemma cont2cont_lambda [cont2cont]:
  assumes f: "\<And>y. cont (\<lambda>x. f x y)"
  shows "cont f"
  by (simp add: f) (* TODO: hat es einen grund, dass das nicht schon in cont2cont ist? HOLCF11-Doku lesen *)

lemma [cont2cont]:"cont f \<Longrightarrow> f\<in> cfun"
  by (simp add: cfun_def)

lemma discr_cont: "monofun f \<Longrightarrow> cont (\<lambda>x. g ((f x)::'a:: discrete_cpo))"
  apply(rule Cont.contI2)
  apply(rule monofunI, insert monofunE[of f],auto)
  by (metis is_ub_thelub)

lemma discr_cont2: "cont f \<Longrightarrow> cont (\<lambda>x. g ((f x)::'a:: discrete_cpo))" (*Not cont2cont, problem with domain definitions, i.e. lnat*)
  by (simp add: cont2mono discr_cont)

(*monofun f should be enough*)
lemma discr_cont3: "cont h \<Longrightarrow> cont f \<Longrightarrow> cont (\<lambda>x. ((h x)) ((f x)::'a:: discrete_cpo))"
  by (simp add: cont2cont_fun cont_apply)

section \<open>Timing information V3\<close>
datatype timeType = TUntimed | TTimed | TTsyn
end

author: yyisgladiator

repo: demo


text:
section \<open>Interleaving Semantics\<close>

theory repliss_sem
  imports Main
    "HOL-Library.Multiset"
    "HOL-Library.Option_ord"
    "HOL-Eisbach.Eisbach"
    "HOL-Library.Countable"
    utils
begin

text \<open>This theory describes the distributed semantics used by Repliss.
We use a fine grained interleaving semantics.
\<close>

datatype invocId = InvocId int
datatype txId = txId int
datatype callId = CallId int

text "A value type is a type that contains unique identifiers.
Since higher kinded classes are not supported, we represent unique ids using natural numbers.
The countable type class can then be used to convert other countable types to nat.

We also expect a default value, which does not include any unique ids.
This will be used for database operations with no result value."

type_synonym uniqueId = nat
class valueType = countable + default +
  fixes uniqueIds :: "'a \<Rightarrow> uniqueId set"
  assumes default_none[simp]: "uniqueIds default = {}"

definition
  "uniqueIdsInList xs = (\<Union>x\<in>set xs. uniqueIds x)"

instantiation bool :: valueType begin
definition [simp]: "uniqueIds_bool \<equiv> \<lambda>b::bool. {}::uniqueId set"
definition [simp]: "default_bool \<equiv> False"
instance by standard auto
end

instantiation unit :: valueType begin
definition [simp]: "uniqueIds_unit \<equiv> \<lambda>b::unit. {}::uniqueId set"
instance by standard auto
end

text_raw \<open>\DefineSnippet{call}{\<close>
datatype ('op, 'any) call = Call (call_operation: 'op) (call_res:"'any")
text_raw \<open>}%EndSnippet\<close>

text_raw \<open>\DefineSnippet{localAction}{\<close>
datatype ('ls, 'op, 'any) localAction =
    LocalStep bool 'ls
  | BeginAtomic 'ls
  | EndAtomic 'ls
  | NewId "'any \<rightharpoonup> 'ls"
  | DbOperation 'op "'any \<Rightarrow> 'ls"
  | Return 'any
text_raw \<open>}%EndSnippet\<close>

text_raw \<open>\DefineSnippet{procedureImpl}{\<close>
type_synonym ('ls, 'op, 'any) procedureImpl =
  "'ls \<Rightarrow> ('ls, 'op, 'any) localAction"
text_raw \<open>}%EndSnippet\<close>

datatype txStatus = Uncommitted | Committed

instantiation txStatus :: linorder
begin
definition "less_eq_txStatus x y \<equiv> x = Uncommitted \<or> y = Committed"
definition "less_txStatus x y \<equiv> x = Uncommitted \<and> y = Committed"
instance
   by (standard; insert txStatus.exhaust;  auto simp add: less_eq_txStatus_def less_txStatus_def)
end

lemmas txStatus_less_simps = less_eq_txStatus_def less_txStatus_def

lemma onlyCommittedGreater: "a \<triangleq> Committed" if "a\<ge>Some Committed" for a
  by (smt dual_order.antisym dual_order.trans less_eq_option_None_is_None less_eq_option_Some less_eq_txStatus_def order_refl split_option_ex that)

text_raw \<open>\DefineSnippet{operationContext}{\<close>
record ('op, 'any) operationContext =
  calls :: "callId \<rightharpoonup> ('op, 'any) call"
  happensBefore :: "callId rel"
text_raw \<open>}%EndSnippet\<close>

text_raw \<open>\DefineSnippet{invContext}{\<close>
record ('proc, 'op, 'any) invContext = "('op, 'any) operationContext" +
  callOrigin :: "callId \<rightharpoonup> txId"
  txOrigin :: "txId \<rightharpoonup> invocId"
  knownIds :: "uniqueId set"
  invocOp :: "invocId \<rightharpoonup> 'proc"
  invocRes :: "invocId \<rightharpoonup> 'any"
text_raw \<open>}%EndSnippet\<close>

text_raw \<open>\DefineSnippet{prog}{\<close>
record ('proc, 'ls, 'op, 'any) prog =
  querySpec :: "'op \<Rightarrow> ('op, 'any) operationContext \<Rightarrow> 'any \<Rightarrow> bool"
  procedure :: "'proc \<Rightarrow> ('ls \<times> ('ls, 'op, 'any) procedureImpl)"
  invariant :: "('proc, 'op, 'any) invContext \<Rightarrow> bool"
text_raw \<open>}%EndSnippet\<close>

text_raw \<open>\DefineSnippet{state}{\<close>
record ('proc, 'ls, 'op, 'any) state = "('proc, 'op, 'any) invContext" +
  prog :: "('proc, 'ls, 'op, 'any) prog"
  txStatus :: "txId \<rightharpoonup> txStatus"
  generatedIds :: "uniqueId \<rightharpoonup> invocId"
  localState :: "invocId \<rightharpoonup> 'ls"
  currentProc :: "invocId \<rightharpoonup> ('ls, 'op, 'any) procedureImpl"
  visibleCalls :: "invocId \<rightharpoonup> callId set"
  currentTx :: "invocId \<rightharpoonup> txId"
text_raw \<open>}%EndSnippet\<close>

lemma operationContext_ext: "((x::('op, 'any) operationContext) = y) \<longleftrightarrow> (
    calls x = calls y
  \<and> happensBefore x = happensBefore y)"
  by auto

lemma state_ext: "((x::('proc, 'ls, 'op, 'any) state) = y) \<longleftrightarrow> (
    calls x = calls y
  \<and> happensBefore x = happensBefore y
  \<and> prog x = prog y
  \<and> localState x = localState y
  \<and> currentProc x = currentProc y
  \<and> visibleCalls x = visibleCalls y
  \<and> currentTx x = currentTx y
  \<and> txStatus x = txStatus y
  \<and> callOrigin x = callOrigin y
  \<and> txOrigin x = txOrigin y
  \<and> generatedIds x = generatedIds y
  \<and> knownIds x = knownIds y
  \<and> invocOp x = invocOp y
  \<and> invocRes x = invocRes y
)"
  by auto

lemmas stateEqI = state_ext[THEN iffToImp, simplified imp_conjL, rule_format]

lemma state_ext_exI:
  fixes P :: "('proc, 'ls, 'op, 'any) state \<Rightarrow> bool"
  assumes "
\<exists>
s_calls
s_happensBefore
s_prog
s_localState
s_currentProc
s_visibleCalls
s_currentTx
s_txStatus
s_callOrigin
s_txOrigin
s_generatedIds
s_knownIds
s_invocOp
s_invocRes. P \<lparr>
calls = s_calls,
happensBefore = s_happensBefore,
callOrigin = s_callOrigin,
txOrigin = s_txOrigin,
knownIds = s_knownIds,
invocOp = s_invocOp,
invocRes = s_invocRes,
prog = s_prog,
txStatus = s_txStatus,
generatedIds = s_generatedIds,
localState = s_localState,
currentProc = s_currentProc,
visibleCalls = s_visibleCalls,
currentTx = s_currentTx
\<rparr>"
  shows "\<exists>s. P s"
  using assms by blast

lemma show_state_calls_eq:
  assumes "A = B"
  shows "\<And>x y. x = y \<Longrightarrow> A\<lparr>calls := x\<rparr> = B\<lparr>calls := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>happensBefore := x\<rparr> = B\<lparr>happensBefore := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>callOrigin := x\<rparr> = B\<lparr>callOrigin := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>txOrigin := x\<rparr> = B\<lparr>txOrigin := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>knownIds := x\<rparr> = B\<lparr>knownIds := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>invocOp := x\<rparr> = B\<lparr>invocOp := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>invocRes := x\<rparr> = B\<lparr>invocRes := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>prog := x\<rparr> = B\<lparr>prog := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>txStatus := x\<rparr> = B\<lparr>txStatus := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>generatedIds := x\<rparr> = B\<lparr>generatedIds := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>localState := x\<rparr> = B\<lparr>localState := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>currentProc := x\<rparr> = B\<lparr>currentProc := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>visibleCalls := x\<rparr> = B\<lparr>visibleCalls := y\<rparr>"
and "\<And>x y. x = y \<Longrightarrow> A\<lparr>currentTx := x\<rparr> = B\<lparr>currentTx := y\<rparr>"
  using assms  by auto

lemma state_updates_normalize:
  shows "\<And>x y. S\<lparr>happensBefore := y, calls := x\<rparr> = S\<lparr>calls := x,  happensBefore := y\<rparr>"
and "\<And>x y. S\<lparr>callOrigin := y, calls := x\<rparr> = S\<lparr>calls := x,  callOrigin := y\<rparr>"
and "\<And>x y. S\<lparr>txOrigin := y, calls := x\<rparr> = S\<lparr>calls := x,  txOrigin := y\<rparr>"
and "\<And>x y. S\<lparr>knownIds := y, calls := x\<rparr> = S\<lparr>calls := x,  knownIds := y\<rparr>"
and "\<And>x y. S\<lparr>invocOp := y, calls := x\<rparr> = S\<lparr>calls := x,  invocOp := y\<rparr>"
and "\<And>x y. S\<lparr>invocRes := y, calls := x\<rparr> = S\<lparr>calls := x,  invocRes := y\<rparr>"
and "\<And>x y. S\<lparr>prog := y, calls := x\<rparr> = S\<lparr>calls := x,  prog := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, calls := x\<rparr> = S\<lparr>calls := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, calls := x\<rparr> = S\<lparr>calls := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, calls := x\<rparr> = S\<lparr>calls := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, calls := x\<rparr> = S\<lparr>calls := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, calls := x\<rparr> = S\<lparr>calls := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, calls := x\<rparr> = S\<lparr>calls := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>callOrigin := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  callOrigin := y\<rparr>"
and "\<And>x y. S\<lparr>txOrigin := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  txOrigin := y\<rparr>"
and "\<And>x y. S\<lparr>knownIds := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  knownIds := y\<rparr>"
and "\<And>x y. S\<lparr>invocOp := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  invocOp := y\<rparr>"
and "\<And>x y. S\<lparr>invocRes := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  invocRes := y\<rparr>"
and "\<And>x y. S\<lparr>prog := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  prog := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, happensBefore := x\<rparr> = S\<lparr>happensBefore := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>txOrigin := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  txOrigin := y\<rparr>"
and "\<And>x y. S\<lparr>knownIds := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  knownIds := y\<rparr>"
and "\<And>x y. S\<lparr>invocOp := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  invocOp := y\<rparr>"
and "\<And>x y. S\<lparr>invocRes := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  invocRes := y\<rparr>"
and "\<And>x y. S\<lparr>prog := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  prog := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, callOrigin := x\<rparr> = S\<lparr>callOrigin := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>knownIds := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  knownIds := y\<rparr>"
and "\<And>x y. S\<lparr>invocOp := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  invocOp := y\<rparr>"
and "\<And>x y. S\<lparr>invocRes := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  invocRes := y\<rparr>"
and "\<And>x y. S\<lparr>prog := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  prog := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, txOrigin := x\<rparr> = S\<lparr>txOrigin := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>invocOp := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  invocOp := y\<rparr>"
and "\<And>x y. S\<lparr>invocRes := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  invocRes := y\<rparr>"
and "\<And>x y. S\<lparr>prog := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  prog := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, knownIds := x\<rparr> = S\<lparr>knownIds := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>invocRes := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  invocRes := y\<rparr>"
and "\<And>x y. S\<lparr>prog := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  prog := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, invocOp := x\<rparr> = S\<lparr>invocOp := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>prog := y, invocRes := x\<rparr> = S\<lparr>invocRes := x,  prog := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, invocRes := x\<rparr> = S\<lparr>invocRes := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, invocRes := x\<rparr> = S\<lparr>invocRes := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, invocRes := x\<rparr> = S\<lparr>invocRes := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, invocRes := x\<rparr> = S\<lparr>invocRes := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, invocRes := x\<rparr> = S\<lparr>invocRes := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, invocRes := x\<rparr> = S\<lparr>invocRes := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>txStatus := y, prog := x\<rparr> = S\<lparr>prog := x,  txStatus := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, prog := x\<rparr> = S\<lparr>prog := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, prog := x\<rparr> = S\<lparr>prog := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, prog := x\<rparr> = S\<lparr>prog := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, prog := x\<rparr> = S\<lparr>prog := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, prog := x\<rparr> = S\<lparr>prog := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>generatedIds := y, txStatus := x\<rparr> = S\<lparr>txStatus := x,  generatedIds := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, txStatus := x\<rparr> = S\<lparr>txStatus := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, txStatus := x\<rparr> = S\<lparr>txStatus := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, txStatus := x\<rparr> = S\<lparr>txStatus := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, txStatus := x\<rparr> = S\<lparr>txStatus := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>localState := y, generatedIds := x\<rparr> = S\<lparr>generatedIds := x,  localState := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, generatedIds := x\<rparr> = S\<lparr>generatedIds := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, generatedIds := x\<rparr> = S\<lparr>generatedIds := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, generatedIds := x\<rparr> = S\<lparr>generatedIds := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>currentProc := y, localState := x\<rparr> = S\<lparr>localState := x,  currentProc := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, localState := x\<rparr> = S\<lparr>localState := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, localState := x\<rparr> = S\<lparr>localState := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>visibleCalls := y, currentProc := x\<rparr> = S\<lparr>currentProc := x,  visibleCalls := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, currentProc := x\<rparr> = S\<lparr>currentProc := x,  currentTx := y\<rparr>"
and "\<And>x y. S\<lparr>currentTx := y, visibleCalls := x\<rparr> = S\<lparr>visibleCalls := x,  currentTx := y\<rparr>"
  by auto

abbreviation "committedTransactions C \<equiv> {txn. txStatus C txn \<triangleq> Committed }"

abbreviation "emptyOperationContext \<equiv> \<lparr> calls = Map.empty, happensBefore = {}\<rparr>"

definition "getContextH" where
  "getContextH state_calls state_happensBefore state_vis = (case state_vis of
      None \<Rightarrow> emptyOperationContext
    | Some vis => \<lparr>
        calls = state_calls |` vis,
        happensBefore = state_happensBefore |r vis
      \<rparr>
  )"

abbreviation
  "getContext state s
 \<equiv> getContextH (calls state) (happensBefore state) (visibleCalls state s) "

abbreviation "emptyInvariantContext \<equiv> \<lparr>
        calls = Map.empty,
        happensBefore = {},
        callOrigin  = Map.empty,
        txOrigin = Map.empty,
        knownIds = {},
        invocOp = Map.empty,
        invocRes = Map.empty
\<rparr>"

definition isCommittedH where
  "isCommittedH state_callOrigin state_txStatus c \<equiv> \<exists>tx. state_callOrigin c \<triangleq> tx \<and> state_txStatus tx \<triangleq> Committed"

abbreviation isCommitted :: "('proc, 'ls, 'op, 'any) state \<Rightarrow> callId \<Rightarrow> bool" where
  "isCommitted state \<equiv> isCommittedH (callOrigin state) (txStatus state)"

definition "committedCallsH state_callOrigin state_txStatus \<equiv>
   {c. isCommittedH state_callOrigin state_txStatus c}"

abbreviation committedCalls :: "('proc, 'ls, 'op, 'any) state \<Rightarrow> callId set" where
  "committedCalls state \<equiv> committedCallsH (callOrigin state) (txStatus state)"

definition invContextH  where
  "invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
   state_calls state_knownIds state_invocOp state_invocRes = \<lparr>
        calls = state_calls |` committedCallsH state_callOrigin state_txStatus ,
        happensBefore = state_happensBefore |r committedCallsH state_callOrigin state_txStatus ,
        callOrigin  = state_callOrigin |` committedCallsH state_callOrigin state_txStatus,
        txOrigin = state_txOrigin |` {t. state_txStatus t \<triangleq> Committed},
        knownIds = state_knownIds,
        invocOp = state_invocOp,
        invocRes = state_invocRes
      \<rparr>"

lemma invContextH_calls:
"calls (invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_calls |` committedCallsH state_callOrigin state_txStatus"
  by (auto simp add: invContextH_def)

lemma invContextH_happensBefore:
"happensBefore (invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes)
= state_happensBefore |r committedCallsH state_callOrigin state_txStatus "
  by (auto simp add: invContextH_def)

lemma invContextH_i_callOrigin:
"callOrigin (invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_callOrigin |` committedCallsH state_callOrigin state_txStatus"
by (auto simp add: invContextH_def)

lemma invContextH_i_txOrigin:
"txOrigin (invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
=  state_txOrigin |` {t. state_txStatus t \<triangleq> Committed}"
  by (auto simp add: invContextH_def)

lemma invContextH_i_knownIds:
"knownIds (invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_knownIds"
  by (auto simp add: invContextH_def)

lemma invContextH_i_invocOp:
"invocOp (invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_invocOp"
by (auto simp add: invContextH_def)

lemma invContextH_i_invocRes:
"invocRes (invContextH state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
=  state_invocRes"
by (auto simp add: invContextH_def)

abbreviation invContext where
  "invContext state \<equiv>
  invContextH
  (callOrigin state)
  (txOrigin state)
  (txStatus state)
  (happensBefore state)
  (calls state)
  (knownIds state)
  (invocOp state)
  (invocRes state)"

definition invContextH2  where
  "invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
   state_calls state_knownIds state_invocOp state_invocRes = \<lparr>
        calls = state_calls ,
        happensBefore = state_happensBefore,
        callOrigin  = state_callOrigin,
        txOrigin = state_txOrigin,
        knownIds = state_knownIds,
        invocOp = state_invocOp,
        invocRes = state_invocRes
      \<rparr>"

lemma invContextH2_calls:
"calls (invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_calls"
  by (auto simp add: invContextH2_def)

lemma invContextH2_happensBefore:
"happensBefore (invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes)
= state_happensBefore"
  by (auto simp add: invContextH2_def)

lemma invContextH2_i_callOrigin:
"callOrigin (invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_callOrigin "
by (auto simp add: invContextH2_def)

lemma invContextH2_i_txOrigin:
"txOrigin (invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
=  state_txOrigin "
  by (auto simp add: invContextH2_def)

lemma invContextH2_i_knownIds:
"knownIds (invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_knownIds"
  by (auto simp add: invContextH2_def)

lemma invContextH2_i_invocOp:
"invocOp (invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
= state_invocOp"
by (auto simp add: invContextH2_def)

lemma invContextH2_i_invocRes:
"invocRes (invContextH2 state_callOrigin state_txOrigin state_txStatus state_happensBefore
      state_calls state_knownIds state_invocOp state_invocRes )
=  state_invocRes"
by (auto simp add: invContextH2_def)

lemmas invContextH2_simps =
invContextH_calls
invContextH_happensBefore
invContextH_i_callOrigin
invContextH_i_txOrigin
invContextH_i_knownIds
invContextH_i_invocOp
invContextH_i_invocRes
invContextH2_calls
invContextH2_happensBefore
invContextH2_i_callOrigin
invContextH2_i_txOrigin
invContextH2_i_knownIds
invContextH2_i_invocOp
invContextH2_i_invocRes

abbreviation invContext' where
  "invContext' state \<equiv>
  invContextH2
  (callOrigin state)
  (txOrigin state)
  (txStatus state)
  (happensBefore state)
  (calls state)
  (knownIds state)
  (invocOp state)
  (invocRes state)"

lemma invContext'_truncate: "invContext' state = invContext.truncate state"
  by (auto simp add: invContextH2_def invContext.defs)

definition callsInTransactionH :: "(callId \<rightharpoonup> txId) \<Rightarrow> txId set \<Rightarrow> callId set" where
  "callsInTransactionH origins txns  \<equiv> {c. \<exists>txn\<in>txns. origins c \<triangleq> txn }"

lemma callsInTransactionH_contains:
  "c\<in>callsInTransactionH origins txns \<longleftrightarrow> (case origins c of Some txn \<Rightarrow>  txn \<in> txns | None \<Rightarrow> False)"
  by (auto simp add: callsInTransactionH_def split: option.splits)

abbreviation
  "callsInTransaction S txns \<equiv> callsInTransactionH (callOrigin S) txns"

lemma invContextSnapshot_eq:
  assumes "c_calls = committedCallsH (callOrigin state) (txStatus state)"
    and "c_txns = {t. txStatus state t \<triangleq> Committed}"
  shows
    "invContext state =  \<lparr>
        calls = calls state |` c_calls ,
        happensBefore = happensBefore state |r c_calls ,
        callOrigin  = callOrigin state |` c_calls,
        txOrigin = txOrigin state |` c_txns,
        knownIds = knownIds state,
        invocOp = invocOp state,
        invocRes = invocRes state\<rparr>"
  by (auto simp add: assms  invContextH_def)

lemma invContext_eqI: "\<lbrakk>
calls x = calls y;
happensBefore x = happensBefore y;
callOrigin x = callOrigin y;
txOrigin x = txOrigin y;
knownIds x = knownIds y;
invocOp x = invocOp y;
invocRes x = invocRes y
\<rbrakk> \<Longrightarrow> x = (y::('proc, 'op, 'any) invContext)"
  by auto

text_raw \<open>\DefineSnippet{repliss_sem_action}{\<close>
datatype ('proc, 'op, 'any) action =
    ALocal bool
  | ANewId 'any
  | ABeginAtomic txId "(callId set)"
  | AEndAtomic
  | ADbOp callId 'op 'any
  | AInvoc 'proc
  | AReturn 'any
  | ACrash
  | AInvcheck bool
text_raw \<open>}%EndSnippet\<close>

definition "is_AInvcheck a \<equiv> \<exists>r. a = AInvcheck r"

definition
  "isACrash a \<equiv> case a of ACrash \<Rightarrow> True | _ \<Rightarrow> False"

schematic_goal [simp]: "isACrash (ALocal b) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (ANewId u) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (ABeginAtomic t newTxns) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (AEndAtomic) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (ADbOp c oper res) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (AInvoc proc) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (AReturn res) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (ACrash) = ?x" by (auto simp add: isACrash_def)
schematic_goal [simp]: "isACrash (AInvcheck c) = ?x" by (auto simp add: isACrash_def)

definition chooseSnapshot_h where
"chooseSnapshot_h snapshot vis txSt cOrigin hb \<equiv>
  \<exists>newTxns newCalls.
  \<comment> \<open>  choose a set of committed transactions to add to the snapshot  \<close>
   (\<forall>txn\<in>newTxns. txSt txn \<triangleq> Committed)
   \<comment> \<open>  determine new visible calls: downwards-closure wrt. causality   \<close>
   \<and> newCalls = callsInTransactionH cOrigin newTxns \<down> hb
   \<comment> \<open>  transaction snapshot  \<close>
   \<and> snapshot = vis \<union> newCalls"

abbreviation chooseSnapshot :: "callId set \<Rightarrow> callId set \<Rightarrow> ('proc::valueType, 'ls, 'op, 'any::valueType) state \<Rightarrow> bool" where
"chooseSnapshot snapshot vis S \<equiv> chooseSnapshot_h snapshot vis (txStatus S) (callOrigin S) (happensBefore S)"

lemma chooseSnapshot_def: \<comment> \<open>old definition\<close>
"chooseSnapshot snapshot vis S = (
  \<exists>newTxns newCalls.
  \<comment> \<open>  choose a set of committed transactions to add to the snapshot  \<close>
   newTxns \<subseteq> committedTransactions S
   \<comment> \<open>  determine new visible calls: downwards-closure wrt. causality   \<close>
   \<and> newCalls = callsInTransaction S newTxns \<down> happensBefore S
   \<comment> \<open>  transaction snapshot  \<close>
   \<and> snapshot = vis \<union> newCalls)"
  by (auto simp add: chooseSnapshot_h_def)

schematic_goal chooseSnapshot_def2:
"chooseSnapshot snapshot vis S = ?x"
  by (subst chooseSnapshot_h_def, rule refl)

thm chooseSnapshot_def2

schematic_goal callsInTransaction_def:
"callsInTransaction S newTxns = ?x"
  by (subst callsInTransactionH_def, rule refl)

 text \<open>
\DefineSnippet{chooseSnapshot_def}{
  @{thm [display] chooseSnapshot_def}
}%EndSnippet

\DefineSnippet{chooseSnapshot_def2}{
  @{thm [display] chooseSnapshot_def2}
}%EndSnippet

\DefineSnippet{downwardsClosure_in}{
  @{thm [display] downwardsClosure_in}
}%EndSnippet

\DefineSnippet{callsInTransaction_def}{
  @{thm [display] callsInTransaction_def}
}%EndSnippet

 \<close>

inductive step :: "('proc::valueType, 'ls, 'op, 'any::valueType) state \<Rightarrow> (invocId \<times> ('proc, 'op, 'any) action) \<Rightarrow> ('proc, 'ls, 'op, 'any) state \<Rightarrow> bool" (infixr "~~ _ \<leadsto>" 60) where
  local:
  "\<lbrakk>localState S i \<triangleq> ls;
   currentProc S i \<triangleq> f;
   f ls = LocalStep ok ls'
   \<rbrakk> \<Longrightarrow> S ~~ (i, ALocal ok)  \<leadsto> (S\<lparr>localState := (localState S)(i \<mapsto> ls') \<rparr>)"
| newId:
  "\<lbrakk>localState S i \<triangleq> ls;
   currentProc S i \<triangleq> f;
   f ls = NewId ls';
   generatedIds S (uid) = None;
   uniqueIds uidv = {uid}; \<comment> \<open>  there is exactly one unique id  \<close>
   ls' uidv \<triangleq> ls'';
   uid = to_nat uidv
   \<rbrakk> \<Longrightarrow> S ~~ (i, ANewId uidv) \<leadsto> (S\<lparr>localState := (localState S)(i \<mapsto> ls''),
                                   generatedIds := (generatedIds S)(uid \<mapsto> i)  \<rparr>)"
| beginAtomic:
  "\<lbrakk>localState S i \<triangleq> ls;
   currentProc S i \<triangleq> f;
   f ls = BeginAtomic ls';
   currentTx S i = None;
   txStatus S t = None;
   visibleCalls S i \<triangleq> vis;
   chooseSnapshot snapshot vis S
   \<rbrakk> \<Longrightarrow> S ~~ (i, ABeginAtomic t snapshot) \<leadsto> (S\<lparr>localState := (localState S)(i \<mapsto> ls'),
                currentTx := (currentTx S)(i \<mapsto> t),
                txStatus := (txStatus S)(t \<mapsto> Uncommitted),
                txOrigin := (txOrigin S)(t \<mapsto> i),
                visibleCalls := (visibleCalls S)(i \<mapsto> snapshot)\<rparr>)"
| endAtomic:
  "\<lbrakk>localState S i \<triangleq> ls;
   currentProc S i \<triangleq> f;
   f ls = EndAtomic ls';
   currentTx S i \<triangleq> t
   \<rbrakk> \<Longrightarrow> S ~~ (i, AEndAtomic) \<leadsto> (S\<lparr>localState := (localState S)(i \<mapsto> ls'),
                currentTx := (currentTx S)(i := None),
                txStatus := (txStatus S)(t \<mapsto> Committed) \<rparr>)"
| dbop:
  "\<lbrakk>localState S i \<triangleq> ls;
   currentProc S i \<triangleq> f;
   f ls = DbOperation Op ls';
   currentTx S i \<triangleq> t;
   calls S c = None;
   querySpec (prog S) Op (getContext S i)  res;
   visibleCalls S i \<triangleq> vis
   \<rbrakk> \<Longrightarrow>  S ~~ (i, ADbOp c Op res) \<leadsto> (S\<lparr>localState := (localState S)(i \<mapsto> ls' res),
                calls := (calls S)(c \<mapsto> Call Op res ),
                callOrigin := (callOrigin S)(c \<mapsto> t),
                visibleCalls := (visibleCalls S)(i \<mapsto> vis \<union> {c}),
                happensBefore := happensBefore S \<union> vis \<times> {c}  \<rparr>)"

| invocation:
  "\<lbrakk>localState S i = None;
   procedure (prog S) proc = (initialState, impl);
   uniqueIds proc \<subseteq> knownIds S;
   invocOp S i = None
   \<rbrakk> \<Longrightarrow>  S ~~ (i, AInvoc proc) \<leadsto> (S\<lparr>localState := (localState S)(i \<mapsto> initialState),
                 currentProc := (currentProc S)(i \<mapsto> impl),
                 visibleCalls := (visibleCalls S)(i \<mapsto> {}),
                 invocOp := (invocOp S)(i \<mapsto> proc) \<rparr>)"
| return:
  "\<lbrakk>localState S i \<triangleq> ls;
   currentProc S i \<triangleq> f;
   f ls = Return res;
   currentTx S i = None
   \<rbrakk> \<Longrightarrow>  S ~~ (i, AReturn res) \<leadsto> (S\<lparr>localState := (localState S)(i := None),
                 currentProc := (currentProc S)(i := None),
                 visibleCalls := (visibleCalls S)(i := None),
                 invocRes := (invocRes S)(i \<mapsto> res),
                 knownIds := knownIds S \<union> uniqueIds res\<rparr>)"
| crash:
  "localState S i \<triangleq> ls
   \<Longrightarrow> S ~~ (i, ACrash) \<leadsto> (S\<lparr>localState := (localState S)(i := None),
                 currentTx := (currentTx S)(i := None),
                 currentProc := (currentProc S)(i := None),
                 visibleCalls := (visibleCalls S)(i := None) \<rparr>)"
| invCheck: \<comment> \<open>checks a snapshot\<close>
  "\<lbrakk>invariant (prog S) (invContext S) = res
   \<rbrakk> \<Longrightarrow>  S ~~ (i, AInvcheck res) \<leadsto> S"

inductive_simps step_simp_ALocal: "A ~~ (s, ALocal ok) \<leadsto> B "
inductive_simps step_simp_ANewId: "A ~~ (s, ANewId n) \<leadsto> B "
inductive_simps step_simp_ABeginAtomic: "A ~~ (s, ABeginAtomic t newTxns) \<leadsto> B "
inductive_simps step_simp_AEndAtomic: "A ~~ (s, AEndAtomic) \<leadsto> B "
inductive_simps step_simp_ADbOp: "A ~~ (s, ADbOp c oper res) \<leadsto> B "
inductive_simps step_simp_AInvoc: "A ~~ (s, AInvoc proc) \<leadsto> B "
inductive_simps step_simp_AReturn: "A ~~ (s, AReturn res) \<leadsto> B "
inductive_simps step_simp_ACrash: "A ~~ (s, ACrash) \<leadsto> B "
inductive_simps step_simp_AInvcheck: "A ~~ (s, AInvcheck res) \<leadsto> B "
inductive_simps step_simps_all: "A ~~ b \<leadsto> B "

lemmas step_simps =
  step_simp_ALocal
  step_simp_ANewId
  step_simp_ABeginAtomic
  step_simp_AEndAtomic
  step_simp_ADbOp
  step_simp_AInvoc
  step_simp_AReturn
  step_simp_ACrash
  step_simp_AInvcheck

lemmas step_intros =
  step_simps[THEN iffToImp, simplified imp_conjL imp_ex, rule_format]

inductive_cases step_elim_ALocal: "A ~~ (s, ALocal ok) \<leadsto> B "
inductive_cases step_elim_ANewId: "A ~~ (s, ANewId n) \<leadsto> B "
inductive_cases step_elim_ABeginAtomic: "A ~~ (s, ABeginAtomic t newTxns) \<leadsto> B "
inductive_cases step_elim_AEndAtomic: "A ~~ (s, AEndAtomic) \<leadsto> B "
inductive_cases step_elim_ADbOp: "A ~~ (s, ADbOp c oper res) \<leadsto> B "
inductive_cases step_elim_AInvoc: "A ~~ (s, AInvoc procname) \<leadsto> B "
inductive_cases step_elim_AReturn: "A ~~ (s, AReturn res) \<leadsto> B "
inductive_cases step_elim_ACrash: "A ~~ (s, ACrash) \<leadsto> B "
inductive_cases step_elim_AInvcheck: "A ~~ (s, AInvcheck i) \<leadsto> B "
inductive_cases step_elim_general: "A ~~ (s, a) \<leadsto> B "

lemmas step_elims =
  step_elim_ALocal
  step_elim_ANewId
  step_elim_ABeginAtomic
  step_elim_AEndAtomic
  step_elim_ADbOp
  step_elim_AInvoc
  step_elim_AReturn
  step_elim_ACrash
  step_elim_AInvcheck

inductive steps :: "('proc::valueType, 'ls, 'op, 'any::valueType) state \<Rightarrow> (invocId \<times> ('proc, 'op, 'any) action) list \<Rightarrow> ('proc, 'ls, 'op, 'any) state \<Rightarrow> bool" (infixr "~~ _ \<leadsto>*" 60) where
  steps_refl:
  "S ~~ [] \<leadsto>* S"
| steps_step:
  "\<lbrakk>S ~~ tr \<leadsto>* S'; S' ~~ a \<leadsto> S''\<rbrakk> \<Longrightarrow> S ~~ tr@[a] \<leadsto>* S''"

\<comment> \<open>Add some nicer syntax for Latex output:\<close>

notation (latex output)
  step ("(_) \<^latex>\<open>$\\step{\\text{\<close> (\<open>unbreakable\<close>_) \<^latex>\<open>}}$\<close> (1_)" [5,5,5]65)
notation (latex output)
  steps  ("(_) \<^latex>\<open>\\steps{\\text{\<close> (\<open>unbreakable\<close> _) \<^latex>\<open>}}\<close> (1_)" [5,5,5]65)

\<comment> \<open>with a given trace, the execution is deterministic\<close>
lemma stepDeterministic:
  assumes e1: "S ~~ tr \<leadsto> Sa"
    and e2: "S ~~ tr \<leadsto> Sb"
  shows "Sa = Sb"
  using e1 e2 proof (induct rule: step.induct)
  qed (erule step.cases; force)+

lemma traceDeterministic:
  assumes e1: "S ~~ tr \<leadsto>* Sa"
    and e2: "S ~~ tr \<leadsto>* Sb"
  shows "Sa = Sb"
  using e1 e2 proof (induct S tr Sa arbitrary: Sb rule: steps.induct)
  case (steps_refl S)
  then show ?case
    using steps.cases by fastforce
next
  case (steps_step S tr S' a S'')
  then show ?case
    by (metis snoc_eq_iff_butlast stepDeterministic steps.cases)
qed

definition initialState :: "('proc, 'ls, 'op, 'any) prog \<Rightarrow> ('proc, 'ls, 'op, 'any) state" where
  "initialState program \<equiv> \<lparr>
  calls = Map.empty,
  happensBefore = {},
  callOrigin = Map.empty,
  txOrigin = Map.empty,
  knownIds = {},
  invocOp = Map.empty,
  invocRes = Map.empty,
  prog = program,
  txStatus = Map.empty,
  generatedIds = Map.empty,
  localState = Map.empty,
  currentProc = Map.empty,
  visibleCalls = Map.empty,
  currentTx = Map.empty
\<rparr>"

type_synonym ('proc, 'op, 'any) trace = "(invocId\<times>('proc, 'op, 'any) action) list"

abbreviation get_invoc :: "invocId\<times>('proc, 'op, 'any) action \<Rightarrow> invocId" where
"get_invoc \<equiv> fst"
abbreviation get_action :: "invocId\<times>('proc, 'op, 'any) action \<Rightarrow> ('proc, 'op, 'any) action" where
"get_action \<equiv> snd"

definition traces where
  "traces program \<equiv> {tr. \<exists>S'. initialState program ~~ tr \<leadsto>* S'}"

definition
  "actionCorrect a \<equiv> a \<noteq> AInvcheck False \<and> a \<noteq> ALocal False"

definition traceCorrect where
  "traceCorrect trace \<equiv> (\<forall>(i,a)\<in>set trace. actionCorrect a)"

lemma traceCorrect_def':
  "traceCorrect trace = (\<forall>e\<in>set trace. actionCorrect (get_action e))"
  by (auto simp add: traceCorrect_def)

definition programCorrect :: "('proc::valueType, 'ls, 'op::valueType, 'any::valueType) prog \<Rightarrow> bool" where
  "programCorrect program \<equiv> (\<forall>trace\<in>traces program. traceCorrect trace)"

definition "isABeginAtomic action = (case action of ABeginAtomic x newTxns \<Rightarrow> True | _ \<Rightarrow> False)"

definition "isAInvoc action = (case action of AInvoc _   \<Rightarrow> True | _ \<Rightarrow> False)"

lemma traceCorrect_append:
"traceCorrect (xs@ys) \<longleftrightarrow> traceCorrect xs \<and> traceCorrect ys"
  by (auto simp add: traceCorrect_def)

lemma traceCorrect_cons:
"traceCorrect (x#ys) \<longleftrightarrow> actionCorrect (get_action x) \<and> traceCorrect ys"
  by (auto simp add: traceCorrect_def)

lemma traceCorrect_empty:
"traceCorrect []"
  by (auto simp add: traceCorrect_def)

lemma show_programCorrect:
  assumes "\<And>trace s. \<lbrakk>initialState program ~~ trace \<leadsto>* s \<rbrakk> \<Longrightarrow> traceCorrect trace"
  shows "programCorrect program"
  by (auto simp add: assms programCorrect_def traces_def)

(*
 splits a trace into three parts

1. part until first (s, EndAtomic) on different sessions
2. part until and including (s, EndAtomic); same invocId
3. rest
*)
fun splitTrace :: "invocId \<Rightarrow> ('proc, 'op, 'any) trace \<Rightarrow> (('proc, 'op, 'any) trace \<times> ('proc, 'op, 'any) trace \<times> ('proc, 'op, 'any) trace)" where
  "splitTrace s [] = ([],[],[])"
| "splitTrace s ((sa, a)#tr) = (
    if s = sa then
      if a = AEndAtomic then
        ([], [(sa,a)], tr)
      else
        let (h, c, t) = splitTrace s tr in
        (h, (sa,a)#c, t)
    else
      let (h, c, t) = splitTrace s tr in
      ((sa,a)#h, c, t)
  )"

lemma splitTrace_complete:
  "splitTrace s tr = (h,c,t) \<Longrightarrow> mset tr= mset h + mset c + mset t"
  proof (induct arbitrary: h c t rule: splitTrace.induct)
  qed (auto split: if_splits prod.splits)

lemma splitTrace_len:
  assumes a: "splitTrace s tr = (h,c,t)"
  shows "length h \<le> length tr"
    and "length c \<le> length tr"
    and "length t \<le> length tr"
  using a proof (induct arbitrary: h c t rule: splitTrace.induct)
qed (auto simp add: le_SucI split: if_splits prod.splits)

lemma splitTrace_len2:
  assumes a: "(h,c,t) = splitTrace s tr"
  shows "length h \<le> length tr"
    and "length c \<le> length tr"
    and "length t \<le> length tr"
  using a by (metis splitTrace_len(1), metis splitTrace_len(2), metis splitTrace_len(3))

declare splitTrace.simps[simp del]

function (sequential) compactTrace :: "invocId \<Rightarrow> ('proc, 'op, 'any) trace \<Rightarrow> ('proc, 'op, 'any) trace" where
  compactTrace_empty:
  "compactTrace s [] = []"
| compactTrace_step:
  "compactTrace s ((sa, a)#tr) = (
    if s = sa \<and> isABeginAtomic a then
      let (h, c, t) = splitTrace s tr in
      h @ (sa,a)#c @ compactTrace s t
    else
      (sa, a) # compactTrace s tr
  )"
by pat_completeness auto
termination
  by (lexicographic_order simp add: splitTrace_len2 )

lemma compactTrace_complete:
  "mset (compactTrace s tr) = mset tr"
proof (induct rule: compactTrace.induct)
qed (auto simp add: splitTrace_complete split: prod.splits)

declare compactTrace_step[simp del]

lemma steps_appendBack:
  "(A ~~ tr @ [a] \<leadsto>* C) \<longleftrightarrow> (\<exists>B. (A ~~ tr \<leadsto>* B) \<and> (B ~~ a \<leadsto> C))"
  by (auto simp add: steps_step, (metis snoc_eq_iff_butlast steps.cases))

lemma steps_append:
  "(A ~~ tra@trb \<leadsto>* C) \<longleftrightarrow> (\<exists>B. (A ~~ tra \<leadsto>* B) \<and> (B ~~ trb \<leadsto>* C))"
proof (induct trb arbitrary: C rule: rev_induct)
  case Nil
  then show ?case
    by (metis append_Nil2 snoc_eq_iff_butlast steps.cases steps_refl)
next
  case (snoc a trb)
  show ?case
    by (metis (no_types, lifting) append_assoc snoc.hyps steps_appendBack)
qed

lemma steps_append2:
  assumes "A ~~ tra \<leadsto>* B"
  shows "(A ~~ tra@trb \<leadsto>* C) \<longleftrightarrow> (B ~~ trb \<leadsto>* C)"
  using assms steps_append traceDeterministic by blast

lemma steps_single: "(A ~~ [a] \<leadsto>* B) \<longleftrightarrow> (A ~~ a \<leadsto> B)"
  by (metis append_Nil steps_appendBack steps_refl traceDeterministic)

lemma steps_empty: "(A ~~ [] \<leadsto>* B) \<longleftrightarrow> (A = B)"
  using steps_refl traceDeterministic by blast

lemma steps_appendFront:
  "(A ~~ a# tr \<leadsto>* C) \<longleftrightarrow> (\<exists>B. (A ~~ a \<leadsto> B) \<and> (B ~~ tr \<leadsto>* C))"
proof -
  have "(A ~~ a# tr \<leadsto>* C)
                     = (A ~~ [a]@tr \<leadsto>* C)" by simp
  moreover have "... = (\<exists>B. (A ~~ [a] \<leadsto>* B) \<and> (B ~~ tr \<leadsto>* C))" by (rule steps_append)
  moreover have "... = (\<exists>B. (A ~~ a \<leadsto> B) \<and> (B ~~ tr \<leadsto>* C))" by (simp add: steps_single)
  ultimately show ?thesis by simp
qed

lemma move_exists_outside_and: "((\<exists>x. P x) \<and> Q) \<longleftrightarrow> (\<exists>x. P x \<and> Q) "
  by auto

lemma exists_eq_rewrite:
  shows "(\<exists>x. x = y \<and> Q x y) \<longleftrightarrow> Q y y"
  by (metis )

lemma exists_reorder1: "(\<exists>x a. P x a) \<longleftrightarrow> (\<exists>a x. P x a)"  by metis
lemma exists_reorder2: "(\<exists>x a b. P x a b) \<longleftrightarrow> (\<exists>a b x. P x a b)"  by metis
lemma exists_reorder3: "(\<exists>x a b c. P x a b c) \<longleftrightarrow> (\<exists>a b c x. P x a b c)"  by metis
lemma exists_reorder4: "(\<exists>x a b c d. P x a b c d) \<longleftrightarrow> (\<exists>a b c d x. P x a b c d)"  by metis
lemma exists_reorder5: "(\<exists>x a b c d e. P x a b c d e) \<longleftrightarrow> (\<exists>a b c d e x. P x a b c d e)"  by metis
lemma exists_reorder6: "(\<exists>x a b c d e f. P x a a b c d e f) \<longleftrightarrow> (\<exists>a a b c d e f x. P x a a b c d e f)"  by metis

method create_step_simp_rule =
  (subst steps_appendFront,
  subst step_simps,
   (subst move_exists_outside_and conj_assoc)+,
  ((subst exists_reorder6
      | subst exists_reorder5
      | subst exists_reorder4
      | subst exists_reorder3
      | subst exists_reorder2
      | subst exists_reorder1)?
    , subst exists_eq_rewrite),
  simp)

schematic_goal steps_simp_ALocal: "(A ~~ (i, ALocal ok)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_ANewId: "(A ~~ (i, ANewId n)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_ABeginAtomic: "(A ~~ (i, ABeginAtomic t newTxns)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_AEndAtomic: "(A ~~ (i, AEndAtomic)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_ADbOp: "(A ~~ (i, ADbOp c oper res)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_AInvoc: "(A ~~ (i, AInvoc procname)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_AReturn: "(A ~~ (i, AReturn res)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_ACrash: "(A ~~ (i, ACrash)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule
schematic_goal steps_simp_AInvcheck: "(A ~~ (i, AInvcheck invi)#rest \<leadsto>* B) \<longleftrightarrow> ?R"  by create_step_simp_rule

lemmas steps_simps =
  steps_simp_ALocal
  steps_simp_ANewId
  steps_simp_ABeginAtomic
  steps_simp_AEndAtomic
  steps_simp_ADbOp
  steps_simp_AInvoc
  steps_simp_AReturn
  steps_simp_ACrash
  steps_simp_AInvcheck

end

author: peterzeller

repo: repliss-isabelle


text:
(*
    Title:      Descartes Roots Test
    Author:     Wenda Li <wl302@cam.ac.uk / liwenda1990@hotmail.com>
*)

section \<open>Descartes Roots Test\<close>

theory Descartes_Roots_Test imports Budan_Fourier
begin

text \<open>The Descartes roots test is a consequence of Descartes' rule of signs:
  through counting sign variations on coefficients of a base-transformed (i.e. Taylor shifted)
  polynomial, it can over-approximate the number of real roots (counting multiplicity)
  within an interval. Its ability is similar to the Budan-Fourier theorem, but is far more
  efficient in practice. Therefore, this test is widely used in modern root isolation procedures.

  More information can be found in the wiki page about Vincent's theorem:
    @{url "https://en.wikipedia.org/wiki/Vincent%27s_theorem"}
  and Collins and Akritas's classic paper of root isolation:
    Collins, G.E., Akritas, A.G.: Polynomial real root isolation using Descarte's rule of signs. SYMSACC. 272--275 (1976).
  A more modern treatment is available from a recent implementation of isolating real roots:
    Kobel, A., Rouillier, F., Sagraloff, M.: Computing Real Roots of Real Polynomials ... and now For Real!
    Proceedings of ISSAC '16, New York, New York, USA (2016).
\<close>

lemma bij_betw_pos_interval:
  fixes a b::real
  assumes "a<b"
  shows "bij_betw (\<lambda>x. (a+b * x) / (1+x)) {x. x>0} {x. a<x \<and> x<b}"
proof (rule bij_betw_imageI)
  show "inj_on (\<lambda>x. (a + b * x) / (1 + x)) {x. 0 < x}"
    unfolding inj_on_def
    apply (auto simp add:field_simps)
    using assms crossproduct_noteq by fastforce
  have "x \<in> (\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x}" when "a < x" "x < b" for x
  proof (rule rev_image_eqI[of "(x-a)/(b-x)"])
    define bx where "bx=b-x"
    have x:"x=b-bx" unfolding bx_def by auto
    have "bx\<noteq>0" "b>a" unfolding bx_def using that by auto
    then show " x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))"
      apply (fold bx_def,unfold x)
      by (auto simp add:field_simps)
    show "(x - a) / (b - x) \<in> {x. 0 < x}" using that by auto
  qed
  then show "(\<lambda>x. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x \<and> x < b}"
    using assms by (auto simp add:divide_simps algebra_simps)
qed

lemma proots_sphere_pos_interval:
  fixes a b::real
  defines "q1\<equiv>[:a,b:]" and "q2\<equiv>[:1,1:]"
  assumes "p\<noteq>0" "a<b"
  shows "proots_count p {x. a < x \<and> x < b} = proots_count (fcompose p q1 q2) {x. 0 < x}"
  apply (rule proots_fcompose_bij_eq[OF _ \<open>p\<noteq>0\<close>])
  unfolding q1_def q2_def using bij_betw_pos_interval[OF \<open>a<b\<close>] \<open>a<b\<close>
  by (auto simp add:algebra_simps infinite_UNIV_char_0)

definition descartes_roots_test::"real \<Rightarrow> real \<Rightarrow> real poly \<Rightarrow> nat" where
  "descartes_roots_test a b p = nat (changes (coeffs (fcompose p [:a,b:] [:1,1:])))"

theorem descartes_roots_test:
  fixes p::"real poly"
  assumes "p\<noteq>0" "a<b"
  shows "proots_count p {x. a < x \<and> x <b} \<le> descartes_roots_test a b p  \<and>
          even (descartes_roots_test a b p - proots_count p {x. a < x \<and> x < b})"
proof -
  define q where "q=fcompose p [:a,b:] [:1,1:]"
  have "q\<noteq>0"
    unfolding q_def
    apply (rule fcompose_nzero[OF \<open>p\<noteq>0\<close>])
    using \<open>a<b\<close> infinite_UNIV_char_0 by auto
  have "proots_count p {x. a < x \<and> x <b} = proots_count q {x. 0 < x}"
    using proots_sphere_pos_interval[OF \<open>p\<noteq>0\<close> \<open>a<b\<close>,folded q_def] .
  moreover have "int (proots_count q {x. 0 < x}) \<le> changes (coeffs q) \<and>
          even (changes (coeffs q) - int (proots_count q {x. 0 < x}))"
    by (rule descartes_sign[OF \<open>q\<noteq>0\<close>])
  then have "proots_count q {x. 0 < x} \<le> nat (changes (coeffs q)) \<and>
          even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})"
    using even_nat_iff by auto
  ultimately show ?thesis
    unfolding descartes_roots_test_def
    apply (fold q_def)
    by auto
qed

text \<open>The roots test @{term descartes_roots_test} is exact if its result is 0 or 1.\<close>

corollary descartes_roots_test_zero:
  fixes p::"real poly"
  assumes "p\<noteq>0" "a<b" "descartes_roots_test a b p = 0"
  shows "\<forall>x. a<x \<and> x<b \<longrightarrow> poly p x\<noteq>0"
proof -
  have "proots_count p {x. a < x \<and> x <b} = 0"
    using descartes_roots_test[OF assms(1,2)] assms(3) by auto
  from proots_count_0_imp_empty[OF this \<open>p\<noteq>0\<close>]
  show ?thesis by auto
qed

corollary descartes_roots_test_one:
  fixes p::"real poly"
  assumes "p\<noteq>0" "a<b" "descartes_roots_test a b p = 1"
  shows "proots_count p {x. a < x \<and> x <b} = 1"
  using descartes_roots_test[OF \<open>p\<noteq>0\<close> \<open>a<b\<close>] \<open>descartes_roots_test a b p = 1\<close>
  by (metis dvd_diffD even_zero le_neq_implies_less less_one odd_one)

text \<open>Similar to the Budan-Fourier theorem, the Descartes roots test result is exact when all roots
      are real.\<close>
corollary descartes_roots_test_real:
  fixes p::"real poly"
  assumes "p\<noteq>0" "a<b"
  assumes "all_roots_real p"
  shows "proots_count p {x. a < x \<and> x <b} = descartes_roots_test a b p"
proof -
  define q where "q=fcompose p [:a,b:] [:1,1:]"
  have "q\<noteq>0"
    unfolding q_def
    apply (rule fcompose_nzero[OF \<open>p\<noteq>0\<close>])
    using \<open>a<b\<close> infinite_UNIV_char_0 by auto
  have "proots_count p {x. a < x \<and> x <b} = proots_count q {x. 0 < x}"
    using proots_sphere_pos_interval[OF \<open>p\<noteq>0\<close> \<open>a<b\<close>,folded q_def] .
  moreover have "int (proots_count q {x. 0 < x}) = changes (coeffs q)"
    apply (rule descartes_sign_real[OF \<open>q\<noteq>0\<close>])
    unfolding q_def by (rule all_real_roots_mobius[OF \<open>all_roots_real p\<close> \<open>a<b\<close>])
  then have "proots_count q {x. 0 < x} = nat (changes (coeffs q))"
    by simp
  ultimately show ?thesis unfolding descartes_roots_test_def
    apply (fold q_def)
    by auto
qed

end

repo: PSL


text:
(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(*
   Miscellaneous library definitions and lemmas.
*)

chapter "Library"

theory NICTALib
imports "~~/src/HOL/Main"
begin

(* FIXME: eliminate *)
lemma hd_map_simp:
  "b \<noteq> [] \<Longrightarrow> hd (map a b) = a (hd b)"
  by (rule hd_map)

(* FIXME: could be added to Set.thy *)
lemma Collect_eq:
  "{x. P x} = {x. Q x} \<longleftrightarrow> (\<forall>x. P x = Q x)"
  by (rule iffI) auto

(* FIXME: move next to HOL.iff_allI *)
lemma iff_impI: "\<lbrakk>P \<Longrightarrow> Q = R\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) = (P \<longrightarrow> R)" by blast

definition
  fun_app :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "$" 10) where
  "f $ x \<equiv> f x"

declare fun_app_def [iff]

lemma fun_app_cong[fundef_cong]:
  "\<lbrakk> f x = f' x' \<rbrakk> \<Longrightarrow> (f $ x) = (f' $ x')"
  by simp

lemma fun_app_apply_cong[fundef_cong]:
  "f x y = f' x' y' \<Longrightarrow> (f $ x) y = (f' $ x') y'"
  by simp

lemma if_apply_cong[fundef_cong]:
  "\<lbrakk> P = P'; x = x'; P' \<Longrightarrow> f x' = f' x'; \<not> P' \<Longrightarrow> g x' = g' x' \<rbrakk>
     \<Longrightarrow> (if P then f else g) x = (if P' then f' else g') x'"
  by simp

lemma split_apply_cong[fundef_cong]:
  "\<lbrakk> f (fst p) (snd p) s = f' (fst p') (snd p') s' \<rbrakk> \<Longrightarrow> split f p s = split f' p' s'"
  by (simp add: split_def)

definition
  pred_conj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "and" 35)
where
  "pred_conj P Q \<equiv> \<lambda>x. P x \<and> Q x"

definition
  pred_disj :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" (infixl "or" 30)
where
  "pred_disj P Q \<equiv> \<lambda>x. P x \<or> Q x"

definition
  pred_neg :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)" ("not _" [40] 40)
where
  "pred_neg P \<equiv> \<lambda>x. \<not> P x"

definition "K \<equiv> \<lambda>x y. x"

definition
  zipWith :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" where
  "zipWith f xs ys \<equiv> map (split f) (zip xs ys)"

primrec
  delete :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "delete y [] = []"
| "delete y (x#xs) = (if y=x then xs else x # delete y xs)"

primrec
  find :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a option"
where
  "find f [] = None"
| "find f (x # xs) = (if f x then Some x else find f xs)"

definition
 "swp f \<equiv> \<lambda>x y. f y x"

primrec (nonexhaustive)
  theRight :: "'a + 'b \<Rightarrow> 'b" where
  "theRight (Inr x) = x"

primrec (nonexhaustive)
  theLeft :: "'a + 'b \<Rightarrow> 'a" where
  "theLeft (Inl x) = x"

definition
 "isLeft x \<equiv> (\<exists>y. x = Inl y)"

definition
 "isRight x \<equiv> (\<exists>y. x = Inr y)"

definition
 "const x \<equiv> \<lambda>y. x"

lemma tranclD2:
  "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R"
  by (erule tranclE) auto

lemma linorder_min_same1 [simp]:
  "(min y x = y) = (y \<le> (x::'a::linorder))"
  by (auto simp: min_def linorder_not_less)

lemma linorder_min_same2 [simp]:
  "(min x y = y) = (y \<le> (x::'a::linorder))"
  by (auto simp: min_def linorder_not_le)

text {* A combinator for pairing up well-formed relations.
        The divisor function splits the population in halves,
        with the True half greater than the False half, and
        the supplied relations control the order within the halves. *}

definition
  wf_sum :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
where
  "wf_sum divisor r r' \<equiv>
     ({(x, y). \<not> divisor x \<and> \<not> divisor y} \<inter> r')
   \<union>  {(x, y). \<not> divisor x \<and> divisor y}
   \<union> ({(x, y). divisor x \<and> divisor y} \<inter> r)"

lemma wf_sum_wf:
  "\<lbrakk> wf r; wf r' \<rbrakk> \<Longrightarrow> wf (wf_sum divisor r r')"
  apply (simp add: wf_sum_def)
  apply (rule wf_Un)+
      apply (erule wf_Int2)
     apply (rule wf_subset
             [where r="measure (\<lambda>x. If (divisor x) 1 0)"])
      apply simp
     apply clarsimp
    apply blast
   apply (erule wf_Int2)
  apply blast
  done

abbreviation(input)
 "option_map == map_option"

lemmas option_map_def = map_option_case

lemma False_implies_equals [simp]:
  "((False \<Longrightarrow> P) \<Longrightarrow> PROP Q) \<equiv> PROP Q"
  apply (rule equal_intr_rule)
   apply (erule meta_mp)
   apply simp
  apply simp
  done

lemma split_paired_Ball:
  "(\<forall>x \<in> A. P x) = (\<forall>x y. (x,y) \<in> A \<longrightarrow> P (x,y))"
  by auto

lemma split_paired_Bex:
  "(\<exists>x \<in> A. P x) = (\<exists>x y. (x,y) \<in> A \<and> P (x,y))"
  by auto

end

author: davidcock

repo: monads

save_path: github-repos/isabelle/davidcock-monads