text:
(* Title:      Kleene Algebras
   Author:     Walter Guttmann
   Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section \<open>Kleene Algebras\<close>

text \<open>
Kleene algebras have been axiomatised by Kozen to describe the equational theory of regular languages \cite{Kozen1994}.
Binary relations are another important model.
This theory implements variants of Kleene algebras based on idempotent left semirings \cite{Moeller2007}.
The weakening of some semiring axioms allows the treatment of further computation models.
The presented algebras are special cases of iterings, so many results can be inherited.
\<close>

theory Kleene_Algebras

imports Iterings

begin

text \<open>
We start with left Kleene algebras, which use the left unfold and left induction axioms of Kleene algebras.
\<close>

class star =
  fixes star :: "'a \<Rightarrow> 'a" ("_\<^sup>\<star>" [100] 100)

class left_kleene_algebra = idempotent_left_semiring + star +
  assumes star_left_unfold : "1 \<squnion> y * y\<^sup>\<star> \<le> y\<^sup>\<star>"
  assumes star_left_induct : "z \<squnion> y * x \<le> x \<longrightarrow> y\<^sup>\<star> * z \<le> x"
begin

no_notation
  trancl ("(_\<^sup>+)" [1000] 999)

abbreviation tc ("_\<^sup>+" [100] 100) where "tc x \<equiv> x * x\<^sup>\<star>"

lemma star_left_unfold_equal:
  "1 \<squnion> x * x\<^sup>\<star> = x\<^sup>\<star>"
  by (metis sup_right_isotone order.antisym mult_right_isotone mult_1_right star_left_induct star_left_unfold)

text \<open>
This means that for some properties of Kleene algebras, only one inequality can be derived, as exemplified by the following sliding rule.
\<close>

lemma star_left_slide:
  "(x * y)\<^sup>\<star> * x \<le> x * (y * x)\<^sup>\<star>"
  by (metis mult_assoc mult_left_sub_dist_sup mult_1_right star_left_induct star_left_unfold_equal)

lemma star_isotone:
  "x \<le> y \<Longrightarrow> x\<^sup>\<star> \<le> y\<^sup>\<star>"
  by (metis sup_right_isotone mult_left_isotone order_trans star_left_unfold mult_1_right star_left_induct)

lemma star_sup_1:
  "(x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>"
proof (rule order.antisym)
  have "y * x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star> \<le> (y * x\<^sup>\<star>)\<^sup>\<star>"
    using sup_right_divisibility star_left_unfold_equal by auto
  also have "... \<le> x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>"
    using mult_left_isotone sup_left_divisibility star_left_unfold_equal by fastforce
  finally have "(x \<squnion> y) * (x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>) \<le> x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>"
    by (metis le_supI mult_right_dist_sup mult_right_sub_dist_sup_right mult_assoc star_left_unfold_equal)
  hence "1 \<squnion> (x \<squnion> y) * (x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>) \<le> x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>"
    using reflexive_mult_closed star_left_unfold by auto
  thus "(x \<squnion> y)\<^sup>\<star> \<le> x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>"
    using star_left_induct by force
next
  have "x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star> \<le> x\<^sup>\<star> * (y * (x \<squnion> y)\<^sup>\<star>)\<^sup>\<star>"
    by (simp add: mult_right_isotone star_isotone)
  also have "... \<le> x\<^sup>\<star> * ((x \<squnion> y) * (x \<squnion> y)\<^sup>\<star>)\<^sup>\<star>"
    by (simp add: mult_right_isotone mult_right_sub_dist_sup_right star_isotone)
  also have "... \<le> x\<^sup>\<star> * (x \<squnion> y)\<^sup>\<star>\<^sup>\<star>"
    using mult_right_isotone star_left_unfold star_isotone by auto
  also have "... \<le> (x \<squnion> y)\<^sup>\<star> * (x \<squnion> y)\<^sup>\<star>\<^sup>\<star>"
    by (simp add: mult_left_isotone star_isotone)
  also have "... \<le> (x \<squnion> y)\<^sup>\<star>"
    by (metis sup.bounded_iff mult_1_right star_left_induct star_left_unfold)
  finally show "x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star> \<le> (x \<squnion> y)\<^sup>\<star>"
    by simp
qed

end

text \<open>
We now show that left Kleene algebras form iterings.
A sublocale is used instead of a subclass, because iterings use a different iteration operation.
\<close>

sublocale left_kleene_algebra < star: left_conway_semiring where circ = star
  apply unfold_locales
  apply (rule star_left_unfold_equal)
  apply (rule star_left_slide)
  by (rule star_sup_1)

context left_kleene_algebra
begin

text \<open>
A number of lemmas in this class are taken from Georg Struth's Kleene algebra theory \cite{ArmstrongGomesStruthWeber2016}.
\<close>

lemma star_sub_one:
  "x \<le> 1 \<Longrightarrow> x\<^sup>\<star> = 1"
  by (metis sup_right_isotone order.eq_iff le_iff_sup mult_1_right star.circ_plus_one star_left_induct)

lemma star_one:
  "1\<^sup>\<star> = 1"
  by (simp add: star_sub_one)

lemma star_left_induct_mult:
  "x * y \<le> y \<Longrightarrow> x\<^sup>\<star> * y \<le> y"
  by (simp add: star_left_induct)

lemma star_left_induct_mult_iff:
  "x * y \<le> y \<longleftrightarrow> x\<^sup>\<star> * y \<le> y"
  using mult_left_isotone order_trans star.circ_increasing star_left_induct_mult by blast

lemma star_involutive:
  "x\<^sup>\<star> = x\<^sup>\<star>\<^sup>\<star>"
  using star.circ_circ_sup star_sup_1 star_one by auto

lemma star_sup_one:
  "(1 \<squnion> x)\<^sup>\<star> = x\<^sup>\<star>"
  using star.circ_circ_sup star_involutive by auto

lemma star_plus_loops:
  "x\<^sup>\<star> \<squnion> 1 = x\<^sup>+ \<squnion> 1"
  using star.circ_plus_one star_left_unfold_equal sup_commute by auto

lemma star_left_induct_equal:
  "z \<squnion> x * y = y \<Longrightarrow> x\<^sup>\<star> * z \<le> y"
  by (simp add: star_left_induct)

lemma star_left_induct_mult_equal:
  "x * y = y \<Longrightarrow> x\<^sup>\<star> * y \<le> y"
  by (simp add: star_left_induct_mult)

lemma star_star_upper_bound:
  "x\<^sup>\<star> \<le> z\<^sup>\<star> \<Longrightarrow> x\<^sup>\<star>\<^sup>\<star> \<le> z\<^sup>\<star>"
  using star_involutive by auto

lemma star_simulation_left:
  assumes "x * z \<le> z * y"
    shows "x\<^sup>\<star> * z \<le> z * y\<^sup>\<star>"
proof -
  have "x * z * y\<^sup>\<star> \<le> z * y * y\<^sup>\<star>"
    by (simp add: assms mult_left_isotone)
  also have "... \<le> z * y\<^sup>\<star>"
    by (simp add: mult_right_isotone star.left_plus_below_circ mult_assoc)
  finally have "z \<squnion> x * z * y\<^sup>\<star> \<le> z * y\<^sup>\<star>"
    using star.circ_back_loop_prefixpoint by auto
  thus ?thesis
    by (simp add: star_left_induct mult_assoc)
qed

lemma quasicomm_1:
  "y * x \<le> x * (x \<squnion> y)\<^sup>\<star> \<longleftrightarrow> y\<^sup>\<star> * x \<le> x * (x \<squnion> y)\<^sup>\<star>"
  by (metis mult_isotone order_refl order_trans star.circ_increasing star_involutive star_simulation_left)

lemma star_rtc_3:
  "1 \<squnion> x \<squnion> y * y = y \<Longrightarrow> x\<^sup>\<star> \<le> y"
  by (metis sup.bounded_iff le_iff_sup mult_left_sub_dist_sup_left mult_1_right star_left_induct_mult_iff star.circ_sub_dist)

lemma star_decompose_1:
  "(x \<squnion> y)\<^sup>\<star> = (x\<^sup>\<star> * y\<^sup>\<star>)\<^sup>\<star>"
  apply (rule order.antisym)
  apply (simp add: star.circ_sup_2)
  using star.circ_sub_dist_3 star_isotone star_involutive by fastforce

lemma star_sum:
  "(x \<squnion> y)\<^sup>\<star> = (x\<^sup>\<star> \<squnion> y\<^sup>\<star>)\<^sup>\<star>"
  using star_decompose_1 star_involutive by auto

lemma star_decompose_3:
  "(x\<^sup>\<star> * y\<^sup>\<star>)\<^sup>\<star> = x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>"
  using star_sup_1 star_decompose_1 by auto

text \<open>
In contrast to iterings, we now obtain that the iteration operation results in least fixpoints.
\<close>

lemma star_loop_least_fixpoint:
  "y * x \<squnion> z = x \<Longrightarrow> y\<^sup>\<star> * z \<le> x"
  by (simp add: sup_commute star_left_induct_equal)

lemma star_loop_is_least_fixpoint:
  "is_least_fixpoint (\<lambda>x . y * x \<squnion> z) (y\<^sup>\<star> * z)"
  by (simp add: is_least_fixpoint_def star.circ_loop_fixpoint star_loop_least_fixpoint)

lemma star_loop_mu:
  "\<mu> (\<lambda>x . y * x \<squnion> z) = y\<^sup>\<star> * z"
  by (metis least_fixpoint_same star_loop_is_least_fixpoint)

lemma affine_has_least_fixpoint:
  "has_least_fixpoint (\<lambda>x . y * x \<squnion> z)"
  by (metis has_least_fixpoint_def star_loop_is_least_fixpoint)

lemma star_outer_increasing:
  "x \<le> y\<^sup>\<star> * x * y\<^sup>\<star>"
  by (metis star.circ_back_loop_prefixpoint star.circ_loop_fixpoint sup.boundedE)

(*
lemma circ_sup: "(x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> = (x \<squnion> y)\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_mult: "1 \<squnion> x * (y * x)\<^sup>\<star> * y = (x * y)\<^sup>\<star>" nitpick [expect=genuine] oops
lemma circ_plus_same: "x\<^sup>\<star> * x = x * x\<^sup>\<star>" nitpick [expect=genuine] oops
lemma circ_unfold_sum: "(x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> \<squnion> x\<^sup>\<star> * y * (x \<squnion> y)\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma mult_zero_sup_circ_2: "(x \<squnion> y * bot)\<^sup>\<star> = x\<^sup>\<star> \<squnion> x\<^sup>\<star> * y * bot" nitpick [expect=genuine,card=7] oops
lemma circ_simulate_left: "x * z \<le> z * y \<squnion> w \<longrightarrow> x\<^sup>\<star> * z \<le> (z \<squnion> x\<^sup>\<star> * w) * y\<^sup>\<star>" nitpick [expect=genuine] oops
lemma circ_simulate_1: "y * x \<le> x * y \<longrightarrow> y\<^sup>\<star> * x\<^sup>\<star> \<le> x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_separate_1: "y * x \<le> x * y \<longrightarrow> (x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma atomicity_refinement: "s = s * q \<and> x = q * x \<and> q * b = bot \<and> r * b \<le> b * r \<and> r * l \<le> l * r \<and> x * l \<le> l * x \<and> b * l \<le> l * b \<and> q * l \<le> l * q \<and> r\<^sup>\<star> * q \<le> q * r\<^sup>\<star> \<and> q \<le> 1 \<longrightarrow> s * (x \<squnion> b \<squnion> r \<squnion> l)\<^sup>\<star> * q \<le> s * (x * b\<^sup>\<star> * q \<squnion> r \<squnion> l)\<^sup>\<star>" nitpick [expect=genuine] oops
lemma circ_simulate_left_plus: "x * z \<le> z * y\<^sup>\<star> \<squnion> w \<longrightarrow> x\<^sup>\<star> * z \<le> (z \<squnion> x\<^sup>\<star> * w) * y\<^sup>\<star>" nitpick [expect=genuine] oops
lemma circ_separate_unfold: "(y * x\<^sup>\<star>)\<^sup>\<star> = y\<^sup>\<star> \<squnion> y\<^sup>\<star> * y * x * x\<^sup>\<star> * (y * x\<^sup>\<star>)\<^sup>\<star>" nitpick [expect=genuine] oops
lemma separation: "y * x \<le> x * y\<^sup>\<star> \<longrightarrow> (x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_simulate_4: "y * x \<le> x * x\<^sup>\<star> * (1 \<squnion> y) \<longrightarrow> y\<^sup>\<star> * x\<^sup>\<star> \<le> x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_simulate_5: "y * x \<le> x * x\<^sup>\<star> * (x \<squnion> y) \<longrightarrow> y\<^sup>\<star> * x\<^sup>\<star> \<le> x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_simulate_6: "y * x \<le> x * (x \<squnion> y) \<longrightarrow> y\<^sup>\<star> * x\<^sup>\<star> \<le> x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_separate_4: "y * x \<le> x * x\<^sup>\<star> * (1 \<squnion> y) \<longrightarrow> (x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_separate_5: "y * x \<le> x * x\<^sup>\<star> * (x \<squnion> y) \<longrightarrow> (x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
lemma circ_separate_6: "y * x \<le> x * (x \<squnion> y) \<longrightarrow> (x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
*)

end

text \<open>
We next add the right induction rule, which allows us to strengthen many inequalities of left Kleene algebras to equalities.
\<close>

class strong_left_kleene_algebra = left_kleene_algebra +
  assumes star_right_induct: "z \<squnion> x * y \<le> x \<longrightarrow> z * y\<^sup>\<star> \<le> x"
begin

lemma star_plus:
  "y\<^sup>\<star> * y = y * y\<^sup>\<star>"
proof (rule order.antisym)
  show "y\<^sup>\<star> * y \<le> y * y\<^sup>\<star>"
    by (simp add: star.circ_plus_sub)
next
  have "y\<^sup>\<star> * y * y \<le> y\<^sup>\<star> * y"
    by (simp add: mult_left_isotone star.right_plus_below_circ)
  hence "y \<squnion> y\<^sup>\<star> * y * y \<le> y\<^sup>\<star> * y"
    by (simp add: star.circ_mult_increasing_2)
  thus "y * y\<^sup>\<star> \<le> y\<^sup>\<star> * y"
    using star_right_induct by blast
qed

lemma star_slide:
  "(x * y)\<^sup>\<star> * x = x * (y * x)\<^sup>\<star>"
proof (rule order.antisym)
  show "(x * y)\<^sup>\<star> * x \<le> x * (y * x)\<^sup>\<star>"
    by (rule star_left_slide)
next
  have "x \<squnion> (x * y)\<^sup>\<star> * x * y * x \<le> (x * y)\<^sup>\<star> * x"
    by (metis (full_types) sup.commute eq_refl star.circ_loop_fixpoint mult.assoc star_plus)
  thus "x * (y * x)\<^sup>\<star> \<le> (x * y)\<^sup>\<star> * x"
    by (simp add: mult_assoc star_right_induct)
qed

lemma star_simulation_right:
  assumes "z * x \<le> y * z"
    shows "z * x\<^sup>\<star> \<le> y\<^sup>\<star> * z"
proof -
  have "y\<^sup>\<star> * z * x \<le> y\<^sup>\<star> * z"
    by (metis assms dual_order.trans mult_isotone mult_left_sub_dist_sup_right star.circ_loop_fixpoint star.circ_transitive_equal sup.cobounded1 mult_assoc)
  thus ?thesis
    by (metis le_supI star.circ_loop_fixpoint star_right_induct sup.cobounded2)
qed

end

text \<open>
Again we inherit results from the itering hierarchy.
\<close>

sublocale strong_left_kleene_algebra < star: itering_1 where circ = star
  apply unfold_locales
  apply (simp add: star_slide)
  by (simp add: star_simulation_right)

context strong_left_kleene_algebra
begin

lemma star_right_induct_mult:
  "y * x \<le> y \<Longrightarrow> y * x\<^sup>\<star> \<le> y"
  by (simp add: star_right_induct)

lemma star_right_induct_mult_iff:
  "y * x \<le> y \<longleftrightarrow> y * x\<^sup>\<star> \<le> y"
  using mult_right_isotone order_trans star.circ_increasing star_right_induct_mult by blast

lemma star_simulation_right_equal:
  "z * x = y * z \<Longrightarrow> z * x\<^sup>\<star> = y\<^sup>\<star> * z"
  by (metis order.eq_iff star_simulation_left star_simulation_right)

lemma star_simulation_star:
  "x * y \<le> y * x \<Longrightarrow> x\<^sup>\<star> * y\<^sup>\<star> \<le> y\<^sup>\<star> * x\<^sup>\<star>"
  by (simp add: star_simulation_left star_simulation_right)

lemma star_right_induct_equal:
  "z \<squnion> y * x = y \<Longrightarrow> z * x\<^sup>\<star> \<le> y"
  by (simp add: star_right_induct)

lemma star_right_induct_mult_equal:
  "y * x = y \<Longrightarrow> y * x\<^sup>\<star> \<le> y"
  by (simp add: star_right_induct_mult)

lemma star_back_loop_least_fixpoint:
  "x * y \<squnion> z = x \<Longrightarrow> z * y\<^sup>\<star> \<le> x"
  by (simp add: sup_commute star_right_induct_equal)

lemma star_back_loop_is_least_fixpoint:
  "is_least_fixpoint (\<lambda>x . x * y \<squnion> z) (z * y\<^sup>\<star>)"
proof (unfold is_least_fixpoint_def, rule conjI)
  have "(z * y\<^sup>\<star> * y \<squnion> z) * y \<le> z * y\<^sup>\<star> * y \<squnion> z"
    using le_supI1 mult_left_isotone star.circ_back_loop_prefixpoint by auto
  hence "z * y\<^sup>\<star> \<le> z * y\<^sup>\<star> * y \<squnion> z"
    by (simp add: star_right_induct)
  thus "z * y\<^sup>\<star> * y \<squnion> z = z * y\<^sup>\<star>"
    using order.antisym star.circ_back_loop_prefixpoint by auto
next
  show "\<forall>x. x * y \<squnion> z = x \<longrightarrow> z * y\<^sup>\<star> \<le> x"
    by (simp add: star_back_loop_least_fixpoint)
qed

lemma star_square:
  "x\<^sup>\<star> = (1 \<squnion> x) * (x * x)\<^sup>\<star>"
proof -
  let ?f = "\<lambda>y . y * x \<squnion> 1"
  have 1: "isotone ?f"
    by (metis sup_left_isotone isotone_def mult_left_isotone)
  have "?f \<circ> ?f = (\<lambda>y . y * (x * x) \<squnion> (1 \<squnion> x))"
    by (simp add: sup_assoc sup_commute mult_assoc mult_right_dist_sup o_def)
  thus ?thesis
    using 1 by (metis mu_square mult_left_one star_back_loop_mu has_least_fixpoint_def star_back_loop_is_least_fixpoint)
qed

lemma star_square_2:
  "x\<^sup>\<star> = (x * x)\<^sup>\<star> * (x \<squnion> 1)"
proof -
  have "(1 \<squnion> x) * (x * x)\<^sup>\<star> = (x * x)\<^sup>\<star> * 1 \<squnion> x * (x * x)\<^sup>\<star>"
    using mult_right_dist_sup by force
  thus ?thesis
    by (metis (no_types) order.antisym mult_left_sub_dist_sup star.circ_square_2 star_slide sup_commute star_square)
qed

lemma star_circ_simulate_right_plus:
  assumes "z * x \<le> y * y\<^sup>\<star> * z \<squnion> w"
    shows "z * x\<^sup>\<star> \<le> y\<^sup>\<star> * (z \<squnion> w * x\<^sup>\<star>)"
proof -
  have "(z \<squnion> w * x\<^sup>\<star>) * x \<le> z * x \<squnion> w * x\<^sup>\<star>"
    using mult_right_dist_sup star.circ_back_loop_prefixpoint sup_right_isotone by auto
  also have "... \<le> y * y\<^sup>\<star> * z \<squnion> w \<squnion> w * x\<^sup>\<star>"
    using assms sup_left_isotone by blast
  also have "... \<le> y * y\<^sup>\<star> * z \<squnion> w * x\<^sup>\<star>"
    using le_supI1 star.circ_back_loop_prefixpoint sup_commute by auto
  also have "... \<le> y\<^sup>\<star> * (z \<squnion> w * x\<^sup>\<star>)"
    by (metis sup.bounded_iff mult_isotone mult_left_isotone mult_left_one mult_left_sub_dist_sup_left star.circ_reflexive star.left_plus_below_circ)
  finally have "y\<^sup>\<star> * (z \<squnion> w * x\<^sup>\<star>) * x \<le> y\<^sup>\<star> * (z \<squnion> w * x\<^sup>\<star>)"
    by (metis mult_assoc mult_right_isotone star.circ_transitive_equal)
  thus ?thesis
    by (metis sup.bounded_iff star_right_induct mult_left_sub_dist_sup_left star.circ_loop_fixpoint)
qed

lemma transitive_star:
  "x * x \<le> x \<Longrightarrow> x\<^sup>\<star> = 1 \<squnion> x"
  by (metis order.antisym star.circ_mult_increasing_2 star.circ_plus_same star_left_induct_mult star_left_unfold_equal)

lemma star_sup_2:
  assumes "x * x \<le> x"
    and "x * y \<le> x"
  shows "(x \<squnion> y)\<^sup>\<star> = y\<^sup>\<star> * (x \<squnion> 1)"
proof -
  have "(x \<squnion> y)\<^sup>\<star> = y\<^sup>\<star> * (x * y\<^sup>\<star>)\<^sup>\<star>"
    by (simp add: star.circ_decompose_6 star_sup_1)
  also have "... = y\<^sup>\<star> * x\<^sup>\<star>"
    using assms(2) dual_order.antisym star.circ_back_loop_prefixpoint star_right_induct_mult by fastforce
  also have "... = y\<^sup>\<star> * (x \<squnion> 1)"
    by (simp add: assms(1) sup_commute transitive_star)
  finally show ?thesis
    .
qed

(*
lemma star_circ_simulate_left_plus: "x * z \<le> z * y\<^sup>\<star> \<squnion> w \<longrightarrow> x\<^sup>\<star> * z \<le> (z \<squnion> x\<^sup>\<star> * w) * y\<^sup>\<star>" nitpick [expect=genuine,card=7] oops
*)

end

text \<open>
The following class contains a generalisation of Kleene algebras, which lacks the right zero axiom.
\<close>

class left_zero_kleene_algebra = idempotent_left_zero_semiring + strong_left_kleene_algebra
begin

lemma star_star_absorb:
  "y\<^sup>\<star> * (y\<^sup>\<star> * x)\<^sup>\<star> * y\<^sup>\<star> = (y\<^sup>\<star> * x)\<^sup>\<star> * y\<^sup>\<star>"
  by (metis star.circ_transitive_equal star_slide mult_assoc)

lemma star_circ_simulate_left_plus:
  assumes "x * z \<le> z * y\<^sup>\<star> \<squnion> w"
    shows "x\<^sup>\<star> * z \<le> (z \<squnion> x\<^sup>\<star> * w) * y\<^sup>\<star>"
proof -
  have "x * (x\<^sup>\<star> * (w * y\<^sup>\<star>)) \<le> x\<^sup>\<star> * (w * y\<^sup>\<star>)"
    by (metis (no_types) mult_right_sub_dist_sup_left star.circ_loop_fixpoint mult_assoc)
  hence "x * ((z \<squnion> x\<^sup>\<star> * w) * y\<^sup>\<star>) \<le> x * z * y\<^sup>\<star> \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
    using mult_left_dist_sup mult_right_dist_sup sup_right_isotone mult_assoc by presburger
  also have "... \<le> (z * y\<^sup>\<star> \<squnion> w) * y\<^sup>\<star> \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
    using assms mult_isotone semiring.add_right_mono by blast
  also have "... = z * y\<^sup>\<star> \<squnion> w * y\<^sup>\<star> \<squnion> x\<^sup>\<star> * w * y\<^sup>\<star>"
    by (simp add: mult_right_dist_sup star.circ_transitive_equal mult_assoc)
  also have "... = (z \<squnion> w \<squnion> x\<^sup>\<star> * w) * y\<^sup>\<star>"
    by (simp add: mult_right_dist_sup)
  also have "... = (z \<squnion> x\<^sup>\<star> * w) * y\<^sup>\<star>"
    by (metis sup_assoc sup_ge2 le_iff_sup star.circ_loop_fixpoint)
  finally show ?thesis
    by (metis sup.bounded_iff mult_left_sub_dist_sup_left mult_1_right star.circ_right_unfold_1 star_left_induct)
qed

lemma star_one_sup_below:
  "x * y\<^sup>\<star> * (1 \<squnion> z) \<le> x * (y \<squnion> z)\<^sup>\<star>"
proof -
  have "y\<^sup>\<star> * z \<le> (y \<squnion> z)\<^sup>\<star>"
    using sup_ge2 order_trans star.circ_increasing star.circ_mult_upper_bound star.circ_sub_dist by blast
  hence "y\<^sup>\<star> \<squnion> y\<^sup>\<star> * z \<le> (y \<squnion> z)\<^sup>\<star>"
    by (simp add: star.circ_sup_upper_bound star.circ_sub_dist)
  hence "y\<^sup>\<star> * (1 \<squnion> z) \<le> (y \<squnion> z)\<^sup>\<star>"
    by (simp add: mult_left_dist_sup)
  thus ?thesis
    by (metis mult_right_isotone mult_assoc)
qed

text \<open>
The following theorem is similar to the puzzle where persons insert themselves always in the middle between two groups of people in a line.
Here, however, items in the middle annihilate each other, leaving just one group of items behind.
\<close>

lemma cancel_separate:
  assumes "x * y \<le> 1"
    shows "x\<^sup>\<star> * y\<^sup>\<star> \<le> x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
proof -
  have "x * y\<^sup>\<star> = x \<squnion> x * y * y\<^sup>\<star>"
    by (metis mult_assoc mult_left_dist_sup mult_1_right star_left_unfold_equal)
  also have "... \<le> x \<squnion> y\<^sup>\<star>"
    by (meson assms dual_order.trans order.refl star.circ_mult_upper_bound star.circ_reflexive sup_right_isotone)
  also have "... \<le> x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
    using star.circ_increasing sup_left_isotone by auto
  finally have 1: "x * y\<^sup>\<star> \<le> x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
    .
  have "x * (x\<^sup>\<star> \<squnion> y\<^sup>\<star>) = x * x\<^sup>\<star> \<squnion> x * y\<^sup>\<star>"
    by (simp add: mult_left_dist_sup)
  also have "... \<le> x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
    using 1 by (metis sup.bounded_iff sup_ge1 order_trans star.left_plus_below_circ)
  finally have 2: "x * (x\<^sup>\<star> \<squnion> y\<^sup>\<star>) \<le> x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
    .
  have "y\<^sup>\<star> \<le> x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
    by simp
  hence "y\<^sup>\<star> \<squnion> x * (x\<^sup>\<star> \<squnion> y\<^sup>\<star>) \<le> x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
    using 2 sup.bounded_iff by blast
  thus ?thesis
    by (metis star_left_induct)
qed

lemma star_separate:
  assumes "x * y = bot"
      and "y * y = bot"
    shows "(x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>"
proof -
  have 1: "y\<^sup>\<star> = 1 \<squnion> y"
    using assms(2) by (simp add: transitive_star)
  have "(x \<squnion> y)\<^sup>\<star> = y\<^sup>\<star> * (x * y\<^sup>\<star>)\<^sup>\<star>"
    by (simp add: star.circ_decompose_6 star_sup_1)
  also have "... = y\<^sup>\<star> * (x * (1 \<squnion> y * y\<^sup>\<star>))\<^sup>\<star>"
    by (simp add: star_left_unfold_equal)
  also have "... = (1 \<squnion> y) * x\<^sup>\<star>"
    using 1 by (simp add: assms mult_left_dist_sup)
  also have "... = x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>"
    by (simp add: mult_right_dist_sup)
  finally show ?thesis
    .
qed

end

text \<open>
We can now inherit from the strongest variant of iterings.
\<close>

sublocale left_zero_kleene_algebra < star: itering where circ = star
  apply unfold_locales
  apply (metis star.circ_sup_9)
  apply (metis star.circ_mult_1)
  apply (simp add: star_circ_simulate_right_plus)
  by (simp add: star_circ_simulate_left_plus)

context left_zero_kleene_algebra
begin

lemma star_absorb:
  "x * y = bot \<Longrightarrow> x * y\<^sup>\<star> = x"
  by (metis sup.bounded_iff antisym_conv star.circ_back_loop_prefixpoint star.circ_elimination)

lemma star_separate_2:
  assumes "x * z\<^sup>+ * y = bot"
      and "y * z\<^sup>+ * y = bot"
      and "z * x = bot"
    shows "(x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star> = z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star>"
proof -
  have 1: "x\<^sup>\<star> * z\<^sup>+ * y = z\<^sup>+ * y"
    by (metis assms mult_assoc mult_1_left mult_left_zero star.circ_zero star_simulation_right_equal)
  have 2: "z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>+ \<le> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star>"
    by (simp add: mult_right_isotone star.left_plus_below_circ)
  have "z\<^sup>\<star> * z\<^sup>+ * y * x\<^sup>\<star> \<le> z\<^sup>\<star> * y * x\<^sup>\<star>"
    by (metis mult_left_isotone star.left_plus_below_circ star.right_plus_circ star_plus)
  also have "... \<le> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>)"
    by (simp add: mult_assoc mult_left_sub_dist_sup_right)
  also have "... \<le> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star>"
    using sup_right_divisibility star.circ_back_loop_fixpoint by blast
  finally have 3: "z\<^sup>\<star> * z\<^sup>+ * y * x\<^sup>\<star> \<le> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star>"
    .
  have "z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star> * (z * (1 \<squnion> y * x\<^sup>\<star>)) = z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>+ \<squnion> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>+ * y * x\<^sup>\<star>"
    by (metis mult_1_right semiring.distrib_left star.circ_plus_same mult_assoc)
  also have "... = z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>+ \<squnion> z\<^sup>\<star> * (1 \<squnion> y) * x\<^sup>\<star> * z\<^sup>+ * y * x\<^sup>\<star>"
    by (simp add: semiring.distrib_right mult_assoc)
  also have "... = z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>+ \<squnion> z\<^sup>\<star> * (1 \<squnion> y) * z\<^sup>+ * y * x\<^sup>\<star>"
    using 1 by (simp add: mult_assoc)
  also have "... = z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>+ \<squnion> z\<^sup>\<star> * z\<^sup>+ * y * x\<^sup>\<star> \<squnion> z\<^sup>\<star> * y * z\<^sup>+ * y * x\<^sup>\<star>"
    using mult_left_dist_sup mult_right_dist_sup sup_assoc by auto
  also have "... = z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>+ \<squnion> z\<^sup>\<star> * z\<^sup>+ * y * x\<^sup>\<star>"
    by (metis assms(2) mult_left_dist_sup mult_left_zero sup_commute sup_monoid.add_0_left mult_assoc)
  also have "... \<le> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star>"
    using 2 3 by simp
  finally have "(x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) \<squnion> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star> * (z * (1 \<squnion> y * x\<^sup>\<star>)) \<le> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star>"
    by (simp add: star_outer_increasing)
  hence 4: "(x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star> \<le> z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star>"
    by (simp add: star_right_induct)
  have 5: "(x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star> \<le> (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star>"
    by (metis sup_ge1 mult_right_isotone mult_1_right star_isotone)
  have "z * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) = z * x\<^sup>\<star> \<squnion> z * y * x\<^sup>\<star>"
    by (simp add: mult_assoc mult_left_dist_sup)
  also have "... = z \<squnion> z * y * x\<^sup>\<star>"
    by (simp add: assms star_absorb)
  also have "... = z * (1 \<squnion> y * x\<^sup>\<star>)"
    by (simp add: mult_assoc mult_left_dist_sup)
  also have "... \<le> (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star>"
    by (simp add: star.circ_increasing)
  also have "... \<le> (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star>"
    by (metis le_supE mult_right_sub_dist_sup_left star.circ_loop_fixpoint)
  finally have "z * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) \<le> (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star>"
    .
  hence "z * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star> \<le> (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star>"
    by (metis mult_assoc mult_left_isotone star.circ_transitive_equal)
  hence "z\<^sup>\<star> * (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * z\<^sup>\<star> \<le> (x\<^sup>\<star> \<squnion> y * x\<^sup>\<star>) * (z * (1 \<squnion> y * x\<^sup>\<star>))\<^sup>\<star>"
    using 5 by (metis star_left_induct sup.bounded_iff mult_assoc)
  thus ?thesis
    using 4 by (simp add: antisym)
qed

lemma cancel_separate_eq:
  "x * y \<le> 1 \<Longrightarrow> x\<^sup>\<star> * y\<^sup>\<star> = x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
  by (metis order.antisym cancel_separate star.circ_plus_one star.circ_sup_sub_sup_one_1 star_involutive)

lemma cancel_separate_1:
  assumes "x * y \<le> 1"
    shows "(x \<squnion> y)\<^sup>\<star> = y\<^sup>\<star> * x\<^sup>\<star>"
proof -
  have "y\<^sup>\<star> * x\<^sup>\<star> * y = y\<^sup>\<star> * x\<^sup>\<star> * x * y \<squnion> y\<^sup>\<star> * y"
    by (metis mult_right_dist_sup star.circ_back_loop_fixpoint)
  also have "... \<le> y\<^sup>\<star> * x\<^sup>\<star> \<squnion> y\<^sup>\<star> * y"
    by (metis assms semiring.add_right_mono mult_right_isotone mult_1_right mult_assoc)
  also have "... \<le> y\<^sup>\<star> * x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
    using semiring.add_left_mono star.right_plus_below_circ by simp
  also have "... = y\<^sup>\<star> * x\<^sup>\<star>"
    by (metis star.circ_back_loop_fixpoint sup.left_idem sup_commute)
  finally have "y\<^sup>\<star> * x\<^sup>\<star> * y \<le> y\<^sup>\<star> * x\<^sup>\<star>"
    by simp
  hence "y\<^sup>\<star> * x\<^sup>\<star> * (x \<squnion> y) \<le> y\<^sup>\<star> * x\<^sup>\<star> * x \<squnion> y\<^sup>\<star> * x\<^sup>\<star>"
    using mult_left_dist_sup order_lesseq_imp by fastforce
  also have "... = y\<^sup>\<star> * x\<^sup>\<star>"
    by (metis star.circ_back_loop_fixpoint sup.left_idem)
  finally have "(x \<squnion> y)\<^sup>\<star> \<le> y\<^sup>\<star> * x\<^sup>\<star>"
    by (metis star.circ_decompose_7 star_right_induct_mult sup_commute)
  thus ?thesis
    using order.antisym star.circ_sub_dist_3 sup_commute by fastforce
qed

lemma plus_sup:
  "(x \<squnion> y)\<^sup>+ = (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>+ \<squnion> (x\<^sup>\<star> * y)\<^sup>+"
  by (metis semiring.distrib_left star.circ_sup_9 star_plus mult_assoc)

lemma plus_half_bot:
  "x * y * x = bot \<Longrightarrow> (x * y)\<^sup>+ = x * y"
  by (metis star_absorb star_slide mult_assoc)

lemma cancel_separate_1_sup:
  assumes "x * y \<le> 1"
      and "y * x \<le> 1"
  shows "(x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> \<squnion> y\<^sup>\<star>"
  by (simp add: assms cancel_separate_1 cancel_separate_eq sup_commute)

text \<open>Lemma \<open>star_separate_3\<close> was contributed by Nicolas Robinson-O'Brien.\<close>

lemma star_separate_3:
  assumes "y * x\<^sup>\<star> * y \<le> y"
    shows "(x \<squnion> y)\<^sup>\<star> = x\<^sup>\<star> \<squnion> x\<^sup>\<star> * y * x\<^sup>\<star>"
proof (rule order.antisym)
  have "x\<^sup>\<star> * y * (x\<^sup>\<star> * y)\<^sup>\<star> * x\<^sup>\<star> \<le> x\<^sup>\<star> * y * x\<^sup>\<star>"
    by (metis assms mult_left_isotone mult_right_isotone star_right_induct_mult mult_assoc)
  thus "(x \<squnion> y)\<^sup>\<star> \<le> x\<^sup>\<star> \<squnion> x\<^sup>\<star> * y * x\<^sup>\<star>"
    by (metis order.antisym semiring.add_left_mono star.circ_sup_2 star.circ_sup_sub star.circ_unfold_sum star_decompose_3 star_slide mult_assoc)
next
  show "x\<^sup>\<star> \<squnion> x\<^sup>\<star> * y * x\<^sup>\<star> \<le> (x \<squnion> y)\<^sup>\<star>"
    using mult_isotone star.circ_increasing star.circ_sub_dist star.circ_sup_9 by auto
qed

end

text \<open>
A Kleene algebra is obtained by requiring an idempotent semiring.
\<close>

class kleene_algebra = left_zero_kleene_algebra + idempotent_semiring

text \<open>
The following classes are variants of Kleene algebras expanded by an additional iteration operation.
This is useful to study the Kleene star in computation models that do not use least fixpoints in the refinement order as the semantics of recursion.
\<close>

class left_kleene_conway_semiring = left_kleene_algebra + left_conway_semiring
begin

lemma star_zero_below_circ_mult:
  "x\<^sup>\<star> * bot \<le> x\<^sup>\<circ> * y"
  by (simp add: mult_isotone star_below_circ)

lemma star_mult_circ:
  "x\<^sup>\<star> * x\<^sup>\<circ> = x\<^sup>\<circ>"
  by (metis sup_right_divisibility order.antisym circ_left_unfold star_left_induct_mult star.circ_loop_fixpoint)

lemma circ_mult_star:
  "x\<^sup>\<circ> * x\<^sup>\<star> = x\<^sup>\<circ>"
  by (metis sup_assoc sup.bounded_iff circ_left_unfold circ_rtc_2 order.eq_iff left_plus_circ star.circ_sup_sub star.circ_back_loop_prefixpoint star.circ_increasing star_below_circ star_mult_circ star_sup_one)

lemma circ_star:
  "x\<^sup>\<circ>\<^sup>\<star> = x\<^sup>\<circ>"
  by (metis order.antisym circ_reflexive circ_transitive_equal star.circ_increasing star.circ_sup_one_right_unfold star_left_induct_mult_equal)

lemma star_circ:
  "x\<^sup>\<star>\<^sup>\<circ> = x\<^sup>\<circ>\<^sup>\<circ>"
  by (metis order.antisym circ_circ_sup circ_sub_dist le_iff_sup star.circ_rtc_2 star_below_circ)

lemma circ_sup_3:
  "(x\<^sup>\<circ> * y\<^sup>\<circ>)\<^sup>\<star> \<le> (x \<squnion> y)\<^sup>\<circ>"
  using circ_star circ_sub_dist_3 star_isotone by fastforce

end

class left_zero_kleene_conway_semiring = left_zero_kleene_algebra + itering
begin

subclass left_kleene_conway_semiring ..

lemma circ_isolate:
  "x\<^sup>\<circ> = x\<^sup>\<circ> * bot \<squnion> x\<^sup>\<star>"
  by (metis sup_commute order.antisym circ_sup_upper_bound circ_mult_star circ_simulate_absorb star.left_plus_below_circ star_below_circ zero_right_mult_decreasing)

lemma circ_isolate_mult:
  "x\<^sup>\<circ> * y = x\<^sup>\<circ> * bot \<squnion> x\<^sup>\<star> * y"
  by (metis circ_isolate mult_assoc mult_left_zero mult_right_dist_sup)

lemma circ_isolate_mult_sub:
  "x\<^sup>\<circ> * y \<le> x\<^sup>\<circ> \<squnion> x\<^sup>\<star> * y"
  by (metis sup_left_isotone circ_isolate_mult zero_right_mult_decreasing)

lemma circ_sub_decompose:
  "(x\<^sup>\<circ> * y)\<^sup>\<circ> \<le> (x\<^sup>\<star> * y)\<^sup>\<circ> * x\<^sup>\<circ>"
proof -
  have "x\<^sup>\<star> * y \<squnion> x\<^sup>\<circ> * bot = x\<^sup>\<circ> * y"
    by (metis sup.commute circ_isolate_mult)
  hence "(x\<^sup>\<star> * y)\<^sup>\<circ> * x\<^sup>\<circ> = ((x\<^sup>\<circ> * y)\<^sup>\<circ> \<squnion> x\<^sup>\<circ>)\<^sup>\<star>"
    by (metis circ_star circ_sup_9 circ_sup_mult_zero star_decompose_1)
  thus ?thesis
    by (metis circ_star le_iff_sup star.circ_decompose_7 star.circ_unfold_sum)
qed

lemma circ_sup_4:
  "(x \<squnion> y)\<^sup>\<circ> = (x\<^sup>\<star> * y)\<^sup>\<circ> * x\<^sup>\<circ>"
  apply (rule order.antisym)
  apply (metis circ_sup circ_sub_decompose circ_transitive_equal mult_assoc mult_left_isotone)
  by (metis circ_sup circ_isotone mult_left_isotone star_below_circ)

lemma circ_sup_5:
  "(x\<^sup>\<circ> * y)\<^sup>\<circ> * x\<^sup>\<circ> = (x\<^sup>\<star> * y)\<^sup>\<circ> * x\<^sup>\<circ>"
  using circ_sup_4 circ_sup_9 by auto

lemma plus_circ:
  "(x\<^sup>\<star> * x)\<^sup>\<circ> = x\<^sup>\<circ>"
  by (metis sup_idem circ_sup_4 circ_decompose_7 circ_star star.circ_decompose_5 star.right_plus_circ)

(*
lemma "(x\<^sup>\<star> * y * x\<^sup>\<star>)\<^sup>\<circ> = (x\<^sup>\<star> * y)\<^sup>\<circ>" nitpick [expect=genuine] oops
*)

end

text \<open>
The following classes add a greatest element.
\<close>

class bounded_left_kleene_algebra = bounded_idempotent_left_semiring + left_kleene_algebra

sublocale bounded_left_kleene_algebra < star: bounded_left_conway_semiring where circ = star ..

class bounded_left_zero_kleene_algebra = bounded_idempotent_left_semiring + left_zero_kleene_algebra

sublocale bounded_left_zero_kleene_algebra < star: bounded_itering where circ = star ..

class bounded_kleene_algebra = bounded_idempotent_semiring + kleene_algebra

sublocale bounded_kleene_algebra < star: bounded_itering where circ = star ..

text \<open>
We conclude with an alternative axiomatisation of Kleene algebras.
\<close>

class kleene_algebra_var = idempotent_semiring + star +
  assumes star_left_unfold_var : "1 \<squnion> y * y\<^sup>\<star> \<le> y\<^sup>\<star>"
  assumes star_left_induct_var : "y * x \<le> x \<longrightarrow> y\<^sup>\<star> * x \<le> x"
  assumes star_right_induct_var : "x * y \<le> x \<longrightarrow> x * y\<^sup>\<star> \<le> x"
begin

subclass kleene_algebra
  apply unfold_locales
  apply (rule star_left_unfold_var)
  apply (meson sup.bounded_iff mult_right_isotone order_trans star_left_induct_var)
  by (meson sup.bounded_iff mult_left_isotone order_trans star_right_induct_var)

end

end

repo: barakzai


text:
subsection \<open>OrNode Phase\<close>

theory OrPhase
  imports
    Common
begin

context stamp_mask
begin

text \<open>
Taking advantage of the truth table of or operations.

\begin{center}
\begin{tabular}{ c c c c }
\# & x & y & $x | y$ \\
1 & 0 & 0 & 0 \\
2 & 0 & 1 & 1 \\
3 & 1 & 0 & 1 \\
4 & 1 & 1 & 1
\end{tabular}
\end{center}

If row 2 never applies, that is, canBeZero x \& canBeOne y = 0,
then $(x | y) = x$.

Likewise, if row 3 never applies, canBeZero y \& canBeOne x = 0,
then $(x | y) = y$.
\<close>

lemma OrLeftFallthrough:
  assumes "(and (not (\<down>x)) (\<up>y)) = 0"
  shows "exp[x | y] \<ge> exp[x]"
  using assms
  apply simp apply ((rule allI)+; rule impI)
  subgoal premises eval for m p v
  proof -
    obtain b vv where e: "[m, p] \<turnstile> exp[x | y] \<mapsto> IntVal b vv"
      by (metis BinaryExprE bin_eval_new_int new_int.simps eval(2))
    from e obtain xv where xv: "[m, p] \<turnstile> x \<mapsto> IntVal b xv"
      apply (subst (asm) unfold_binary_width)
      by force+
    from e obtain yv where yv: "[m, p] \<turnstile> y \<mapsto> IntVal b yv"
      apply (subst (asm) unfold_binary_width)
      by force+
    have vdef: "v = intval_or (IntVal b xv) (IntVal b yv)"
      by (metis bin_eval.simps(5) eval(2) evalDet unfold_binary xv yv)
    have "\<forall> i. (bit xv i) | (bit yv i) = (bit xv i)"
      by (metis assms bit_and_iff not_down_up_mask_and_zero_implies_zero xv yv)
    then have "IntVal b xv = intval_or (IntVal b xv) (IntVal b yv)"
      by (smt (verit, ccfv_threshold) and.idem assms bit.conj_disj_distrib eval_unused_bits_zero
          intval_or.simps(1) new_int.simps new_int_bin.simps not_down_up_mask_and_zero_implies_zero
          word_ao_absorbs(3) xv yv)
    then show ?thesis
      using xv vdef by presburger
  qed
  done

lemma OrRightFallthrough:
  assumes "(and (not (\<down>y)) (\<up>x)) = 0"
  shows "exp[x | y] \<ge> exp[y]"
  using assms
  apply simp apply ((rule allI)+; rule impI)
  subgoal premises eval for m p v
  proof -
    obtain b vv where e: "[m, p] \<turnstile> exp[x | y] \<mapsto> IntVal b vv"
      by (metis BinaryExprE bin_eval_new_int new_int.simps eval(2))
    from e obtain xv where xv: "[m, p] \<turnstile> x \<mapsto> IntVal b xv"
      apply (subst (asm) unfold_binary_width)
      by force+
    from e obtain yv where yv: "[m, p] \<turnstile> y \<mapsto> IntVal b yv"
      apply (subst (asm) unfold_binary_width)
      by force+
    have vdef: "v = intval_or (IntVal b xv) (IntVal b yv)"
      by (metis bin_eval.simps(5) eval(2) evalDet unfold_binary xv yv)
    have "\<forall> i. (bit xv i) | (bit yv i) = (bit yv i)"
      by (metis assms bit_and_iff not_down_up_mask_and_zero_implies_zero xv yv)
    then have "IntVal b yv = intval_or (IntVal b xv) (IntVal b yv)"
      by (metis (no_types, lifting) assms eval_unused_bits_zero intval_or.simps(1) new_int.elims
          new_int_bin.elims stamp_mask.not_down_up_mask_and_zero_implies_zero stamp_mask_axioms
          word_ao_absorbs(8) xv yv)
    then show ?thesis
      using vdef yv by presburger
  qed
  done

end

phase OrNode
  terminating size
begin

(* Word level proofs *)
lemma bin_or_equal:
  "bin[x | x] = bin[x]"
  by simp

lemma bin_shift_const_right_helper:
 "x | y = y | x"
  by simp

lemma bin_or_not_operands:
 "(~x | ~y) = (~(x & y))"
  by simp

(* Value level proofs *)
lemma val_or_equal:
  assumes "x = new_int b v"
  and    "(val[x | x] \<noteq> UndefVal)"
  shows   "val[x | x] = val[x]"
   apply (cases x; auto) using bin_or_equal assms
  by auto+

lemma val_elim_redundant_false:
  assumes "x = new_int b v"
  and     "val[x | false] \<noteq> UndefVal"
  shows   "val[x | false] = val[x]"
   using assms apply (cases x; auto) by presburger

lemma val_shift_const_right_helper:
   "val[x | y] = val[y | x]"
   apply (cases x; cases y; auto)
  by (simp add: or.commute)+

lemma val_or_not_operands:
 "val[~x | ~y] = val[~(x & y)]"
  apply (cases x; cases y; auto)
  by (simp add: take_bit_not_take_bit)

(* Exp level proofs *)
lemma exp_or_equal:
  "exp[x | x] \<ge> exp[x]"
   using val_or_equal apply auto[1]
   by (smt (verit, ccfv_SIG) evalDet eval_unused_bits_zero intval_negate.elims intval_or.simps(2)
       intval_or.simps(6) intval_or.simps(7) new_int.simps val_or_equal)

lemma exp_elim_redundant_false:
 "exp[x | false] \<ge> exp[x]"
   using val_elim_redundant_false apply auto[1]
   by (smt (verit) Value.sel(1) eval_unused_bits_zero intval_or.elims new_int.simps
       new_int_bin.simps val_elim_redundant_false)

text \<open>Optimisations\<close>

optimization OrEqual: "x | x \<longmapsto> x"
  by (meson exp_or_equal)

optimization OrShiftConstantRight: "((const x) | y) \<longmapsto> y | (const x) when \<not>(is_ConstantExpr y)"
  using size_flip_binary apply force
  apply auto[1]
  by (simp add: BinaryExpr unfold_const val_shift_const_right_helper)

optimization EliminateRedundantFalse: "x | false \<longmapsto> x"
  by (meson exp_elim_redundant_false)

optimization OrNotOperands: "(~x | ~y) \<longmapsto> ~(x & y)"
   apply (metis add_2_eq_Suc' less_SucI not_add_less1 not_less_eq size_binary_const size_non_add)
   apply auto[1]
  by (metis BinaryExpr UnaryExpr bin_eval.simps(4) intval_not.simps(2) unary_eval.simps(3)
      val_or_not_operands)

optimization OrLeftFallthrough:
  "x | y \<longmapsto> x when ((and (not (IRExpr_down x)) (IRExpr_up y)) = 0)"
  using simple_mask.OrLeftFallthrough by blast

optimization OrRightFallthrough:
  "x | y \<longmapsto> y when ((and (not (IRExpr_down y)) (IRExpr_up x)) = 0)"
  using simple_mask.OrRightFallthrough by blast

end (* End of OrPhase *)

end (* End of file *)

author: uqcyber

repo: veriopt-releases


text:
(*  Title:      HOL/Quotient_Examples/Quotient_FSet.thy
    Author:     Cezary Kaliszyk, TU Munich
    Author:     Christian Urban, TU Munich

Type of finite sets.
*)

(********************************************************************
  WARNING: There is a formalization of 'a fset as a subtype of sets in
  HOL/Library/FSet.thy using Lifting/Transfer. The user should use
  that file rather than this file unless there are some very specific
  reasons.
*********************************************************************)

theory Quotient_FSet
imports "HOL-Library.Multiset" "HOL-Library.Quotient_List"
begin

text \<open>
  The type of finite sets is created by a quotient construction
  over lists. The definition of the equivalence:
\<close>

definition
  list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50)
where
  [simp]: "xs \<approx> ys \<longleftrightarrow> set xs = set ys"

lemma list_eq_reflp:
  "reflp list_eq"
  by (auto intro: reflpI)

lemma list_eq_symp:
  "symp list_eq"
  by (auto intro: sympI)

lemma list_eq_transp:
  "transp list_eq"
  by (auto intro: transpI)

lemma list_eq_equivp:
  "equivp list_eq"
  by (auto intro: equivpI list_eq_reflp list_eq_symp list_eq_transp)

text \<open>The \<open>fset\<close> type\<close>

quotient_type
  'a fset = "'a list" / "list_eq"
  by (rule list_eq_equivp)

text \<open>
  Definitions for sublist, cardinality,
  intersection, difference and respectful fold over
  lists.
\<close>

declare List.member_def [simp]

definition
  sub_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
where
  [simp]: "sub_list xs ys \<longleftrightarrow> set xs \<subseteq> set ys"

definition
  card_list :: "'a list \<Rightarrow> nat"
where
  [simp]: "card_list xs = card (set xs)"

definition
  inter_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  [simp]: "inter_list xs ys = [x \<leftarrow> xs. x \<in> set xs \<and> x \<in> set ys]"

definition
  diff_list :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  [simp]: "diff_list xs ys = [x \<leftarrow> xs. x \<notin> set ys]"

definition
  rsp_fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> bool"
where
  "rsp_fold f \<longleftrightarrow> (\<forall>u v. f u \<circ> f v = f v \<circ> f u)"

lemma rsp_foldI:
  "(\<And>u v. f u \<circ> f v = f v \<circ> f u) \<Longrightarrow> rsp_fold f"
  by (simp add: rsp_fold_def)

lemma rsp_foldE:
  assumes "rsp_fold f"
  obtains "f u \<circ> f v = f v \<circ> f u"
  using assms by (simp add: rsp_fold_def)

definition
  fold_once :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
where
  "fold_once f xs = (if rsp_fold f then fold f (remdups xs) else id)"

lemma fold_once_default [simp]:
  "\<not> rsp_fold f \<Longrightarrow> fold_once f xs = id"
  by (simp add: fold_once_def)

lemma fold_once_fold_remdups:
  "rsp_fold f \<Longrightarrow> fold_once f xs = fold f (remdups xs)"
  by (simp add: fold_once_def)

section \<open>Quotient composition lemmas\<close>

lemma list_all2_refl':
  assumes q: "equivp R"
  shows "(list_all2 R) r r"
  by (rule list_all2_refl) (metis equivp_def q)

lemma compose_list_refl:
  assumes q: "equivp R"
  shows "(list_all2 R OOO (\<approx>)) r r"
proof
  have *: "r \<approx> r" by (rule equivp_reflp[OF fset_equivp])
  show "list_all2 R r r" by (rule list_all2_refl'[OF q])
  with * show "((\<approx>) OO list_all2 R) r r" ..
qed

lemma map_list_eq_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba"
  by (simp only: list_eq_def set_map)

lemma quotient_compose_list_g:
  assumes q: "Quotient3 R Abs Rep"
  and     e: "equivp R"
  shows  "Quotient3 ((list_all2 R) OOO (\<approx>))
    (abs_fset \<circ> (map Abs)) ((map Rep) \<circ> rep_fset)"
  unfolding Quotient3_def comp_def
proof (intro conjI allI)
  fix a r s
  show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
    by (simp add: abs_o_rep[OF q] Quotient3_abs_rep[OF Quotient3_fset] List.map.id)
  have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule list_all2_refl'[OF e])
  have c: "((\<approx>) OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule, rule equivp_reflp[OF fset_equivp]) (rule b)
  show "(list_all2 R OOO (\<approx>)) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
    by (rule, rule list_all2_refl'[OF e]) (rule c)
  show "(list_all2 R OOO (\<approx>)) r s = ((list_all2 R OOO (\<approx>)) r r \<and>
        (list_all2 R OOO (\<approx>)) s s \<and> abs_fset (map Abs r) = abs_fset (map Abs s))"
  proof (intro iffI conjI)
    show "(list_all2 R OOO (\<approx>)) r r" by (rule compose_list_refl[OF e])
    show "(list_all2 R OOO (\<approx>)) s s" by (rule compose_list_refl[OF e])
  next
    assume a: "(list_all2 R OOO (\<approx>)) r s"
    then have b: "map Abs r \<approx> map Abs s"
    proof (elim relcomppE)
      fix b ba
      assume c: "list_all2 R r b"
      assume d: "b \<approx> ba"
      assume e: "list_all2 R ba s"
      have f: "map Abs r = map Abs b"
        using Quotient3_rel[OF list_quotient3[OF q]] c by blast
      have "map Abs ba = map Abs s"
        using Quotient3_rel[OF list_quotient3[OF q]] e by blast
      then have g: "map Abs s = map Abs ba" by simp
      then show "map Abs r \<approx> map Abs s" using d f map_list_eq_cong by simp
    qed
    then show "abs_fset (map Abs r) = abs_fset (map Abs s)"
      using Quotient3_rel[OF Quotient3_fset] by blast
  next
    assume a: "(list_all2 R OOO (\<approx>)) r r \<and> (list_all2 R OOO (\<approx>)) s s
      \<and> abs_fset (map Abs r) = abs_fset (map Abs s)"
    then have s: "(list_all2 R OOO (\<approx>)) s s" by simp
    have d: "map Abs r \<approx> map Abs s"
      by (subst Quotient3_rel [OF Quotient3_fset, symmetric]) (simp add: a)
    have b: "map Rep (map Abs r) \<approx> map Rep (map Abs s)"
      by (rule map_list_eq_cong[OF d])
    have y: "list_all2 R (map Rep (map Abs s)) s"
      by (fact rep_abs_rsp_left[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of s]])
    have c: "((\<approx>) OO list_all2 R) (map Rep (map Abs r)) s"
      by (rule relcomppI) (rule b, rule y)
    have z: "list_all2 R r (map Rep (map Abs r))"
      by (fact rep_abs_rsp[OF list_quotient3[OF q], OF list_all2_refl'[OF e, of r]])
    then show "(list_all2 R OOO (\<approx>)) r s"
      using a c relcomppI by simp
  qed
qed

lemma quotient_compose_list[quot_thm]:
  shows  "Quotient3 ((list_all2 (\<approx>)) OOO (\<approx>))
    (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)"
  by (rule quotient_compose_list_g, rule Quotient3_fset, rule list_eq_equivp)

section \<open>Quotient definitions for fsets\<close>

subsection \<open>Finite sets are a bounded, distributive lattice with minus\<close>

instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
begin

quotient_definition
  "bot :: 'a fset"
  is "Nil :: 'a list" done

abbreviation
  empty_fset  ("{||}")
where
  "{||} \<equiv> bot :: 'a fset"

quotient_definition
  "less_eq_fset :: ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)"
  is "sub_list :: ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" by simp

abbreviation
  subset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50)
where
  "xs |\<subseteq>| ys \<equiv> xs \<le> ys"

definition
  less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool"
where
  "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)"

abbreviation
  psubset_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50)
where
  "xs |\<subset>| ys \<equiv> xs < ys"

quotient_definition
  "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
  is "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp

abbreviation
  union_fset (infixl "|\<union>|" 65)
where
  "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)"

quotient_definition
  "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
  is "inter_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by simp

abbreviation
  inter_fset (infixl "|\<inter>|" 65)
where
  "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)"

quotient_definition
  "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
  is "diff_list :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" by fastforce

instance
proof
  fix x y z :: "'a fset"
  show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x"
    by (unfold less_fset_def, descending) auto
  show "x |\<subseteq>| x" by (descending) (simp)
  show "{||} |\<subseteq>| x" by (descending) (simp)
  show "x |\<subseteq>| x |\<union>| y" by (descending) (simp)
  show "y |\<subseteq>| x |\<union>| y" by (descending) (simp)
  show "x |\<inter>| y |\<subseteq>| x" by (descending) (auto)
  show "x |\<inter>| y |\<subseteq>| y" by (descending) (auto)
  show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)"
    by (descending) (auto)
next
  fix x y z :: "'a fset"
  assume a: "x |\<subseteq>| y"
  assume b: "y |\<subseteq>| z"
  show "x |\<subseteq>| z" using a b by (descending) (simp)
next
  fix x y :: "'a fset"
  assume a: "x |\<subseteq>| y"
  assume b: "y |\<subseteq>| x"
  show "x = y" using a b by (descending) (auto)
next
  fix x y z :: "'a fset"
  assume a: "y |\<subseteq>| x"
  assume b: "z |\<subseteq>| x"
  show "y |\<union>| z |\<subseteq>| x" using a b by (descending) (simp)
next
  fix x y z :: "'a fset"
  assume a: "x |\<subseteq>| y"
  assume b: "x |\<subseteq>| z"
  show "x |\<subseteq>| y |\<inter>| z" using a b by (descending) (auto)
qed

end

subsection \<open>Other constants for fsets\<close>

quotient_definition
  "insert_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
  is "Cons" by auto

syntax
  "_insert_fset"     :: "args => 'a fset"  ("{|(_)|}")

translations
  "{|x, xs|}" == "CONST insert_fset x {|xs|}"
  "{|x|}"     == "CONST insert_fset x {||}"

quotient_definition
  fset_member
where
  "fset_member :: 'a fset \<Rightarrow> 'a \<Rightarrow> bool" is "List.member" by fastforce

abbreviation
  in_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50)
where
  "x |\<in>| S \<equiv> fset_member S x"

abbreviation
  notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50)
where
  "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"

subsection \<open>Other constants on the Quotient Type\<close>

quotient_definition
  "card_fset :: 'a fset \<Rightarrow> nat"
  is card_list by simp

quotient_definition
  "map_fset :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
  is map by simp

quotient_definition
  "remove_fset :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
  is removeAll by simp

quotient_definition
  "fset :: 'a fset \<Rightarrow> 'a set"
  is "set" by simp

lemma fold_once_set_equiv:
  assumes "xs \<approx> ys"
  shows "fold_once f xs = fold_once f ys"
proof (cases "rsp_fold f")
  case False then show ?thesis by simp
next
  case True
  then have "\<And>x y. x \<in> set (remdups xs) \<Longrightarrow> y \<in> set (remdups xs) \<Longrightarrow> f x \<circ> f y = f y \<circ> f x"
    by (rule rsp_foldE)
  moreover from assms have "mset (remdups xs) = mset (remdups ys)"
    by (simp add: set_eq_iff_mset_remdups_eq)
  ultimately have "fold f (remdups xs) = fold f (remdups ys)"
    by (rule fold_multiset_equiv)
  with True show ?thesis by (simp add: fold_once_fold_remdups)
qed

quotient_definition
  "fold_fset :: ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b \<Rightarrow> 'b"
  is fold_once by (rule fold_once_set_equiv)

lemma concat_rsp_pre:
  assumes a: "list_all2 (\<approx>) x x'"
  and     b: "x' \<approx> y'"
  and     c: "list_all2 (\<approx>) y' y"
  and     d: "\<exists>x\<in>set x. xa \<in> set x"
  shows "\<exists>x\<in>set y. xa \<in> set x"
proof -
  obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto
  have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_all2_find_element[OF e a])
  then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto
  have "ya \<in> set y'" using b h by simp
  then have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" using c by (rule list_all2_find_element)
  then show ?thesis using f i by auto
qed

quotient_definition
  "concat_fset :: ('a fset) fset \<Rightarrow> 'a fset"
  is concat
proof (elim relcomppE)
fix a b ba bb
  assume a: "list_all2 (\<approx>) a ba"
  with list_symp [OF list_eq_symp] have a': "list_all2 (\<approx>) ba a" by (rule sympE)
  assume b: "ba \<approx> bb"
  with list_eq_symp have b': "bb \<approx> ba" by (rule sympE)
  assume c: "list_all2 (\<approx>) bb b"
  with list_symp [OF list_eq_symp] have c': "list_all2 (\<approx>) b bb" by (rule sympE)
  have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
  proof
    fix x
    show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)"
    proof
      assume d: "\<exists>xa\<in>set a. x \<in> set xa"
      show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d])
    next
      assume e: "\<exists>xa\<in>set b. x \<in> set xa"
      show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e])
    qed
  qed
  then show "concat a \<approx> concat b" by auto
qed

quotient_definition
  "filter_fset :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
  is filter by force

subsection \<open>Compositional respectfulness and preservation lemmas\<close>

lemma Nil_rsp2 [quot_respect]:
  shows "(list_all2 (\<approx>) OOO (\<approx>)) Nil Nil"
  by (rule compose_list_refl, rule list_eq_equivp)

lemma Cons_rsp2 [quot_respect]:
  shows "((\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>)) Cons Cons"
  apply (auto intro!: rel_funI)
  apply (rule_tac b="x # b" in relcomppI)
  apply auto
  apply (rule_tac b="x # ba" in relcomppI)
  apply auto
  done

lemma Nil_prs2 [quot_preserve]:
  assumes "Quotient3 R Abs Rep"
  shows "(Abs \<circ> map f) [] = Abs []"
  by simp

lemma Cons_prs2 [quot_preserve]:
  assumes q: "Quotient3 R1 Abs1 Rep1"
  and     r: "Quotient3 R2 Abs2 Rep2"
  shows "(Rep1 ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) (#) = (id ---> Rep2 ---> Abs2) (#)"
  by (auto simp add: fun_eq_iff comp_def Quotient3_abs_rep [OF q])

lemma append_prs2 [quot_preserve]:
  assumes q: "Quotient3 R1 Abs1 Rep1"
  and     r: "Quotient3 R2 Abs2 Rep2"
  shows "((map Rep1 \<circ> Rep2) ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) (@) =
    (Rep2 ---> Rep2 ---> Abs2) (@)"
  by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id)

lemma list_all2_app_l:
  assumes a: "reflp R"
  and b: "list_all2 R l r"
  shows "list_all2 R (z @ l) (z @ r)"
  using a b by (induct z) (auto elim: reflpE)

lemma append_rsp2_pre0:
  assumes a:"list_all2 (\<approx>) x x'"
  shows "list_all2 (\<approx>) (x @ z) (x' @ z)"
  using a apply (induct x x' rule: list_induct2')
  by simp_all (rule list_all2_refl'[OF list_eq_equivp])

lemma append_rsp2_pre1:
  assumes a:"list_all2 (\<approx>) x x'"
  shows "list_all2 (\<approx>) (z @ x) (z @ x')"
  using a apply (induct x x' arbitrary: z rule: list_induct2')
  apply (rule list_all2_refl'[OF list_eq_equivp])
  apply (simp_all del: list_eq_def)
  apply (rule list_all2_app_l)
  apply (simp_all add: reflpI)
  done

lemma append_rsp2_pre:
  assumes "list_all2 (\<approx>) x x'"
    and "list_all2 (\<approx>) z z'"
  shows "list_all2 (\<approx>) (x @ z) (x' @ z')"
  using assms by (rule list_all2_appendI)

lemma compositional_rsp3:
  assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C"
  shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C"
  by (auto intro!: rel_funI)
     (metis (full_types) assms rel_funE relcomppI)

lemma append_rsp2 [quot_respect]:
  "(list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>)) append append"
  by (intro compositional_rsp3)
     (auto intro!: rel_funI simp add: append_rsp2_pre)

lemma map_rsp2 [quot_respect]:
  "(((\<approx>) ===> (\<approx>)) ===> list_all2 (\<approx>) OOO (\<approx>) ===> list_all2 (\<approx>) OOO (\<approx>)) map map"
proof (auto intro!: rel_funI)
  fix f f' :: "'a list \<Rightarrow> 'b list"
  fix xa ya x y :: "'a list list"
  assume fs: "((\<approx>) ===> (\<approx>)) f f'" and x: "list_all2 (\<approx>) xa x" and xy: "set x = set y" and y: "list_all2 (\<approx>) y ya"
  have a: "(list_all2 (\<approx>)) (map f xa) (map f x)"
    using x
    by (induct xa x rule: list_induct2')
       (simp_all, metis fs rel_funE list_eq_def)
  have b: "set (map f x) = set (map f y)"
    using xy fs
    by (induct x y rule: list_induct2')
       (simp_all, metis image_insert)
  have c: "(list_all2 (\<approx>)) (map f y) (map f' ya)"
    using y fs
    by (induct y ya rule: list_induct2')
       (simp_all, metis apply_rsp' list_eq_def)
  show "(list_all2 (\<approx>) OOO (\<approx>)) (map f xa) (map f' ya)"
    by (metis a b c list_eq_def relcomppI)
qed

lemma map_prs2 [quot_preserve]:
  shows "((abs_fset ---> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) map = (id ---> rep_fset ---> abs_fset) map"
  by (auto simp add: fun_eq_iff)
     (simp only: map_map[symmetric] map_prs_aux[OF Quotient3_fset Quotient3_fset])

section \<open>Lifted theorems\<close>

subsection \<open>fset\<close>

lemma fset_simps [simp]:
  shows "fset {||} = {}"
  and   "fset (insert_fset x S) = insert x (fset S)"
  by (descending, simp)+

lemma finite_fset [simp]:
  shows "finite (fset S)"
  by (descending) (simp)

lemma fset_cong:
  shows "fset S = fset T \<longleftrightarrow> S = T"
  by (descending) (simp)

lemma filter_fset [simp]:
  shows "fset (filter_fset P xs) = Collect P \<inter> fset xs"
  by (descending) (auto)

lemma remove_fset [simp]:
  shows "fset (remove_fset x xs) = fset xs - {x}"
  by (descending) (simp)

lemma inter_fset [simp]:
  shows "fset (xs |\<inter>| ys) = fset xs \<inter> fset ys"
  by (descending) (auto)

lemma union_fset [simp]:
  shows "fset (xs |\<union>| ys) = fset xs \<union> fset ys"
  by (lifting set_append)

lemma minus_fset [simp]:
  shows "fset (xs - ys) = fset xs - fset ys"
  by (descending) (auto)

subsection \<open>in_fset\<close>

lemma in_fset:
  shows "x |\<in>| S \<longleftrightarrow> x \<in> fset S"
  by descending simp

lemma notin_fset:
  shows "x |\<notin>| S \<longleftrightarrow> x \<notin> fset S"
  by (simp add: in_fset)

lemma notin_empty_fset:
  shows "x |\<notin>| {||}"
  by (simp add: in_fset)

lemma fset_eq_iff:
  shows "S = T \<longleftrightarrow> (\<forall>x. (x |\<in>| S) = (x |\<in>| T))"
  by descending auto

lemma none_in_empty_fset:
  shows "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}"
  by descending simp

subsection \<open>insert_fset\<close>

lemma in_insert_fset_iff [simp]:
  shows "x |\<in>| insert_fset y S \<longleftrightarrow> x = y \<or> x |\<in>| S"
  by descending simp

lemma
  shows insert_fsetI1: "x |\<in>| insert_fset x S"
  and   insert_fsetI2: "x |\<in>| S \<Longrightarrow> x |\<in>| insert_fset y S"
  by simp_all

lemma insert_absorb_fset [simp]:
  shows "x |\<in>| S \<Longrightarrow> insert_fset x S = S"
  by (descending) (auto)

lemma empty_not_insert_fset[simp]:
  shows "{||} \<noteq> insert_fset x S"
  and   "insert_fset x S \<noteq> {||}"
  by (descending, simp)+

lemma insert_fset_left_comm:
  shows "insert_fset x (insert_fset y S) = insert_fset y (insert_fset x S)"
  by (descending) (auto)

lemma insert_fset_left_idem:
  shows "insert_fset x (insert_fset x S) = insert_fset x S"
  by (descending) (auto)

lemma singleton_fset_eq[simp]:
  shows "{|x|} = {|y|} \<longleftrightarrow> x = y"
  by (descending) (auto)

lemma in_fset_mdef:
  shows "x |\<in>| F \<longleftrightarrow> x |\<notin>| (F - {|x|}) \<and> F = insert_fset x (F - {|x|})"
  by (descending) (auto)

subsection \<open>union_fset\<close>

lemmas [simp] =
  sup_bot_left[where 'a="'a fset"]
  sup_bot_right[where 'a="'a fset"]

lemma union_insert_fset [simp]:
  shows "insert_fset x S |\<union>| T = insert_fset x (S |\<union>| T)"
  by (lifting append.simps(2))

lemma singleton_union_fset_left:
  shows "{|a|} |\<union>| S = insert_fset a S"
  by simp

lemma singleton_union_fset_right:
  shows "S |\<union>| {|a|} = insert_fset a S"
  by (subst sup.commute) simp

lemma in_union_fset:
  shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T"
  by (descending) (simp)

subsection \<open>minus_fset\<close>

lemma minus_in_fset:
  shows "x |\<in>| (xs - ys) \<longleftrightarrow> x |\<in>| xs \<and> x |\<notin>| ys"
  by (descending) (simp)

lemma minus_insert_fset:
  shows "insert_fset x xs - ys = (if x |\<in>| ys then xs - ys else insert_fset x (xs - ys))"
  by (descending) (auto)

lemma minus_insert_in_fset[simp]:
  shows "x |\<in>| ys \<Longrightarrow> insert_fset x xs - ys = xs - ys"
  by (simp add: minus_insert_fset)

lemma minus_insert_notin_fset[simp]:
  shows "x |\<notin>| ys \<Longrightarrow> insert_fset x xs - ys = insert_fset x (xs - ys)"
  by (simp add: minus_insert_fset)

lemma in_minus_fset:
  shows "x |\<in>| F - S \<Longrightarrow> x |\<notin>| S"
  unfolding in_fset minus_fset
  by blast

lemma notin_minus_fset:
  shows "x |\<in>| S \<Longrightarrow> x |\<notin>| F - S"
  unfolding in_fset minus_fset
  by blast

subsection \<open>remove_fset\<close>

lemma in_remove_fset:
  shows "x |\<in>| remove_fset y S \<longleftrightarrow> x |\<in>| S \<and> x \<noteq> y"
  by (descending) (simp)

lemma notin_remove_fset:
  shows "x |\<notin>| remove_fset x S"
  by (descending) (simp)

lemma notin_remove_ident_fset:
  shows "x |\<notin>| S \<Longrightarrow> remove_fset x S = S"
  by (descending) (simp)

lemma remove_fset_cases:
  shows "S = {||} \<or> (\<exists>x. x |\<in>| S \<and> S = insert_fset x (remove_fset x S))"
  by (descending) (auto simp add: insert_absorb)

subsection \<open>inter_fset\<close>

lemma inter_empty_fset_l:
  shows "{||} |\<inter>| S = {||}"
  by simp

lemma inter_empty_fset_r:
  shows "S |\<inter>| {||} = {||}"
  by simp

lemma inter_insert_fset:
  shows "insert_fset x S |\<inter>| T = (if x |\<in>| T then insert_fset x (S |\<inter>| T) else S |\<inter>| T)"
  by (descending) (auto)

lemma in_inter_fset:
  shows "x |\<in>| (S |\<inter>| T) \<longleftrightarrow> x |\<in>| S \<and> x |\<in>| T"
  by (descending) (simp)

subsection \<open>subset_fset and psubset_fset\<close>

lemma subset_fset:
  shows "xs |\<subseteq>| ys \<longleftrightarrow> fset xs \<subseteq> fset ys"
  by (descending) (simp)

lemma psubset_fset:
  shows "xs |\<subset>| ys \<longleftrightarrow> fset xs \<subset> fset ys"
  unfolding less_fset_def
  by (descending) (auto)

lemma subset_insert_fset:
  shows "(insert_fset x xs) |\<subseteq>| ys \<longleftrightarrow> x |\<in>| ys \<and> xs |\<subseteq>| ys"
  by (descending) (simp)

lemma subset_in_fset:
  shows "xs |\<subseteq>| ys = (\<forall>x. x |\<in>| xs \<longrightarrow> x |\<in>| ys)"
  by (descending) (auto)

lemma subset_empty_fset:
  shows "xs |\<subseteq>| {||} \<longleftrightarrow> xs = {||}"
  by (descending) (simp)

lemma not_psubset_empty_fset:
  shows "\<not> xs |\<subset>| {||}"
  by (metis fset_simps(1) psubset_fset not_psubset_empty)

subsection \<open>map_fset\<close>

lemma map_fset_simps [simp]:
   shows "map_fset f {||} = {||}"
  and   "map_fset f (insert_fset x S) = insert_fset (f x) (map_fset f S)"
  by (descending, simp)+

lemma map_fset_image [simp]:
  shows "fset (map_fset f S) = f ` (fset S)"
  by (descending) (simp)

lemma inj_map_fset_cong:
  shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T"
  by (descending) (metis inj_vimage_image_eq list_eq_def set_map)

lemma map_union_fset:
  shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T"
  by (descending) (simp)

lemma in_fset_map_fset[simp]: "a |\<in>| map_fset f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
  by descending auto

subsection \<open>card_fset\<close>

lemma card_fset:
  shows "card_fset xs = card (fset xs)"
  by (descending) (simp)

lemma card_insert_fset_iff [simp]:
  shows "card_fset (insert_fset x S) = (if x |\<in>| S then card_fset S else Suc (card_fset S))"
  by (descending) (simp add: insert_absorb)

lemma card_fset_0[simp]:
  shows "card_fset S = 0 \<longleftrightarrow> S = {||}"
  by (descending) (simp)

lemma card_empty_fset[simp]:
  shows "card_fset {||} = 0"
  by (simp add: card_fset)

lemma card_fset_1:
  shows "card_fset S = 1 \<longleftrightarrow> (\<exists>x. S = {|x|})"
  by (descending) (auto simp add: card_Suc_eq)

lemma card_fset_gt_0:
  shows "x \<in> fset S \<Longrightarrow> 0 < card_fset S"
  by (descending) (auto simp add: card_gt_0_iff)

lemma card_notin_fset:
  shows "(x |\<notin>| S) = (card_fset (insert_fset x S) = Suc (card_fset S))"
  by simp

lemma card_fset_Suc:
  shows "card_fset S = Suc n \<Longrightarrow> \<exists>x T. x |\<notin>| T \<and> S = insert_fset x T \<and> card_fset T = n"
  apply(descending)
  apply(auto dest!: card_eq_SucD)
  by (metis Diff_insert_absorb set_removeAll)

lemma card_remove_fset_iff [simp]:
  shows "card_fset (remove_fset y S) = (if y |\<in>| S then card_fset S - 1 else card_fset S)"
  by (descending) (simp)

lemma card_Suc_exists_in_fset:
  shows "card_fset S = Suc n \<Longrightarrow> \<exists>a. a |\<in>| S"
  by (drule card_fset_Suc) (auto)

lemma in_card_fset_not_0:
  shows "a |\<in>| A \<Longrightarrow> card_fset A \<noteq> 0"
  by (descending) (auto)

lemma card_fset_mono:
  shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset xs \<le> card_fset ys"
  unfolding card_fset psubset_fset
  by (simp add: card_mono subset_fset)

lemma card_subset_fset_eq:
  shows "xs |\<subseteq>| ys \<Longrightarrow> card_fset ys \<le> card_fset xs \<Longrightarrow> xs = ys"
  unfolding card_fset subset_fset
  by (auto dest: card_seteq[OF finite_fset] simp add: fset_cong)

lemma psubset_card_fset_mono:
  shows "xs |\<subset>| ys \<Longrightarrow> card_fset xs < card_fset ys"
  unfolding card_fset subset_fset
  by (metis finite_fset psubset_fset psubset_card_mono)

lemma card_union_inter_fset:
  shows "card_fset xs + card_fset ys = card_fset (xs |\<union>| ys) + card_fset (xs |\<inter>| ys)"
  unfolding card_fset union_fset inter_fset
  by (rule card_Un_Int[OF finite_fset finite_fset])

lemma card_union_disjoint_fset:
  shows "xs |\<inter>| ys = {||} \<Longrightarrow> card_fset (xs |\<union>| ys) = card_fset xs + card_fset ys"
  unfolding card_fset union_fset
  apply (rule card_Un_disjoint[OF finite_fset finite_fset])
  by (metis inter_fset fset_simps(1))

lemma card_remove_fset_less1:
  shows "x |\<in>| xs \<Longrightarrow> card_fset (remove_fset x xs) < card_fset xs"
  unfolding card_fset in_fset remove_fset
  by (rule card_Diff1_less[OF finite_fset])

lemma card_remove_fset_less2:
  shows "x |\<in>| xs \<Longrightarrow> y |\<in>| xs \<Longrightarrow> card_fset (remove_fset y (remove_fset x xs)) < card_fset xs"
  unfolding card_fset remove_fset in_fset
  by (rule card_Diff2_less[OF finite_fset])

lemma card_remove_fset_le1:
  shows "card_fset (remove_fset x xs) \<le> card_fset xs"
  by simp

lemma card_psubset_fset:
  shows "ys |\<subseteq>| xs \<Longrightarrow> card_fset ys < card_fset xs \<Longrightarrow> ys |\<subset>| xs"
  unfolding card_fset psubset_fset subset_fset
  by (rule card_psubset[OF finite_fset])

lemma card_map_fset_le:
  shows "card_fset (map_fset f xs) \<le> card_fset xs"
  unfolding card_fset map_fset_image
  by (rule card_image_le[OF finite_fset])

lemma card_minus_insert_fset[simp]:
  assumes "a |\<in>| A" and "a |\<notin>| B"
  shows "card_fset (A - insert_fset a B) = card_fset (A - B) - 1"
  using assms  by (simp add: in_fset card_fset)

lemma card_minus_subset_fset:
  assumes "B |\<subseteq>| A"
  shows "card_fset (A - B) = card_fset A - card_fset B"
  using assms
  by (simp add: subset_fset card_fset card_Diff_subset)

lemma card_minus_fset:
  shows "card_fset (A - B) = card_fset A - card_fset (A |\<inter>| B)"
  by (simp add: card_fset card_Diff_subset_Int)

subsection \<open>concat_fset\<close>

lemma concat_empty_fset [simp]:
  shows "concat_fset {||} = {||}"
  by descending simp

lemma concat_insert_fset [simp]:
  shows "concat_fset (insert_fset x S) = x |\<union>| concat_fset S"
  by descending simp

lemma concat_union_fset [simp]:
  shows "concat_fset (xs |\<union>| ys) = concat_fset xs |\<union>| concat_fset ys"
  by descending simp

lemma map_concat_fset:
  shows "map_fset f (concat_fset xs) = concat_fset (map_fset (map_fset f) xs)"
  by (lifting map_concat)

subsection \<open>filter_fset\<close>

lemma subset_filter_fset:
  "filter_fset P xs |\<subseteq>| filter_fset Q xs = (\<forall> x. x |\<in>| xs \<longrightarrow> P x \<longrightarrow> Q x)"
  by descending auto

lemma eq_filter_fset:
  "(filter_fset P xs = filter_fset Q xs) = (\<forall>x. x |\<in>| xs \<longrightarrow> P x = Q x)"
  by descending auto

lemma psubset_filter_fset:
  "(\<And>x. x |\<in>| xs \<Longrightarrow> P x \<Longrightarrow> Q x) \<Longrightarrow> (x |\<in>| xs & \<not> P x & Q x) \<Longrightarrow>
    filter_fset P xs |\<subset>| filter_fset Q xs"
  unfolding less_fset_def by (auto simp add: subset_filter_fset eq_filter_fset)

subsection \<open>fold_fset\<close>

lemma fold_empty_fset:
  "fold_fset f {||} = id"
  by descending (simp add: fold_once_def)

lemma fold_insert_fset: "fold_fset f (insert_fset a A) =
  (if rsp_fold f then if a |\<in>| A then fold_fset f A else fold_fset f A \<circ> f a else id)"
  by descending (simp add: fold_once_fold_remdups)

lemma remdups_removeAll:
  "remdups (removeAll x xs) = remove1 x (remdups xs)"
  by (induct xs) auto

lemma member_commute_fold_once:
  assumes "rsp_fold f"
    and "x \<in> set xs"
  shows "fold_once f xs = fold_once f (removeAll x xs) \<circ> f x"
proof -
  from assms have "fold f (remdups xs) = fold f (remove1 x (remdups xs)) \<circ> f x"
    by (auto intro!: fold_remove1_split elim: rsp_foldE)
  then show ?thesis using \<open>rsp_fold f\<close> by (simp add: fold_once_fold_remdups remdups_removeAll)
qed

lemma in_commute_fold_fset:
  "rsp_fold f \<Longrightarrow> h |\<in>| b \<Longrightarrow> fold_fset f b = fold_fset f (remove_fset h b) \<circ> f h"
  by descending (simp add: member_commute_fold_once)

subsection \<open>Choice in fsets\<close>

lemma fset_choice:
  assumes a: "\<forall>x. x |\<in>| A \<longrightarrow> (\<exists>y. P x y)"
  shows "\<exists>f. \<forall>x. x |\<in>| A \<longrightarrow> P x (f x)"
  using a
  apply(descending)
  using finite_set_choice
  by (auto simp add: Ball_def)

section \<open>Induction and Cases rules for fsets\<close>

lemma fset_exhaust [case_names empty insert, cases type: fset]:
  assumes empty_fset_case: "S = {||} \<Longrightarrow> P"
  and     insert_fset_case: "\<And>x S'. S = insert_fset x S' \<Longrightarrow> P"
  shows "P"
  using assms by (lifting list.exhaust)

lemma fset_induct [case_names empty insert]:
  assumes empty_fset_case: "P {||}"
  and     insert_fset_case: "\<And>x S. P S \<Longrightarrow> P (insert_fset x S)"
  shows "P S"
  using assms
  by (descending) (blast intro: list.induct)

lemma fset_induct_stronger [case_names empty insert, induct type: fset]:
  assumes empty_fset_case: "P {||}"
  and     insert_fset_case: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (insert_fset x S)"
  shows "P S"
proof(induct S rule: fset_induct)
  case empty
  show "P {||}" using empty_fset_case by simp
next
  case (insert x S)
  have "P S" by fact
  then show "P (insert_fset x S)" using insert_fset_case
    by (cases "x |\<in>| S") (simp_all)
qed

lemma fset_card_induct:
  assumes empty_fset_case: "P {||}"
  and     card_fset_Suc_case: "\<And>S T. Suc (card_fset S) = (card_fset T) \<Longrightarrow> P S \<Longrightarrow> P T"
  shows "P S"
proof (induct S)
  case empty
  show "P {||}" by (rule empty_fset_case)
next
  case (insert x S)
  have h: "P S" by fact
  have "x |\<notin>| S" by fact
  then have "Suc (card_fset S) = card_fset (insert_fset x S)"
    using card_fset_Suc by auto
  then show "P (insert_fset x S)"
    using h card_fset_Suc_case by simp
qed

lemma fset_raw_strong_cases:
  obtains "xs = []"
    | ys x where "\<not> List.member ys x" and "xs \<approx> x # ys"
proof (induct xs)
  case Nil
  then show thesis by simp
next
  case (Cons a xs)
  have a: "\<lbrakk>xs = [] \<Longrightarrow> thesis; \<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis"
    by (rule Cons(1))
  have b: "\<And>x' ys'. \<lbrakk>\<not> List.member ys' x'; a # xs \<approx> x' # ys'\<rbrakk> \<Longrightarrow> thesis" by fact
  have c: "xs = [] \<Longrightarrow> thesis" using b
    apply(simp)
    by (metis list.set(1) emptyE empty_subsetI)
  have "\<And>x ys. \<lbrakk>\<not> List.member ys x; xs \<approx> x # ys\<rbrakk> \<Longrightarrow> thesis"
  proof -
    fix x :: 'a
    fix ys :: "'a list"
    assume d:"\<not> List.member ys x"
    assume e:"xs \<approx> x # ys"
    show thesis
    proof (cases "x = a")
      assume h: "x = a"
      then have f: "\<not> List.member ys a" using d by simp
      have g: "a # xs \<approx> a # ys" using e h by auto
      show thesis using b f g by simp
    next
      assume h: "x \<noteq> a"
      then have f: "\<not> List.member (a # ys) x" using d by auto
      have g: "a # xs \<approx> x # (a # ys)" using e h by auto
      show thesis using b f g by (simp del: List.member_def)
    qed
  qed
  then show thesis using a c by blast
qed

lemma fset_strong_cases:
  obtains "xs = {||}"
    | ys x where "x |\<notin>| ys" and "xs = insert_fset x ys"
  by (lifting fset_raw_strong_cases)

lemma fset_induct2:
  "P {||} {||} \<Longrightarrow>
  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (insert_fset x xs) {||}) \<Longrightarrow>
  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (insert_fset y ys)) \<Longrightarrow>
  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (insert_fset x xs) (insert_fset y ys)) \<Longrightarrow>
  P xsa ysa"
  apply (induct xsa arbitrary: ysa)
  apply (induct_tac x rule: fset_induct_stronger)
  apply simp_all
  apply (induct_tac xa rule: fset_induct_stronger)
  apply simp_all
  done

text \<open>Extensionality\<close>

lemma fset_eqI:
  assumes "\<And>x. x \<in> fset A \<longleftrightarrow> x \<in> fset B"
  shows "A = B"
using assms proof (induct A arbitrary: B)
  case empty then show ?case
    by (auto simp add: in_fset none_in_empty_fset [symmetric] sym)
next
  case (insert x A)
  from insert.prems insert.hyps(1) have "\<And>z. z \<in> fset A \<longleftrightarrow> z \<in> fset (B - {|x|})"
    by (auto simp add: in_fset)
  then have A: "A = B - {|x|}" by (rule insert.hyps(2))
  with insert.prems [symmetric, of x] have "x |\<in>| B" by (simp add: in_fset)
  with A show ?case by (metis in_fset_mdef)
qed

subsection \<open>alternate formulation with a different decomposition principle
  and a proof of equivalence\<close>

inductive
  list_eq2 :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>2 _")
where
  "(a # b # xs) \<approx>2 (b # a # xs)"
| "[] \<approx>2 []"
| "xs \<approx>2 ys \<Longrightarrow> ys \<approx>2 xs"
| "(a # a # xs) \<approx>2 (a # xs)"
| "xs \<approx>2 ys \<Longrightarrow> (a # xs) \<approx>2 (a # ys)"
| "xs1 \<approx>2 xs2 \<Longrightarrow> xs2 \<approx>2 xs3 \<Longrightarrow> xs1 \<approx>2 xs3"

lemma list_eq2_refl:
  shows "xs \<approx>2 xs"
  by (induct xs) (auto intro: list_eq2.intros)

lemma cons_delete_list_eq2:
  shows "(a # (removeAll a A)) \<approx>2 (if List.member A a then A else a # A)"
  apply (induct A)
  apply (simp add: list_eq2_refl)
  apply (case_tac "List.member (aa # A) a")
  apply (simp_all)
  apply (case_tac [!] "a = aa")
  apply (simp_all)
  apply (case_tac "List.member A a")
  apply (auto)[2]
  apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))
  apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))
  apply (auto simp add: list_eq2_refl)
  done

lemma member_delete_list_eq2:
  assumes a: "List.member r e"
  shows "(e # removeAll e r) \<approx>2 r"
  using a cons_delete_list_eq2[of e r]
  by simp

lemma list_eq2_equiv:
  "(l \<approx> r) \<longleftrightarrow> (list_eq2 l r)"
proof
  show "list_eq2 l r \<Longrightarrow> l \<approx> r" by (induct rule: list_eq2.induct) auto
next
  {
    fix n
    assume a: "card_list l = n" and b: "l \<approx> r"
    have "l \<approx>2 r"
      using a b
    proof (induct n arbitrary: l r)
      case 0
      have "card_list l = 0" by fact
      then have "\<forall>x. \<not> List.member l x" by auto
      then have z: "l = []" by auto
      then have "r = []" using \<open>l \<approx> r\<close> by simp
      then show ?case using z list_eq2_refl by simp
    next
      case (Suc m)
      have b: "l \<approx> r" by fact
      have d: "card_list l = Suc m" by fact
      then have "\<exists>a. List.member l a"
        apply(simp)
        apply(drule card_eq_SucD)
        apply(blast)
        done
      then obtain a where e: "List.member l a" by auto
      then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b
        by auto
      have f: "card_list (removeAll a l) = m" using e d by (simp)
      have g: "removeAll a l \<approx> removeAll a r" using remove_fset.rsp b by simp
      have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
      then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
      have i: "l \<approx>2 (a # removeAll a l)"
        by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]])
      have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
      then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp
    qed
    }
  then show "l \<approx> r \<Longrightarrow> l \<approx>2 r" by blast
qed

(* We cannot write it as "assumes .. shows" since Isabelle changes
   the quantifiers to schematic variables and reintroduces them in
   a different order *)
lemma fset_eq_cases:
 "\<lbrakk>a1 = a2;
   \<And>a b xs. \<lbrakk>a1 = insert_fset a (insert_fset b xs); a2 = insert_fset b (insert_fset a xs)\<rbrakk> \<Longrightarrow> P;
   \<lbrakk>a1 = {||}; a2 = {||}\<rbrakk> \<Longrightarrow> P; \<And>xs ys. \<lbrakk>a1 = ys; a2 = xs; xs = ys\<rbrakk> \<Longrightarrow> P;
   \<And>a xs. \<lbrakk>a1 = insert_fset a (insert_fset a xs); a2 = insert_fset a xs\<rbrakk> \<Longrightarrow> P;
   \<And>xs ys a. \<lbrakk>a1 = insert_fset a xs; a2 = insert_fset a ys; xs = ys\<rbrakk> \<Longrightarrow> P;
   \<And>xs1 xs2 xs3. \<lbrakk>a1 = xs1; a2 = xs3; xs1 = xs2; xs2 = xs3\<rbrakk> \<Longrightarrow> P\<rbrakk>
  \<Longrightarrow> P"
  by (lifting list_eq2.cases[simplified list_eq2_equiv[symmetric]])

lemma fset_eq_induct:
  assumes "x1 = x2"
  and "\<And>a b xs. P (insert_fset a (insert_fset b xs)) (insert_fset b (insert_fset a xs))"
  and "P {||} {||}"
  and "\<And>xs ys. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P ys xs"
  and "\<And>a xs. P (insert_fset a (insert_fset a xs)) (insert_fset a xs)"
  and "\<And>xs ys a. \<lbrakk>xs = ys; P xs ys\<rbrakk> \<Longrightarrow> P (insert_fset a xs) (insert_fset a ys)"
  and "\<And>xs1 xs2 xs3. \<lbrakk>xs1 = xs2; P xs1 xs2; xs2 = xs3; P xs2 xs3\<rbrakk> \<Longrightarrow> P xs1 xs3"
  shows "P x1 x2"
  using assms
  by (lifting list_eq2.induct[simplified list_eq2_equiv[symmetric]])

ML \<open>
fun dest_fsetT (Type (\<^type_name>\<open>fset\<close>, [T])) = T
  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
\<close>

no_notation
  list_eq (infix "\<approx>" 50) and
  list_eq2 (infix "\<approx>2" 50)

end

repo: isabelle


text:
header{*Inductive Study of Confidentiality against the General Attacker*}

theory  ConfidentialityGA imports NS_Public_Bad_GA begin

text{*New subsidiary lemmas to reason on a generic agent initial state*}

lemma parts_initState: "parts(initState C) = initState C"
by (cases C, simp)

lemma analz_initState: "analz(initState C) = initState C"
by (cases C, force dest: analz_into_parts)

text{*Generalising over all initial secrets the existing treatment, which is limited to private encryption keys*}

definition staticSecret :: "agent \<Rightarrow> msg set" where
 [simp]: "staticSecret A == {Key (priEK A), Key (priSK A), Key (shrK A)}"

text{*More subsidiary lemmas combining initial secrets and knowledge of generic agent*}

lemma staticSecret_in_initState [simp]:
"staticSecret A \<subseteq> initState A"
by (cases A, simp)
thm parts_insert

lemma staticSecretA_notin_initStateB:
"m \<in> staticSecret A \<Longrightarrow> m \<in> initState B = (A=B)"
by (cases B, auto)

lemma staticSecretA_notin_parts_initStateB:
"m \<in> staticSecret A \<Longrightarrow> m \<in> parts(initState B) = (A=B)"
by (cases B, auto)

lemma staticSecretA_notin_analz_initStateB:
"m \<in> staticSecret A \<Longrightarrow> m \<in> analz(initState B) = (A=B)"
by (cases B, force dest: analz_into_parts)

lemma staticSecret_synth_eq:
"m \<in> staticSecret A \<Longrightarrow> (m \<in> synth H) = (m \<in> H)"
apply force
done

declare staticSecret_def [simp del]

lemma nonce_notin_analz_initState:
  "Nonce N \<notin> analz(initState A)"
by(cases A, auto dest: analz_into_parts)

subsection{*Protocol independent study*}

lemma staticSecret_parts_agent:
 "\<lbrakk>m \<in> parts (knows C evs); m \<in> staticSecret A\<rbrakk> \<Longrightarrow>
   A=C \<or>
  (\<exists>D E X. Says D E X \<in> set evs \<and> m \<in> parts{X}) \<or>
  (\<exists>Y. Notes C Y \<in> set evs \<and> m \<in> parts{Y})"
apply (erule rev_mp)
apply (induct_tac evs)
txt{*@{subgoals [display,indent =1]}*}
apply (simp add: staticSecretA_notin_parts_initStateB)
apply (induct_tac a)
(*Says*)
apply (rule impI)
apply simp
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
(*Gets*)
apply simp
(*Notes*)
apply simp
apply clarify
txt{*@{subgoals [display,indent =1]}*}
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
done

lemma staticSecret_analz_agent:
 "\<lbrakk>m \<in> analz (knows C evs); m \<in> staticSecret A\<rbrakk> \<Longrightarrow>
   A=C \<or>
  (\<exists>D E X. Says D E X \<in> set evs \<and> m \<in> parts{X}) \<or>
  (\<exists>Y. Notes C Y \<in> set evs \<and> m \<in> parts{Y})"
by (drule analz_into_parts [THEN staticSecret_parts_agent])

lemma secret_parts_agent:
 "m \<in> parts (knows C evs)  \<Longrightarrow> m \<in> initState C \<or>
 (\<exists>A B X. Says A B X \<in> set evs \<and> m \<in> parts{X}) \<or>
 (\<exists>Y. Notes C Y \<in> set evs \<and> m \<in> parts{Y})"
apply (erule rev_mp)
apply (induct_tac "evs")
apply (simp add: parts_initState)
apply (induct_tac "a")
(*Says*)
apply (rule impI)
apply simp
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
(*Gets*)
apply simp
(*Notes*)
apply simp
apply clarify
apply (drule parts_insert [THEN equalityD1, THEN subsetD])
apply blast
done

subsection{*Protocol dependent study*}

(*NS_no_Notes moved up in NS_Public_Bad_GA.thy so that it's visible to a sibling theory of this one's

As with DolevYao, studying a guarantee similar to
NS_no_Says_staticSecret makes the specialisation proof strategy collapse, because it elicits the same assumptions of the theorem that should be specified.
*)

lemma NS_staticSecret_parts_agent_weak:
 "\<lbrakk>m \<in> parts (knows C evs); m \<in> staticSecret A;
   evs \<in> ns_public\<rbrakk> \<Longrightarrow>
  A=C \<or> (\<exists>D E X. Says D E X \<in> set evs \<and> m \<in> parts{X})"
apply (blast dest: NS_no_Notes staticSecret_parts_agent)
done

text{*Can't prove the homologous theorem of NS\_Says\_Spy\_staticSecret, hence the specialisation proof strategy cannot be applied*}

(*Simple though illustrative corollary*)
(*note use of Says_imp_knows, an enforcement of the threat model*)
lemma NS_staticSecret_parts_agent_parts:
"\<lbrakk>m \<in> parts (knows C evs); m \<in> staticSecret A; A\<noteq>C; evs \<in> ns_public\<rbrakk> \<Longrightarrow>
  m \<in> parts(knows D evs)"
apply (blast dest: NS_staticSecret_parts_agent_weak Says_imp_knows [THEN parts.Inj] parts_trans)
(*Alternative proof
apply (blast dest: staticSecret_parts_agent NS_no_Notes Says_imp_knows [THEN parts.Inj] parts_trans)*)
done

text{*
The previous theorems show that in general any agent could send anybody's initial secret, namely the threat model does not impose anything against it. However, the actual protocol specification will, where agents either follow the protocol or build messages out of their traffic analysis - this is actually the same in DY

Therefore, we are only left with the direct proof strategy.
*}

lemma NS_staticSecret_parts_agent:
 "\<lbrakk>m \<in> parts (knows C evs); m \<in> staticSecret A;
   C\<noteq>A; evs \<in> ns_public\<rbrakk>
 \<Longrightarrow> \<exists> B X. Says A B X \<in> set evs \<and> m \<in> parts {X}"
apply (erule rev_mp, erule ns_public.induct)
(*Nil*)
apply (simp add: staticSecretA_notin_parts_initStateB)
(*Fake*)
apply simp
apply clarify
apply (drule parts_insert [THEN equalityD1, THEN subsetD])(*shot1*)
apply (case_tac "Aa=A")
apply clarify
txt{*@{subgoals [display,indent=1,goals_limit=2]}*}
apply blast
(*Aa\<noteq>A*)
apply simp
apply clarify (*applies induction hypothesis!*)(*shot2*)
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (drule Fake_parts_sing [THEN subsetD], simp)  (*shot3*)
apply (simp add: staticSecret_synth_eq)
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (blast dest: NS_staticSecret_parts_agent_parts)
(*rest!*)
apply (force simp add: staticSecret_def)+
done

lemma NS_agent_see_staticSecret:
 "\<lbrakk>m \<in> staticSecret A; C\<noteq>A; evs \<in> ns_public\<rbrakk>
 \<Longrightarrow> m \<in> parts (knows C evs) = (\<exists> B X. Says A B X \<in> set evs \<and> m \<in> parts {X})"
apply (force dest: NS_staticSecret_parts_agent Says_imp_knows [THEN parts.Inj] intro: parts_trans)
done

declare analz.Decrypt [rule del]

lemma analz_insert_analz: "
\<lbrakk> c \<notin> parts{Z}; \<forall>K. Key K \<notin> parts{Z}; c \<in> analz(insert Z H)\<rbrakk> \<Longrightarrow> c \<in> analz H"
apply (erule rev_mp, erule rev_mp)
apply (erule analz.induct)
prefer 4
apply clarify
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (blast dest: parts.Body analz.Decrypt)
apply blast+
done

lemma Agent_not_see_NA:
     "\<lbrakk> Key (priEK B) \<notin> analz(knows C evs);
        Key (priEK A) \<notin> analz(knows C evs);
        \<forall>S R Y. Says S R Y \<in> set evs \<longrightarrow>
         Y = Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<or>
         Y = Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<or>
         Nonce NA \<notin> parts{Y} \<and> (\<forall>K. Key K \<notin> parts{Y});
        C\<noteq>A; C\<noteq>B;  evs \<in> ns_public\<rbrakk>
       \<Longrightarrow> Nonce NA \<notin> analz (knows C evs)"
apply (erule rev_mp, erule rev_mp, erule rev_mp, erule ns_public.induct)
apply (simp add: nonce_notin_analz_initState)
apply clarify
apply simp
(*fixing confidentiality of both private keys*)
apply (drule subset_insertI [THEN analz_mono, THEN contra_subsetD])+
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (subgoal_tac "
        \<forall>S R Y.
           (S = Aa \<and> R = Ba \<and> Y = X \<longrightarrow>
            X = Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<or>
            X = Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<or>
            Nonce NA \<notin> parts {X} \<and> (\<forall>K. Key K \<notin> parts {X}))")
prefer 2
apply blast
apply simp
txt{*@{subgoals [display,indent=1,goals_limit=1]}*}
apply (force dest!: analz_insert_analz)
(*Alternative proof
apply (erule disjE) apply simp
apply (erule disjE) apply simp
apply (blast dest: analz_insert_analz)
*)
apply auto
done

end

author: Josh-Tilles

repo: AFP

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