text:
theory NP4_Struct_Action_Semantics
  imports
  Complex_Main
  NP4_Struct_Action_Values
(*  These files contain a minimalistic semantics of P4's action constructs. These files
    specifically extend the previously implemented simple semantics with more complex
    datastructures, in this case the struct datastructure. P4 knows structs, headers,
    enums, header unions and stacks, and tuples. The struct type however is the most
    general of these. Showing that structs are verifiable thus also shows that headers
    (and thus header unions and header stacks), enums, and tuples can be verified using
    Isabelle/HOL. *)
begin
(* ============================================================================================================== *)
(*                                      SMALL STEP SEMANTICS RULES                                                *)
(* ============================================================================================================== *)

(* The way P4 statements update the state and progress. The natural number included is to prove
   that computation always progresses. With every step of the computation this number always
   decreases, indicating progression and ultimately termination. Note that method invocations and
   switch statements are omitted as these can be modelled with the present statements as well. *)
inductive small_step :: "(statOrDecl * state * nat) \<Rightarrow> (statOrDecl * state * nat) \<Rightarrow> bool"
 (infix "\<leadsto>" 55) where
    Exit:       "(ExitStat, s, n) \<leadsto> (EmptyStat, s, n-1)"
  | CondTrue:   "eval e s (BOOL True) \<Longrightarrow> ((ConditionalStat e stmt1 stmt2), s, n) \<leadsto> (stmt1, s, n-1)"
  | CondFalse:  "eval e s (BOOL False) \<Longrightarrow> ((ConditionalStat e stmt1 stmt2), s, n) \<leadsto> (stmt2, s, n-1)"
  | EmptyBlock: "(BlockStat [], s, n) \<leadsto> (EmptyStat, s, n-1)"
  | EmptyFirst: "(BlockStat (EmptyStat # rest), s, n) \<leadsto> (BlockStat rest, s, n-1)"
  | FullBlock:  "(stmt, s, n) \<leadsto> (stmt', s', n') \<Longrightarrow> n' \<le> n \<Longrightarrow> (BlockStat (stmt # rest), s, n) \<leadsto> (BlockStat (stmt' # rest), s', n')"
  | Assign:     "eval e s v \<Longrightarrow> (AssignmentStat (NameLVal vName) e, s, n) \<leadsto> (EmptyStat, s (vName := v), n-1)"
  | VarDecl:    "(VariableDecl (NameLVal vName) (None), s, n) \<leadsto> (EmptyStat, s, n-1)"
  | VarInit:    "eval e s v \<Longrightarrow> (VariableDecl (NameLVal vName) (Some e), s, n) \<leadsto> (EmptyStat, s (vName := v), n-1)"
  | ConstInit:  "eval e s v \<Longrightarrow> (ConstantDecl (NameLVal vName) e, s, n) \<leadsto> (EmptyStat, s (vName := v), n-1)"

declare small_step.intros[simp, intro]

inductive_cases [elim!]: "(EmptyStat, s, n) \<leadsto> ct" "(ExitStat, s, n) \<leadsto> ct" "(ConditionalStat e stmt1 stmt2, s, n) \<leadsto> ct"
  "(BlockStat stmts, s, n) \<leadsto> ct" "(AssignmentStat l e, s, n) \<leadsto> ct" "(VariableDecl l e, s, n) \<leadsto> ct" "(ConstantDecl l e, s, n) \<leadsto> ct"

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

code_pred small_step .

lemma small_step_deterministic: "cs \<leadsto> cs' \<Longrightarrow> cs \<leadsto> cs'' \<Longrightarrow> cs'' = cs'"
proof (induction arbitrary: cs'' rule: small_step.induct)
  case (CondTrue e s stmt1 stmt2 n)
  then show ?case
    using eval_deterministic by auto
next
  case (CondFalse e s stmt1 stmt2 n)
  then show ?case
    using eval_deterministic by auto
next
  case (EmptyFirst rest s n)
  then show ?case
    using eval_deterministic by auto
next
  case (Assign e s v vName n)
  then show ?case
    using eval_deterministic by auto
next
  case (VarInit e s v vName n)
  then show ?case
    using eval_deterministic by auto
next
  case (ConstInit e s v vName n)
  then show ?case
    using eval_deterministic by auto
qed (auto)+

lemma step_equal_or_smaller: "(c, s, n) \<leadsto> (c', s', n') \<Longrightarrow> n' \<le> n"
  apply (induction c rule: statOrDecl.induct)
  apply (auto)
  done

abbreviation equiv_stmt :: "statOrDecl \<Rightarrow> statOrDecl \<Rightarrow> bool" (infix "~" 50) where
  "c ~ c' \<equiv> (\<forall>s t. ((c, s) \<leadsto> t) = ((c', s) \<leadsto> t))"

lemma equiv_refl:  "c ~ c" by simp
lemma equiv_sym:   "(c ~ c') = (c' ~ c)" by auto
lemma equiv_trans: "(c ~ c') \<Longrightarrow> (c' ~ c'') \<Longrightarrow> (c ~ c'')" by simp

(* ============================================================================================================== *)
(*                                        REFLEXIVE TRANSITIVE CLOSURE                                            *)
(* ============================================================================================================== *)

(* Define the reflexive transitive closure on the signature of the small-step semantics. *)
inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
  for r :: "('a \<Rightarrow> 'a \<Rightarrow> bool)" where
refl:   "star r x x" |
step:   "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"

hide_fact (open) refl step

lemma star_trans: "star r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
  apply (induction rule: star.induct)
   apply (assumption)
  apply (metis star.step)
  done

lemmas star_induct = star.induct[of "r:: 'a*'b*'c \<Rightarrow> 'a*'b*'c \<Rightarrow> bool", split_format(complete)]

declare star.refl[simp, intro]

lemma star_step1[simp, intro]: "r x y \<Longrightarrow> star r x y"
  by (metis star.refl star.step)

code_pred star .

(* The reflexive transitive closure of the small step function yields whether a state is reachable in any number of
   steps from the starting state and thereby models complete execution. *)
abbreviation small_steps :: "(statOrDecl * state * nat) \<Rightarrow> (statOrDecl * state * nat) \<Rightarrow> bool" (infix "\<leadsto>*" 55)
  where "x \<leadsto>* y \<equiv> star small_step x y"

lemma star_equal_or_smaller: "(c, s, n) \<leadsto>* (c', s', n') \<Longrightarrow> n' \<le> n"
proof (induction rule: star_induct)
  case (refl a a b)
  then show ?case
    by simp
next
  case (step a a b a a b a a b)
  then show ?case
    by (smt diff_le_self le_trans prod.sel(2) small_step.cases)
qed

(* ============================================================================================================== *)
(*                                          TYPING SYSTEM DEFINITION                                              *)
(* ============================================================================================================== *)

datatype ty = UINTty
  | SINTty
  | IINTty
  | VINTty
  | BOOLty
  | STRINGty
  | ERRORty
  | MATCHty
  | STRUCTty "(vname * ty option) list"

(* Mapping from a variable name to a type symbol *)
type_synonym typeEnv = "vname \<Rightarrow> ty"

(* ============================================================================================================== *)
(*                                STRUCT TYPING SYSTEM HELPER FUNCTIONS DEFINITION                                *)
(* ============================================================================================================== *)

fun
  getValType :: "val \<Rightarrow> ty"
and
  structEntryToType :: "(identifier * vname * val option) \<Rightarrow> (vname * ty option)"
  where
    "structEntryToType (tName, vName, None) = (vName, None)"
  | "structEntryToType (tName, vName, Some v) = (vName, Some (getValType v))"
  | "getValType (UINT n) = UINTty"
  | "getValType (SINT n) = SINTty"
  | "getValType (IINT n) = IINTty"
  | "getValType (VINT n) = VINTty"
  | "getValType (BOOL b) = BOOLty"
  | "getValType (STRING s) = STRINGty"
  | "getValType (ERROR e) = ERRORty"
  | "getValType (MATCH m) = MATCHty"
  | "getValType (STRUCT entries) = STRUCTty (map structEntryToType entries)"

fun
  baseStructEntryToType :: "(identifier * vname * basicType option) \<Rightarrow> (vname * ty option)"
and
  getBaseType :: "basicType \<Rightarrow> ty"
  where
    "baseStructEntryToType (tName, vName, None) = (vName, None)"
  | "baseStructEntryToType (tName, vName, Some v) = (vName, Some (getBaseType v))"
  | "getBaseType (BUINT n) = UINTty"
  | "getBaseType (BSINT n) = SINTty"
  | "getBaseType (BIINT n) = IINTty"
  | "getBaseType (BVINT n) = VINTty"
  | "getBaseType (BBOOL b) = BOOLty"
  | "getBaseType (BSTRING s) = STRINGty"
  | "getBaseType (BERROR e) = ERRORty"
  | "getBaseType (BMATCH m) = MATCHty"
  | "getBaseType (DSTRUCT entries) = STRUCTty (map baseStructEntryToType entries)"

lemma equals: "getBaseType base = getValType (baseToVal base)"
proof (induction base)
  case (DSTRUCT x)
  note ih = this(1)
  then show ?case
    apply (simp)
    by (smt DSTRUCT baseStructEntryToType.elims option.set_intros prod.sel(2) snds.intros structEntryToType.simps(1) structEntryToType.simps(2) structEntryToVal.simps(1) structEntryToVal.simps(2))
qed simp+

fun getMemTy :: "val \<Rightarrow> vname \<Rightarrow> ty option" where
    "getMemTy (STRUCT []) sName = None"
  | "getMemTy (STRUCT ((tName, vName, None) # rest)) sName = getMemTy (STRUCT rest) sName"
  | "getMemTy (STRUCT ((tName, vName, Some v) # rest)) sName = (if vName = sName then Some (getValType v) else getMemTy (STRUCT rest) sName)"
  | "getMemTy _ sName = None"

lemma get_mem_ty_determ: "getMemTy v vName = t \<Longrightarrow> getMemTy v vName = t' \<Longrightarrow> t' = t"
  by simp

fun getTyMemTy :: "ty \<Rightarrow> vname \<Rightarrow> ty option" where
    "getTyMemTy (STRUCTty []) vName = None"
  | "getTyMemTy (STRUCTty ((eName, None) # xs)) vName = getTyMemTy (STRUCTty xs) vName"
  | "getTyMemTy (STRUCTty ((eName, Some eTy) # xs)) vName = (if eName = vName then Some eTy else getTyMemTy (STRUCTty xs) vName)"
  | "getTyMemTy _ vName = None"

lemma get_ty_mem_ty_determ: "getTyMemTy vT vName = t \<Longrightarrow> getTyMemTy vT vName = t' \<Longrightarrow> t' = t"
  by simp

lemma tyMem_none_if_mem: "getStructMem v vName = None \<longrightarrow> getMemTy v vName = None"
proof (induction v arbitrary: vName)
  case (STRUCT x)
  then show ?case
  proof (induction x)
    case (Cons a x)
    then show ?case
      by (smt Pair_inject getMemTy.elims getMemTy.simps(10) getMemTy.simps(11) getMemTy.simps(4) getMemTy.simps(5) getMemTy.simps(6) getMemTy.simps(7) getMemTy.simps(9) getStructMem.elims list.distinct(1) list.inject list.set_intros(2) option.distinct(1) val.inject(9) val.simps(69))
  qed simp+
qed simp+

lemma mem_none_if_tyMem: "getMemTy v vName = None \<longrightarrow> getStructMem v vName = None"
proof (induction v arbitrary: vName)
  case (STRUCT x)
  then show ?case
  proof (induction x)
    case (Cons a x)
    then show ?case
      by (smt getMemTy.simps(2) getMemTy.simps(3) getStructMem.simps(2) getStructMem.simps(3) list.set_intros(2) option.distinct(1) structEntryToType.cases)
  qed simp+
qed simp+

lemma tyMem_if_mem: "(\<forall>e. \<exists>t. getStructMem v vName = Some e \<longrightarrow> getMemTy v vName = Some t)"
proof (induction v arbitrary: vName e t)
  case (STRUCT x)
  then show ?case
  proof (induction x)
    case (Cons a x)
    then show ?case
      by (metis mem_none_if_tyMem not_Some_eq)
  qed simp+
qed simp+

lemma mem_if_tyMem: "\<forall>t. \<exists>e. getMemTy v vName = Some t \<longrightarrow> getStructMem v vName = Some e"
proof (induction v arbitrary: vName e t)
  case (STRUCT x)
  then show ?case
  proof (induction x)
    case (Cons a x)
    then show ?case
      by (metis not_Some_eq tyMem_none_if_mem)
  qed simp+
qed simp+

lemma mem_some: "getMemTy v vName = Some t1 \<Longrightarrow> getTyMemTy (getValType v) vName = Some t2 \<Longrightarrow> t2 = t1"
proof (induction v arbitrary: t2)
  case (STRUCT x)
  then show ?case
  proof (induction x)
    case (Cons a x)
    then show ?case
      apply (auto)
      by (smt getMemTy.elims getTyMemTy.simps(2) getTyMemTy.simps(3) list.inject list.set_intros(2) local.Cons(2) option.inject option.set_intros prod_set_simps(2) singletonI structEntryToType.simps(1) structEntryToType.simps(2) val.inject(9))
  qed simp+
qed simp+

lemma none_mem: "getTyMemTy (getValType v) vName = None \<longrightarrow> getMemTy v vName = None"
proof (induction v)
  case (STRUCT x)
  then show ?case
    proof (induction x)
      case (Cons a l)
      then show ?case
        by (smt getMemTy.elims getTyMemTy.simps(2) getTyMemTy.simps(3) getValType.simps(9) list.inject list.set_intros(2) list.simps(9) structEntryToType.simps(1) structEntryToType.simps(2) val.inject(9))
    qed simp+
qed simp+

lemma mem_none: "getMemTy v vName = None \<longrightarrow> getTyMemTy (getValType v) vName = None"
proof (induction v arbitrary: vName)
  case (STRUCT x)
  then show ?case
    proof (induction x)
      case (Cons a x)
      then show ?case
        apply (simp)
        by (smt Cons.prems getMemTy.simps(2) getMemTy.simps(3) getStructMem.simps(3) getTyMemTy.simps(2) getTyMemTy.simps(3) list.inject list.set_intros(2) list.simps(9) map_eq_Cons_D mem_none_if_tyMem option.distinct(1) option.set_intros structEntryToType.cases structEntryToType.simps(1) structEntryToType.simps(2))
  qed simp+
qed simp+

lemma mem_equals: "getMemTy v vName = getTyMemTy (getValType v) vName"
  by (metis mem_none mem_some none_mem option.exhaust)

lemma tyMemTy_none_if_mem: "getStructMem v vName = None \<longrightarrow> getTyMemTy (getValType v) vName = None"
  by (simp add: mem_none tyMem_none_if_mem)
lemma mem_none_if_tyMemTy: "getTyMemTy (getValType v) vName = None \<longrightarrow> getStructMem v vName = None"
  by (simp add: mem_equals mem_none_if_tyMem)
lemma tyMemTy_if_mem: "(\<forall>e. \<exists>t. getStructMem v vName = Some e \<longrightarrow> getTyMemTy (getValType v) vName = Some t)"
  using mem_equals tyMem_if_mem by auto
lemma mem_if_tyMemTy: "\<forall>t. \<exists>e. getTyMemTy (getValType v) vName = Some t \<longrightarrow> getStructMem v vName = Some e"
  using mem_equals mem_if_tyMem by auto

(* ============================================================================================================== *)
(*                                          TYPING SYSTEM DEFINITION                                              *)
(* ============================================================================================================== *)

(* The typing environment for expressions. If a case is defined it implies the expression is well-typed
   given the context of the typing environment. *)
inductive exprTyping :: "typeEnv \<Rightarrow> expression \<Rightarrow> ty \<Rightarrow> bool" ("(1_/ \<turnstile>/ (_ ::/ _))" [50,0,50] 50) where
(* =============== Base types =============== *)
    BASE_ty: "\<Gamma> \<turnstile> (BASE b) :: getBaseType (b)"
(* =============== Miscellaneous expressions =============== *)
  | TERNEXPR_ty: "\<Gamma> \<turnstile> e1 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: \<tau> \<Longrightarrow> \<Gamma> \<turnstile> e3 :: \<tau> \<Longrightarrow> \<Gamma> \<turnstile> TernExpr e1 e2 e3 :: \<tau>"
  | EXPRMEM_ty:  "\<Gamma> \<turnstile> e1 :: (STRUCTty entries) \<Longrightarrow> getTyMemTy (STRUCTty entries) vName = (Some \<tau>) \<Longrightarrow> \<Gamma> \<turnstile> ExprMem e1 vName :: \<tau>"
(* =============== Variable mapping  =============== *)
  | VAR_ty: "\<Gamma> \<turnstile> NamedVar vName :: \<Gamma> vName"
(* =============== Operations that yield a single bit (SBIT)  =============== *)
          (* Empty for now *)
(* =============== Operations that yield a boolean (BOOL)  =============== *)
    (* Boolean operations *)
  | ULNEB_ty: "\<Gamma> \<turnstile> e1 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> UNA_LNE e1 :: BOOLty"
  | BEQUB_ty: "\<Gamma> \<turnstile> e1 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> BIN_EQU e1 e2 :: BOOLty"
(*  | BNEQB_ty: "\<Gamma> \<turnstile> e1 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> BIN_NEQ e1 e2 :: BOOLty" *)
  | BFANB_ty: "\<Gamma> \<turnstile> e1 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> BIN_FAN e1 e2 :: BOOLty"
  | BFORB_ty: "\<Gamma> \<turnstile> e1 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: BOOLty \<Longrightarrow> \<Gamma> \<turnstile> BIN_FOR e1 e2 :: BOOLty"
    (* Signed integer operations *)
  | BEQUS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_EQU e1 e2 :: BOOLty"
  | BNEQS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_NEQ e1 e2 :: BOOLty"
  | BLEQS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_LEQ e1 e2 :: BOOLty"
  | BGEQS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_GEQ e1 e2 :: BOOLty"
  | BLESS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_LES e1 e2 :: BOOLty"
  | BGRES_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_GRE e1 e2 :: BOOLty"
    (* Unsigned integer operations *)
  | BEQUU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_EQU e1 e2 :: BOOLty"
  | BNEQU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_NEQ e1 e2 :: BOOLty"
  | BLEQU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_LEQ e1 e2 :: BOOLty"
  | BGEQU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_GEQ e1 e2 :: BOOLty"
  | BLESU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_LES e1 e2 :: BOOLty"
  | BGREU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_GRE e1 e2 :: BOOLty"
    (* Infinite precision integer operations *)
  | BEQUI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_EQU e1 e2 :: BOOLty"
  | BNEQI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_NEQ e1 e2 :: BOOLty"
  | BLEQI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_LEQ e1 e2 :: BOOLty"
  | BGEQI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_GEQ e1 e2 :: BOOLty"
  | BLESI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_LES e1 e2 :: BOOLty"
  | BGREI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_GRE e1 e2 :: BOOLty"
    (* Variable size bitstring operations *)
  | BEQUV_ty: "\<Gamma> \<turnstile> e1 :: VINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: VINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_EQU e1 e2 :: BOOLty"
  | BNEQV_ty: "\<Gamma> \<turnstile> e1 :: VINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: VINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_NEQ e1 e2 :: BOOLty"
(* =============== Operations that yield an unsigned integer (UINT)  =============== *)
  | UNEGU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> UNA_NEG e1 :: UINTty"
  | UPOSU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> UNA_POS e1 :: UINTty"
  | UCOMU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> UNA_COM e1 :: UINTty"
  | BADDU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_ADD e1 e2 :: UINTty"
  | BMINU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_MIN e1 e2 :: UINTty"
  | BANDU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_AND e1 e2 :: UINTty"
  | BXORU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_XOR e1 e2 :: UINTty"
  | BLORU_ty: "\<Gamma> \<turnstile> e1 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: UINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_LOR e1 e2 :: UINTty"
(* =============== Operations that yield a signed integer (SINT)  =============== *)
  | UNEGS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> UNA_NEG e1 :: SINTty"
  | UPOSS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> UNA_POS e1 :: SINTty"
  | BADDS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_ADD e1 e2 :: SINTty"
  | BMINS_ty: "\<Gamma> \<turnstile> e1 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: SINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_MIN e1 e2 :: SINTty"
(* =============== Operations that yield an infinite-precision integer (IINT)  =============== *)
  | UNEGI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> UNA_NEG e1 :: IINTty"
  | UPOSI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> UNA_POS e1 :: IINTty"
  | BADDI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_ADD e1 e2 :: IINTty"
  | BMINI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_MIN e1 e2 :: IINTty"
  | BMULI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_MUL e1 e2 :: IINTty"
  | BDIVI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_DIV e1 e2 :: IINTty"
  | BMODI_ty: "\<Gamma> \<turnstile> e1 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> e2 :: IINTty \<Longrightarrow> \<Gamma> \<turnstile> BIN_MOD e1 e2 :: IINTty"
(* =============== Operations that yield a variable-width integer (VINT)  =============== *)
          (* Empty for now *)

declare exprTyping.intros [intro!]
inductive_cases [elim!]:
  "\<Gamma> \<turnstile> BASE b :: \<tau>" "\<Gamma> \<turnstile> UNA_LNE e1 :: \<tau>" "\<Gamma> \<turnstile> UNA_COM e1 :: \<tau>" "\<Gamma> \<turnstile> UNA_NEG e1 :: \<tau>" "\<Gamma> \<turnstile> UNA_POS e1 :: \<tau>"
  "\<Gamma> \<turnstile> BIN_DIV e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_MOD e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_ADD e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_MIN e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_AND e1 e2 :: \<tau>"
  "\<Gamma> \<turnstile> BIN_XOR e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_LOR e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_LEQ e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_GEQ e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_LES e1 e2 :: \<tau>"
  "\<Gamma> \<turnstile> BIN_GRE e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_NEQ e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_EQU e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_FAN e1 e2 :: \<tau>" "\<Gamma> \<turnstile> BIN_FOR e1 e2 :: \<tau>"
  "\<Gamma> \<turnstile> BIN_MUL e1 e2 :: \<tau>" "\<Gamma> \<turnstile> TernExpr e1 e2 e3 :: \<tau>" "\<Gamma> \<turnstile> NamedVar v :: \<tau>" "\<Gamma> \<turnstile> ExprMem e1 vName :: \<tau>"

lemma expr_typing_deterministic: "\<Gamma> \<turnstile> e :: t \<Longrightarrow> \<Gamma> \<turnstile> e :: t' \<Longrightarrow> t' = t"
proof (induction arbitrary: t' rule: exprTyping.induct)
  case (EXPRMEM_ty \<Gamma> e1 entries vName \<tau>)
  note th = this(4)
  then show ?case
    using EXPRMEM_ty.IH EXPRMEM_ty.hyps(2) by auto
qed blast+

(* ============================================================================================================== *)
(*                                                 STATE MAPPING                                                  *)
(* ============================================================================================================== *)

definition noll_state ("||") where
  "noll_state \<equiv> \<lambda>x. (UINTty)"
syntax
  "_SState" :: "updbinds \<Rightarrow> 'a" ("|_|")
translations
  "_SState ms" == "_Update || ms"
  "_SState (_updbinds b bs)" <= "_Update (_SState b) bs"

code_pred exprTyping .

(* ============================================================================================================== *)
(*                                                STATEMENT TYPING                                                *)
(* ============================================================================================================== *)

(* The typing environment for statements. If a case is defined it implies the statement is well-typed
   given the context of the typing environment. *)
inductive stmtTyping :: "typeEnv \<Rightarrow> statOrDecl \<Rightarrow> bool" (infix "\<Turnstile>" 50) where
    Empty_ty: "\<Gamma> \<Turnstile> EmptyStat"
  | Exit_ty: "\<Gamma> \<Turnstile> ExitStat"
  | Conditional_ty: "\<Gamma> \<turnstile> e :: (BOOLty) \<Longrightarrow> \<Gamma> \<Turnstile> stmt1 \<Longrightarrow> \<Gamma> \<Turnstile> stmt2 \<Longrightarrow> \<Gamma> \<Turnstile> (ConditionalStat e stmt1 stmt2)"
  | Block_Empty_ty: "\<Gamma> \<Turnstile> (BlockStat [])"
  | BlockFull_ty: "\<Gamma> \<Turnstile> stmt \<Longrightarrow> \<Gamma> \<Turnstile> (BlockStat rest) \<Longrightarrow> \<Gamma> \<Turnstile> (BlockStat (stmt # rest))"
  | Assign_ty: "\<Gamma> \<turnstile> e :: \<Gamma> (vName) \<Longrightarrow> \<Gamma> \<Turnstile> (AssignmentStat (NameLVal vName) e)"
  | VarDecl_ty: "\<Gamma> \<Turnstile> (VariableDecl (NameLVal vName) (None))"
(* Remove \<Gamma> (vName) in below with just \<tau> because they should allow to change the type *)
  | VarInit_ty: "\<Gamma> \<turnstile> e :: \<Gamma> (vName) \<Longrightarrow> \<Gamma> \<Turnstile> (VariableDecl (NameLVal vName) (Some e))"
  | ConstInit_ty: "\<Gamma> \<turnstile> e :: \<Gamma> (vName) \<Longrightarrow> \<Gamma> \<Turnstile> (ConstantDecl (NameLVal vName) (e))"

declare stmtTyping.intros [intro!]
inductive_cases [elim!]:
  "\<Gamma> \<Turnstile> ExitStat" "\<Gamma> \<Turnstile> ConditionalStat e stmt1 stmt2" "\<Gamma> \<Turnstile> BlockStat l" "\<Gamma> \<Turnstile> AssignmentStat n e" "\<Gamma> \<Turnstile> VariableDecl n e"
  "\<Gamma> \<Turnstile> ConstantDecl n e"

(* The typing environment for the state. It states that a state is correctly typed if and only if the type
   of all variables in the state correspond with the typing environment. *)
definition stateTyping :: "typeEnv \<Rightarrow> state \<Rightarrow> bool" (infix "\<TTurnstile>" 50)
  where "\<Gamma> \<TTurnstile> s \<longleftrightarrow> (\<forall>x. getValType (s x) = \<Gamma> x)"

code_pred stmtTyping .

(* ============================================================================================================== *)
(*                                            TYPING SYSTEM PROOF                                                 *)
(* ============================================================================================================== *)

(* Prove that if the type of a particular variable is a given type, there always exists a concrete value with the
   matching type to satisfy the constraint. *)
lemma type_eq_UINT[simp]:   "getValType v = UINTty     \<longleftrightarrow> (\<exists>i. v = UINT i)"
  by (cases v) simp_all
lemma type_eq_SINT[simp]:   "getValType v = SINTty     \<longleftrightarrow> (\<exists>i. v = SINT i)"
  by (cases v) simp_all
lemma type_eq_IINT[simp]:   "getValType v = IINTty     \<longleftrightarrow> (\<exists>i. v = IINT i)"
  by (cases v) simp_all
lemma type_eq_VINT[simp]:   "getValType v = VINTty     \<longleftrightarrow> (\<exists>i. v = VINT i)"
  by (cases v) simp_all
lemma type_eq_BOOL[simp]:   "getValType v = BOOLty     \<longleftrightarrow> (\<exists>i. v = BOOL i)"
  by (cases v) simp_all
lemma type_eq_STRING[simp]: "getValType v = STRINGty   \<longleftrightarrow> (\<exists>i. v = STRING i)"
  by (cases v) simp_all
lemma type_eq_ERROR[simp]:  "getValType v = ERRORty    \<longleftrightarrow> (\<exists>i. v = ERROR i)"
  by (cases v) simp_all
lemma type_eq_MATCH[simp]:  "getValType v = MATCHty    \<longleftrightarrow> (\<exists>i. v = MATCH i)"
  by (cases v) simp_all
lemma type_eq_STRUCT[simp]: "(\<exists>l. getValType v = STRUCTty l) \<longleftrightarrow> (\<exists>i. v = STRUCT i)"
  by (cases v) simp_all

lemma member_same_type: "getStructMem v vName = Some e \<Longrightarrow> getMemTy v vName = Some t \<Longrightarrow> (getValType e) = t"
proof (induction v arbitrary: e t)
  case (STRUCT x)
  then show ?case
  proof (induction x)
    case (Cons a x)
    then show ?case
      by (smt getMemTy.simps(2) getMemTy.simps(3) getStructMem.simps(2) getStructMem.simps(3) list.set_intros(2) option.inject structEntryToType.cases)
  qed simp+
qed simp+

lemma type_member_same_type: "getStructMem v vName = Some e \<Longrightarrow> getTyMemTy (getValType v) vName = Some t \<Longrightarrow> (getValType e) = t"
proof (induction v arbitrary: e t)
  case (STRUCT x)
  then show ?case
  proof (induction x)
    case (Cons a x)
    then show ?case
      using mem_equals member_same_type by auto
  qed simp+
qed simp+

lemma type_tyMem_if_mem: "getStructMem strct vName = Some e \<Longrightarrow> getMemTy strct vName = Some t \<Longrightarrow> (getValType e) = t"
  using member_same_type by auto

lemma type_tyMemTy_if_mem: "getStructMem v vName = Some e \<Longrightarrow> getTyMemTy (getValType v) vName = Some t \<Longrightarrow> getValType e = t"
  by (simp add: mem_equals type_tyMem_if_mem)

lemma eval_member_same_type: "eval expr s v \<Longrightarrow> eval (ExprMem expr vName) s e \<Longrightarrow> getMemTy v vName = Some t \<Longrightarrow> (getValType e) = t"
  using eval_deterministic member_same_type by fastforce

lemma eval_type_member_same_type: "eval expr s v \<Longrightarrow> eval (ExprMem expr vName) s e \<Longrightarrow> getTyMemTy (getValType v) vName = Some t \<Longrightarrow> (getValType e) = t"
  by (simp add: eval_member_same_type mem_equals)

(* Theorem to state that if expression are well-typed, the result is necessarily also well-typed. *)
theorem expr_preservation: "\<Gamma> \<turnstile> expr :: \<tau> \<Longrightarrow> eval expr s v \<Longrightarrow> \<Gamma> \<TTurnstile> s \<Longrightarrow> getValType v = \<tau>"
proof (induction arbitrary: v rule: exprTyping.induct)
  case (BASE_ty \<Gamma> b)
  then show ?case
    using equals by auto
next
  case (EXPRMEM_ty \<Gamma> e1 entries vName \<tau>)
  then show ?case
    apply (auto simp: stateTyping_def)
    using type_member_same_type by presburger
qed (fastforce simp: stateTyping_def)+

lemma expr_progress: "\<Gamma> \<turnstile> e :: \<tau> \<Longrightarrow> \<Gamma> \<TTurnstile> s \<Longrightarrow> \<exists>v. eval e s v"
proof (induction rule: exprTyping.induct)
  case (BASE_ty \<Gamma> b)
  then show ?case
    by blast
next
  case (TERNEXPR_ty \<Gamma> e1 e2 \<tau> e3)
  then show ?case
    by (metis TERNFALSE TERNTRUE expr_preservation type_eq_BOOL)
next
  case (EXPRMEM_ty \<Gamma> e1 entries vName \<tau>)
  then show ?case
    by (metis STRUCTMEM expr_preservation mem_equals mem_if_tyMem type_eq_STRUCT)
next
  case (VAR_ty \<Gamma> vName)
  then show ?case
    using NAMEDVAR by blast
next
  case (ULNEB_ty \<Gamma> e1)
  then show ?case
    by (metis ULNEB expr_preservation type_eq_BOOL)
next
  case (BEQUB_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BEQUB expr_preservation type_eq_BOOL)
next
  case (BFANB_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BFANB expr_preservation type_eq_BOOL)
next
  case (BFORB_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BFORB expr_preservation type_eq_BOOL)
next
  case (BEQUS_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BEQUS expr_preservation type_eq_SINT)
next
  case (BNEQS_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BNEQS expr_preservation type_eq_SINT)
next
  case (BLEQS_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BLEQS expr_preservation type_eq_SINT)
next
  case (BGEQS_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BGEQS expr_preservation type_eq_SINT)
next
  case (BLESS_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BLESS expr_preservation type_eq_SINT)
next
  case (BGRES_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BGRES expr_preservation type_eq_SINT)
next
  case (BEQUU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BEQUU expr_preservation type_eq_UINT)
next
  case (BNEQU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BNEQU expr_preservation type_eq_UINT)
next
  case (BLEQU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BLEQU expr_preservation type_eq_UINT)
next
  case (BGEQU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BGEQU expr_preservation type_eq_UINT)
next
  case (BLESU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BLESU expr_preservation type_eq_UINT)
next
  case (BGREU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BGREU expr_preservation type_eq_UINT)
next
  case (BEQUI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BEQUI expr_preservation type_eq_IINT)
next
  case (BNEQI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BNEQI expr_preservation type_eq_IINT)
next
  case (BLEQI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BLEQI expr_preservation type_eq_IINT)
next
  case (BGEQI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BGEQI expr_preservation type_eq_IINT)
next
  case (BLESI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BLESI expr_preservation type_eq_IINT)
next
  case (BGREI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BGREI expr_preservation type_eq_IINT)
next
  case (BEQUV_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BEQUV expr_preservation type_eq_VINT)
next
  case (BNEQV_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BNEQV expr_preservation type_eq_VINT)
next
  case (UNEGS_ty \<Gamma> e1)
  then show ?case
    by (metis UNEGS expr_preservation type_eq_SINT)
next
  case (UPOSS_ty \<Gamma> e1)
  then show ?case
    by (metis UPOSS expr_preservation type_eq_SINT)
next
  case (BADDS_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BADDS expr_preservation type_eq_SINT)
next
  case (BMINS_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BMINS expr_preservation type_eq_SINT)
next
  case (UNEGU_ty \<Gamma> e1)
  then show ?case
    by (metis UNEGU expr_preservation type_eq_UINT)
next
  case (UPOSU_ty \<Gamma> e1)
  then show ?case
    by (metis UPOSU expr_preservation type_eq_UINT)
next
  case (UCOMU_ty \<Gamma> e1)
  then show ?case
    by (metis UCOMU expr_preservation type_eq_UINT)
next
  case (BADDU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BADDU expr_preservation type_eq_UINT)
next
  case (BMINU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BMINU expr_preservation type_eq_UINT)
next
  case (BANDU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BANDU expr_preservation type_eq_UINT)
next
  case (BXORU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BXORU expr_preservation type_eq_UINT)
next
  case (BLORU_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BLORU expr_preservation type_eq_UINT)
next
  case (UNEGI_ty \<Gamma> e1)
  then show ?case
    by (metis UNEGI expr_preservation type_eq_IINT)
next
  case (UPOSI_ty \<Gamma> e1)
  then show ?case
    by (metis UPOSI expr_preservation type_eq_IINT)
next
  case (BADDI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BADDI expr_preservation type_eq_IINT)
next
  case (BMINI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BMINI expr_preservation type_eq_IINT)
next
  case (BMULI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BMULI expr_preservation type_eq_IINT)
next
  case (BDIVI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BDIVI expr_preservation type_eq_IINT)
next
  case (BMODI_ty \<Gamma> e1 e2)
  then show ?case
    by (metis BMODI expr_preservation type_eq_IINT)
qed

theorem progress: "\<Gamma> \<Turnstile> c \<Longrightarrow> \<Gamma> \<TTurnstile> s \<Longrightarrow> c \<noteq> EmptyStat \<Longrightarrow> \<exists>cs'. (c, s, n) \<leadsto> cs'"
proof (induction rule: stmtTyping.induct)
  case (Conditional_ty \<Gamma> e stmnt1 stmnt2)
  then show ?case
    by (smt CondFalse CondTrue expr_preservation expr_progress type_eq_BOOL)
next
  case (BlockFull_ty \<Gamma> firstStat remainder)
  then show ?case
    by (metis (full_types) EmptyFirst FullBlock old.prod.exhaust step_equal_or_smaller)
next
  case (Block_Empty_ty \<Gamma>)
  then show ?case
    using expr_progress by blast
next
  case (Assign_ty \<Gamma> e vName)
  then show ?case
    using expr_progress by blast
next
  case (VarInit_ty \<Gamma> e vName)
  then show ?case
    using expr_progress by blast
next
  case (ConstInit_ty \<Gamma> e vName)
  then show ?case
    using expr_progress by blast
qed blast+

theorem state_preservation: "(c, s, n) \<leadsto> (c', s', n') \<Longrightarrow> \<Gamma> \<Turnstile> c \<Longrightarrow> \<Gamma> \<TTurnstile> s \<Longrightarrow> \<Gamma> \<TTurnstile> s'"
proof (induct rule: small_step_induct)
  case (Assign e s v vName n)
  then show ?case
    using expr_preservation stateTyping_def by fastforce
next
  case (VarDecl vName s n)
  then show ?case
    using expr_preservation stateTyping_def by fastforce
next
  case (VarInit e s v vName n)
  then show ?case
    using expr_preservation stateTyping_def by fastforce
next
  case (ConstInit e s v vName n)
  then show ?case
    using expr_preservation stateTyping_def by fastforce
qed blast+

theorem stmt_preservation: "(c, s, n) \<leadsto> (c', s', n') \<Longrightarrow> \<Gamma> \<Turnstile> c \<Longrightarrow> \<Gamma> \<Turnstile> c'"
proof (induction rule: small_step_induct)
  case (FullBlock stmt s n stmt' s' n' rest)
  then show ?case
  proof -
    have "\<Gamma> \<Turnstile> stmt"
      using FullBlock.prems by blast
    then have "\<Gamma> \<Turnstile> stmt'"
      by (simp add: FullBlock.IH \<open>\<Gamma> \<Turnstile> stmt\<close>)
    then have "\<Gamma> \<Turnstile> (BlockStat (stmt # rest))"
      by (simp add: FullBlock.prems)
    then have "\<Gamma> \<Turnstile> (BlockStat (stmt' # rest))"
      using \<open>\<Gamma> \<Turnstile> stmt'\<close> by blast
    thus ?case by auto
  qed
qed auto

theorem type_sound: "(c, s, n) \<leadsto>* (c', s', n') \<Longrightarrow> \<Gamma> \<Turnstile> c \<Longrightarrow> \<Gamma> \<TTurnstile> s \<Longrightarrow> c' \<noteq> EmptyStat \<Longrightarrow> \<exists>cs''. (c', s', n') \<leadsto> cs''"
proof (induction rule: star_induct)
  case (refl a a b)
  then show ?case
    using progress by auto
next
  case (step a a b a a b a a b)
  then show ?case
    using state_preservation stmt_preservation by auto
qed

(* ============================================================================================================== *)
(*                                           FINAL STATE PROPERTIES                                               *)
(* ============================================================================================================== *)

definition "final cs \<longleftrightarrow> (\<nexists>cs'. cs \<leadsto> cs')"

lemma EmptyFinal: "c = EmptyStat \<Longrightarrow> final (c, s, n)"
  using final_def by blast

lemma FinalEmpty: "final (c, s, n) \<Longrightarrow> \<Gamma> \<Turnstile> c \<Longrightarrow> \<Gamma> \<TTurnstile> s \<Longrightarrow> c = EmptyStat"
  using final_def progress by blast

(* P4:
  ttl = struct.ttl
  ttl = ttl - 1
  if (ttl = 0) {
    OUT_PORT = DROP_PORT
  }
*)

value "small_step (BlockStat [AssignmentStat (NameLVal ''ttl'') (ExprMem (BASE (DSTRUCT [(''ttl_field'', ''ttl'', Some (BUINT 32))])) ''ttl''), AssignmentStat (NameLVal ''ttl'') (BIN_MIN (NamedVar ''ttl'') (BASE (BUINT 1))), ConditionalStat (BIN_EQU (NamedVar ''ttl'') (BASE (BUINT 0))) (AssignmentStat (NameLVal ''OUT_PORT'') (NamedVar (''DROP_PORT''))) EmptyStat], <''OUT_PORT'' := (UINT 0), ''DROP_PORT'' := (UINT 64)>, 1000)"

(* ============================================================================================================== *)
(*                                          REACHABILITY PROPERTIES                                               *)
(* ============================================================================================================== *)

definition reachable :: "statOrDecl \<Rightarrow> statOrDecl set" where
  "reachable c = {c'. \<exists>s s' n n'. (c, s, n) \<leadsto>* (c', s', n')}"

fun small_steps_n :: "(statOrDecl * state * nat) \<Rightarrow> nat \<Rightarrow> (statOrDecl * state * nat) \<Rightarrow> bool" ("_ \<leadsto>'(_') _" [55,0,55] 55)
  where
    "(cs \<leadsto>(0) cs') = (cs' = cs)"
  | "(cs \<leadsto>(Suc n) cs'') = (\<exists>cs'. cs \<leadsto> cs' \<and> cs' \<leadsto>(n) cs'')"

lemma steps_n_if_star: "cs \<leadsto>* cs' \<Longrightarrow> \<exists>n. cs \<leadsto>(n) cs'"
proof (induction rule: star.induct)
  case (refl x)
  then show ?case
    using small_steps_n.simps(1) by blast
next
  case (step x y z)
  then show ?case
    using small_steps_n.simps(2) by blast
qed

lemma star_if_steps_n: "cs \<leadsto>(n) cs' \<Longrightarrow> cs \<leadsto>* cs'"
  apply (induction n arbitrary: cs)
  apply (simp)
  apply (meson small_steps_n.simps(2) star.simps)
  done

lemma steps_n_decreases: "(c, s, n) \<leadsto>(x) (c', s', n') \<Longrightarrow> n' \<le> n"
  using star_equal_or_smaller star_if_steps_n by blast

end

author: Johanmyst


text:
section \<open>CCW Vector Space\<close>
theory Counterclockwise_Vector
imports Counterclockwise
begin

locale ccw_vector_space = ccw_system12 ccw S for ccw::"'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" and S +
  assumes translate_plus[simp]: "ccw (a + x) (b + x) (c + x) \<longleftrightarrow> ccw a b c"
  assumes scaleR1_eq[simp]: "0 < e \<Longrightarrow> ccw 0 (e*\<^sub>Ra) b = ccw 0 a b"
  assumes uminus1[simp]: "ccw 0 (-a) b = ccw 0 b a"
  assumes add1: "ccw 0 a b \<Longrightarrow> ccw 0 c b \<Longrightarrow> ccw 0 (a + c) b"
begin

lemma translate_plus'[simp]:
  "ccw (x + a) (x + b) (x + c) \<longleftrightarrow> ccw a b c"
  by (auto simp: ac_simps)

lemma uminus2[simp]: "ccw 0 a (- b) = ccw 0 b a"
  by (metis minus_minus uminus1)

lemma uminus_all[simp]: "ccw (-a) (-b) (-c) \<longleftrightarrow> ccw a b c"
proof -
  have "ccw (-a) (-b) (-c) \<longleftrightarrow> ccw 0 (- (b - a)) (- (c - a))"
    using translate_plus[of "-a" a "-b" "-c"]
    by simp
  also have "\<dots> \<longleftrightarrow> ccw 0 (b - a) (c - a)"
    by (simp del: minus_diff_eq)
  also have "\<dots> \<longleftrightarrow> ccw a b c"
    using translate_plus[of a "-a" b c]
    by simp
  finally show ?thesis .
qed

lemma translate_origin: "NO_MATCH 0 p \<Longrightarrow> ccw p q r \<longleftrightarrow> ccw 0 (q - p) (r - p)"
  using translate_plus[of p "- p" q r]
  by simp

lemma translate[simp]: "ccw a (a + b) (a + c) \<longleftrightarrow> ccw 0 b c"
  by (simp add: translate_origin)

lemma translate_plus3: "ccw (a - x) (b - x) c \<longleftrightarrow> ccw a b (c + x)"
  using translate_plus[of a "-x" b "c + x"] by simp

lemma renormalize:
  "ccw 0 (a - b) (c - a) \<Longrightarrow> ccw b a c"
  by (metis diff_add_cancel diff_self cyclic minus_diff_eq translate_plus3 uminus1)

lemma cyclicI: "ccw p q r \<Longrightarrow> ccw q r p"
  by (metis cyclic)

lemma
  scaleR2_eq[simp]:
  "0 < e \<Longrightarrow> ccw 0 xr (e *\<^sub>R P) \<longleftrightarrow> ccw 0 xr P"
  using scaleR1_eq[of e "-P" xr]
  by simp

lemma scaleR1_nonzero_eq:
  "e \<noteq> 0 \<Longrightarrow> ccw 0 (e *\<^sub>R a) b = (if e > 0 then ccw 0 a b else ccw 0 b a)"
proof cases
  assume "e < 0"
  define e' where "e' = - e"
  hence "e = -e'" "e' > 0" using \<open>e < 0\<close> by simp_all
  thus ?thesis by simp
qed simp

lemma neg_scaleR[simp]: "x < 0 \<Longrightarrow> ccw 0 (x *\<^sub>R b) c \<longleftrightarrow> ccw 0 c b"
  using scaleR1_nonzero_eq by auto

lemma
  scaleR1:
  "0 < e \<Longrightarrow> ccw 0 xr P \<Longrightarrow> ccw 0 (e *\<^sub>R xr) P"
  by simp

lemma
  add3: "ccw 0 a b \<and> ccw 0 a c \<Longrightarrow> ccw 0 a (b + c)"
  using add1[of "-b" a "-c"] uminus1[of "b + c" a]
  by simp

lemma add3_self[simp]: "ccw 0 p (p + q) \<longleftrightarrow> ccw 0 p q"
  using translate[of "-p" p "p + q"]
  apply (simp add: cyclic)
  apply (metis cyclic uminus2)
  done

lemma add2_self[simp]: "ccw 0 (p + q) p \<longleftrightarrow> ccw 0 q p"
  using translate[of "-p" "p + q" p]
  apply simp
  apply (metis cyclic uminus1)
  done

lemma scale_add3[simp]: "ccw 0 a (x *\<^sub>R a + b) \<longleftrightarrow> ccw 0 a b"
proof -
  {
    assume "x = 0"
    hence ?thesis by simp
  } moreover {
    assume "x > 0"
    hence ?thesis using add3_self scaleR1_eq by blast
  } moreover {
    assume "x < 0"
    define x' where "x' = - x"
    hence "x = -x'" "x' > 0" using \<open>x < 0\<close> by simp_all
    hence "ccw 0 a (x *\<^sub>R a + b) = ccw 0 (x' *\<^sub>R a + - b) (x' *\<^sub>R a)"
      by (subst uminus1[symmetric]) simp
    also have "\<dots> = ccw 0 (- b) a"
      unfolding add2_self by (simp add: \<open>x' > 0\<close>)
    also have "\<dots> = ccw 0 a b"
      by simp
    finally have ?thesis .
  } ultimately show ?thesis by arith
qed

lemma scale_add3'[simp]: "ccw 0 a (b + x *\<^sub>R a) \<longleftrightarrow> ccw 0 a b"
  and scale_minus3[simp]: "ccw 0 a (x *\<^sub>R a - b) \<longleftrightarrow> ccw 0 b a"
  and scale_minus3'[simp]: "ccw 0 a (b - x *\<^sub>R a) \<longleftrightarrow> ccw 0 a b"
  using
    scale_add3[of a x b]
    scale_add3[of a "-x" b]
    scale_add3[of a x "-b"]
  by (simp_all add: ac_simps)

lemma sum:
  assumes fin: "finite X"
  assumes ne: "X\<noteq>{}"
  assumes ncoll: "(\<And>x. x \<in> X \<Longrightarrow> ccw 0 a (f x))"
  shows "ccw 0 a (sum f X)"
proof -
  from ne obtain x where "x \<in> X" "insert x X = X" by auto
  have "ccw 0 a (sum f (insert x X))"
    using fin ncoll
  proof (induction X)
    case empty thus ?case using \<open>x \<in> X\<close> ncoll
      by auto
  next
    case (insert y F)
    hence "ccw 0 a (sum f (insert y (insert x F)))"
      by (cases "y = x") (auto intro!: add3)
    thus ?case
      by (simp add: insert_commute)
  qed
  thus ?thesis using \<open>insert x X = X\<close> by simp
qed

lemma sum2:
  assumes fin: "finite X"
  assumes ne: "X\<noteq>{}"
  assumes ncoll: "(\<And>x. x \<in> X \<Longrightarrow> ccw 0 (f x) a)"
  shows "ccw 0 (sum f X) a"
  using sum[OF assms(1,2), of "-a" f] ncoll
  by simp

lemma translate_minus[simp]:
  "ccw (x - a) (x - b) (x - c) = ccw (-a) (-b) (-c)"
  using translate_plus[of "-a" x "-b" "-c"]
  by simp

end

locale ccw_convex = ccw_system ccw S for ccw and S::"'a::real_vector set" +
  fixes oriented
  assumes convex2:
    "u \<ge> 0 \<Longrightarrow> v \<ge> 0 \<Longrightarrow> u + v = 1 \<Longrightarrow> ccw a b c \<Longrightarrow> ccw a b d \<Longrightarrow> oriented a b \<Longrightarrow>
      ccw a b (u *\<^sub>R c + v *\<^sub>R d)"
begin

lemma convex_hull:
  assumes [intro, simp]: "finite C"
  assumes ccw: "\<And>c. c \<in> C \<Longrightarrow> ccw a b c"
  assumes ch: "x \<in> convex hull C"
  assumes oriented: "oriented a b"
  shows "ccw a b x"
proof -
  define D where "D = C"
  have D: "C \<subseteq> D" "\<And>c. c \<in> D \<Longrightarrow> ccw a b c" by (simp_all add: D_def ccw)
  show "ccw a b x"
    using \<open>finite C\<close> D ch
  proof (induct arbitrary: x)
    case empty thus ?case by simp
  next
    case (insert c C)
    hence "C \<subseteq> D" by simp
    {
      assume "C = {}"
      hence ?case
        using insert
        by simp
    } moreover {
      assume "C \<noteq> {}"
      from convex_hull_insert[OF this, of c] insert(6)
      obtain u v d where "u \<ge> 0" "v \<ge> 0" "d \<in> convex hull C" "u + v = 1"
        and x: "x = u *\<^sub>R c + v *\<^sub>R d"
        by blast
      have "ccw a b d"
        by (auto intro: insert.hyps(3)[OF \<open>C \<subseteq> D\<close>] insert.prems \<open>d \<in> convex hull C\<close>)
      from insert
      have "ccw a b c"
        by simp
      from convex2[OF \<open>0 \<le> u\<close> \<open>0 \<le> v\<close> \<open>u + v = 1\<close> \<open>ccw a b c\<close> \<open>ccw a b d\<close> \<open>oriented a b\<close>]
      have ?case by (simp add: x)
    } ultimately show ?case by blast
  qed
qed

end

end

repo: PSL


text:
(*  File:       Sequential_Composition.thy
    Copyright   2021  Karlsruhe Institute of Technology (KIT)
*)
\<^marker>\<open>creator "Karsten Diekhoff, Karlsruhe Institute of Technology (KIT)"\<close>
\<^marker>\<open>contributor "Jonas Kraemer, Karlsruhe Institute of Technology (KIT)"\<close>
\<^marker>\<open>contributor "Michael Kirsten, Karlsruhe Institute of Technology (KIT)"\<close>

section \<open>Sequential Composition\<close>

theory Sequential_Composition
  imports "Basic_Modules/Component_Types/Electoral_Module"
begin

text \<open>
  The sequential composition creates a new electoral module from
  two electoral modules. In a sequential composition, the second
  electoral module makes decisions over alternatives deferred by
  the first electoral module.
\<close>

subsection \<open>Definition\<close>

fun sequential_composition :: "'a Electoral_Module \<Rightarrow> 'a Electoral_Module \<Rightarrow>
        'a Electoral_Module" where
  "sequential_composition m n A p =
    (let new_A = defer m A p;
        new_p = limit_profile new_A p in (
                  (elect m A p) \<union> (elect n new_A new_p),
                  (reject m A p) \<union> (reject n new_A new_p),
                  defer n new_A new_p))"

abbreviation sequence ::
  "'a Electoral_Module \<Rightarrow> 'a Electoral_Module \<Rightarrow> 'a Electoral_Module"
     (infix "\<triangleright>" 50) where
  "m \<triangleright> n == sequential_composition m n"

lemma seq_comp_presv_disj:
  assumes module_m: "electoral_module m" and
          module_n: "electoral_module n" and
          f_prof:  "finite_profile A p"
  shows "disjoint3 ((m \<triangleright> n) A p)"
proof -
  let ?new_A = "defer m A p"
  let ?new_p = "limit_profile ?new_A p"
  have fin_def: "finite (defer m A p)"
    using def_presv_fin_prof f_prof module_m
    by metis
  have prof_def_lim:
    "profile (defer m A p) (limit_profile (defer m A p) p)"
    using def_presv_fin_prof f_prof module_m
    by metis
  have defer_in_A:
    "\<forall> prof f a A.
      (profile A prof \<and> finite A \<and> electoral_module f \<and>
        (a::'a) \<in> defer f A prof) \<longrightarrow>
          a \<in> A"
    using UnCI result_presv_alts
    by (metis (mono_tags))
  from module_m f_prof
  have disjoint_m: "disjoint3 (m A p)"
    unfolding electoral_module_def well_formed.simps
    by blast
  from module_m module_n def_presv_fin_prof f_prof
  have disjoint_n:
    "(disjoint3 (n ?new_A ?new_p))"
    unfolding electoral_module_def well_formed.simps
    by metis
  have disj_n:
    "elect m A p \<inter> reject m A p = {} \<and>
      elect m A p \<inter> defer m A p = {} \<and>
      reject m A p \<inter> defer m A p = {}"
    using f_prof module_m
    by (simp add: result_disj)
  from f_prof module_m module_n
  have rej_n_in_def_m:
    "reject n (defer m A p)
      (limit_profile (defer m A p) p) \<subseteq> defer m A p"
    using def_presv_fin_prof reject_in_alts
    by metis
  with disjoint_m module_m module_n f_prof
  have 0:
    "(elect m A p \<inter> reject n ?new_A ?new_p) = {}"
    using disj_n
    by (simp add: disjoint_iff_not_equal subset_eq)
  from f_prof module_m module_n
  have elec_n_in_def_m:
    "elect n (defer m A p)
      (limit_profile (defer m A p) p) \<subseteq> defer m A p"
    using def_presv_fin_prof elect_in_alts
    by metis
  from disjoint_m disjoint_n def_presv_fin_prof f_prof
       module_m module_n
  have 1:
    "(elect m A p \<inter> defer n ?new_A ?new_p) = {}"
  proof -
    obtain sf :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where
      "\<forall> a b.
        (\<exists> c. c \<in> b \<and> (\<exists> d. d \<in> a \<and> c = d)) =
          (sf a b \<in> b \<and>
            (\<exists> e. e \<in> a \<and> sf a b = e))"
      by moura
    then obtain sf2 :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a" where
      "\<forall> A B.
        (A \<inter> B \<noteq> {} \<or> (\<forall>a. a \<notin> A \<or> (\<forall>b. b \<notin> B \<or> a \<noteq> b))) \<and>
          (A \<inter> B = {} \<or> sf B A \<in> A \<and> sf2 B A \<in> B \<and>
            sf B A = sf2 B A)"
      by auto
    thus ?thesis
      using defer_in_A disj_n fin_def module_n prof_def_lim
      by (metis (no_types))
  qed
  from disjoint_m disjoint_n def_presv_fin_prof f_prof
       module_m module_n
  have 2:
    "(reject m A p \<inter> reject n ?new_A ?new_p) = {}"
    using disjoint_iff_not_equal reject_in_alts
          set_rev_mp result_disj Int_Un_distrib2
          Un_Diff_Int boolean_algebra_cancel.inf2
          inf.order_iff inf_sup_aci(1) subsetD
          rej_n_in_def_m disj_n
    by auto
  have "\<forall> A A'. \<not> (A::'a set) \<subseteq> A' \<or> A = A \<inter> A'"
    by blast
  with disjoint_m disjoint_n def_presv_fin_prof f_prof
       module_m module_n elec_n_in_def_m
  have 3:
    "(reject m A p \<inter> elect n ?new_A ?new_p) = {}"
    using disj_n
    by blast
  have
    "(elect m A p \<union> elect n ?new_A ?new_p) \<inter>
          (reject m A p \<union> reject n ?new_A ?new_p) = {}"
  proof (safe)
    fix x :: "'a"
    assume
      elec_x: "x \<in> elect m A p" and
      rej_x: "x \<in> reject m A p"
    from elec_x rej_x
    have "x \<in> elect m A p \<inter> reject m A p"
      by simp
    thus "x \<in> {}"
      using disj_n
      by simp
  next
    fix x :: "'a"
    assume
      elec_x: "x \<in> elect m A p" and
      rej_lim_x:
      "x \<in> reject n (defer m A p)
        (limit_profile (defer m A p) p)"
    from elec_x rej_lim_x
    show "x \<in> {}"
      using 0
      by blast
  next
    fix x :: "'a"
    assume
      elec_lim_x:
      "x \<in> elect n (defer m A p) (limit_profile (defer m A p) p)" and
      rej_x: "x \<in> reject m A p"
    from elec_lim_x rej_x
    show "x \<in> {}"
      using 3
      by blast
  next
    fix x :: "'a"
    assume
      elec_lim_x:
      "x \<in> elect n (defer m A p) (limit_profile (defer m A p) p)" and
      rej_lim_x:
      "x \<in> reject n (defer m A p) (limit_profile (defer m A p) p)"
    from elec_lim_x rej_lim_x
    show "x \<in> {}"
      using disjoint_iff_not_equal elec_lim_x fin_def
            module_n prof_def_lim rej_lim_x result_disj
      by metis
  qed
  moreover from 0 1 2 3 disjoint_n module_m module_n f_prof
  have
    "(elect m A p \<union> elect n ?new_A ?new_p) \<inter>
          (defer n ?new_A ?new_p) = {}"
    using Int_Un_distrib2 Un_empty def_presv_fin_prof result_disj
    by metis
  moreover from 0 1 2 3 f_prof disjoint_m disjoint_n module_m module_n
  have
    "(reject m A p \<union> reject n ?new_A ?new_p) \<inter>
          (defer n ?new_A ?new_p) = {}"
  proof (safe)
    fix x :: "'a"
    assume
      elec_rej_disj:
      "elect m A p \<inter>
        reject n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      elec_def_disj:
      "elect m A p \<inter>
        defer n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      rej_rej_disj:
      "reject m A p \<inter>
        reject n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      rej_elec_disj:
      "reject m A p \<inter>
        elect n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      disj_p: "disjoint3 (m A p)" and
      disj_limit:
      "disjoint3 (n (defer m A p) (limit_profile (defer m A p) p))" and
      mod_m: "electoral_module m" and
      mod_n: "electoral_module n" and
      fin_A: "finite A" and
      prof_A: "profile A p" and
      x_in_def:
      "x \<in> defer n (defer m A p) (limit_profile (defer m A p) p)" and
      x_in_rej: "x \<in> reject m A p"
    from x_in_def
    have "x \<in> defer m A p"
      using defer_in_A fin_def module_n prof_def_lim
      by blast
    with x_in_rej
    have "x \<in> reject m A p \<inter> defer m A p"
      by fastforce
    thus "x \<in> {}"
      using disj_n
      by blast
  next
    fix x :: "'a"
    assume
      elec_rej_disj:
      "elect m A p \<inter>
        reject n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      elec_def_disj:
      "elect m A p \<inter>
        defer n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      rej_rej_disj:
      "reject m A p \<inter>
        reject n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      rej_elec_disj:
      "reject m A p \<inter>
        elect n (defer m A p) (limit_profile (defer m A p) p) = {}" and
      disj_p: "disjoint3 (m A p)" and
      disj_limit:
      "disjoint3 (n (defer m A p) (limit_profile (defer m A p) p))" and
      mod_m: "electoral_module m" and
      mod_n: "electoral_module n" and
      fin_A: "finite A" and
      prof_A: "profile A p" and
      x_in_def:
      "x \<in> defer n (defer m A p) (limit_profile (defer m A p) p)" and
      x_in_rej:
      "x \<in> reject n (defer m A p) (limit_profile (defer m A p) p)"
    from x_in_def x_in_rej
    show "x \<in> {}"
      using fin_def module_n prof_def_lim reject_not_elec_or_def
      by fastforce
  qed
  ultimately have
    "disjoint3 (elect m A p \<union> elect n ?new_A ?new_p,
                reject m A p \<union> reject n ?new_A ?new_p,
                defer n ?new_A ?new_p)"
    by simp
  thus ?thesis
    unfolding sequential_composition.simps
    by metis
qed

lemma seq_comp_presv_alts:
  assumes module_m: "electoral_module m" and
          module_n: "electoral_module n" and
          f_prof:  "finite_profile A p"
  shows "set_equals_partition A ((m \<triangleright> n) A p)"
proof -
  let ?new_A = "defer m A p"
  let ?new_p = "limit_profile ?new_A p"
  from module_m f_prof
  have "set_equals_partition A (m A p)"
    unfolding electoral_module_def
    by simp
  with module_m f_prof
  have 0:
    "elect m A p \<union> reject m A p \<union> ?new_A = A"
    by (simp add: result_presv_alts)
  from module_n def_presv_fin_prof f_prof module_m
  have
    "set_equals_partition ?new_A (n ?new_A ?new_p)"
    unfolding electoral_module_def well_formed.simps
    by metis
  with module_m module_n f_prof
  have 1:
    "elect n ?new_A ?new_p \<union>
        reject n ?new_A ?new_p \<union>
        defer n ?new_A ?new_p = ?new_A"
    using def_presv_fin_prof result_presv_alts
    by metis
  from 0 1
  have
    "(elect m A p \<union> elect n ?new_A ?new_p) \<union>
        (reject m A p \<union> reject n ?new_A ?new_p) \<union>
         defer n ?new_A ?new_p = A"
    by blast
  hence
    "set_equals_partition A
      (elect m A p \<union> elect n ?new_A ?new_p,
      reject m A p \<union> reject n ?new_A ?new_p,
      defer n ?new_A ?new_p)"
    by simp
  thus ?thesis
    unfolding sequential_composition.simps
    by metis
qed

subsection \<open>Soundness\<close>

theorem seq_comp_sound[simp]:
  assumes
    module_m: "electoral_module m" and
    module_n: "electoral_module n"
  shows "electoral_module (m \<triangleright> n)"
proof (unfold electoral_module_def, safe)
  fix
    A :: "'a set" and
    p :: "'a Profile"
  assume
    fin_A: "finite A" and
    prof_A: "profile A p"
  have "\<forall> r. well_formed (A::'a set) r =
          (disjoint3 r \<and> set_equals_partition A r)"
    by simp
  thus "well_formed A ((m \<triangleright> n) A p)"
    using module_m module_n seq_comp_presv_disj
          seq_comp_presv_alts fin_A prof_A
    by metis
qed

subsection \<open>Lemmata\<close>

lemma seq_comp_dec_only_def:
  assumes
    module_m: "electoral_module m" and
    module_n: "electoral_module n" and
    f_prof: "finite_profile A p" and
    empty_defer: "defer m A p = {}"
  shows "(m \<triangleright> n) A p =  m A p"
proof
  have
    "\<forall> f A prof.
      (electoral_module f \<and> finite_profile A prof) \<longrightarrow>
        finite_profile (defer f A prof)
          (limit_profile (defer f A prof) prof)"
    using def_presv_fin_prof
    by metis
  hence prof_no_alt:
    "profile {} (limit_profile (defer m A p) p)"
    using empty_defer f_prof module_m
    by metis
  hence
    "(elect m A p) \<union>
      (elect n (defer m A p)
        (limit_profile (defer m A p) p))
    = elect m A p"
    using elect_in_alts empty_defer module_n
    by auto
  thus "elect (m \<triangleright> n) A p = elect m A p"
    using fst_conv
    unfolding sequential_composition.simps
    by metis
next
  have rej_empty:
    "\<forall> f prof.
      (electoral_module f \<and> profile ({}::'a set) prof) \<longrightarrow>
        reject f {} prof = {}"
    using bot.extremum_uniqueI infinite_imp_nonempty reject_in_alts
    by metis
  have prof_no_alt: "profile {} (limit_profile (defer m A p) p)"
    using empty_defer f_prof module_m limit_profile_sound
    by auto
  hence "(reject m A p, defer n {} (limit_profile {} p)) = snd (m A p)"
    using bot.extremum_uniqueI defer_in_alts empty_defer
          infinite_imp_nonempty module_n prod.collapse
    by (metis (no_types))
  thus "snd ((m \<triangleright> n) A p) = snd (m A p)"
    using rej_empty empty_defer module_n prof_no_alt
    by simp
qed

lemma seq_comp_def_then_elect:
  assumes
    n_electing_m: "non_electing m" and
    def_one_m: "defers 1 m" and
    electing_n: "electing n" and
    f_prof: "finite_profile A p"
  shows "elect (m \<triangleright> n) A p = defer m A p"
proof cases
  assume "A = {}"
  with electing_n n_electing_m f_prof
  show ?thesis
    using bot.extremum_uniqueI defer_in_alts elect_in_alts seq_comp_sound
    unfolding electing_def non_electing_def
    by metis
next
  assume assm: "A \<noteq> {}"
  from n_electing_m f_prof
  have ele: "elect m A p = {}"
    unfolding non_electing_def
    by simp
  from assm def_one_m f_prof finite
  have def_card:
    "card (defer m A p) = 1"
    unfolding defers_def
    by (simp add: Suc_leI card_gt_0_iff)
  with n_electing_m f_prof
  have def:
    "\<exists> a \<in> A. defer m A p = {a}"
    using card_1_singletonE defer_in_alts singletonI subsetCE
    unfolding non_electing_def
    by metis
  from ele def n_electing_m
  have rej:
    "\<exists> a \<in> A. reject m A p = A - {a}"
    using Diff_empty def_one_m f_prof reject_not_elec_or_def
    unfolding defers_def
    by metis
  from ele rej def n_electing_m f_prof
  have res_m:
    "\<exists> a \<in> A. m A p = ({}, A - {a}, {a})"
    using Diff_empty combine_ele_rej_def reject_not_elec_or_def
    unfolding non_electing_def
    by metis
  hence
    "\<exists> a \<in> A. elect (m \<triangleright> n) A p =
        elect n {a} (limit_profile {a} p)"
    using prod.sel(1) prod.sel(2) sup_bot.left_neutral
    unfolding sequential_composition.simps
    by metis
  with def_card def electing_n n_electing_m f_prof
  have
    "\<exists> a \<in> A. elect (m \<triangleright> n) A p = {a}"
    using electing_for_only_alt prod.sel(1) def_presv_fin_prof sup_bot.left_neutral
    unfolding non_electing_def sequential_composition.simps
    by metis
  with def def_card electing_n n_electing_m f_prof res_m
  show ?thesis
    using def_presv_fin_prof electing_for_only_alt fst_conv sup_bot.left_neutral
    unfolding non_electing_def sequential_composition.simps
    by metis
qed

lemma seq_comp_def_card_bounded:
  assumes
    module_m: "electoral_module m" and
    module_n: "electoral_module n" and
    f_prof: "finite_profile A p"
  shows "card (defer (m \<triangleright> n) A p) \<le> card (defer m A p)"
  using card_mono defer_in_alts module_m module_n f_prof def_presv_fin_prof snd_conv
  unfolding sequential_composition.simps
  by metis

lemma seq_comp_def_set_bounded:
  assumes
    module_m: "electoral_module m" and
    module_n: "electoral_module n" and
    f_prof: "finite_profile A p"
  shows "defer (m \<triangleright> n) A p \<subseteq> defer m A p"
  using defer_in_alts module_m module_n prod.sel(2) f_prof def_presv_fin_prof
  unfolding sequential_composition.simps
  by metis

lemma seq_comp_defers_def_set:
  assumes
    module_m: "electoral_module m" and
    module_n: "electoral_module n" and
    f_prof: "finite_profile A p"
  shows
    "defer (m \<triangleright> n) A p =
      defer n (defer m A p) (limit_profile (defer m A p) p)"
  using snd_conv
  unfolding sequential_composition.simps
  by metis

lemma seq_comp_def_then_elect_elec_set:
  assumes
    module_m: "electoral_module m" and
    module_n: "electoral_module n" and
    f_prof: "finite_profile A p"
  shows
    "elect (m \<triangleright> n) A p =
      elect n (defer m A p) (limit_profile (defer m A p) p) \<union>
      (elect m A p)"
  using Un_commute fst_conv
  unfolding sequential_composition.simps
  by metis

lemma seq_comp_elim_one_red_def_set:
  assumes
    module_m: "electoral_module m" and
    module_n: "eliminates 1 n" and
    f_prof: "finite_profile A p" and
    enough_leftover: "card (defer m A p) > 1"
  shows "defer (m \<triangleright> n) A p \<subset> defer m A p"
  using enough_leftover module_m module_n f_prof snd_conv
        def_presv_fin_prof single_elim_imp_red_def_set
  unfolding sequential_composition.simps
  by metis

lemma seq_comp_def_set_sound:
  assumes
    e_mod_m: "electoral_module m" and
    e_mod_n: "electoral_module n" and
    fin_prof_p: "finite_profile A p"
  shows "defer (m \<triangleright> n) A p \<subseteq> defer m A p"
proof (safe)
  fix x :: "'a"
  assume "x \<in> defer (m \<triangleright> n) A p"
  thus "x \<in> defer m A p"
    using e_mod_m e_mod_n fin_prof_p in_mono seq_comp_def_set_bounded
    by (metis (no_types, lifting))
qed

lemma seq_comp_def_set_trans:
  assumes
    "a \<in> (defer (m \<triangleright> n) A p)" and
    "electoral_module m \<and> electoral_module n" and
    "finite_profile A p"
  shows "a \<in> defer n (defer m A p) (limit_profile (defer m A p) p) \<and> a \<in> defer m A p"
  using seq_comp_def_set_bounded assms
        in_mono seq_comp_defers_def_set
  by (metis (no_types, opaque_lifting))

subsection \<open>Composition Rules\<close>

text \<open>
  The sequential composition preserves the non-blocking property.
\<close>

theorem seq_comp_presv_non_blocking[simp]:
  assumes
    non_blocking_m: "non_blocking m" and
    non_blocking_n: "non_blocking n"
  shows "non_blocking (m \<triangleright> n)"
proof -
  fix
    A :: "'a set" and
    p :: "'a Profile"
  let ?input_sound = "((A::'a set) \<noteq> {} \<and> finite_profile A p)"
  from non_blocking_m have
    "?input_sound \<longrightarrow> reject m A p \<noteq> A"
    unfolding non_blocking_def
    by simp
  with non_blocking_m have 0:
    "?input_sound \<longrightarrow> A - reject m A p \<noteq> {}"
    using Diff_eq_empty_iff reject_in_alts subset_antisym
    unfolding non_blocking_def
    by metis
  from non_blocking_m have
    "?input_sound \<longrightarrow> well_formed A (m A p)"
    unfolding electoral_module_def non_blocking_def
    by simp
  hence
    "?input_sound \<longrightarrow>
        elect m A p \<union> defer m A p = A - reject m A p"
    using non_blocking_m elec_and_def_not_rej
    unfolding non_blocking_def
    by metis
  with 0 have
    "?input_sound \<longrightarrow> elect m A p \<union> defer m A p \<noteq> {}"
    by simp
  hence "?input_sound \<longrightarrow> (elect m A p \<noteq> {} \<or> defer m A p \<noteq> {})"
    by simp
  with non_blocking_m non_blocking_n
  show ?thesis
  proof (unfold non_blocking_def)
    assume
      emod_reject_m:
      "electoral_module m \<and>
        (\<forall> A p. A \<noteq> {} \<and> finite_profile A p \<longrightarrow>
          reject m A p \<noteq> A)" and
      emod_reject_n:
      "electoral_module n \<and>
        (\<forall> A p. A \<noteq> {} \<and> finite_profile A p \<longrightarrow>
          reject n A p \<noteq> A)"
    show
      "electoral_module (m \<triangleright> n) \<and>
        (\<forall> A p.
          A \<noteq> {} \<and> finite_profile A p \<longrightarrow>
            reject (m \<triangleright> n) A p \<noteq> A)"
    proof (safe)
      show "electoral_module (m \<triangleright> n)"
        using emod_reject_m emod_reject_n
        by simp
    next
      fix
        A :: "'a set" and
        p :: "'a Profile" and
        x :: "'a"
      assume
        fin_A: "finite A" and
        prof_A: "profile A p" and
        rej_mn: "reject (m \<triangleright> n) A p = A" and
        x_in_A: "x \<in> A"
      from emod_reject_m fin_A prof_A
      have fin_defer:
        "finite_profile (defer m A p) (limit_profile (defer m A p) p)"
        using def_presv_fin_prof
        by (metis (no_types))
      from emod_reject_m emod_reject_n fin_A prof_A
      have seq_elect:
        "elect (m \<triangleright> n) A p =
          elect n (defer m A p) (limit_profile (defer m A p) p) \<union>
            elect m A p"
        using seq_comp_def_then_elect_elec_set
        by metis
      from emod_reject_n emod_reject_m fin_A prof_A
      have def_limit:
        "defer (m \<triangleright> n) A p =
          defer n (defer m A p) (limit_profile (defer m A p) p)"
        using seq_comp_defers_def_set
        by metis
      from emod_reject_n emod_reject_m fin_A prof_A
      have
        "elect (m \<triangleright> n) A p \<union> defer (m \<triangleright> n) A p = A - reject (m \<triangleright> n) A p"
        using elec_and_def_not_rej seq_comp_sound
        by metis
      hence elect_def_disj:
        "elect n (defer m A p) (limit_profile (defer m A p) p) \<union>
          elect m A p \<union>
          defer n (defer m A p) (limit_profile (defer m A p) p) = {}"
        using def_limit seq_elect Diff_cancel rej_mn
        by auto
      have rej_def_eq_set:
        "defer n (defer m A p) (limit_profile (defer m A p) p) -
          defer n (defer m A p) (limit_profile (defer m A p) p) = {} \<longrightarrow>
            reject n (defer m A p) (limit_profile (defer m A p) p) =
              defer m A p"
        using elect_def_disj emod_reject_n fin_defer
        by (simp add: reject_not_elec_or_def)
      have
        "defer n (defer m A p) (limit_profile (defer m A p) p) -
          defer n (defer m A p) (limit_profile (defer m A p) p) = {} \<longrightarrow>
            elect m A p = elect m A p \<inter> defer m A p"
        using elect_def_disj
        by blast
      thus "x \<in> {}"
        using rej_def_eq_set result_disj fin_defer Diff_cancel Diff_empty
              emod_reject_m emod_reject_n fin_A prof_A reject_not_elec_or_def x_in_A
        by metis
    qed
  qed
qed

text \<open>
  Sequential composition preserves the non-electing property.
\<close>

theorem seq_comp_presv_non_electing[simp]:
  assumes
    m_elect: "non_electing m" and
    n_elect: "non_electing n"
  shows "non_electing (m \<triangleright> n)"
proof (unfold non_electing_def, safe)
  from m_elect n_elect
  have "electoral_module m \<and> electoral_module n"
    unfolding non_electing_def
    by blast
  thus "electoral_module (m \<triangleright> n)"
    by simp
next
  fix
    A :: "'a set" and
    p :: "'a Profile" and
    x :: "'a"
  assume
    "finite A" and
    "profile A p" and
    "x \<in> elect (m \<triangleright> n) A p"
  with m_elect n_elect
  show "x \<in> {}"
    unfolding non_electing_def
    using seq_comp_def_then_elect_elec_set def_presv_fin_prof
          Diff_empty Diff_partition empty_subsetI
    by metis
qed

text \<open>
  Composing an electoral module that defers exactly 1 alternative
  in sequence after an electoral module that is electing
  results (still) in an electing electoral module.
\<close>

theorem seq_comp_electing[simp]:
  assumes
    def_one_m1:  "defers 1 m1" and
    electing_m2: "electing m2"
  shows "electing (m1 \<triangleright> m2)"
proof -
  have
    "\<forall> A p. (card A \<ge> 1 \<and> finite_profile A p) \<longrightarrow>
        card (defer m1 A p) = 1"
    using def_one_m1
    unfolding defers_def
    by blast
  hence def_m1_not_empty:
    "\<forall> A p. (A \<noteq> {} \<and> finite_profile A p) \<longrightarrow>
        defer m1 A p \<noteq> {}"
    using One_nat_def Suc_leI card_eq_0_iff
          card_gt_0_iff zero_neq_one
    by metis
  thus ?thesis
  proof -
    obtain
      f_set ::
      "('a set \<Rightarrow> 'a Profile \<Rightarrow> 'a Result) \<Rightarrow> 'a set" and
      f_prof ::
      "('a set \<Rightarrow> 'a Profile \<Rightarrow> 'a Result) \<Rightarrow> 'a Profile" where
      f_mod:
      "\<forall> f.
        (\<not> electing f \<or> electoral_module f \<and>
          (\<forall> A prof.
            (A \<noteq> {} \<and> finite A \<and> profile A prof) \<longrightarrow>
              elect f A prof \<noteq> {})) \<and>
        (electing f \<or> \<not> electoral_module f \<or> f_set f \<noteq> {} \<and> finite (f_set f) \<and>
          profile (f_set f) (f_prof f) \<and> elect f (f_set f) (f_prof f) = {})"
      unfolding electing_def
      by moura
    hence f_elect:
      "electoral_module m2 \<and>
        (\<forall> A prof. (A \<noteq> {} \<and> finite A \<and> profile A prof) \<longrightarrow> elect m2 A prof \<noteq> {})"
      using electing_m2
      by metis
    have def_card_one:
      "electoral_module m1 \<and>
        (\<forall> A prof.
          (1 \<le> card A \<and> finite A \<and> profile A prof) \<longrightarrow>
            card (defer m1 A prof) = 1)"
      using def_one_m1
      unfolding defers_def
      by blast
    hence "electoral_module (m1 \<triangleright> m2)"
      using f_elect seq_comp_sound
      by metis
    with f_mod f_elect def_card_one
    show ?thesis
      using seq_comp_def_then_elect_elec_set def_presv_fin_prof
            def_m1_not_empty bot_eq_sup_iff
      by metis
  qed
qed

lemma def_lift_inv_seq_comp_help:
  assumes
    monotone_m: "defer_lift_invariance m" and
    monotone_n: "defer_lift_invariance n" and
    def_and_lifted: "a \<in> (defer (m \<triangleright> n) A p) \<and> lifted A p q a"
  shows "(m \<triangleright> n) A p = (m \<triangleright> n) A q"
proof -
  let ?new_Ap = "defer m A p"
  let ?new_Aq = "defer m A q"
  let ?new_p = "limit_profile ?new_Ap p"
  let ?new_q = "limit_profile ?new_Aq q"
  from monotone_m monotone_n
  have modules:
    "electoral_module m \<and> electoral_module n"
    unfolding defer_lift_invariance_def
    by simp
  hence "finite_profile A p \<longrightarrow> defer (m \<triangleright> n) A p \<subseteq> defer m A p"
    using seq_comp_def_set_bounded
    by metis
  moreover have profile_p: "lifted A p q a \<longrightarrow> finite_profile A p"
    unfolding lifted_def
    by simp
  ultimately have defer_subset: "defer (m \<triangleright> n) A p \<subseteq> defer m A p"
    using def_and_lifted
    by blast
  hence mono_m: "m A p = m A q"
    using monotone_m def_and_lifted modules profile_p
          seq_comp_def_set_trans
    unfolding defer_lift_invariance_def
    by metis
  hence new_A_eq: "?new_Ap = ?new_Aq"
    by presburger
  have defer_eq:
    "defer (m \<triangleright> n) A p = defer n ?new_Ap ?new_p"
    using snd_conv
    unfolding sequential_composition.simps
    by metis
  hence mono_n:
    "n ?new_Ap ?new_p = n ?new_Aq ?new_q"
  proof cases
    assume "lifted ?new_Ap ?new_p ?new_q a"
    thus ?thesis
      using defer_eq mono_m monotone_n def_and_lifted
      unfolding defer_lift_invariance_def
      by (metis (no_types, lifting))
  next
    assume a2: "\<not>lifted ?new_Ap ?new_p ?new_q a"
    from def_and_lifted
    have "finite_profile A q"
      unfolding lifted_def
      by simp
    with modules new_A_eq
    have 1:
      "finite_profile ?new_Ap ?new_q"
      using def_presv_fin_prof
      by (metis (no_types))
    moreover from modules profile_p def_and_lifted
    have 0:
      "finite_profile ?new_Ap ?new_p"
      using def_presv_fin_prof
      by (metis (no_types))
    moreover from defer_subset def_and_lifted
    have 2: "a \<in> ?new_Ap"
      by blast
    moreover from def_and_lifted
    have eql_lengths:
      "length ?new_p = length ?new_q"
      unfolding lifted_def
      by simp
    ultimately have 0:
      "(\<forall> i::nat. i < length ?new_p \<longrightarrow>
          \<not>Preference_Relation.lifted ?new_Ap (?new_p!i) (?new_q!i) a) \<or>
       (\<exists> i::nat. i < length ?new_p \<and>
          \<not>Preference_Relation.lifted ?new_Ap (?new_p!i) (?new_q!i) a \<and>
              (?new_p!i) \<noteq> (?new_q!i))"
      using a2
      unfolding lifted_def
      by (metis (no_types, lifting))
    from def_and_lifted modules
    have
      "\<forall> i. (0 \<le> i \<and> i < length ?new_p) \<longrightarrow>
          (Preference_Relation.lifted A (p!i) (q!i) a \<or> (p!i) = (q!i))"
      using limit_prof_presv_size
      unfolding Profile.lifted_def
      by metis
    with def_and_lifted modules mono_m
    have
      "\<forall> i. (0 \<le> i \<and> i < length ?new_p) \<longrightarrow>
          (Preference_Relation.lifted ?new_Ap (?new_p!i) (?new_q!i) a \<or>
           (?new_p!i) = (?new_q!i))"
      using limit_lifted_imp_eq_or_lifted defer_in_alts
            limit_prof_presv_size nth_map
      unfolding Profile.lifted_def limit_profile.simps
      by (metis (no_types, lifting))
    with 0 eql_lengths mono_m
    show ?thesis
      using leI not_less_zero nth_equalityI
      by metis
  qed
  from mono_m mono_n
  show ?thesis
    unfolding sequential_composition.simps
    by (metis (full_types))
qed

text \<open>
  Sequential composition preserves the property defer-lift-invariance.
\<close>

theorem seq_comp_presv_def_lift_inv[simp]:
  assumes
    monotone_m: "defer_lift_invariance m" and
    monotone_n: "defer_lift_invariance n"
  shows "defer_lift_invariance (m \<triangleright> n)"
  using monotone_m monotone_n def_lift_inv_seq_comp_help
        seq_comp_sound defer_lift_invariance_def
  by (metis (full_types))

text \<open>
  Composing a non-blocking, non-electing electoral module
  in sequence with an electoral module that defers exactly
  one alternative results in an electoral module that defers
  exactly one alternative.
\<close>

theorem seq_comp_def_one[simp]:
  assumes
    non_blocking_m: "non_blocking m" and
    non_electing_m: "non_electing m" and
    def_1_n: "defers 1 n"
  shows "defers 1 (m \<triangleright> n)"
proof (unfold defers_def, safe)
  have electoral_mod_m: "electoral_module m"
    using non_electing_m
    unfolding non_electing_def
    by simp
  have electoral_mod_n: "electoral_module n"
    using def_1_n
    unfolding defers_def
    by simp
  show "electoral_module (m \<triangleright> n)"
    using electoral_mod_m electoral_mod_n
    by simp
next
  fix
    A :: "'a set" and
    p :: "'a Profile"
  assume
    pos_card: "1 \<le> card A" and
    fin_A: "finite A" and
    prof_A: "profile A p"
  from pos_card have
    "A \<noteq> {}"
    by auto
  with fin_A prof_A have m_non_blocking:
    "reject m A p \<noteq> A"
    using non_blocking_m
    unfolding non_blocking_def
    by simp
  hence
    "\<exists> a. a \<in> A \<and> a \<notin> reject m A p"
    using pos_card non_electing_m
          reject_in_alts subset_antisym subset_iff
          fin_A prof_A subsetI
    unfolding non_electing_def
    by slow
  hence "defer m A p \<noteq> {}"
    using electoral_mod_defer_elem empty_iff pos_card
          non_electing_m fin_A prof_A
    unfolding non_electing_def
    by (metis (no_types))
  hence defer_non_empty:
    "card (defer m A p) \<ge> 1"
    using Suc_leI card_gt_0_iff pos_card fin_A prof_A
          non_blocking_m def_presv_fin_prof
    unfolding One_nat_def non_blocking_def
    by metis
  have defer_fun:
    "defer (m \<triangleright> n) A p =
      defer n (defer m A p) (limit_profile (defer m A p) p)"
    using def_1_n fin_A non_blocking_m prof_A seq_comp_defers_def_set
    unfolding defers_def non_blocking_def
    by (metis (no_types, opaque_lifting))
  have
    "\<forall> n f. defers n f =
      (electoral_module f \<and>
        (\<forall> A prof.
          (\<not> n \<le> card (A::'a set) \<or> infinite A \<or>
            \<not> profile A prof) \<or>
          card (defer f A prof) = n))"
    unfolding defers_def
    by blast
  hence
    "card (defer n (defer m A p)
      (limit_profile (defer m A p) p)) = 1"
    using defer_non_empty def_1_n fin_A prof_A
          non_blocking_m def_presv_fin_prof
    unfolding non_blocking_def
    by metis
  thus "card (defer (m \<triangleright> n) A p) = 1"
    using defer_fun
    by simp
qed

text \<open>
  Composing a defer-lift invariant and a non-electing
  electoral module that defers exactly one alternative
  in sequence with an electing electoral module
  results in a monotone electoral module.
\<close>

theorem disj_compat_seq[simp]:
  assumes
    compatible: "disjoint_compatibility m n" and
    module_m2: "electoral_module m2"
  shows "disjoint_compatibility (m \<triangleright> m2) n"
proof (unfold disjoint_compatibility_def, safe)
  show "electoral_module (m \<triangleright> m2)"
    using compatible module_m2 seq_comp_sound
    unfolding disjoint_compatibility_def
    by metis
next
  show "electoral_module n"
    using compatible
    unfolding disjoint_compatibility_def
    by metis
next
  fix S :: "'a set"
  assume fin_S: "finite S"
  have modules:
    "electoral_module (m \<triangleright> m2) \<and> electoral_module n"
    using compatible module_m2 seq_comp_sound
    unfolding disjoint_compatibility_def
    by metis
  obtain A where A:
    "A \<subseteq> S \<and>
      (\<forall> a \<in> A. indep_of_alt m S a \<and>
        (\<forall> p. finite_profile S p \<longrightarrow> a \<in> reject m S p)) \<and>
      (\<forall> a \<in> S - A. indep_of_alt n S a \<and>
        (\<forall> p. finite_profile S p \<longrightarrow> a \<in> reject n S p))"
    using compatible fin_S
    unfolding disjoint_compatibility_def
    by (metis (no_types, lifting))
  show
    "\<exists> A \<subseteq> S.
      (\<forall> a \<in> A. indep_of_alt (m \<triangleright> m2) S a \<and>
        (\<forall> p. finite_profile S p \<longrightarrow> a \<in> reject (m \<triangleright> m2) S p)) \<and>
      (\<forall> a \<in> S - A. indep_of_alt n S a \<and>
        (\<forall> p. finite_profile S p \<longrightarrow> a \<in> reject n S p))"
  proof
    have
      "\<forall> a p q.
        a \<in> A \<and> equiv_prof_except_a S p q a \<longrightarrow>
          (m \<triangleright> m2) S p = (m \<triangleright> m2) S q"
    proof (safe)
      fix
        a :: "'a" and
        p :: "'a Profile" and
        q :: "'a Profile"
      assume
        a: "a \<in> A" and
        b: "equiv_prof_except_a S p q a"
      have eq_def:
        "defer m S p = defer m S q"
        using A a b
        unfolding indep_of_alt_def
        by metis
      from a b have profiles:
        "finite_profile S p \<and> finite_profile S q"
        unfolding equiv_prof_except_a_def
        by simp
      hence "(defer m S p) \<subseteq> S"
        using compatible defer_in_alts
        unfolding disjoint_compatibility_def
        by metis
      hence
        "limit_profile (defer m S p) p =
          limit_profile (defer m S q) q"
        using A DiffD2 a b compatible defer_not_elec_or_rej
              profiles negl_diff_imp_eq_limit_prof
        unfolding disjoint_compatibility_def eq_def
        by (metis (no_types, lifting))
      with eq_def have
        "m2 (defer m S p) (limit_profile (defer m S p) p) =
          m2 (defer m S q) (limit_profile (defer m S q) q)"
        by simp
      moreover have "m S p = m S q"
        using A a b
        unfolding indep_of_alt_def
        by metis
      ultimately show
        "(m \<triangleright> m2) S p = (m \<triangleright> m2) S q"
        unfolding sequential_composition.simps
        by (metis (full_types))
    qed
    moreover have
      "\<forall> a \<in> A. \<forall> p. finite_profile S p \<longrightarrow> a \<in> reject (m \<triangleright> m2) S p"
      using A UnI1 prod.sel
      unfolding sequential_composition.simps
      by metis
    ultimately show
      "A \<subseteq> S \<and>
        (\<forall> a \<in> A. indep_of_alt (m \<triangleright> m2) S a \<and>
          (\<forall> p. finite_profile S p \<longrightarrow> a \<in> reject (m \<triangleright> m2) S p)) \<and>
        (\<forall> a \<in> S - A. indep_of_alt n S a \<and>
          (\<forall> p. finite_profile S p \<longrightarrow> a \<in> reject n S p))"
      using A indep_of_alt_def modules
      by (metis (mono_tags, lifting))
  qed
qed

text \<open>
  Composing a defer-lift invariant and a non-electing
  electoral module that defers exactly one alternative
  in sequence with an electing electoral module
  results in a monotone electoral module.
\<close>

theorem seq_comp_mono[simp]:
  assumes
    def_monotone_m: "defer_lift_invariance m" and
    non_ele_m: "non_electing m" and
    def_one_m: "defers 1 m" and
    electing_n: "electing n"
  shows "monotonicity (m \<triangleright> n)"
proof (unfold monotonicity_def, safe)
  have electoral_mod_m: "electoral_module m"
    using non_ele_m
    unfolding non_electing_def
    by simp
  have electoral_mod_n: "electoral_module n"
    using electing_n
    unfolding electing_def
    by simp
  show "electoral_module (m \<triangleright> n)"
    using electoral_mod_m electoral_mod_n
    by simp
next
  fix
    A :: "'a set" and
    p :: "'a Profile" and
    q :: "'a Profile" and
    w :: "'a"
  assume
    fin_A: "finite A" and
    elect_w_in_p: "w \<in> elect (m \<triangleright> n) A p" and
    lifted_w: "Profile.lifted A p q w"
  have "finite_profile A p \<and> finite_profile A q"
    using lifted_w
    unfolding lifted_def
    by metis
  thus "w \<in> elect (m \<triangleright> n) A q"
    using seq_comp_def_then_elect elect_w_in_p lifted_w
          def_monotone_m non_ele_m def_one_m electing_n
    unfolding defer_lift_invariance_def
    by metis
qed

text \<open>
  Composing a defer-invariant-monotone electoral module in sequence before
  a non-electing, defer-monotone electoral module that defers exactly
  1 alternative results in a defer-lift-invariant electoral module.
\<close>

theorem def_inv_mono_imp_def_lift_inv[simp]:
  assumes
    strong_def_mon_m: "defer_invariant_monotonicity m" and
    non_electing_n: "non_electing n" and
    defers_1: "defers 1 n" and
    defer_monotone_n: "defer_monotonicity n"
  shows "defer_lift_invariance (m \<triangleright> n)"
proof (unfold defer_lift_invariance_def, safe)
  have electoral_mod_m: "electoral_module m"
    using strong_def_mon_m
    unfolding defer_invariant_monotonicity_def
    by metis
  have electoral_mod_n: "electoral_module n"
    using defers_1
    unfolding defers_def
    by metis
  show "electoral_module (m \<triangleright> n)"
    using electoral_mod_m electoral_mod_n
    by simp
next
  fix
    A :: "'a set" and
    p :: "'a Profile" and
    q :: "'a Profile" and
    a :: "'a"
  assume
    defer_a_p: "a \<in> defer (m \<triangleright> n) A p" and
    lifted_a: "Profile.lifted A p q a"
  from strong_def_mon_m
  have non_electing_m: "non_electing m"
    unfolding defer_invariant_monotonicity_def
    by simp
  have electoral_mod_m: "electoral_module m"
    using strong_def_mon_m
    unfolding defer_invariant_monotonicity_def
    by metis
  have electoral_mod_n: "electoral_module n"
    using defers_1
    unfolding defers_def
    by metis
  have finite_profile_q: "finite_profile A q"
    using lifted_a
    unfolding Profile.lifted_def
    by simp
  have finite_profile_p: "profile A p"
    using lifted_a
    unfolding Profile.lifted_def
    by simp
  show "(m \<triangleright> n) A p = (m \<triangleright> n) A q"
  proof (cases)
    assume not_unchanged: "defer m A q \<noteq> defer m A p"
    from not_unchanged
    have a_single_defer: "{a} = defer m A q"
      using strong_def_mon_m electoral_mod_n defer_a_p
            lifted_a seq_comp_def_set_trans finite_profile_p
            finite_profile_q
      unfolding defer_invariant_monotonicity_def
      by metis
    moreover have
      "{a} = defer m A q \<longrightarrow> defer (m \<triangleright> n) A q \<subseteq> {a}"
      using finite_profile_q electoral_mod_m electoral_mod_n
            seq_comp_def_set_sound
      by (metis (no_types, opaque_lifting))
    ultimately have
      "(a \<in> defer m A p) \<longrightarrow> defer (m \<triangleright> n) A q \<subseteq> {a}"
      by simp
    moreover have def_card_one:
      "(a \<in> defer m A p) \<longrightarrow> card (defer (m \<triangleright> n) A q) = 1"
      using a_single_defer card_eq_0_iff card_insert_disjoint defers_1
            electoral_mod_m empty_iff finite.emptyI
            seq_comp_defers_def_set order_refl
            def_presv_fin_prof finite_profile_q
      unfolding One_nat_def defers_def
      by metis
    moreover have defer_a_in_m_p:
      "a \<in> defer m A p"
      using electoral_mod_m electoral_mod_n defer_a_p
            seq_comp_def_set_bounded finite_profile_p
            finite_profile_q
      by blast
    ultimately have
      "defer (m \<triangleright> n) A q = {a}"
      using Collect_mem_eq card_1_singletonE empty_Collect_eq
            insertCI subset_singletonD
      by metis
    moreover have
      "defer (m \<triangleright> n) A p = {a}"
    proof (safe)
      fix x :: "'a"
      assume
        defer_x: "x \<in> defer (m \<triangleright> n) A p" and
        x_exists: "x \<notin> {}"
      have fin_defer:
        "\<forall> f (A::'a set) prof.
          (electoral_module f \<and> finite A \<and> profile A prof) \<longrightarrow>
            finite_profile (defer f A prof)
              (limit_profile (defer f A prof) prof)"
        using def_presv_fin_prof
        by (metis (no_types))
      have "finite_profile (defer m A p) (limit_profile (defer m A p) p)"
        using electoral_mod_m finite_profile_p finite_profile_q fin_defer
        by blast
      hence "Suc (card (defer m A p - {a})) = card (defer m A p)"
        using card_Suc_Diff1 defer_a_in_m_p
        by metis
      hence min_card:
        "Suc 0 \<le> card (defer m A p)"
        by linarith
      have emod_n_then_mn:
        "electoral_module n \<longrightarrow> electoral_module (m \<triangleright> n)"
        using electoral_mod_m
        by simp
      have "defers (Suc 0) n"
        using defers_1
        by simp
      hence defer_card_one:
        "electoral_module n \<and>
          (\<forall> A prof.
            (Suc 0 \<le> card A \<and> finite A \<and> profile A prof) \<longrightarrow>
              card (defer n A prof) = Suc 0)"
        unfolding defers_def
        by simp
      hence emod_mn: "electoral_module (m \<triangleright> n)"
        using emod_n_then_mn
        by blast
      have nat_diff:
        "\<forall> (i::nat) j. i \<le> j \<longrightarrow> i - j = 0"
        by auto
      have nat_comp:
        "\<forall> (i::nat) j k.
          i \<le> j \<and> j \<le> k \<or>
            j \<le> i \<and> i \<le> k \<or>
            i \<le> k \<and> k \<le> j \<or>
            k \<le> j \<and> j \<le> i \<or>
            j \<le> k \<and> k \<le> i \<or>
            k \<le> i \<and> i \<le> j"
        using le_cases3
        by linarith
      have fin_diff_card:
        "\<forall> A a.
          (finite A \<and> (a::'a) \<in> A) \<longrightarrow>
            card (A - {a}) = card A - 1"
        using card_Diff_singleton
        by metis
      with fin_defer defer_card_one min_card
      have "card (defer (m \<triangleright> n) A p) = Suc 0"
        using electoral_mod_m seq_comp_defers_def_set
          finite_profile_p finite_profile_q
        by metis
      with fin_diff_card nat_comp nat_diff emod_mn fin_defer
      have "{a} = {x}"
        using One_nat_def card_1_singletonE singletonD
              defer_a_p defer_x
        by metis
      thus "x = a"
        by force
    next
      show "a \<in> defer (m \<triangleright> n) A p"
        using defer_a_p
        by linarith
    qed
    ultimately have "defer (m \<triangleright> n) A p = defer (m \<triangleright> n) A q"
      by blast
    moreover have "elect (m \<triangleright> n) A p = elect (m \<triangleright> n) A q"
      using finite_profile_p finite_profile_q
            non_electing_m non_electing_n
            seq_comp_presv_non_electing
            non_electing_def
      by metis
    thus ?thesis
      using calculation eq_def_and_elect_imp_eq
            electoral_mod_m electoral_mod_n
            finite_profile_p seq_comp_sound
            finite_profile_q
      by metis
  next
    assume not_different_alternatives:
      "\<not>(defer m A q \<noteq> defer m A p)"
    have "elect m A p = {}"
      using non_electing_m finite_profile_p finite_profile_q
      by (simp add: non_electing_def)
    moreover have "elect m A q = {}"
      using non_electing_m finite_profile_q
      by (simp add: non_electing_def)
    ultimately have elect_m_equal: "elect m A p = elect m A q"
      by simp
    from not_different_alternatives
    have same_alternatives: "defer m A q = defer m A p"
      by simp
    hence
      "(limit_profile (defer m A p) p) =
        (limit_profile (defer m A p) q) \<or>
          lifted (defer m A q)
            (limit_profile (defer m A p) p)
              (limit_profile (defer m A p) q) a"
      using defer_in_alts electoral_mod_m
            lifted_a finite_profile_q
            limit_prof_eq_or_lifted
      by metis
    thus ?thesis
    proof
      assume
        "limit_profile (defer m A p) p =
          limit_profile (defer m A p) q"
      hence same_profile:
        "limit_profile (defer m A p) p =
          limit_profile (defer m A q) q"
        using same_alternatives
        by simp
      hence results_equal_n:
        "n (defer m A q) (limit_profile (defer m A q) q) =
          n (defer m A p) (limit_profile (defer m A p) p)"
        by (simp add: same_alternatives)
      moreover have results_equal_m: "m A p = m A q"
        using elect_m_equal same_alternatives
              finite_profile_p finite_profile_q
        by (simp add: electoral_mod_m eq_def_and_elect_imp_eq)
      hence "(m \<triangleright> n) A p = (m \<triangleright> n) A q"
        using same_profile
        by auto
      thus ?thesis
        by blast
    next
      assume still_lifted:
        "lifted (defer m A q) (limit_profile (defer m A p) p)
          (limit_profile (defer m A p) q) a"
      hence a_in_def_p:
        "a \<in> defer n (defer m A p)
          (limit_profile (defer m A p) p)"
        using electoral_mod_m electoral_mod_n
              finite_profile_p defer_a_p
              seq_comp_def_set_trans
              finite_profile_q
        by metis
      hence a_still_deferred_p:
        "{a} \<subseteq> defer n (defer m A p)
          (limit_profile (defer m A p) p)"
        by simp
      have card_le_1_p: "card (defer m A p) \<ge> 1"
        using One_nat_def Suc_leI card_gt_0_iff
              electoral_mod_m electoral_mod_n
              equals0D finite_profile_p defer_a_p
              seq_comp_def_set_trans def_presv_fin_prof
              finite_profile_q
        by metis
      hence
        "card (defer n (defer m A p)
          (limit_profile (defer m A p) p)) = 1"
        using defers_1 electoral_mod_m
              finite_profile_p def_presv_fin_prof
              finite_profile_q
        unfolding defers_def
        by metis
      hence def_set_is_a_p:
        "{a} = defer n (defer m A p) (limit_profile (defer m A p) p)"
        using a_still_deferred_p card_1_singletonE
              insert_subset singletonD
        by metis
      have a_still_deferred_q:
        "a \<in> defer n (defer m A q)
          (limit_profile (defer m A p) q)"
        using still_lifted a_in_def_p
              defer_monotone_n electoral_mod_m
              same_alternatives
              def_presv_fin_prof finite_profile_q
        unfolding defer_monotonicity_def
        by metis
      have "card (defer m A q) \<ge> 1"
        using card_le_1_p same_alternatives
        by simp
      hence
        "card (defer n (defer m A q)
          (limit_profile (defer m A q) q)) = 1"
        using defers_1 electoral_mod_m
              finite_profile_q def_presv_fin_prof
        unfolding defers_def
        by metis
      hence def_set_is_a_q:
        "{a} =
          defer n (defer m A q)
            (limit_profile (defer m A q) q)"
        using a_still_deferred_q card_1_singletonE
              same_alternatives singletonD
        by metis
      have
        "defer n (defer m A p)
          (limit_profile (defer m A p) p) =
            defer n (defer m A q)
              (limit_profile (defer m A q) q)"
        using def_set_is_a_q def_set_is_a_p
        by auto
      thus ?thesis
        using seq_comp_presv_non_electing
              eq_def_and_elect_imp_eq non_electing_def
              finite_profile_p finite_profile_q
              non_electing_m non_electing_n
              seq_comp_defers_def_set
        by metis
    qed
  qed
qed

end

author: guillerplazas

repo: BachelorThesisRodriguez

sha: master