text:
(*  Title:       Isabelle Collections Library
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section {* \isaheader{Specification of Sets} *}
theory SetSpec
imports ICF_Spec_Base
begin
text_raw{*\label{thy:SetSpec}*}

(*@intf Set
  @abstype 'a set
  Sets
*)

text {*
  This theory specifies set operations by means of a mapping to
  HOL's standard sets.
*}

(* Drop some notation that gets in the way here*)
(*no_notation member (infixl "mem" 55)*)
notation insert ("set'_ins")

type_synonym ('x,'s) set_\<alpha> = "'s \<Rightarrow> 'x set"
type_synonym ('x,'s) set_invar = "'s \<Rightarrow> bool"
locale set =
  -- "Abstraction to set"
  fixes \<alpha> :: "'s \<Rightarrow> 'x set"
  -- "Invariant"
  fixes invar :: "'s \<Rightarrow> bool"

locale set_no_invar = set +
  assumes invar[simp, intro!]: "\<And>s. invar s"

subsection "Basic Set Functions"

subsubsection "Empty set"

locale set_empty = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes empty :: "unit \<Rightarrow> 's"
  assumes empty_correct:
    "\<alpha> (empty ()) = {}"
    "invar (empty ())"

subsubsection "Membership Query"

locale set_memb = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes memb :: "'x \<Rightarrow> 's \<Rightarrow> bool"
  assumes memb_correct:
    "invar s \<Longrightarrow> memb x s \<longleftrightarrow> x \<in> \<alpha> s"

subsubsection "Insertion of Element"

locale set_ins = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes ins :: "'x \<Rightarrow> 's \<Rightarrow> 's"
  assumes ins_correct:
    "invar s \<Longrightarrow> \<alpha> (ins x s) = set_ins x (\<alpha> s)"
    "invar s \<Longrightarrow> invar (ins x s)"

subsubsection "Disjoint Insert"

locale set_ins_dj = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes ins_dj :: "'x \<Rightarrow> 's \<Rightarrow> 's"
  assumes ins_dj_correct:
    "\<lbrakk>invar s; x\<notin>\<alpha> s\<rbrakk> \<Longrightarrow> \<alpha> (ins_dj x s) = set_ins x (\<alpha> s)"
    "\<lbrakk>invar s; x\<notin>\<alpha> s\<rbrakk> \<Longrightarrow> invar (ins_dj x s)"

subsubsection "Deletion of Single Element"

locale set_delete = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes delete :: "'x \<Rightarrow> 's \<Rightarrow> 's"
  assumes delete_correct:
    "invar s \<Longrightarrow> \<alpha> (delete x s) = \<alpha> s - {x}"
    "invar s \<Longrightarrow> invar (delete x s)"

subsubsection "Emptiness Check"

locale set_isEmpty = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes isEmpty :: "'s \<Rightarrow> bool"
  assumes isEmpty_correct:
    "invar s \<Longrightarrow> isEmpty s \<longleftrightarrow> \<alpha> s = {}"

subsubsection "Bounded Quantifiers"

locale set_ball = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes ball :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> bool"
  assumes ball_correct: "invar S \<Longrightarrow> ball S P \<longleftrightarrow> (\<forall>x\<in>\<alpha> S. P x)"

locale set_bex = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes bex :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> bool"
  assumes bex_correct: "invar S \<Longrightarrow> bex S P \<longleftrightarrow> (\<exists>x\<in>\<alpha> S. P x)"

subsubsection "Finite Set"
locale finite_set = set +
  assumes finite[simp, intro!]: "invar s \<Longrightarrow> finite (\<alpha> s)"

subsubsection "Size"

locale set_size = finite_set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes size :: "'s \<Rightarrow> nat"
  assumes size_correct:
    "invar s \<Longrightarrow> size s = card (\<alpha> s)"

locale set_size_abort = finite_set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes size_abort :: "nat \<Rightarrow> 's \<Rightarrow> nat"
  assumes size_abort_correct:
    "invar s \<Longrightarrow> size_abort m s = min m (card (\<alpha> s))"

subsubsection "Singleton sets"

locale set_sng = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes sng :: "'x \<Rightarrow> 's"
  assumes sng_correct:
    "\<alpha> (sng x) = {x}"
    "invar (sng x)"

locale set_isSng = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes isSng :: "'s \<Rightarrow> bool"
  assumes isSng_correct:
    "invar s \<Longrightarrow> isSng s \<longleftrightarrow> (\<exists>e. \<alpha> s = {e})"
begin
  lemma isSng_correct_exists1 :
    "invar s \<Longrightarrow> (isSng s \<longleftrightarrow> (\<exists>!e. (e \<in> \<alpha> s)))"
  by (auto simp add: isSng_correct)

  lemma isSng_correct_card :
    "invar s \<Longrightarrow> (isSng s \<longleftrightarrow> (card (\<alpha> s) = 1))"
  by (auto simp add: isSng_correct card_Suc_eq)
end

subsection "Iterators"
text {*
  An iterator applies a
  function to a state and all the elements of the set.
  The function is applied in any order. Proofs over the iteration are
  done by establishing invariants over the iteration.
  Iterators may have a break-condition, that interrupts the iteration before
  the last element has been visited.
*}

(* Deprecated *)
(*
locale set_iteratei = finite_set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes iteratei :: "'s \<Rightarrow> ('x, '\<sigma>) set_iterator"

  assumes iteratei_rule: "invar S \<Longrightarrow> set_iterator (iteratei S) (\<alpha> S)"
begin
  lemma iteratei_rule_P:
    "\<lbrakk>
      invar S;
      I (\<alpha> S) \<sigma>0;
      !!x it \<sigma>. \<lbrakk> c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>);
      !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>;
      !!\<sigma> it. \<lbrakk> it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)"
   apply (rule set_iterator_rule_P [OF iteratei_rule, of S I \<sigma>0 c f P])
   apply simp_all
  done

  lemma iteratei_rule_insert_P:
    "\<lbrakk>
      invar S;
      I {} \<sigma>0;
      !!x it \<sigma>. \<lbrakk> c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (insert x it) (f x \<sigma>);
      !!\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>;
      !!\<sigma> it. \<lbrakk> it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)"
    apply (rule set_iterator_rule_insert_P [OF iteratei_rule, of S I \<sigma>0 c f P])
    apply simp_all
  done

  text {* Versions without break condition. *}
  lemma iterate_rule_P:
    "\<lbrakk>
      invar S;
      I (\<alpha> S) \<sigma>0;
      !!x it \<sigma>. \<lbrakk> x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>);
      !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S (\<lambda>_. True) f \<sigma>0)"
   apply (rule set_iterator_no_cond_rule_P [OF iteratei_rule, of S I \<sigma>0 f P])
   apply simp_all
  done

  lemma iterate_rule_insert_P:
    "\<lbrakk>
      invar S;
      I {} \<sigma>0;
      !!x it \<sigma>. \<lbrakk> x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (insert x it) (f x \<sigma>);
      !!\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S (\<lambda>_. True) f \<sigma>0)"
    apply (rule set_iterator_no_cond_rule_insert_P [OF iteratei_rule, of S I \<sigma>0 f P])
    apply simp_all
  done
end

lemma set_iteratei_I :
assumes "\<And>s. invar s \<Longrightarrow> set_iterator (iti s) (\<alpha> s)"
shows "set_iteratei \<alpha> invar iti"
proof
  fix s
  assume invar_s: "invar s"
  from assms(1)[OF invar_s] show it_OK: "set_iterator (iti s) (\<alpha> s)" .

  from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_def]]
  show "finite (\<alpha> s)" .
qed
*)

type_synonym ('x,'s) set_list_it
  = "'s \<Rightarrow> ('x,'x list) set_iterator"
locale poly_set_iteratei_defs =
  fixes list_it :: "'s \<Rightarrow> ('x,'x list) set_iterator"
begin
  definition iteratei :: "'s \<Rightarrow> ('x,'\<sigma>) set_iterator"
    where "iteratei S \<equiv> it_to_it (list_it S)"
  (*local_setup {* Locale_Code.lc_decl_del @{term iteratei} *}*)

  abbreviation "iterate s \<equiv> iteratei s (\<lambda>_. True)"
end

locale poly_set_iteratei =
  finite_set + poly_set_iteratei_defs list_it
  for list_it :: "'s \<Rightarrow> ('x,'x list) set_iterator" +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  assumes list_it_correct: "invar s \<Longrightarrow> set_iterator (list_it s) (\<alpha> s)"
begin
  lemma iteratei_correct: "invar S \<Longrightarrow> set_iterator (iteratei S) (\<alpha> S)"
    unfolding iteratei_def
    apply (rule it_to_it_correct)
    by (rule list_it_correct)

  lemma pi_iteratei[icf_proper_iteratorI]:
    "proper_it (iteratei S) (iteratei S)"
    unfolding iteratei_def
    by (intro icf_proper_iteratorI)

  lemma iteratei_rule_P:
    "\<lbrakk>
      invar S;
      I (\<alpha> S) \<sigma>0;
      !!x it \<sigma>. \<lbrakk> c \<sigma>; x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>);
      !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>;
      !!\<sigma> it. \<lbrakk> it \<subseteq> \<alpha> S; it \<noteq> {}; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)"
   apply (rule set_iterator_rule_P [OF iteratei_correct, of S I \<sigma>0 c f P])
   apply simp_all
  done

  lemma iteratei_rule_insert_P:
    "\<lbrakk>
      invar S;
      I {} \<sigma>0;
      !!x it \<sigma>. \<lbrakk> c \<sigma>; x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (insert x it) (f x \<sigma>);
      !!\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>;
      !!\<sigma> it. \<lbrakk> it \<subseteq> \<alpha> S; it \<noteq> \<alpha> S; \<not> c \<sigma>; I it \<sigma> \<rbrakk> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S c f \<sigma>0)"
    apply (rule
      set_iterator_rule_insert_P[OF iteratei_correct, of S I \<sigma>0 c f P])
    apply simp_all
  done

  text {* Versions without break condition. *}
  lemma iterate_rule_P:
    "\<lbrakk>
      invar S;
      I (\<alpha> S) \<sigma>0;
      !!x it \<sigma>. \<lbrakk> x \<in> it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (it - {x}) (f x \<sigma>);
      !!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S (\<lambda>_. True) f \<sigma>0)"
   apply (rule set_iterator_no_cond_rule_P [OF iteratei_correct, of S I \<sigma>0 f P])
   apply simp_all
  done

  lemma iterate_rule_insert_P:
    "\<lbrakk>
      invar S;
      I {} \<sigma>0;
      !!x it \<sigma>. \<lbrakk> x \<in> \<alpha> S - it; it \<subseteq> \<alpha> S; I it \<sigma> \<rbrakk> \<Longrightarrow> I (insert x it) (f x \<sigma>);
      !!\<sigma>. I (\<alpha> S) \<sigma> \<Longrightarrow> P \<sigma>
    \<rbrakk> \<Longrightarrow> P (iteratei S (\<lambda>_. True) f \<sigma>0)"
    apply (rule set_iterator_no_cond_rule_insert_P [OF iteratei_correct,
      of S I \<sigma>0 f P])
    apply simp_all
  done

end

subsection "More Set Operations"

subsubsection "Copy"
locale set_copy = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes copy :: "'s1 \<Rightarrow> 's2"
  assumes copy_correct:
    "invar1 s1 \<Longrightarrow> \<alpha>2 (copy s1) = \<alpha>1 s1"
    "invar1 s1 \<Longrightarrow> invar2 (copy s1)"

subsubsection "Union"

locale set_union = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2 + s3: set \<alpha>3 invar3
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  and \<alpha>3 :: "'s3 \<Rightarrow> 'a set" and invar3
  +
  fixes union :: "'s1 \<Rightarrow> 's2 \<Rightarrow> 's3"
  assumes union_correct:
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> \<alpha>3 (union s1 s2) = \<alpha>1 s1 \<union> \<alpha>2 s2"
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> invar3 (union s1 s2)"

locale set_union_dj =
  s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2 + s3: set \<alpha>3 invar3
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  and \<alpha>3 :: "'s3 \<Rightarrow> 'a set" and invar3
  +
  fixes union_dj :: "'s1 \<Rightarrow> 's2 \<Rightarrow> 's3"
  assumes union_dj_correct:
    "\<lbrakk>invar1 s1; invar2 s2; \<alpha>1 s1 \<inter> \<alpha>2 s2 = {}\<rbrakk> \<Longrightarrow> \<alpha>3 (union_dj s1 s2) = \<alpha>1 s1 \<union> \<alpha>2 s2"
    "\<lbrakk>invar1 s1; invar2 s2; \<alpha>1 s1 \<inter> \<alpha>2 s2 = {}\<rbrakk> \<Longrightarrow> invar3 (union_dj s1 s2)"

locale set_union_list = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes union_list :: "'s1 list \<Rightarrow> 's2"
  assumes union_list_correct:
    "\<forall>s1\<in>set l. invar1 s1 \<Longrightarrow> \<alpha>2 (union_list l) = \<Union>{\<alpha>1 s1 |s1. s1 \<in> set l}"
    "\<forall>s1\<in>set l. invar1 s1 \<Longrightarrow> invar2 (union_list l)"

subsubsection "Difference"

locale set_diff = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes diff :: "'s1 \<Rightarrow> 's2 \<Rightarrow> 's1"
  assumes diff_correct:
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> \<alpha>1 (diff s1 s2) = \<alpha>1 s1 - \<alpha>2 s2"
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> invar1 (diff s1 s2)"

subsubsection "Intersection"

locale set_inter = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2 + s3: set \<alpha>3 invar3
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  and \<alpha>3 :: "'s3 \<Rightarrow> 'a set" and invar3
  +
  fixes inter :: "'s1 \<Rightarrow> 's2 \<Rightarrow> 's3"
  assumes inter_correct:
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> \<alpha>3 (inter s1 s2) = \<alpha>1 s1 \<inter> \<alpha>2 s2"
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> invar3 (inter s1 s2)"

subsubsection "Subset"

locale set_subset = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes subset :: "'s1 \<Rightarrow> 's2 \<Rightarrow> bool"
  assumes subset_correct:
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> subset s1 s2 \<longleftrightarrow> \<alpha>1 s1 \<subseteq> \<alpha>2 s2"

subsubsection "Equal"

locale set_equal = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes equal :: "'s1 \<Rightarrow> 's2 \<Rightarrow> bool"
  assumes equal_correct:
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> equal s1 s2 \<longleftrightarrow> \<alpha>1 s1 = \<alpha>2 s2"

subsubsection "Image and Filter"

locale set_image_filter = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'b set" and invar2
  +
  fixes image_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 's1 \<Rightarrow> 's2"
  assumes image_filter_correct_aux:
    "invar1 s \<Longrightarrow> \<alpha>2 (image_filter f s) = { b . \<exists>a\<in>\<alpha>1 s. f a = Some b }"
    "invar1 s \<Longrightarrow> invar2 (image_filter f s)"
begin
  -- "This special form will be checked first by the simplifier: "
  lemma image_filter_correct_aux2:
    "invar1 s \<Longrightarrow>
    \<alpha>2 (image_filter (\<lambda>x. if P x then (Some (f x)) else None) s)
    = f ` {x\<in>\<alpha>1 s. P x}"
    by (auto simp add: image_filter_correct_aux)

  lemmas image_filter_correct =
    image_filter_correct_aux2 image_filter_correct_aux

end

locale set_inj_image_filter = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'b set" and invar2
  +
  fixes inj_image_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 's1 \<Rightarrow> 's2"
  assumes inj_image_filter_correct:
    "\<lbrakk>invar1 s; inj_on f (\<alpha>1 s \<inter> dom f)\<rbrakk> \<Longrightarrow> \<alpha>2 (inj_image_filter f s) = { b . \<exists>a\<in>\<alpha>1 s. f a = Some b }"
    "\<lbrakk>invar1 s; inj_on f (\<alpha>1 s \<inter> dom f)\<rbrakk> \<Longrightarrow> invar2 (inj_image_filter f s)"

subsubsection "Image"

locale set_image = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'b set" and invar2
  +
  fixes image :: "('a \<Rightarrow> 'b) \<Rightarrow> 's1 \<Rightarrow> 's2"
  assumes image_correct:
    "invar1 s \<Longrightarrow> \<alpha>2 (image f s) = f`\<alpha>1 s"
    "invar1 s \<Longrightarrow> invar2 (image f s)"

locale set_inj_image = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'b set" and invar2
  +
  fixes inj_image :: "('a \<Rightarrow> 'b) \<Rightarrow> 's1 \<Rightarrow> 's2"
  assumes inj_image_correct:
    "\<lbrakk>invar1 s; inj_on f (\<alpha>1 s)\<rbrakk> \<Longrightarrow> \<alpha>2 (inj_image f s) = f`\<alpha>1 s"
    "\<lbrakk>invar1 s; inj_on f (\<alpha>1 s)\<rbrakk> \<Longrightarrow> invar2 (inj_image f s)"

subsubsection "Filter"

locale set_filter = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes filter :: "('a \<Rightarrow> bool) \<Rightarrow> 's1 \<Rightarrow> 's2"
  assumes filter_correct:
    "invar1 s \<Longrightarrow> \<alpha>2 (filter P s) = {e. e \<in> \<alpha>1 s \<and> P e}"
    "invar1 s \<Longrightarrow> invar2 (filter P s)"

subsubsection "Union of Set of Sets"

locale set_Union_image =
  s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2 + s3: set \<alpha>3 invar3
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'b set" and invar2
  and \<alpha>3 :: "'s3 \<Rightarrow> 'b set" and invar3
  +
  fixes Union_image :: "('a \<Rightarrow> 's2) \<Rightarrow> 's1 \<Rightarrow> 's3"
  assumes Union_image_correct:
    "\<lbrakk> invar1 s; !!x. x\<in>\<alpha>1 s \<Longrightarrow> invar2 (f x) \<rbrakk> \<Longrightarrow>
      \<alpha>3 (Union_image f s) = \<Union>(\<alpha>2`f`\<alpha>1 s)"
    "\<lbrakk> invar1 s; !!x. x\<in>\<alpha>1 s \<Longrightarrow> invar2 (f x) \<rbrakk> \<Longrightarrow> invar3 (Union_image f s)"

subsubsection "Disjointness Check"

locale set_disjoint = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes disjoint :: "'s1 \<Rightarrow> 's2 \<Rightarrow> bool"
  assumes disjoint_correct:
    "invar1 s1 \<Longrightarrow> invar2 s2 \<Longrightarrow> disjoint s1 s2 \<longleftrightarrow> \<alpha>1 s1 \<inter> \<alpha>2 s2 = {}"

subsubsection "Disjointness Check With Witness"

locale set_disjoint_witness = s1: set \<alpha>1 invar1 + s2: set \<alpha>2 invar2
  for \<alpha>1 :: "'s1 \<Rightarrow> 'a set" and invar1
  and \<alpha>2 :: "'s2 \<Rightarrow> 'a set" and invar2
  +
  fixes disjoint_witness :: "'s1 \<Rightarrow> 's2 \<Rightarrow> 'a option"
  assumes disjoint_witness_correct:
    "\<lbrakk>invar1 s1; invar2 s2\<rbrakk>
      \<Longrightarrow> disjoint_witness s1 s2 = None \<Longrightarrow> \<alpha>1 s1 \<inter> \<alpha>2 s2 = {}"
    "\<lbrakk>invar1 s1; invar2 s2; disjoint_witness s1 s2 = Some a\<rbrakk>
      \<Longrightarrow> a\<in>\<alpha>1 s1 \<inter> \<alpha>2 s2"
begin
  lemma disjoint_witness_None: "\<lbrakk>invar1 s1; invar2 s2\<rbrakk>
    \<Longrightarrow> disjoint_witness s1 s2 = None \<longleftrightarrow> \<alpha>1 s1 \<inter> \<alpha>2 s2 = {}"
    by (case_tac "disjoint_witness s1 s2")
       (auto dest: disjoint_witness_correct)

  lemma disjoint_witnessI: "\<lbrakk>
    invar1 s1;
    invar2 s2;
    \<alpha>1 s1 \<inter> \<alpha>2 s2 \<noteq> {};
    !!a. \<lbrakk>disjoint_witness s1 s2 = Some a\<rbrakk> \<Longrightarrow> P
                            \<rbrakk> \<Longrightarrow> P"
    by (case_tac "disjoint_witness s1 s2")
       (auto dest: disjoint_witness_correct)

end

subsubsection "Selection of Element"

locale set_sel = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes sel :: "'s \<Rightarrow> ('x \<Rightarrow> 'r option) \<Rightarrow> 'r option"
  assumes selE:
    "\<lbrakk> invar s; x\<in>\<alpha> s; f x = Some r;
       !!x r. \<lbrakk>sel s f = Some r; x\<in>\<alpha> s; f x = Some r \<rbrakk> \<Longrightarrow> Q
     \<rbrakk> \<Longrightarrow> Q"
  assumes selI: "\<lbrakk>invar s; \<forall>x\<in>\<alpha> s. f x = None \<rbrakk> \<Longrightarrow> sel s f = None"
begin

  lemma sel_someD:
    "\<lbrakk> invar s; sel s f = Some r; !!x. \<lbrakk>x\<in>\<alpha> s; f x = Some r\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
    apply (cases "\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r")
    apply (safe)
    apply (erule_tac f=f and x=x in selE)
    apply auto
    apply (drule (1) selI)
    apply simp
    done

  lemma sel_noneD:
    "\<lbrakk> invar s; sel s f = None; x\<in>\<alpha> s \<rbrakk> \<Longrightarrow> f x = None"
    apply (cases "\<exists>x\<in>\<alpha> s. \<exists>r. f x = Some r")
    apply (safe)
    apply (erule_tac f=f and x=xa in selE)
    apply auto
    done
end

-- "Selection of element (without mapping)"
locale set_sel' = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes sel' :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> 'x option"
  assumes sel'E:
    "\<lbrakk> invar s; x\<in>\<alpha> s; P x;
       !!x. \<lbrakk>sel' s P = Some x; x\<in>\<alpha> s; P x \<rbrakk> \<Longrightarrow> Q
     \<rbrakk> \<Longrightarrow> Q"
  assumes sel'I: "\<lbrakk>invar s; \<forall>x\<in>\<alpha> s. \<not> P x \<rbrakk> \<Longrightarrow> sel' s P = None"
begin

  lemma sel'_someD:
    "\<lbrakk> invar s; sel' s P = Some x \<rbrakk> \<Longrightarrow> x\<in>\<alpha> s \<and> P x"
    apply (cases "\<exists>x\<in>\<alpha> s. P x")
    apply (safe)
    apply (erule_tac P=P and x=xa in sel'E)
    apply auto
    apply (erule_tac P=P and x=xa in sel'E)
    apply auto
    apply (drule (1) sel'I)
    apply simp
    apply (drule (1) sel'I)
    apply simp
    done

  lemma sel'_noneD:
    "\<lbrakk> invar s; sel' s P = None; x\<in>\<alpha> s \<rbrakk> \<Longrightarrow> \<not>P x"
    apply (cases "\<exists>x\<in>\<alpha> s. P x")
    apply (safe)
    apply (erule_tac P=P and x=xa in sel'E)
    apply auto
    done
end

subsubsection "Conversion of Set to List"

locale set_to_list = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes to_list :: "'s \<Rightarrow> 'x list"
  assumes to_list_correct:
    "invar s \<Longrightarrow> set (to_list s) = \<alpha> s"
    "invar s \<Longrightarrow> distinct (to_list s)"

subsubsection "Conversion of List to Set"

locale list_to_set = set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x set"
  fixes to_set :: "'x list \<Rightarrow> 's"
  assumes to_set_correct:
    "\<alpha> (to_set l) = set l"
    "invar (to_set l)"

subsection "Ordered Sets"

  locale ordered_set = set \<alpha> invar
    for \<alpha> :: "'s \<Rightarrow> ('u::linorder) set" and invar

  locale ordered_finite_set = finite_set \<alpha> invar + ordered_set \<alpha> invar
    for \<alpha> :: "'s \<Rightarrow> ('u::linorder) set" and invar

subsubsection "Ordered Iteration"
  (* Deprecated *)
(*  locale set_iterateoi = ordered_finite_set \<alpha> invar
    for \<alpha> :: "'s \<Rightarrow> ('u::linorder) set" and invar
    +
    fixes iterateoi :: "'s \<Rightarrow> ('u,'\<sigma>) set_iterator"
    assumes iterateoi_rule:
      "invar s \<Longrightarrow> set_iterator_linord (iterateoi s) (\<alpha> s)"
  begin
    lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I (\<alpha> m) \<sigma>0"
      assumes IP: "!!k it \<sigma>. \<lbrakk>
        c \<sigma>;
        k \<in> it;
        \<forall>j\<in>it. k\<le>j;
        \<forall>j\<in>\<alpha> m - it. j\<le>k;
        it \<subseteq> \<alpha> m;
        I it \<sigma>
      \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
      assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      assumes II: "!!\<sigma> it. \<lbrakk>
        it \<subseteq> \<alpha> m;
        it \<noteq> {};
        \<not> c \<sigma>;
        I it \<sigma>;
        \<forall>k\<in>it. \<forall>j\<in>\<alpha> m - it. j\<le>k
      \<rbrakk> \<Longrightarrow> P \<sigma>"
      shows "P (iterateoi m c f \<sigma>0)"
    using set_iterator_linord_rule_P [OF iterateoi_rule, OF MINV, of I \<sigma>0 c f P,
       OF I0 _ IF] IP II
    by simp

    lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
      assumes MINV: "invar m"
      assumes I0: "I ((\<alpha> m)) \<sigma>0"
      assumes IP: "!!k it \<sigma>. \<lbrakk> k \<in> it; \<forall>j\<in>it. k\<le>j; \<forall>j\<in>(\<alpha> m) - it. j\<le>k; it \<subseteq> (\<alpha> m); I it \<sigma> \<rbrakk>
                  \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
      assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
    shows "P (iterateoi m (\<lambda>_. True) f \<sigma>0)"
      apply (rule iterateoi_rule_P [where I = I])
      apply (simp_all add: assms)
    done
  end

  lemma set_iterateoi_I :
  assumes "\<And>s. invar s \<Longrightarrow> set_iterator_linord (itoi s) (\<alpha> s)"
  shows "set_iterateoi \<alpha> invar itoi"
  proof
    fix s
    assume invar_s: "invar s"
    from assms(1)[OF invar_s] show it_OK: "set_iterator_linord (itoi s) (\<alpha> s)" .

    from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_linord_def]]
    show "finite (\<alpha> s)" by simp
  qed

  (* Deprecated *)
  locale set_reverse_iterateoi = ordered_finite_set \<alpha> invar
    for \<alpha> :: "'s \<Rightarrow> ('u::linorder) set" and invar
    +
    fixes reverse_iterateoi :: "'s \<Rightarrow> ('u,'\<sigma>) set_iterator"
    assumes reverse_iterateoi_rule: "
      invar m \<Longrightarrow> set_iterator_rev_linord (reverse_iterateoi m) (\<alpha> m)"
  begin
    lemma reverse_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
      assumes MINV: "invar m"
      assumes I0: "I ((\<alpha> m)) \<sigma>0"
      assumes IP: "!!k it \<sigma>. \<lbrakk>
        c \<sigma>;
        k \<in> it;
        \<forall>j\<in>it. k\<ge>j;
        \<forall>j\<in>(\<alpha> m) - it. j\<ge>k;
        it \<subseteq> (\<alpha> m);
        I it \<sigma>
      \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
      assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
      assumes II: "!!\<sigma> it. \<lbrakk>
        it \<subseteq> (\<alpha> m);
        it \<noteq> {};
        \<not> c \<sigma>;
        I it \<sigma>;
        \<forall>k\<in>it. \<forall>j\<in>(\<alpha> m) - it. j\<ge>k
      \<rbrakk> \<Longrightarrow> P \<sigma>"
    shows "P (reverse_iterateoi m c f \<sigma>0)"
    using set_iterator_rev_linord_rule_P [OF reverse_iterateoi_rule, OF MINV, of I \<sigma>0 c f P,
       OF I0 _ IF] IP II
    by simp

    lemma reverse_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
      assumes MINV: "invar m"
      assumes I0: "I ((\<alpha> m)) \<sigma>0"
      assumes IP: "!!k it \<sigma>. \<lbrakk>
        k \<in> it;
        \<forall>j\<in>it. k\<ge>j;
        \<forall>j\<in> (\<alpha> m) - it. j\<ge>k;
        it \<subseteq> (\<alpha> m);
        I it \<sigma>
      \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
      assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
    shows "P (reverse_iterateoi m (\<lambda>_. True) f \<sigma>0)"
      apply (rule reverse_iterateoi_rule_P [where I = I])
      apply (simp_all add: assms)
    done
  end

  lemma set_reverse_iterateoi_I :
  assumes "\<And>s. invar s \<Longrightarrow> set_iterator_rev_linord (itoi s) (\<alpha> s)"
  shows "set_reverse_iterateoi \<alpha> invar itoi"
  proof
    fix s
    assume invar_s: "invar s"
    from assms(1)[OF invar_s] show it_OK: "set_iterator_rev_linord (itoi s) (\<alpha> s)" .

    from set_iterator_genord.finite_S0 [OF it_OK[unfolded set_iterator_rev_linord_def]]
    show "finite (\<alpha> s)" by simp
  qed
*)

locale poly_set_iterateoi_defs =
  fixes olist_it :: "'s \<Rightarrow> ('x,'x list) set_iterator"
begin
  definition iterateoi :: "'s \<Rightarrow> ('x,'\<sigma>) set_iterator"
    where "iterateoi S \<equiv> it_to_it (olist_it S)"
  (*local_setup {* Locale_Code.lc_decl_del @{term iterateoi} *}*)

  abbreviation "iterateo s \<equiv> iterateoi s (\<lambda>_. True)"
end

locale poly_set_iterateoi =
  finite_set \<alpha> invar + poly_set_iterateoi_defs list_ordered_it
  for \<alpha> :: "'s \<Rightarrow> 'x::linorder set"
  and invar
  and list_ordered_it :: "'s \<Rightarrow> ('x,'x list) set_iterator" +
  assumes list_ordered_it_correct: "invar x
    \<Longrightarrow> set_iterator_linord (list_ordered_it x) (\<alpha> x)"
begin
  lemma iterateoi_correct:
    "invar S \<Longrightarrow> set_iterator_linord (iterateoi S) (\<alpha> S)"
    unfolding iterateoi_def
    apply (rule it_to_it_linord_correct)
    by (rule list_ordered_it_correct)

  lemma pi_iterateoi[icf_proper_iteratorI]:
    "proper_it (iterateoi S) (iterateoi S)"
    unfolding iterateoi_def
    by (intro icf_proper_iteratorI)

  lemma iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
    assumes MINV: "invar s"
    assumes I0: "I (\<alpha> s) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk>
      c \<sigma>;
      k \<in> it;
      \<forall>j\<in>it. k\<le>j;
      \<forall>j\<in>\<alpha> s - it. j\<le>k;
      it \<subseteq> \<alpha> s;
      I it \<sigma>
    \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
    assumes II: "!!\<sigma> it. \<lbrakk>
      it \<subseteq> \<alpha> s;
      it \<noteq> {};
      \<not> c \<sigma>;
      I it \<sigma>;
      \<forall>k\<in>it. \<forall>j\<in>\<alpha> s - it. j\<le>k
    \<rbrakk> \<Longrightarrow> P \<sigma>"
    shows "P (iterateoi s c f \<sigma>0)"
  using set_iterator_linord_rule_P [OF iterateoi_correct,
    OF MINV, of I \<sigma>0 c f P, OF I0 _ IF] IP II
  by simp

  lemma iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
    assumes MINV: "invar s"
    assumes I0: "I ((\<alpha> s)) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk> k \<in> it; \<forall>j\<in>it. k\<le>j;
        \<forall>j\<in>(\<alpha> s) - it. j\<le>k; it \<subseteq> (\<alpha> s); I it \<sigma> \<rbrakk>
      \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
  shows "P (iterateo s f \<sigma>0)"
    apply (rule iterateoi_rule_P [where I = I])
    apply (simp_all add: assms)
  done
end

locale poly_set_rev_iterateoi_defs =
  fixes list_rev_it :: "'s \<Rightarrow> ('x::linorder,'x list) set_iterator"
begin
  definition rev_iterateoi :: "'s \<Rightarrow> ('x,'\<sigma>) set_iterator"
    where "rev_iterateoi S \<equiv> it_to_it (list_rev_it S)"
  (*local_setup {* Locale_Code.lc_decl_del @{term rev_iterateoi} *}*)

  abbreviation "rev_iterateo m \<equiv> rev_iterateoi m (\<lambda>_. True)"
  abbreviation "reverse_iterateoi \<equiv> rev_iterateoi"
  abbreviation "reverse_iterateo \<equiv> rev_iterateo"
end

locale poly_set_rev_iterateoi =
  finite_set \<alpha> invar + poly_set_rev_iterateoi_defs list_rev_it
  for \<alpha> :: "'s \<Rightarrow> 'x::linorder set"
  and invar
  and list_rev_it :: "'s \<Rightarrow> ('x,'x list) set_iterator" +
  assumes list_rev_it_correct:
    "invar s \<Longrightarrow> set_iterator_rev_linord (list_rev_it s) (\<alpha> s)"
begin
  lemma rev_iterateoi_correct:
    "invar S \<Longrightarrow> set_iterator_rev_linord (rev_iterateoi S) (\<alpha> S)"
    unfolding rev_iterateoi_def
    apply (rule it_to_it_rev_linord_correct)
    by (rule list_rev_it_correct)

  lemma pi_rev_iterateoi[icf_proper_iteratorI]:
    "proper_it (rev_iterateoi S) (rev_iterateoi S)"
    unfolding rev_iterateoi_def
    by (intro icf_proper_iteratorI)

  lemma rev_iterateoi_rule_P[case_names minv inv0 inv_pres i_complete i_inter]:
    assumes MINV: "invar s"
    assumes I0: "I ((\<alpha> s)) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk>
      c \<sigma>;
      k \<in> it;
      \<forall>j\<in>it. k\<ge>j;
      \<forall>j\<in>(\<alpha> s) - it. j\<ge>k;
      it \<subseteq> (\<alpha> s);
      I it \<sigma>
    \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
    assumes II: "!!\<sigma> it. \<lbrakk>
      it \<subseteq> (\<alpha> s);
      it \<noteq> {};
      \<not> c \<sigma>;
      I it \<sigma>;
      \<forall>k\<in>it. \<forall>j\<in>(\<alpha> s) - it. j\<ge>k
    \<rbrakk> \<Longrightarrow> P \<sigma>"
  shows "P (rev_iterateoi s c f \<sigma>0)"
  using set_iterator_rev_linord_rule_P [OF rev_iterateoi_correct,
    OF MINV, of I \<sigma>0 c f P, OF I0 _ IF] IP II
  by simp

  lemma reverse_iterateo_rule_P[case_names minv inv0 inv_pres i_complete]:
    assumes MINV: "invar s"
    assumes I0: "I ((\<alpha> s)) \<sigma>0"
    assumes IP: "!!k it \<sigma>. \<lbrakk>
      k \<in> it;
      \<forall>j\<in>it. k\<ge>j;
      \<forall>j\<in> (\<alpha> s) - it. j\<ge>k;
      it \<subseteq> (\<alpha> s);
      I it \<sigma>
    \<rbrakk> \<Longrightarrow> I (it - {k}) (f k \<sigma>)"
    assumes IF: "!!\<sigma>. I {} \<sigma> \<Longrightarrow> P \<sigma>"
  shows "P (rev_iterateo s f \<sigma>0)"
    apply (rule rev_iterateoi_rule_P [where I = I])
    apply (simp_all add: assms)
  done

end

subsubsection "Minimal and Maximal Element"

  locale set_min = ordered_set +
    constrains \<alpha> :: "'s \<Rightarrow> 'u::linorder set"
    fixes min :: "'s \<Rightarrow> ('u \<Rightarrow> bool) \<Rightarrow> 'u option"
    assumes min_correct:
      "\<lbrakk> invar s; x\<in>\<alpha> s; P x \<rbrakk> \<Longrightarrow> min s P \<in> Some ` {x\<in>\<alpha> s. P x}"
      "\<lbrakk> invar s; x\<in>\<alpha> s; P x \<rbrakk> \<Longrightarrow> (the (min s P)) \<le> x"
      "\<lbrakk> invar s; {x\<in>\<alpha> s. P x} = {} \<rbrakk> \<Longrightarrow> min s P = None"
  begin
   lemma minE:
     assumes A: "invar s" "x\<in>\<alpha> s" "P x"
     obtains x' where
     "min s P = Some x'" "x'\<in>\<alpha> s" "P x'" "\<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<le> x"
   proof -
     from min_correct(1)[of s x P, OF A] have
       MIS: "min s P \<in> Some ` {x \<in> \<alpha> s. P x}" .
     then obtain x' where KV: "min s P = Some x'" "x'\<in>\<alpha> s" "P x'"
       by auto
     show thesis
       apply (rule that[OF KV])
       apply (clarify)
       apply (drule (1) min_correct(2)[OF `invar s`])
       apply (simp add: KV(1))
       done
   qed

   lemmas minI = min_correct(3)

   lemma min_Some:
     "\<lbrakk> invar s; min s P = Some x \<rbrakk> \<Longrightarrow> x\<in>\<alpha> s"
     "\<lbrakk> invar s; min s P = Some x \<rbrakk> \<Longrightarrow> P x"
     "\<lbrakk> invar s; min s P = Some x; x'\<in>\<alpha> s; P x'\<rbrakk> \<Longrightarrow> x\<le>x'"
     apply -
     apply (cases "{x \<in> \<alpha> s. P x} = {}")
     apply (drule (1) min_correct(3))
     apply simp
     apply simp
     apply (erule exE)
     apply clarify
     apply (drule (2) min_correct(1)[of s _ P])
     apply auto [1]

     apply (cases "{x \<in> \<alpha> s. P x} = {}")
     apply (drule (1) min_correct(3))
     apply simp
     apply simp
     apply (erule exE)
     apply clarify
     apply (drule (2) min_correct(1)[of s _ P])
     apply auto [1]

     apply (drule (2) min_correct(2)[where P=P])
     apply auto
     done

   lemma min_None:
     "\<lbrakk> invar s; min s P = None \<rbrakk> \<Longrightarrow> {x\<in>\<alpha> s. P x} = {}"
     apply (cases "{x\<in>\<alpha> s. P x} = {}")
     apply simp
     apply simp
     apply (erule exE)
     apply clarify
     apply (drule (2) min_correct(1)[where P=P])
     apply auto
     done

  end

  locale set_max = ordered_set +
    constrains \<alpha> :: "'s \<Rightarrow> 'u::linorder set"
    fixes max :: "'s \<Rightarrow> ('u \<Rightarrow> bool) \<Rightarrow> 'u option"
    assumes max_correct:
      "\<lbrakk> invar s; x\<in>\<alpha> s; P x \<rbrakk> \<Longrightarrow> max s P \<in> Some ` {x\<in>\<alpha> s. P x}"
      "\<lbrakk> invar s; x\<in>\<alpha> s; P x \<rbrakk> \<Longrightarrow> the (max s P) \<ge> x"
      "\<lbrakk> invar s; {x\<in>\<alpha> s. P x} = {} \<rbrakk> \<Longrightarrow> max s P = None"
  begin
   lemma maxE:
     assumes A: "invar s" "x\<in>\<alpha> s" "P x"
     obtains x' where
     "max s P = Some x'" "x'\<in>\<alpha> s" "P x'" "\<forall>x\<in>\<alpha> s. P x \<longrightarrow> x' \<ge> x"
   proof -
     from max_correct(1)[where P=P, OF A] have
       MIS: "max s P \<in> Some ` {x\<in>\<alpha> s. P x}" .
     then obtain x' where KV: "max s P = Some x'" "x'\<in> \<alpha> s" "P x'"
       by auto
     show thesis
       apply (rule that[OF KV])
       apply (clarify)
       apply (drule (1) max_correct(2)[OF `invar s`])
       apply (simp add: KV(1))
       done
   qed

   lemmas maxI = max_correct(3)

     apply (cases "{x\<in>\<alpha> s. P x} = {}")
     apply (drule (1) max_correct(3))
     apply simp
     apply simp
     apply (erule exE)
     apply clarify
     apply (drule (2) max_correct(1)[of s _ P])
     apply auto [1]

     apply (drule (1) max_correct(2)[where P=P])
     apply auto
     done

   lemma max_None:
     "\<lbrakk> invar s; max s P = None \<rbrakk> \<Longrightarrow> {x\<in>\<alpha> s. P x} = {}"
     apply (cases "{x\<in>\<alpha> s. P x} = {}")
     apply simp
     apply simp
     apply (erule exE)
     apply clarify
     apply (drule (1) max_correct(1)[where P=P])
     apply auto
     done

  end

subsection "Conversion to List"
  locale set_to_sorted_list = ordered_set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x::linorder set"
  fixes to_sorted_list :: "'s \<Rightarrow> 'x list"
  assumes to_sorted_list_correct:
    "invar s \<Longrightarrow> set (to_sorted_list s) = \<alpha> s"
    "invar s \<Longrightarrow> distinct (to_sorted_list s)"
    "invar s \<Longrightarrow> sorted (to_sorted_list s)"

  locale set_to_rev_list = ordered_set +
  constrains \<alpha> :: "'s \<Rightarrow> 'x::linorder set"
  fixes to_rev_list :: "'s \<Rightarrow> 'x list"
  assumes to_rev_list_correct:
    "invar s \<Longrightarrow> set (to_rev_list s) = \<alpha> s"
    "invar s \<Longrightarrow> distinct (to_rev_list s)"
    "invar s \<Longrightarrow> sorted (rev (to_rev_list s))"

subsection "Record Based Interface"
  record ('x,'s) set_ops =
    set_op_\<alpha> :: "'s \<Rightarrow> 'x set"
    set_op_invar :: "'s \<Rightarrow> bool"
    set_op_empty :: "unit \<Rightarrow> 's"
    set_op_memb :: "'x \<Rightarrow> 's \<Rightarrow> bool"
    set_op_ins :: "'x \<Rightarrow> 's \<Rightarrow> 's"
    set_op_ins_dj :: "'x \<Rightarrow> 's \<Rightarrow> 's"
    set_op_delete :: "'x \<Rightarrow> 's \<Rightarrow> 's"
    set_op_list_it :: "('x,'s) set_list_it"
    set_op_sng :: "'x \<Rightarrow> 's"
    set_op_isEmpty :: "'s \<Rightarrow> bool"
    set_op_isSng :: "'s \<Rightarrow> bool"
    set_op_ball :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> bool"
    set_op_bex :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> bool"
    set_op_size :: "'s \<Rightarrow> nat"
    set_op_size_abort :: "nat \<Rightarrow> 's \<Rightarrow> nat"
    set_op_union :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    set_op_union_dj :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    set_op_diff :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    set_op_filter :: "('x \<Rightarrow> bool) \<Rightarrow> 's \<Rightarrow> 's"
    set_op_inter :: "'s \<Rightarrow> 's \<Rightarrow> 's"
    set_op_subset :: "'s \<Rightarrow> 's \<Rightarrow> bool"
    set_op_equal :: "'s \<Rightarrow> 's \<Rightarrow> bool"
    set_op_disjoint :: "'s \<Rightarrow> 's \<Rightarrow> bool"
    set_op_disjoint_witness :: "'s \<Rightarrow> 's \<Rightarrow> 'x option"
    set_op_sel :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> 'x option" -- "Version without mapping"
    set_op_to_list :: "'s \<Rightarrow> 'x list"
    set_op_from_list :: "'x list \<Rightarrow> 's"

  locale StdSetDefs =
    poly_set_iteratei_defs "set_op_list_it ops"
    for ops :: "('x,'s,'more) set_ops_scheme"
  begin
    abbreviation \<alpha> where "\<alpha> == set_op_\<alpha> ops"
    abbreviation invar where "invar == set_op_invar ops"
    abbreviation empty where "empty == set_op_empty ops"
    abbreviation memb where "memb == set_op_memb ops"
    abbreviation ins where "ins == set_op_ins ops"
    abbreviation ins_dj where "ins_dj == set_op_ins_dj ops"
    abbreviation delete where "delete == set_op_delete ops"
    abbreviation list_it where "list_it \<equiv> set_op_list_it ops"
    abbreviation sng where "sng == set_op_sng ops"
    abbreviation isEmpty where "isEmpty == set_op_isEmpty ops"
    abbreviation isSng where "isSng == set_op_isSng ops"
    abbreviation ball where "ball == set_op_ball ops"
    abbreviation bex where "bex == set_op_bex ops"
    abbreviation size where "size == set_op_size ops"
    abbreviation size_abort where "size_abort == set_op_size_abort ops"
    abbreviation union where "union == set_op_union ops"
    abbreviation union_dj where "union_dj == set_op_union_dj ops"
    abbreviation diff where "diff == set_op_diff ops"
    abbreviation filter where "filter == set_op_filter ops"
    abbreviation inter where "inter == set_op_inter ops"
    abbreviation subset where "subset == set_op_subset ops"
    abbreviation equal where "equal == set_op_equal ops"
    abbreviation disjoint where "disjoint == set_op_disjoint ops"
    abbreviation disjoint_witness
      where "disjoint_witness == set_op_disjoint_witness ops"
    abbreviation sel where "sel == set_op_sel ops"
    abbreviation to_list where "to_list == set_op_to_list ops"
    abbreviation from_list where "from_list == set_op_from_list ops"
  end

  locale StdSet = StdSetDefs ops +
    set \<alpha> invar +
    set_empty \<alpha> invar empty +
    set_memb \<alpha> invar memb +
    set_ins \<alpha> invar ins +
    set_ins_dj \<alpha> invar ins_dj +
    set_delete \<alpha> invar delete +
    poly_set_iteratei \<alpha> invar list_it +
    set_sng \<alpha> invar sng +
    set_isEmpty \<alpha> invar isEmpty +
    set_isSng \<alpha> invar isSng +
    set_ball \<alpha> invar ball +
    set_bex \<alpha> invar bex +
    set_size \<alpha> invar size +
    set_size_abort \<alpha> invar size_abort +
    set_union \<alpha> invar \<alpha> invar \<alpha> invar union +
    set_union_dj \<alpha> invar \<alpha> invar \<alpha> invar union_dj +
    set_diff \<alpha> invar \<alpha> invar diff +
    set_filter \<alpha> invar \<alpha> invar filter +
    set_inter \<alpha> invar \<alpha> invar \<alpha> invar inter +
    set_subset \<alpha> invar \<alpha> invar subset +
    set_equal \<alpha> invar \<alpha> invar equal +
    set_disjoint \<alpha> invar \<alpha> invar disjoint +
    set_disjoint_witness \<alpha> invar \<alpha> invar disjoint_witness +
    set_sel' \<alpha> invar sel +
    set_to_list \<alpha> invar to_list +
    list_to_set \<alpha> invar from_list
    for ops :: "('x,'s,'more) set_ops_scheme"
  begin

    lemmas correct =
      empty_correct
      sng_correct
      memb_correct
      ins_correct
      ins_dj_correct
      delete_correct
      isEmpty_correct
      isSng_correct
      ball_correct
      bex_correct
      size_correct
      size_abort_correct
      union_correct
      union_dj_correct
      diff_correct
      filter_correct
      inter_correct
      subset_correct
      equal_correct
      disjoint_correct
      disjoint_witness_correct
      to_list_correct
      to_set_correct

  end

  lemmas StdSet_intro = StdSet.intro[rem_dup_prems]

  locale StdSet_no_invar = StdSet + set_no_invar \<alpha> invar

  record ('x,'s) oset_ops = "('x::linorder,'s) set_ops" +
    set_op_ordered_list_it :: "'s \<Rightarrow> ('x,'x list) set_iterator"
    set_op_rev_list_it :: "'s \<Rightarrow> ('x,'x list) set_iterator"
    set_op_min :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> 'x option"
    set_op_max :: "'s \<Rightarrow> ('x \<Rightarrow> bool) \<Rightarrow> 'x option"
    set_op_to_sorted_list :: "'s \<Rightarrow> 'x list"
    set_op_to_rev_list :: "'s \<Rightarrow> 'x list"

  locale StdOSetDefs = StdSetDefs ops
    + poly_set_iterateoi_defs "set_op_ordered_list_it ops"
    + poly_set_rev_iterateoi_defs "set_op_rev_list_it ops"
    for ops :: "('x::linorder,'s,'more) oset_ops_scheme"
  begin
    abbreviation "ordered_list_it \<equiv> set_op_ordered_list_it ops"
    abbreviation "rev_list_it \<equiv> set_op_rev_list_it ops"
    abbreviation min where "min == set_op_min ops"
    abbreviation max where "max == set_op_max ops"
    abbreviation to_sorted_list where
      "to_sorted_list \<equiv> set_op_to_sorted_list ops"
    abbreviation to_rev_list where "to_rev_list \<equiv> set_op_to_rev_list ops"
  end

  locale StdOSet =
    StdOSetDefs ops +
    StdSet ops +
    poly_set_iterateoi \<alpha> invar ordered_list_it +
    poly_set_rev_iterateoi \<alpha> invar rev_list_it +
    set_min \<alpha> invar min +
    set_max \<alpha> invar max +
    set_to_sorted_list \<alpha> invar to_sorted_list +
    set_to_rev_list \<alpha> invar to_rev_list
    for ops :: "('x::linorder,'s,'more) oset_ops_scheme"
  begin
  end

  lemmas StdOSet_intro =
    StdOSet.intro[OF StdSet_intro, rem_dup_prems]

no_notation insert ("set'_ins")
(*notation member (infixl "mem" 55)*)

end

author: andredidier

repo: phd

save_path: github-repos/isabelle/andredidier-phd


text:
theory testind
imports Main
        "$HIPSTER_HOME/IsaHipster"
begin
  datatype 'a list = Nil2 | Cons2 "'a" "'a list"
  datatype ('a, 'b) Pair2 = Pair "'a" "'b"
  datatype Nat = Z | S "Nat"
  fun zip2 :: "'a list => 'b list => (('a, 'b) Pair2) list" where
  "zip2 (Nil2) y = Nil2"
  | "zip2 (Cons2 z x2) (Nil2) = Nil2"
  | "zip2 (Cons2 z x2) (Cons2 x3 x4) = Cons2 (Pair z x3) (zip2 x2 x4)"
  fun take :: "Nat => 'a list => 'a list" where
  "take (Z) y = Nil2"
  | "take (S z) (Nil2) = Nil2"
  | "take (S z) (Cons2 x2 x3) = Cons2 x2 (take z x3)"
  fun len :: "'a list => Nat" where
  "len (Nil2) = Z"
  | "len (Cons2 y xs) = S (len xs)"
  fun drop :: "Nat => 'a list => 'a list" where
  "drop (Z) y = y"
  | "drop (S z) (Nil2) = Nil2"
  | "drop (S z) (Cons2 x2 x3) = drop z x3"
  fun append :: "'a list => 'a list => 'a list" where
  "append (Nil2) y = y"
  | "append (Cons2 z xs) y = Cons2 z (append xs y)"
  (*hipster zip2 take len drop append *)

lemma lemma_a [thy_expl]: "drop x3 Nil2 = Nil2"
by (hipster_induct_simp_metis drop.simps)

lemma lemma_aa [thy_expl]: "drop (S Z) (drop x3 y3) = drop (S x3) y3"
by (hipster_induct_simp_metis drop.simps Nat.exhaust list.exhaust)

lemma lemma_ai [thy_expl]: "take x3 Nil2 = Nil2"
by (hipster_induct_simp_metis take.simps)

lemma lemma_aj [thy_expl]: "take x3 (take x3 y3) = take x3 y3"
by (hipster_induct_simp_metis take.simps Nat.exhaust list.exhaust)

lemma lemma_ak []: "take (S x3) (take x3 y3) = take x3 y3"
by (hipster_induct_simp_metis take.simps Nat.exhaust list.exhaust)

(*hipster append*)
lemma lemma_ab [thy_expl]: "append x2 Nil2 = x2"
by (hipster_induct_simp_metis append.simps)

lemma lemma_ac [thy_expl]: "append (append x2 y2) z2 =
append x2 (append y2 z2)"
by (hipster_induct_simp_metis append.simps Nat.exhaust list.exhaust)

lemma lemma_abz [thy_expl]: "zip2 Nil2 x1 = zip2 x1 Nil2"
by (hipster_induct_simp_metis zip2.simps)

lemma lemma_acz [thy_expl]: "zip2 Nil2 x1 = zip2 y1 Nil2"
by (hipster_induct_simp_metis zip2.simps)

(*hipster zip2 append take len drop*)
lemma lemma_ad [thy_expl]: "zip2 x1 (testind.append x1 y1) = zip2 x1 x1"
by (hipster_induct_simp_metis testind.zip2.simps testind.append.simps testind.take.simps testind.len.simps testind.drop.simps testind.list.exhaust testind.Pair2.exhaust testind.Nat.exhaust)

lemma lemma_ae [thy_expl]: "zip2 (testind.append x5 y5) x5 = zip2 x5 x5"
by (hipster_induct_simp_metis testind.zip2.simps testind.append.simps testind.take.simps testind.len.simps testind.drop.simps testind.list.exhaust testind.Pair2.exhaust testind.Nat.exhaust)

lemma lemma_af [thy_expl]: "testind.take (len x2) x2 = x2"
by (hipster_induct_simp_metis testind.zip2.simps testind.append.simps testind.take.simps testind.len.simps testind.drop.simps testind.list.exhaust testind.Pair2.exhaust testind.Nat.exhaust)

lemma lemma_ag [thy_expl]: "testind.drop (len x1) (testind.append x1 y1) = y1"
by (hipster_induct_simp_metis testind.zip2.simps testind.append.simps testind.take.simps testind.len.simps testind.drop.simps testind.list.exhaust testind.Pair2.exhaust testind.Nat.exhaust)

lemma lemma_ah [thy_expl]: "testind.take (len x1) (testind.append x1 y1) = x1"
by (hipster_induct_simp_metis testind.zip2.simps testind.append.simps testind.take.simps testind.len.simps testind.drop.simps testind.list.exhaust testind.Pair2.exhaust testind.Nat.exhaust)

lemma unknown [thy_expl]: "testind.drop x (testind.drop y z) = testind.drop y (testind.drop x z)"
oops

lemma unknown [thy_expl]: "testind.take x (testind.take y z) = testind.take y (testind.take x z)"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) z = zip2 y (testind.take x z)"
oops

lemma unknown [thy_expl]: "testind.drop x (testind.take x y) = testind.drop x (testind.take x z)"
oops

lemma unknown [thy_expl]: "testind.drop x (testind.take x y) = testind.drop z (testind.take z y)"
oops

lemma unknown [thy_expl]: "testind.drop x (testind.take x y) = testind.drop z (testind.take z xa)"
oops

lemma unknown [thy_expl]: "len (testind.append x y) = len (testind.append y x)"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) y = zip2 y (testind.take x y)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) x = testind.drop y (testind.take y x)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) x = testind.drop y (testind.take y z)"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) (testind.take z xa) =
zip2 (testind.take z y) (testind.take x xa)"
oops

lemma unknown [thy_expl]: "zip2 (testind.append x y) (testind.drop z x) = zip2 x (testind.drop z x)"
oops

lemma unknown [thy_expl]: "zip2 (testind.append x y) (testind.take z x) = zip2 x (testind.take z x)"
oops

lemma unknown [thy_expl]: "zip2 (testind.drop x y) (testind.append y z) = zip2 (testind.drop x y) y"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) (testind.append y z) = zip2 y (testind.take x y)"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) (testind.take x z) = zip2 y (testind.take x z)"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) (testind.take z y) =
zip2 (testind.take z y) (testind.take x y)"
oops

lemma unknown [thy_expl]: "zip2 (testind.drop x y) (testind.append y y) = zip2 (testind.drop x y) y"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) (testind.take x y) = zip2 y (testind.take x y)"
oops

lemma unknown [thy_expl]: "zip2 (testind.take x y) (testind.append y y) = zip2 y (testind.take x y)"
oops

lemma unknown [thy_expl]: "testind.append (testind.take x y) (testind.drop x y) = y"
oops

lemma unknown [thy_expl]: "zip2 (testind.append x x) (testind.drop y x) = zip2 x (testind.drop y x)"
oops

lemma unknown [thy_expl]: "zip2 (testind.append x x) (testind.take y x) = zip2 x (testind.take y x)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.drop y x) = testind.drop y (testind.take y x)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.drop y x) = testind.drop z (testind.take z x)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.take y x) = testind.drop y (testind.take y x)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.take y x) = testind.drop z (testind.take z x)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.drop y x) = testind.drop y (testind.take y z)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.drop y x) = testind.drop z (testind.take z xa)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.take y x) = testind.drop y (testind.take y z)"
oops

lemma unknown [thy_expl]: "testind.drop (len x) (testind.take y x) = testind.drop z (testind.take z xa)"
oops

lemma unknown [thy_expl]: "testind.take (len x) (testind.drop y x) = testind.drop y x"
oops

lemma unknown [thy_expl]: "testind.take (len x) (testind.take y x) = testind.take y x"
oops

theorem t: "len a = len b \<Longrightarrow> append (zip2 a b) (zip2 c d) = zip2 (append a c) (append b d)"
       apply(induction d arbitrary: a b c)
       apply simp_all
       sledgehammer
       by (hipster_induct_simp_metis zip2.simps len.simps take.simps drop.simps append.simps Nat.exhaust list.exhaust)

  theorem x0 :
    "(zip2 (append xs ys) zs) =
       (append (zip2 xs (take (len xs) zs)) (zip2 ys (drop (len xs) zs)))"
       apply(induction zs arbitrary: ys xs)
       apply simp_all

apply (metis lemma_a lemma_acz lemma_ai testind.append.simps(1) zip2.simps(1))
sledgehammer
       by (hipster_induct_simp_metis zip2.simps len.simps take.simps drop.simps append.simps Nat.exhaust list.exhaust)

end

author: moajohansson

repo: IsaHipster


text:
section "Implementing Labelled Transition Systems by a TripleSet"
theory LTSByTripleSetQAQ
imports TripleSetSpec LTSSpec LTSGA
begin

locale ltsbm_QAQ_defs =
  ts: triple_set ts_\<alpha> ts_invar
  for ts_\<alpha>::"'ts \<Rightarrow> ('Q \<times> 'A \<times> 'Q) set"
  and ts_invar
begin

  abbreviation ltsbm_\<alpha> :: "('Q,'A,'ts) lts_\<alpha>" where "ltsbm_\<alpha> \<equiv> ts_\<alpha>"
  abbreviation "ltsbm_invar \<equiv> ts_invar"

  lemma ltsbm_empty_correct:
    "triple_set_empty ts_\<alpha> ts_invar emp \<Longrightarrow>
     lts_empty ltsbm_\<alpha> ltsbm_invar emp"
    unfolding lts_empty_def triple_set_empty_def
    by simp

  lemma ltsbm_memb_correct:
    "triple_set_memb ts_\<alpha> ts_invar memb \<Longrightarrow>
     lts_memb ltsbm_\<alpha> ltsbm_invar memb"
    unfolding lts_memb_def triple_set_memb_def
    by simp

  lemma ltsbm_add_correct:
    "triple_set_add ts_\<alpha> ts_invar add \<Longrightarrow>
     lts_add ltsbm_\<alpha> ltsbm_invar add"
  unfolding lts_add_def triple_set_add_def by simp

  lemma ltsbm_add_succs_correct:
    "triple_set_add_Cl ts_\<alpha> ts_invar add_Cl \<Longrightarrow>
     lts_add_succs ltsbm_\<alpha> ltsbm_invar add_Cl"
    unfolding lts_add_succs_def triple_set_add_Cl_def by auto

  lemma ltsbm_delete_correct:
    "triple_set_delete ts_\<alpha> ts_invar ts_del \<Longrightarrow>
     lts_delete ltsbm_\<alpha> ltsbm_invar ts_del"
    unfolding lts_delete_def triple_set_delete_def by simp

  lemma ltsbm_succ_it_correct :
    assumes "triple_set_C_it ts_\<alpha> ts_invar it"
    shows "lts_succ_it ltsbm_\<alpha> ltsbm_invar it"
  using assms unfolding lts_succ_it_def triple_set_C_it_def by simp

  lemma ltsbm_succ_label_it_correct :
    assumes "triple_set_BC_it ts_\<alpha> ts_invar it"
    shows "lts_succ_label_it ltsbm_\<alpha> ltsbm_invar it"
  using assms
  unfolding lts_succ_label_it_def triple_set_BC_it_def
  by simp

  lemma ltsbm_filter_it_correct :
    assumes "triple_set_filter_it ts_\<alpha> ts_invar it"
    shows "lts_filter_it ltsbm_\<alpha> ltsbm_invar it"
  using assms
  unfolding lts_filter_it_def triple_set_filter_it_def
  by simp

  lemma ltsbm_it_correct :
    assumes "triple_set_iterator ts_\<alpha> ts_invar it"
    shows "lts_iterator ltsbm_\<alpha> ltsbm_invar it"
  using assms
  unfolding lts_iterator_def triple_set_iterator_def
  by simp

  definition ltsbm_pre_it where
   "ltsbm_pre_it it (ts::'ts) (q'::'Q) (a::'A) = it ts a q'"

  lemma ltsbm_pre_it_correct :
    assumes "triple_set_A_it ts_\<alpha> ts_invar it"
    shows "lts_pre_it ltsbm_\<alpha> ltsbm_invar (ltsbm_pre_it it)"
  using assms
  unfolding lts_pre_it_def triple_set_A_it_def ltsbm_pre_it_def
  by simp

  lemma ltsbm_pre_label_it_correct :
    assumes "triple_set_AB_it ts_\<alpha> ts_invar it"
    shows "lts_pre_label_it ltsbm_\<alpha> ltsbm_invar it"
  using assms
  unfolding lts_pre_label_it_def triple_set_AB_it_def
  by simp
end

end

author: VTrelat


text:
(*  Title:      JinjaThreads/Compiler/Correctness.thy
    Author:     Andreas Lochbihler
*)

header {* \isaheader{Correctness of both stages} *}

theory Correctness
imports
  J0Bisim
  J1Deadlock
  "../Framework/FWBisimDeadlock"
  Correctness2
  Correctness1Threaded
  Correctness1
  JJ1WellForm
  Compiler
begin

locale J_JVM_heap_conf_base =
  J0_J1_heap_base
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
  +
  J1_JVM_heap_conf_base
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    hconf "compP1 P"
  for addr2thread_id :: "('addr :: addr) \<Rightarrow> 'thread_id"
  and thread_id2addr :: "'thread_id \<Rightarrow> 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap \<Rightarrow> htype \<Rightarrow> ('heap \<times> 'addr) set"
  and typeof_addr :: "'heap \<Rightarrow> 'addr \<rightharpoonup> htype"
  and heap_read :: "'heap \<Rightarrow> 'addr \<Rightarrow> addr_loc \<Rightarrow> 'addr val \<Rightarrow> bool"
  and heap_write :: "'heap \<Rightarrow> 'addr \<Rightarrow> addr_loc \<Rightarrow> 'addr val \<Rightarrow> 'heap \<Rightarrow> bool"
  and hconf :: "'heap \<Rightarrow> bool"
  and P :: "'addr J_prog"
begin

definition bisimJ2JVM ::
  "(('addr,'thread_id,'addr expr\<times>'addr locals,'heap,'addr) state,
    ('addr,'thread_id,'addr option \<times> 'addr frame list,'heap,'addr) state) bisim"
where "bisimJ2JVM = red_red0.mbisim \<circ>\<^sub>B red0_Red1'.mbisim \<circ>\<^sub>B mbisim_Red1'_Red1 \<circ>\<^sub>B Red1_execd.mbisim"

definition tlsimJ2JVM ::
  "('thread_id \<times> ('addr, 'thread_id, 'heap) J_thread_action,
    'thread_id \<times> ('addr, 'thread_id, 'heap) jvm_thread_action) bisim"
where "tlsimJ2JVM = red_red0.mta_bisim \<circ>\<^sub>B red0_Red1'.mta_bisim \<circ>\<^sub>B op = \<circ>\<^sub>B Red1_execd.mta_bisim"

end

lemma compP2_has_method [simp]: "compP2 P \<turnstile> C has M \<longleftrightarrow> P \<turnstile> C has M"
by(auto simp add: compP2_def compP_has_method)

locale J_JVM_conf_read =
  J1_JVM_conf_read
    addr2thread_id thread_id2addr
    spurious_wakeups
    empty_heap allocate typeof_addr heap_read heap_write
    hconf "compP1 P"
  for addr2thread_id :: "('addr :: addr) \<Rightarrow> 'thread_id"
  and thread_id2addr :: "'thread_id \<Rightarrow> 'addr"
  and spurious_wakeups :: bool
  and empty_heap :: "'heap"
  and allocate :: "'heap \<Rightarrow> htype \<Rightarrow> ('heap \<times> 'addr) set"
  and typeof_addr :: "'heap \<Rightarrow> 'addr \<rightharpoonup> htype"
  and heap_read :: "'heap \<Rightarrow> 'addr \<Rightarrow> addr_loc \<Rightarrow> 'addr val \<Rightarrow> bool"
  and heap_write :: "'heap \<Rightarrow> 'addr \<Rightarrow> addr_loc \<Rightarrow> 'addr val \<Rightarrow> 'heap \<Rightarrow> bool"
  and hconf :: "'heap \<Rightarrow> bool"
  and P :: "'addr J_prog"

sublocale J_JVM_conf_read < J_JVM_heap_conf_base
by(unfold_locales)

context J_JVM_conf_read begin

theorem bisimJ2JVM_weak_bisim:
  assumes wf: "wf_J_prog P"
  shows "delay_bisimulation_diverge_final (mredT P) (execd_mthr.redT (J2JVM P)) bisimJ2JVM tlsimJ2JVM
            (red_mthr.m\<tau>move P) (execd_mthr.m\<tau>move (J2JVM P)) red_mthr.mfinal exec_mthr.mfinal"
unfolding bisimJ2JVM_def tlsimJ2JVM_def J2JVM_def o_apply
apply(rule delay_bisimulation_diverge_final_compose)
 apply(rule FWdelay_bisimulation_diverge.mthr_delay_bisimulation_diverge_final)
 apply(rule red_red0_FWbisim[OF wf_prog_wwf_prog[OF wf]])
apply(rule delay_bisimulation_diverge_final_compose)
 apply(rule FWdelay_bisimulation_diverge.mthr_delay_bisimulation_diverge_final)
 apply(rule red0_Red1'_FWweak_bisim[OF wf])
apply(rule delay_bisimulation_diverge_final_compose)
 apply(rule delay_bisimulation_diverge_final.intro)
  apply(rule bisimulation_into_delay.delay_bisimulation)
  apply(rule Red1'_Red1_bisim_into_weak[OF compP1_pres_wf[OF wf]])
 apply(rule bisimulation_final.delay_bisimulation_final_base)
 apply(rule Red1'_Red1_bisimulation_final[OF compP1_pres_wf[OF wf]])
apply(rule FWdelay_bisimulation_diverge.mthr_delay_bisimulation_diverge_final)
apply(rule Red1_exec1_FWwbisim[OF compP1_pres_wf[OF wf]])
done

lemma bisimJ2JVM_start:
  assumes wf: "wf_J_prog P"
  and start: "wf_start_state P C M vs"
  shows "bisimJ2JVM (J_start_state P C M vs) (JVM_start_state (J2JVM P) C M vs)"
using assms
unfolding bisimJ2JVM_def J2JVM_def o_def
apply(intro bisim_composeI)
   apply(erule (1) bisim_J_J0_start[OF wf_prog_wwf_prog])
  apply(erule (1) bisim_J0_J1_start)
 apply(erule bisim_J1_J1_start[OF compP1_pres_wf])
 apply simp
apply(erule bisim_J1_JVM_start[OF compP1_pres_wf])
apply simp
done

end

fun exception :: "'addr expr \<times> 'addr locals \<Rightarrow> 'addr option \<times> 'addr frame list"
where "exception (Throw a, xs) = (\<lfloor>a\<rfloor>, [])"
| "exception _ = (None, [])"

definition mexception ::
  "('addr,'thread_id,'addr expr\<times>'addr locals,'heap,'addr) state \<Rightarrow>
   ('addr,'thread_id,'addr option\<times>'addr frame list,'heap,'addr) state"
where
  "mexception s \<equiv>
  (locks s, (\<lambda>t. case thr s t of \<lfloor>(e, ln)\<rfloor> \<Rightarrow> \<lfloor>(exception e, ln)\<rfloor> | None \<Rightarrow> None, shr s), wset s, interrupts s)"

declare compP1_def [simp del]

context J_JVM_heap_conf_base begin

lemma bisimJ2JVM_mfinal_mexception:
  assumes bisim: "bisimJ2JVM s s'"
  and fin: "exec_mthr.mfinal s'"
  and fin': "red_mthr.mfinal s"
  and tsNotEmpty: "thr s t \<noteq> None"
  shows "s' = mexception s"
proof -
  obtain ls ts m ws "is" where s: "s = (ls, (ts, m), ws, is)" by(cases s) fastforce
  from bisim obtain s0 s1 where bisimJ0: "red_red0.mbisim s s0"
    and bisim01: "red0_Red1'.mbisim s0 s1"
    and bisim1JVM: "Red1_execd.mbisim s1 s'"
    unfolding bisimJ2JVM_def by(fastforce simp add: mbisim_Red1'_Red1_def)
  from bisimJ0 s have [simp]: "locks s0 = ls" "wset s0 = ws" "interrupts s0 = is"
    and tbisimJ0: "\<And>t. red_red0.tbisim (ws t = None) t (ts t) m (thr s0 t) (shr s0)"
    by(auto simp add: red_red0.mbisim_def)
  from bisim01 have [simp]: "locks s1 = ls" "wset s1 = ws" "interrupts s1 = is"
    and tbisim01: "\<And>t. red0_Red1'.tbisim (ws t = None) t (thr s0 t) (shr s0) (thr s1 t) (shr s1)"
    by(auto simp add: red0_Red1'.mbisim_def)
  from bisim1JVM have "locks s' = ls" "wset s' = ws" "interrupts s' = is"
    and tbisim1JVM: "\<And>t. Red1_execd.tbisim (ws t = None) t (thr s1 t) (shr s1) (thr s' t) (shr s')"
    by(auto simp add: Red1_execd.mbisim_def)
  then obtain ts' m' where s': "s' = (ls, (ts', m'), ws, is)" by(cases s') fastforce
  { fix t e x ln
    assume tst: "ts t = \<lfloor>((e, x), ln)\<rfloor>"
    from tbisimJ0[of t] tst obtain e' exs' where ts0t: "thr s0 t = \<lfloor>((e', exs'), ln)\<rfloor>"
      and bisimtJ0: "bisim_red_red0 ((e, x), m) ((e', exs'), shr s0)"
      by(auto simp add: red_red0.tbisim_def)
    from tbisim01[of t] ts0t obtain e'' xs'' exs''
      where ts1t: "thr s1 t = \<lfloor>(((e'', xs''), exs''), ln)\<rfloor>"
      and bisimt01: "bisim_red0_Red1 ((e', exs'), shr s0) (((e'', xs''), exs''), shr s1)"
      by(auto simp add: red0_Red1'.tbisim_def)
    from tbisim1JVM[of t] ts1t s' obtain xcp frs
      where ts't: "ts' t = \<lfloor>((xcp, frs), ln)\<rfloor>" and [simp]: "m' = shr s1"
      and bisimt1JVM: "bisim1_list1 t m' (e'', xs'') exs'' xcp frs"
      by(fastforce simp add: Red1_execd.tbisim_def)

    from fin ts't s s' have [simp]: "frs = []" by(auto dest: exec_mthr.mfinalD)
    from bisimt1JVM have [simp]: "exs'' = []" by(auto elim: bisim1_list1.cases)
    from bisimt01 have [simp]: "exs' = []"
      by(auto simp add: bisim_red0_Red1_def elim!: bisim_list1E elim: bisim_list.cases)
    from tst fin' s have fine: "final e" by(auto dest: red_mthr.mfinalD)
    hence "exception (e, x) = (xcp, frs)"
    proof(cases)
      fix v
      assume [simp]: "e = Val v"
      from bisimtJ0 have "e' = Val v" by(auto elim!: bisim_red_red0.cases)
      with bisimt01 have "e'' = Val v" by(auto simp add: bisim_red0_Red1_def elim: bisim_list1E)
      with bisimt1JVM have "xcp = None" by(auto elim: bisim1_list1.cases)
      thus ?thesis by simp
    next
      fix a
      assume [simp]: "e = Throw a"
      from bisimtJ0 have "e' = Throw a" by(auto elim!: bisim_red_red0.cases)
      with bisimt01 have "e'' = Throw a" by(auto simp add: bisim_red0_Red1_def elim: bisim_list1E)
      with bisimt1JVM have "xcp = \<lfloor>a\<rfloor>" by(auto elim: bisim1_list1.cases)
      thus ?thesis by simp
    qed
    moreover from bisimtJ0 have "shr s0 = m" by(auto elim: bisim_red_red0.cases)
    moreover from bisimt01 have "shr s1 = shr s0" by(auto simp add: bisim_red0_Red1_def)
    ultimately have "ts' t = \<lfloor>(exception (e, x), ln)\<rfloor>" "m' = m" using ts't by simp_all }
  moreover {
    fix t
    assume "ts t = None"
    with red_red0.mbisim_thrNone_eq[OF bisimJ0, of t] s have "thr s0 t = None" by simp
    with bisim01 have "thr s1 t = None" by(auto simp add: red0_Red1'.mbisim_thrNone_eq)
    with bisim1JVM s' have "ts' t = None" by(simp add: Red1_execd.mbisim_thrNone_eq) }
  ultimately show ?thesis using s s' tsNotEmpty by(auto simp add: mexception_def fun_eq_iff)
qed

end

context J_JVM_conf_read begin

theorem J2JVM_correct1:
  fixes C M vs
  defines s: "s \<equiv> J_start_state P C M vs"
  and comps: "cs \<equiv> JVM_start_state (J2JVM P) C M vs"
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  and red: "red_mthr.mthr.\<tau>Runs P s \<xi>"
  obtains \<xi>'
  where "execd_mthr.mthr.\<tau>Runs (J2JVM P) cs \<xi>'" "tllist_all2 tlsimJ2JVM (rel_option bisimJ2JVM) \<xi> \<xi>'"
  and "\<And>s'. \<lbrakk> tfinite \<xi>; terminal \<xi> = \<lfloor>s'\<rfloor>; red_mthr.mfinal s' \<rbrakk>
      \<Longrightarrow> tfinite \<xi>' \<and> terminal \<xi>' = \<lfloor>mexception s'\<rfloor>"
  and "\<And>s'. \<lbrakk> tfinite \<xi>; terminal \<xi> = \<lfloor>s'\<rfloor>; red_mthr.deadlock P s' \<rbrakk>
      \<Longrightarrow> \<exists>cs'. tfinite \<xi>' \<and> terminal \<xi>' = \<lfloor>cs'\<rfloor> \<and> execd_mthr.deadlock (J2JVM P) cs' \<and> bisimJ2JVM s' cs'"
  and "\<lbrakk> tfinite \<xi>; terminal \<xi> = None \<rbrakk> \<Longrightarrow> tfinite \<xi>' \<and> terminal \<xi>' = None"
  and "\<not> tfinite \<xi> \<Longrightarrow> \<not> tfinite \<xi>'"
proof -
  from wf wf_start have bisim: "bisimJ2JVM s cs" unfolding s comps by(rule bisimJ2JVM_start)

  note divfin = delay_bisimulation_diverge_final.delay_bisimulation_diverge[OF bisimJ2JVM_weak_bisim[OF wf]]
  note divfin2 = delay_bisimulation_diverge_final.delay_bisimulation_final_base[OF bisimJ2JVM_weak_bisim[OF wf]]

  from delay_bisimulation_diverge.simulation_\<tau>Runs1[OF divfin, OF bisim red] obtain \<xi>'
    where exec: "execd_mthr.mthr.\<tau>Runs (J2JVM P) cs \<xi>'"
    and tlsim: "tllist_all2 tlsimJ2JVM (rel_option bisimJ2JVM) \<xi> \<xi>'" by blast
  moreover {
    fix s'
    assume fin: "tfinite \<xi>" and s': "terminal \<xi> = \<lfloor>s'\<rfloor>" and final: "red_mthr.mfinal s'"
    from delay_bisimulation_final_base.\<tau>Runs_terminate_final1[OF divfin2, OF red exec tlsim fin s' final]
    obtain cs' where fin': "tfinite \<xi>'" and cs': "terminal \<xi>' = \<lfloor>cs'\<rfloor>"
      and final': "exec_mthr.mfinal cs'" by blast
    from tlsim fin s' cs' have bisim': "bisimJ2JVM s' cs'" by(auto dest: tllist_all2_tfinite1_terminalD)
    from red_mthr.mthr.\<tau>Runs_into_\<tau>rtrancl3p[OF red fin s']
    have "thr s' start_tid \<noteq> None" unfolding s
      by(rule red_mthr.\<tau>rtrancl3p_redT_thread_not_disappear)(simp add: start_state_def)
    with bisim' final final' have [simp]: "cs' = mexception s'"
      by(intro bisimJ2JVM_mfinal_mexception disjI1)
    with fin' cs' have "tfinite \<xi>' \<and> terminal \<xi>' = \<lfloor>mexception s'\<rfloor>" by simp }
  moreover {
    fix s'
    assume fin: "tfinite \<xi>" and s': "terminal \<xi> = \<lfloor>s'\<rfloor>" and dead: "red_mthr.deadlock P s'"
    from tlsim fin s'
    obtain cs' where "tfinite \<xi>'" and cs': "terminal \<xi>' = \<lfloor>cs'\<rfloor>"
      and bisim': "bisimJ2JVM s' cs'"
      by(cases "terminal \<xi>'")(fastforce dest: tllist_all2_tfinite1_terminalD tllist_all2_tfiniteD)+
    from bisim' obtain s0' s1' S1' where bisim0: "red_red0.mbisim s' s0'"
      and bisim01: "red0_Red1'.mbisim s0' s1'"
      and bisim11: "mbisim_Red1'_Red1 s1' S1'"
      and bisim12: "Red1_execd.mbisim S1' cs'"
      unfolding bisimJ2JVM_def by auto

    note b0 = red_red0_FWbisim[OF wf_prog_wwf_prog[OF wf]]
    note b01 = red0_Red1'_FWweak_bisim[OF wf]
    note b01mthr = FWdelay_bisimulation_diverge.mbisim_delay_bisimulation[OF b01]
    note b11 = Red1'_Red1_bisim_into_weak[OF compP1_pres_wf[OF wf]]
    note b11delay = bisimulation_into_delay.delay_bisimulation[OF b11]
    note b12 = Red1_exec1_FWwbisim[OF compP1_pres_wf[OF wf]]
    note b12mthr = FWdelay_bisimulation_diverge.mbisim_delay_bisimulation[OF b12]

    from FWdelay_bisimulation_diverge.deadlock1_imp_\<tau>s_deadlock2[OF b0, OF bisim0 dead, of convert_RA]
    obtain s0'' where "red0_mthr.mthr.silent_moves P s0' s0''"
      and bisim0': "red_red0.mbisim s' s0''"
      and dead0: "red0_mthr.deadlock P s0''" by auto

    from delay_bisimulation_diverge.simulation_silents1[OF b01mthr, OF bisim01 `red0_mthr.mthr.silent_moves P s0' s0''`]
    obtain s1'' where "Red1_mthr.mthr.silent_moves False (compP1 P) s1' s1''"
      and "red0_Red1'.mbisim s0'' s1''" by auto
    from FWdelay_bisimulation_diverge.deadlock1_imp_\<tau>s_deadlock2[OF b01, OF `red0_Red1'.mbisim s0'' s1''` dead0, of convert_RA]
    obtain s1''' where "Red1_mthr.mthr.silent_moves False (compP1 P) s1'' s1'''"
      and dead1: "Red1_mthr.deadlock False (compP1 P) s1'''"
      and bisim01': "red0_Red1'.mbisim s0'' s1'''" by auto
    from `Red1_mthr.mthr.silent_moves False (compP1 P) s1' s1''` `Red1_mthr.mthr.silent_moves False (compP1 P) s1'' s1'''`
    have "Red1_mthr.mthr.silent_moves False (compP1 P) s1' s1'''" by(rule rtranclp_trans)

    from delay_bisimulation_diverge.simulation_silents1[OF b11delay, OF bisim11 this]
    obtain S1'' where "Red1_mthr.mthr.silent_moves True (compP1 P) S1' S1''"
      and bisim11': "mbisim_Red1'_Red1 s1''' S1''" by auto
    from bisim11' have "s1''' = S1''" by(simp add: mbisim_Red1'_Red1_def)
    with dead1 have dead1': "Red1_mthr.deadlock True (compP1 P) S1''"
      by(simp add: Red1_Red1'_deadlock_inv)

    from delay_bisimulation_diverge.simulation_silents1[OF b12mthr, OF bisim12 `Red1_mthr.mthr.silent_moves True (compP1 P) S1' S1''`]
    obtain cs'' where "execd_mthr.mthr.silent_moves (compP2 (compP1 P)) cs' cs''"
      and "Red1_execd.mbisim S1'' cs''" by auto
    from FWdelay_bisimulation_diverge.deadlock1_imp_\<tau>s_deadlock2[OF b12 `Red1_execd.mbisim S1'' cs''` dead1', of convert_RA]
    obtain cs''' where "execd_mthr.mthr.silent_moves (compP2 (compP1 P)) cs'' cs'''"
      and bisim12': "Red1_execd.mbisim S1'' cs'''"
      and dead': "execd_mthr.deadlock (compP2 (compP1 P)) cs'''" by auto
    from `execd_mthr.mthr.silent_moves (compP2 (compP1 P)) cs' cs''` `execd_mthr.mthr.silent_moves (compP2 (compP1 P)) cs'' cs'''`
    have "execd_mthr.mthr.silent_moves (compP2 (compP1 P)) cs' cs'''" by(rule rtranclp_trans)
    hence "cs''' = cs'" using execd_mthr.mthr.\<tau>Runs_terminal_stuck[OF exec `tfinite \<xi>'` `terminal \<xi>' = \<lfloor>cs'\<rfloor>`]
      by(cases rule: converse_rtranclpE)(fastforce simp add: J2JVM_def)+
    with dead' have "execd_mthr.deadlock (J2JVM P) cs'" by(simp add: J2JVM_def)
    hence "\<exists>cs'. tfinite \<xi>' \<and> terminal \<xi>' = \<lfloor>cs'\<rfloor> \<and> execd_mthr.deadlock (J2JVM P) cs' \<and> bisimJ2JVM s' cs'"
      using `tfinite \<xi>'` `terminal \<xi>' = \<lfloor>cs'\<rfloor>` bisim' by blast }
  moreover {
    assume "tfinite \<xi>" and "terminal \<xi> = None"
    hence "tfinite \<xi>' \<and> terminal \<xi>' = None" using tlsim tllist_all2_tfiniteD[OF tlsim]
      by(cases "terminal \<xi>'")(auto dest: tllist_all2_tfinite1_terminalD) }
  moreover {
    assume "\<not> tfinite \<xi>"
      hence "\<not> tfinite \<xi>'" using tlsim by(blast dest: tllist_all2_tfiniteD) }
  ultimately show thesis by(rule that)
qed

theorem J2JVM_correct2:
  fixes C M vs
  defines s: "s \<equiv> J_start_state P C M vs"
  and comps: "cs \<equiv> JVM_start_state (J2JVM P) C M vs"
  assumes wf: "wf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  and exec: "execd_mthr.mthr.\<tau>Runs (J2JVM P) cs \<xi>'"
  obtains \<xi>
  where "red_mthr.mthr.\<tau>Runs P s \<xi>" "tllist_all2 tlsimJ2JVM (rel_option bisimJ2JVM) \<xi> \<xi>'"
  and "\<And>cs'. \<lbrakk> tfinite \<xi>'; terminal \<xi>' = \<lfloor>cs'\<rfloor>; exec_mthr.mfinal cs' \<rbrakk>
      \<Longrightarrow> \<exists>s'. tfinite \<xi> \<and> terminal \<xi> = \<lfloor>s'\<rfloor> \<and> cs' = mexception s' \<and> bisimJ2JVM s' cs'"
  and "\<And>cs'. \<lbrakk> tfinite \<xi>'; terminal \<xi>' = \<lfloor>cs'\<rfloor>; execd_mthr.deadlock (J2JVM P) cs' \<rbrakk>
      \<Longrightarrow> \<exists>s'. tfinite \<xi> \<and> terminal \<xi> = \<lfloor>s'\<rfloor> \<and> red_mthr.deadlock P s' \<and> bisimJ2JVM s' cs'"
  and "\<lbrakk> tfinite \<xi>'; terminal \<xi>' = None \<rbrakk> \<Longrightarrow> tfinite \<xi> \<and> terminal \<xi> = None"
  and "\<not> tfinite \<xi>' \<Longrightarrow> \<not> tfinite \<xi>"
proof -
  from wf wf_start have bisim: "bisimJ2JVM s cs" unfolding s comps by(rule bisimJ2JVM_start)

  note divfin = delay_bisimulation_diverge_final.delay_bisimulation_diverge[OF bisimJ2JVM_weak_bisim[OF wf]]
  note divfin2 = delay_bisimulation_diverge_final.delay_bisimulation_final_base[OF bisimJ2JVM_weak_bisim[OF wf]]

  from delay_bisimulation_diverge.simulation_\<tau>Runs2[OF divfin, OF bisim exec] obtain \<xi>
    where red: "red_mthr.mthr.\<tau>Runs P s \<xi>"
    and tlsim: "tllist_all2 tlsimJ2JVM (rel_option bisimJ2JVM) \<xi> \<xi>'" by blast
  moreover {
    fix cs'
    assume fin: "tfinite \<xi>'" and cs': "terminal \<xi>' = \<lfloor>cs'\<rfloor>" and final: "exec_mthr.mfinal cs'"
    from delay_bisimulation_final_base.\<tau>Runs_terminate_final2[OF divfin2, OF red exec tlsim fin cs' final]
    obtain s' where fin': "tfinite \<xi>" and s': "terminal \<xi> = \<lfloor>s'\<rfloor>"
      and final': "red_mthr.mfinal s'" by blast
    from tlsim fin s' cs' have bisim': "bisimJ2JVM s' cs'" by(auto dest: tllist_all2_tfinite2_terminalD)
    from red_mthr.mthr.\<tau>Runs_into_\<tau>rtrancl3p[OF red fin' s']
    have "thr s' start_tid \<noteq> None" unfolding s
      by(rule red_mthr.\<tau>rtrancl3p_redT_thread_not_disappear)(simp add: start_state_def)
    with bisim' final final' have [simp]: "cs' = mexception s'"
      by(intro bisimJ2JVM_mfinal_mexception)
    with fin' s' bisim' have "\<exists>s'. tfinite \<xi> \<and> terminal \<xi> = \<lfloor>s'\<rfloor> \<and> cs' = mexception s' \<and> bisimJ2JVM s' cs'" by simp }
  moreover {
    fix cs'
    assume fin: "tfinite \<xi>'" and cs': "terminal \<xi>' = \<lfloor>cs'\<rfloor>" and dead': "execd_mthr.deadlock (J2JVM P) cs'"
    from tlsim fin cs'
    obtain s' where "tfinite \<xi>" and s': "terminal \<xi> = \<lfloor>s'\<rfloor>"
      and bisim': "bisimJ2JVM s' cs'"
      by(cases "terminal \<xi>")(fastforce dest: tllist_all2_tfinite2_terminalD tllist_all2_tfiniteD)+
    from bisim' obtain s0' s1' S1' where bisim0: "red_red0.mbisim s' s0'"
      and bisim01: "red0_Red1'.mbisim s0' s1'"
      and bisim11: "mbisim_Red1'_Red1 s1' S1'"
      and bisim12: "Red1_execd.mbisim S1' cs'"
      unfolding bisimJ2JVM_def by auto

    note b0 = red_red0_FWbisim[OF wf_prog_wwf_prog[OF wf]]
    note b0mthr = FWdelay_bisimulation_diverge.mbisim_delay_bisimulation[OF b0]
    note b01 = red0_Red1'_FWweak_bisim[OF wf]
    note b01mthr = FWdelay_bisimulation_diverge.mbisim_delay_bisimulation[OF b01]
    note b11 = Red1'_Red1_bisim_into_weak[OF compP1_pres_wf[OF wf]]
    note b11delay = bisimulation_into_delay.delay_bisimulation[OF b11]
    note b12 = Red1_exec1_FWwbisim[OF compP1_pres_wf[OF wf]]

    from FWdelay_bisimulation_diverge.deadlock2_imp_\<tau>s_deadlock1[OF b12 bisim12, of convert_RA] dead'
    obtain S1'' where "Red1_mthr.mthr.silent_moves True (compP1 P) S1' S1''"
      and bisim12': "Red1_execd.mbisim S1'' cs'"
      and dead': "Red1_mthr.deadlock True (compP1 P) S1''" by(auto simp add: J2JVM_def)
    from delay_bisimulation_diverge.simulation_silents2[OF b11delay, OF bisim11 `Red1_mthr.mthr.silent_moves True (compP1 P) S1' S1''`]
    obtain s1'' where "Red1_mthr.mthr.silent_moves False (compP1 P) s1' s1''"
      and bisim11': "mbisim_Red1'_Red1 s1'' S1''" by blast
    from bisim11' have "s1'' = S1''" by(simp add: mbisim_Red1'_Red1_def)
    with dead' have dead1: "Red1_mthr.deadlock False (compP1 P) s1''"
      by(simp add: Red1_Red1'_deadlock_inv)
    from delay_bisimulation_diverge.simulation_silents2[OF b01mthr, OF bisim01 `Red1_mthr.mthr.silent_moves False (compP1 P) s1' s1''`]
    obtain s0'' where "red0_mthr.mthr.silent_moves P s0' s0''"
      and bisim01': "red0_Red1'.mbisim s0'' s1''" by auto
    from FWdelay_bisimulation_diverge.deadlock2_imp_\<tau>s_deadlock1[OF b01 bisim01' dead1, of convert_RA]
    obtain s0''' where "red0_mthr.mthr.silent_moves P s0'' s0'''"
      and bisim01'': "red0_Red1'.mbisim s0''' s1''"
      and dead0: "red0_mthr.deadlock P s0'''" by auto
    from `red0_mthr.mthr.silent_moves P s0' s0''` `red0_mthr.mthr.silent_moves P s0'' s0'''`
    have "red0_mthr.mthr.silent_moves P s0' s0'''" by(rule rtranclp_trans)
    from delay_bisimulation_diverge.simulation_silents2[OF b0mthr, OF bisim0 this]
    obtain s'' where "red_mthr.mthr.silent_moves P s' s''"
      and "red_red0.mbisim s'' s0'''" by blast
    from FWdelay_bisimulation_diverge.deadlock2_imp_\<tau>s_deadlock1[OF b0 `red_red0.mbisim s'' s0'''` dead0, of convert_RA]
    obtain s''' where "red_mthr.mthr.silent_moves P s'' s'''"
      and "red_red0.mbisim s''' s0'''"
      and dead: "red_mthr.deadlock P s'''" by blast
    from `red_mthr.mthr.silent_moves P s' s''` `red_mthr.mthr.silent_moves P s'' s'''`
    have "red_mthr.mthr.silent_moves P s' s'''" by(rule rtranclp_trans)
    hence "s''' = s'" using red_mthr.mthr.\<tau>Runs_terminal_stuck[OF red `tfinite \<xi>` `terminal \<xi> = \<lfloor>s'\<rfloor>`]
      by(cases rule: converse_rtranclpE) fastforce+
    with dead have "red_mthr.deadlock P s'" by(simp)
    hence "\<exists>s'. tfinite \<xi> \<and> terminal \<xi> = \<lfloor>s'\<rfloor> \<and> red_mthr.deadlock P s' \<and> bisimJ2JVM s' cs'"
      using `tfinite \<xi>` `terminal \<xi> = \<lfloor>s'\<rfloor>` bisim' by blast }
  moreover {
    assume "tfinite \<xi>'" and "terminal \<xi>' = None"
    hence "tfinite \<xi> \<and> terminal \<xi> = None" using tlsim tllist_all2_tfiniteD[OF tlsim]
      by(cases "terminal \<xi>")(auto dest: tllist_all2_tfinite2_terminalD) }
  moreover {
    assume "\<not> tfinite \<xi>'"
      hence "\<not> tfinite \<xi>" using tlsim by(blast dest: tllist_all2_tfiniteD) }
  ultimately show thesis by(rule that)
qed

end

declare compP1_def [simp]

theorem wt_J2JVM: "wf_J_prog P \<Longrightarrow> wf_jvm_prog (J2JVM P)"
unfolding J2JVM_def o_def
by(rule wt_compP2)(rule compP1_pres_wf)

end

author: Josh-Tilles

repo: AFP

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