text:
theory PreferenceLogicTests2      (*** Benzmüller & Fuenmayor, 2021 ***)
   imports PreferenceLogicCeterisParibus
begin (*** Tests for the SSE of van Benthem et al, JPL 2009 ***)
(*** Section 5: Equality-based Ceteris Paribus Preference Logic ***)
 (*Some tests: dualities*)
lemma "\<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>) \<^bold>\<leftrightarrow> \<^bold>\<not>([\<Gamma>]\<^sup>\<preceq>\<^bold>\<not>\<phi>)\<rfloor>"  by auto
lemma "\<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>\<phi>) \<^bold>\<leftrightarrow> \<^bold>\<not>([\<Gamma>]\<^sup>\<prec>\<^bold>\<not>\<phi>)\<rfloor>"  by auto
lemma "\<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<phi>)  \<^bold>\<leftrightarrow> \<^bold>\<not>([\<Gamma>]\<^bold>\<not>\<phi>)\<rfloor>"    by auto
 (*Lemma 2*)
lemma lemma2_1: "(\<^bold>\<diamond>\<^sup>\<preceq>\<phi>) w \<longleftrightarrow> (\<^bold>\<langle>\<^bold>\<emptyset>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>) w" by auto
lemma lemma2_2: "(\<^bold>\<diamond>\<^sup>\<prec>\<phi>) w \<longleftrightarrow> (\<^bold>\<langle>\<^bold>\<emptyset>\<^bold>\<rangle>\<^sup>\<prec>\<phi>) w" by auto
lemma lemma2_3: "((\<^bold>E\<phi>) w \<longleftrightarrow> (\<^bold>\<langle>\<^bold>\<emptyset>\<^bold>\<rangle>\<phi>) w) \<and> ((\<^bold>A\<phi>) w \<longleftrightarrow> ([\<^bold>\<emptyset>]\<phi>) w)" by auto
(**Axiomatization:**)
 (*inclusion and interaction axioms *)
lemma Inc1: "\<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>\<phi>) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>)\<rfloor>" using SBR_def by auto
lemma Inc2: "\<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<phi>)\<rfloor>"  by auto
lemma Int3: "\<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>)) \<^bold>\<rightarrow>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>)\<rfloor>"  by (meson tBR)
lemma Int4: "\<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>)) \<^bold>\<rightarrow>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>\<phi>)\<rfloor>"  by (metis SBR_def tBR)
lemma Int5: "\<lfloor>(\<psi>\<^bold>\<and>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>)) \<^bold>\<rightarrow> ((\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>\<phi>)\<^bold>\<or>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>(\<phi>\<^bold>\<and>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>))))\<rfloor>" by (metis rBR)
 (*ceteris paribus reflexivity*)
lemma CetPar6: "\<phi> \<^bold>\<in> \<Gamma> \<longrightarrow> \<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<phi>) \<^bold>\<rightarrow> \<phi>\<rfloor>"    by blast
lemma CetPar7: "\<phi> \<^bold>\<in> \<Gamma> \<longrightarrow> \<lfloor>(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^bold>\<not>\<phi>) \<^bold>\<rightarrow> \<^bold>\<not>\<phi>\<rfloor>" by blast
 (*monotonicity*)
lemma CetPar8:  "\<Gamma> \<^bold>\<subseteq> \<Gamma>' \<longrightarrow> \<lfloor>(\<^bold>\<langle>\<Gamma>'\<^bold>\<rangle>\<phi>) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<phi>)\<rfloor>"   by auto
lemma CetPar9:  "\<Gamma> \<^bold>\<subseteq> \<Gamma>' \<longrightarrow> \<lfloor>(\<^bold>\<langle>\<Gamma>'\<^bold>\<rangle>\<^sup>\<preceq>\<phi>) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>)\<rfloor>" by auto
lemma CetPar10: "\<Gamma> \<^bold>\<subseteq> \<Gamma>' \<longrightarrow> \<lfloor>(\<^bold>\<langle>\<Gamma>'\<^bold>\<rangle>\<^sup>\<prec>\<phi>) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>\<phi>)\<rfloor>" by auto
 (*increase (decrease) of ceteris paribus sets*)
lemma CetPar11a: "\<lfloor>(\<phi> \<^bold>\<and> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>(\<alpha> \<^bold>\<and> \<phi>) )) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<union>\<^bold>{\<phi>\<^bold>}\<^bold>\<rangle>\<alpha>)\<rfloor>"       by auto
lemma CetPar11b: "\<lfloor>((\<^bold>\<not>\<phi>) \<^bold>\<and> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>(\<alpha> \<^bold>\<and> \<^bold>\<not>\<phi>))) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<union>\<^bold>{\<phi>\<^bold>}\<^bold>\<rangle>\<alpha>)\<rfloor>"   by auto
lemma CetPar12a: "\<lfloor>(\<phi> \<^bold>\<and> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>(\<alpha> \<^bold>\<and> \<phi>) )) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<union>\<^bold>{\<phi>\<^bold>}\<^bold>\<rangle>\<^sup>\<preceq>\<alpha>)\<rfloor>"     by auto
lemma CetPar12b: "\<lfloor>((\<^bold>\<not>\<phi>) \<^bold>\<and> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>(\<alpha> \<^bold>\<and> \<^bold>\<not>\<phi>))) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<union>\<^bold>{\<phi>\<^bold>}\<^bold>\<rangle>\<^sup>\<preceq>\<alpha>)\<rfloor>" by auto
lemma CetPar13a: "\<lfloor>(\<phi> \<^bold>\<and> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>(\<alpha> \<^bold>\<and> \<phi>) )) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<union>\<^bold>{\<phi>\<^bold>}\<^bold>\<rangle>\<^sup>\<prec>\<alpha>)\<rfloor>"     by auto
lemma CetPar13b: "\<lfloor>((\<^bold>\<not>\<phi>) \<^bold>\<and> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<prec>(\<alpha> \<^bold>\<and> \<^bold>\<not>\<phi>))) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<union>\<^bold>{\<phi>\<^bold>}\<^bold>\<rangle>\<^sup>\<prec>\<alpha>)\<rfloor>" by auto
 (*Example 1, Lemma 4, Corollary 1 and Lemma5*)
lemma Ex1:  "\<lfloor>(([\<Gamma>]\<^sup>\<preceq>\<phi>) \<^bold>\<and> (\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<alpha>)) \<^bold>\<rightarrow> (\<^bold>\<langle>\<Gamma>\<^bold>\<union>\<^bold>{\<phi>\<^bold>}\<^bold>\<rangle>\<^sup>\<preceq>\<alpha>)\<rfloor>" using rBR by auto
lemma Lemma4: "(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<^sup>\<preceq>\<phi>) w \<longrightarrow> (\<exists>v. (w \<^bold>\<unlhd>\<^sub>\<Gamma> v) \<and> (\<phi> v))"  by simp
lemma Cor1:   "(\<^bold>\<langle>\<Gamma>\<^bold>\<rangle>\<phi>)  w \<longrightarrow> (\<exists>v. (w \<^bold>\<equiv>\<^sub>\<Gamma> v) \<and> (\<phi> v))"  by simp
lemma Lemma5: "(w \<^bold>\<unlhd>\<^sub>\<Gamma> v) \<longleftrightarrow> ((w \<preceq> v) \<and> (w \<^bold>\<equiv>\<^sub>\<Gamma> v))"    by auto
(**** Section 6: Ceteris Paribus Counterparts ****)
 (*AA-variant (drawing upon von Wright's)*)
lemma "(\<phi> \<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u \<longleftrightarrow> (\<phi> \<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u" nitpick oops (*Ctm*)
lemma "(\<phi> \<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u \<longrightarrow> (\<phi> \<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u" nitpick oops (*Ctm*)
lemma "(\<phi> \<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u \<longrightarrow> (\<phi> \<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u" using SBR_def by auto
lemma "is_total SBR \<longrightarrow> (\<phi> \<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u \<longleftrightarrow> (\<phi> \<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u" by (smt SBR_def)
lemma "(\<phi> \<^bold>\<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u  \<longleftrightarrow> (\<phi> \<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u" nitpick oops (*Ctm*)
lemma "(\<phi> \<^bold>\<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u \<longrightarrow> (\<phi> \<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u"  nitpick oops (*Ctm*)
lemma "(\<phi> \<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u \<longrightarrow> (\<phi> \<^bold>\<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u"  using SBR_def by auto
lemma "is_total SBR \<longrightarrow> (\<phi> \<^bold>\<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u \<longleftrightarrow> (\<phi> \<preceq>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) u" by (smt SBR_def)
 (*AE-variant*)
lemma leAE_cp_pref: "(\<phi> \<^bold>\<preceq>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) u \<longleftrightarrow> (\<phi> \<preceq>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) u" by auto
lemma leqAE_cp_pref: "(\<phi> \<^bold>\<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) u \<longleftrightarrow> (\<phi> \<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) u" by auto
 (*miscelaneous tests*)
lemma "let \<Gamma>=\<^bold>\<emptyset> in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) \<^bold>\<leftrightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A \<psi>)\<rfloor>" by simp
lemma "let \<Gamma>=\<^bold>{\<^bold>\<bottom>\<^bold>} in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) \<^bold>\<leftrightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A \<psi>)\<rfloor>" by simp
lemma "let \<Gamma>=\<^bold>{\<^bold>\<bottom>,A\<^bold>} in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) \<^bold>\<leftrightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A \<psi>)\<rfloor>" nitpick oops (*Ctm*)
lemma "let \<Gamma>=\<^bold>{A\<^bold>} in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>) \<^bold>\<rightarrow> (A \<^bold>\<rightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A \<psi>))\<rfloor>" nitpick oops (*Ctm*)
lemma "let \<Gamma>=\<^bold>{A\<^bold>} in \<lfloor>(A \<^bold>\<rightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A \<psi>)) \<^bold>\<rightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>A\<^sup>\<Gamma> \<psi>)\<rfloor>" nitpick oops (*Ctm*)
lemma "let \<Gamma>=\<^bold>\<emptyset> in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) \<^bold>\<leftrightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E \<psi>)\<rfloor>" by simp
lemma "let \<Gamma>=\<^bold>{\<^bold>\<bottom>\<^bold>} in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) \<^bold>\<leftrightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E \<psi>)\<rfloor>" by simp
lemma "let \<Gamma>=\<^bold>{\<^bold>\<bottom>,A\<^bold>} in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) \<^bold>\<leftrightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E \<psi>)\<rfloor>" nitpick oops (*Ctm*)
lemma "let \<Gamma>=\<^bold>{A\<^bold>} in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) \<^bold>\<rightarrow> (A \<^bold>\<rightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E \<psi>))\<rfloor>" by auto
lemma "let \<Gamma>=\<^bold>{A,B\<^bold>} in \<lfloor>(\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>) \<^bold>\<rightarrow> ((A \<^bold>\<and> B) \<^bold>\<rightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E \<psi>))\<rfloor>" by auto
lemma "let \<Gamma>=\<^bold>{A\<^bold>} in \<lfloor>(A \<^bold>\<rightarrow> (\<phi>\<^bold>\<prec>\<^sub>A\<^sub>E \<psi>)) \<^bold>\<rightarrow> (\<phi> \<^bold>\<prec>\<^sub>A\<^sub>E\<^sup>\<Gamma> \<psi>)\<rfloor>" nitpick oops (*Ctm*)
end

author: cbenzmueller

repo: LogiKEy


text:
theory AMonad
imports
  "../lib/NondetExtensions"
  "../Machine/Machine"
begin

record Session =
  nonceEven :: NONCE
  nonceOdd :: NONCE
  continueSession :: bool

definition
  empty_Session :: "(TPM.AUTHHANDLE, Session) lookup"
where
  "empty_Session \<equiv> \<lambda>_. None"

definition
  update_Session :: "(TPM.AUTHHANDLE, Session) lookup \<Rightarrow> TPM.AUTHHANDLE \<Rightarrow> Session
    \<Rightarrow> (TPM.AUTHHANDLE, Session) lookup"
where
  "update_Session m h s \<equiv> \<lambda>h'. if h' = h then Some s else m h'"

record astate =
  machine :: machine_state
  sessions :: "(TPM.AUTHHANDLE, Session) lookup"

type_synonym 'a s_monad = "(astate, 'a) nondet_monad"
type_synonym ('e, 'a) se_monad = "(astate, 'e + 'a) nondet_monad"

datatype ERROR =
  E_BAD_ELF_HEADER
| E_SHA1_DATA_SIZE
| E_NO_MODULE
| E_BAD_MODULE
| E_BAD_MBI
| E_NO_MBI
| E_BAD_TPM_VENDOR
| E_TIS_TRANSMIT
| E_TIS_LOCALITY_REGISTER_INVALID
| E_TIS_LOCALITY_ACCESS_TIMEOUT
| E_TIS_LOCALITY_ALREADY_ACCESSED
| E_TIS_LOCALITY_DEACTIVATE
| E_PCI
| E_APIC
| E_DEV
| E_SVM_ENABLE
| E_NO_EXT
| E_NO_APIC
| E_NO_SVM
| E_BUFFER_OVERFLOW
| E_TPM_BAD_OUTPUT_PARAM
| E_TPM_BAD_OUTPUT_AUTH
| E_TPM TPM.ERROR

type_synonym 'a E_monad = "(ERROR, 'a) se_monad"

definition
  machine_op_lift :: "'a machine_monad \<Rightarrow> 'a s_monad"
where
  "machine_op_lift m \<equiv>
   do
    s \<leftarrow> gets machine;
    (r, s') \<leftarrow> select_f (m s);
    modify (\<lambda>s. s \<lparr> machine := s' \<rparr>);
    return r
   od"

lemma machine_op_lift_wp[wp]:
  "(\<And>ss. \<lbrace>\<lambda>s. P (ss\<lparr> machine := s \<rparr>)\<rbrace> m \<lbrace>\<lambda>r s'. Q r (ss\<lparr> machine := s' \<rparr>)\<rbrace>)
    \<Longrightarrow> \<lbrace>P\<rbrace> machine_op_lift m \<lbrace>Q\<rbrace>"
  unfolding machine_op_lift_def apply wp unfolding valid_def
proof -
  fix s :: astate and r
  let ?m_state = "machine s"
  assume a: "\<And>ss. \<forall>s. P (ss\<lparr>machine := s\<rparr>) \<longrightarrow> (\<forall>(r, s')\<in>fst (m s). Q r (ss\<lparr>machine := s'\<rparr>))"
     and "P s"
  have s: "s = s\<lparr>machine := ?m_state\<rparr>" by auto
  with `P s` have "P (s\<lparr>machine := ?m_state\<rparr>)" by presburger
  with a have "\<forall>(r, s')\<in>fst (m ?m_state). Q r (s\<lparr>machine := s'\<rparr>)" by blast
  thus "\<forall>x\<in>fst (m (machine s)). (case x of (r, s') \<Rightarrow> \<lambda>s. Q r (s\<lparr>machine := s'\<rparr>)) s"
    by auto
qed

definition "m_tpm_lift \<equiv> machine_op_lift \<circ> tpm_lift"

definition
  exit :: "unit s_monad"
where
  "exit \<equiv> machine_op_lift $ modify (\<lambda>s. s\<lparr> powerOn := False \<rparr>)"

definition
  exit_r :: "'a s_monad"
where
  "exit_r \<equiv>
   do
    exit;
    unknown
   od"

end

author: CriticalTechnologiesInc

repo: SableModel


(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory parse_someops
imports "CParser.CTranslation"
begin

external_file "parse_someops.c"
install_C_file "parse_someops.c"

print_locale parse_someops_global_addresses

context parse_someops_global_addresses
begin
thm f_body_def
thm g_body_def
thm condexp_body_def
thm cbools_body_def
thm bitwise_body_def
thm shifts_body_def
thm callbool_body_def
thm ptr_compare_body_def
thm large_literal_rshift_body_def
end

lemma (in parse_someops_global_addresses) foo:
  "\<Gamma> \<turnstile> \<lbrace> True \<rbrace> \<acute>ret__int :== CALL callbool(1) \<lbrace> \<acute>ret__int = 1 \<rbrace>"
apply vcg
apply simp
done

end


text:
theory T71
imports Main
begin
lemma "(
(\<forall> x::nat. \<forall> y::nat. meet(x, y) = meet(y, x)) &
(\<forall> x::nat. \<forall> y::nat. join(x, y) = join(y, x)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, meet(y, z)) = meet(meet(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(x, join(y, z)) = join(join(x, y), z)) &
(\<forall> x::nat. \<forall> y::nat. meet(x, join(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. join(x, meet(x, y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(x, join(y, z)) = join(mult(x, y), mult(x, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(join(x, y), z) = join(mult(x, z), mult(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(x, over(join(mult(x, y), z), y)) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. meet(y, undr(x, join(mult(x, y), z))) = y) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(over(x, y), y), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. join(mult(y, undr(y, x)), x) = x) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. mult(meet(x, y), z) = meet(mult(x, z), mult(y, z))) &
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. over(join(x, y), z) = join(over(x, z), over(y, z))) &
(\<forall> x::nat. \<forall> y::nat. invo(join(x, y)) = meet(invo(x), invo(y))) &
(\<forall> x::nat. \<forall> y::nat. invo(meet(x, y)) = join(invo(x), invo(y))) &
(\<forall> x::nat. invo(invo(x)) = x)
) \<longrightarrow>
(\<forall> x::nat. \<forall> y::nat. \<forall> z::nat. undr(x, join(y, z)) = join(undr(x, y), undr(x, z)))
"
nitpick[card nat=4,timeout=86400]
oops
end

author: inpefess

repo: residuated-binars


text:
section\<open>IDEM\<close>
theory IDEM
imports "../../TopoS_Impl"
begin

ML\<open>
case !Graphviz.open_viewer of
    OpenImmediately => Graphviz.open_viewer := AskTimeouted 3.0
  | AskTimeouted _ => ()
  | DoNothing => ()
\<close>

definition policy :: "string list_graph" where
  "policy \<equiv> \<lparr> nodesL = [''Logger'',
                        ''Sensor_Controller'',
                        ''P4S_in'',
                        ''P4S_filter_A'',
                        ''P4S_filter_B'',
                        ''P4S_filter_C'',
                        ''P4S_aggregator_C'',
                        ''P4S_encrypt_A'',
                        ''P4S_encrypt_B'',
                        ''P4S_encrypt_C'',
                        ''P4S_encrypt_C_low'',
                        ''P4S_out'',
                        ''P4S_DB'',

                        ''Adversary''],
              edgesL = [
              (''Logger'', ''Sensor_Controller''),
              (''Sensor_Controller'', ''P4S_in''),
              (''P4S_in'',       ''P4S_filter_A''),
              (''P4S_in'',       ''P4S_filter_B''),
              (''P4S_in'',       ''P4S_filter_C''),

              (''P4S_filter_A''    , ''P4S_encrypt_A''),
              (''P4S_filter_B''    , ''P4S_encrypt_B''),
              (''P4S_filter_C''    , ''P4S_encrypt_C''),
              (''P4S_filter_C''    , ''P4S_aggregator_C''),
              (''P4S_aggregator_C'', ''P4S_encrypt_C_low''),

              (''P4S_encrypt_A''      , ''P4S_out''),
              (''P4S_encrypt_B''      , ''P4S_out''),
              (''P4S_encrypt_C''      , ''P4S_out''),
              (''P4S_encrypt_C_low''  , ''P4S_out''),

              (''P4S_out'', ''P4S_DB'')
              ] \<rparr>"

lemma "wf_list_graph policy" by eval

context begin
  definition "tainiting_host_attributes \<equiv> [
                           ''Logger'' \<mapsto> TaintsUntaints {''A'',''B'',''C'',''D''} {},
                           ''Sensor_Controller'' \<mapsto> TaintsUntaints {''A'',''B'',''C'',''D''} {},
                           ''P4S_in'' \<mapsto> TaintsUntaints {''A'',''B'',''C'',''D''} {},
                           ''P4S_filter_A'' \<mapsto> TaintsUntaints {''A''} {''B'',''C'',''D''},
                           ''P4S_filter_B'' \<mapsto> TaintsUntaints {''B''} {''A'',''C'',''D''},
                           ''P4S_filter_C'' \<mapsto> TaintsUntaints {''C''} {''A'',''B'',''D''},
                           ''P4S_aggregator_C'' \<mapsto> TaintsUntaints {''C_low''} {''C''},
                           ''P4S_encrypt_A'' \<mapsto> TaintsUntaints {} {''A''},
                           ''P4S_encrypt_B'' \<mapsto> TaintsUntaints {} {''B''},
                           ''P4S_encrypt_C'' \<mapsto> TaintsUntaints {} {''C''},
                           ''P4S_encrypt_C_low'' \<mapsto> TaintsUntaints {}{''C_low''}
                           ]"
  private lemma "dom (tainiting_host_attributes) \<subseteq> set (nodesL policy)"
    by(simp add: tainiting_host_attributes_def policy_def)
  definition "Tainting_m \<equiv> new_configured_list_SecurityInvariant SINVAR_LIB_TaintingTrusted \<lparr>
        node_properties = tainiting_host_attributes \<rparr> ''critical energy data'' "
end

context begin
  private definition "system_EMS \<equiv>
                [(''Logger'',  SystemComponent),
                 (''Sensor_Controller'',  SystemBoundaryOutput)
                 ]"
  private lemma "dom(map_of system_EMS) \<subseteq> set (nodesL policy)"
    by(simp add: system_EMS_def policy_def)
  definition "system_EMS_m \<equiv> new_meta_system_boundary system_EMS ''EMS''"
end

context begin
  private definition "system_P4S \<equiv>
                [(''P4S_in'',  SystemBoundaryInput),
                 (''P4S_filter_A'',  SystemComponent),
                 (''P4S_filter_B'',  SystemComponent),
                 (''P4S_filter_C'',  SystemComponent),
                 (''P4S_aggregator_C'',  SystemComponent),
                 (''P4S_encrypt_A'',  SystemComponent),
                 (''P4S_encrypt_B'',  SystemComponent),
                 (''P4S_encrypt_C'',  SystemComponent),
                 (''P4S_encrypt_C_low'',  SystemComponent),
                 (''P4S_out'',  SystemBoundaryOutput)
                 ]"
  private lemma "dom(map_of system_P4S) \<subseteq> set (nodesL policy)"
    by(simp add: system_P4S_def policy_def)
  definition "system_P4S_m \<equiv> new_meta_system_boundary system_P4S ''P4S''"
end

context begin
  private definition "system_P4Sstorage \<equiv>
                [(''P4S_DB'',  SystemBoundaryInput)
                 ]"
  private lemma "dom(map_of system_P4Sstorage) \<subseteq> set (nodesL policy)"
    by(simp add: system_P4Sstorage_def policy_def)
  definition "system_P4Sstorage_m \<equiv> new_meta_system_boundary system_P4Sstorage ''P4S storage''"
end

definition "invariants \<equiv> [Tainting_m] @ system_EMS_m @ system_P4S_m @system_P4Sstorage_m"

lemma "all_security_requirements_fulfilled invariants policy" by eval
ML\<open>
visualize_graph @{context} @{term "invariants"} @{term "policy"};
\<close>

value[code] "implc_get_offending_flows invariants (policy\<lparr> edgesL := edgesL policy\<rparr>)"
(*ML{*
visualize_graph @{context} @{term "invariants"} @{term "(policy\<lparr> edgesL := edgesL policy\<rparr>)"};
*}*)
ML\<open>
visualize_graph_header @{context} @{term "invariants"} @{term "policy"} @{term tainiting_host_attributes};
\<close>

definition make_policy :: "('a SecurityInvariant) list \<Rightarrow> 'a list \<Rightarrow> 'a list_graph" where
  "make_policy sinvars Vs \<equiv> generate_valid_topology sinvars \<lparr>nodesL = Vs, edgesL = List.product Vs Vs \<rparr>"

value[code] "make_policy invariants (nodesL policy)"

ML_val\<open>
visualize_edges @{context} @{term "edgesL policy"}
    [("edge [dir=\"arrow\", style=dashed, color=\"#FF8822\", constraint=false]",
     @{term "[(e1, e2) \<leftarrow>  List.product  (nodesL policy) (nodesL policy).
     (e1,e2) \<notin> set (edgesL (make_policy invariants (nodesL policy))) \<and> (e2 = ''Adversary'') \<and> (e1 \<noteq> ''Adversary'')]"})] "";
\<close>

end

repo: PSL


text:
(* Title: Rank_Argument_General.thy
   Author: Chelsea Edmonds
*)

section \<open>Rank Argument - General \<close>
text \<open>General lemmas to enable reasoning using the rank argument. This is described by Godsil
\<^cite>\<open>"godsilToolsLinearAlgebra"\<close> and Bukh \<^cite>\<open>"bukhAlgebraicMethodsCombinatoricsa"\<close>, both of whom
present it as a foundational technique \<close>
theory Rank_Argument_General imports Dual_Systems Jordan_Normal_Form.Determinant
Jordan_Normal_Form.DL_Rank Jordan_Normal_Form.Ring_Hom_Matrix BenOr_Kozen_Reif.More_Matrix
begin

subsection \<open>Row/Column Operations \<close>
text \<open>Extensions to the existing elementary operations are made to enable reasoning on multiple
operations at once, similar to mathematical literature\<close>

lemma index_mat_addrow_basic [simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> addrow a k l A $$ (i,j) = (if k = i then
    ( a * (A $$ (l,j)) + (A $$ (i,j))) else A $$ (i,j))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> addrow a i l A $$ (i,j) = (a * (A $$ (l,j)) + (A $$ (i,j)))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> k \<noteq> i \<Longrightarrow> addrow a k l A $$ (i,j) = A $$(i,j)"
  "dim_row (addrow a k l A) = dim_row A" "dim_col (addrow a k l A) = dim_col A"
  unfolding mat_addrow_def by auto

text\<open>Function to add a column to multiple other columns \<close>
fun add_col_to_multiple :: "'a :: semiring_1 \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> 'a mat \<Rightarrow> 'a mat" where
"add_col_to_multiple a [] l A = A" |
"add_col_to_multiple a (k # ks) l A = (addcol a k l (add_col_to_multiple a ks l A))"

text \<open>Function to add a row to multiple other rows \<close>
fun add_row_to_multiple :: "'a :: semiring_1 \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> 'a mat \<Rightarrow> 'a mat" where
"add_row_to_multiple a [] l A = A" |
"add_row_to_multiple a (k # ks) l A = (addrow a k l (add_row_to_multiple a ks l A))"

text \<open>Function to add multiple rows to a single row \<close>
fun add_multiple_rows :: "'a :: semiring_1 \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a mat \<Rightarrow> 'a mat" where
"add_multiple_rows a k [] A = A" |
"add_multiple_rows a k (l # ls) A = (addrow a k l (add_multiple_rows a k ls A))"

text \<open>Function to add multiple columns to a single col \<close>
fun add_multiple_cols :: "'a :: semiring_1 \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a mat \<Rightarrow> 'a mat" where
"add_multiple_cols a k [] A = A" |
"add_multiple_cols a k (l # ls) A = (addcol a k l (add_multiple_cols a k ls A))"

text \<open>Basic lemmas on dimension and indexing of resulting matrix from above functions \<close>
lemma add_multiple_rows_dim [simp]:
"dim_row (add_multiple_rows a k ls A) = dim_row A"
"dim_col (add_multiple_rows a k ls A) = dim_col A"
  by (induct ls) simp_all

lemma add_multiple_rows_index_unchanged [simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> k \<noteq> i \<Longrightarrow> add_multiple_rows a k ls A $$ (i,j) = A $$(i,j)"
  by (induct ls) (simp_all)

lemma add_multiple_rows_index_eq:
  assumes "i < dim_row A" and "j < dim_col A" and "i \<notin> set ls" and "\<And> l . l \<in> set ls \<Longrightarrow> l < dim_row A"
  shows "add_multiple_rows a i ls A $$ (i,j) = (\<Sum>l\<leftarrow>ls. a * A $$(l,j)) + A$$(i,j)"
  using assms proof (induct ls)
  case Nil
  then show ?case by simp
next
  case (Cons aa ls)
  then have ne: "i \<noteq> aa"
    by auto
  have lt: "aa < dim_row A" using assms(1)
    by (simp add: Cons.prems(4))
  have "(add_multiple_rows a i (aa # ls) A) $$ (i, j) =
      (addrow a i aa (add_multiple_rows a i ls A)) $$ (i, j)"
    by simp
  also have "... = a * add_multiple_rows a i ls A $$ (aa, j) + (add_multiple_rows a i ls A) $$ (i, j)"
    using assms(1) assms(2) index_mat_addrow_basic(2)[of "i" "(add_multiple_rows a i ls A)" "j" "a" "aa"]
    by simp
  also have "... = a * A $$(aa, j) + (add_multiple_rows a i ls A) $$ (i, j)"
    using lt ne by (simp add: assms(2))
  also have "... = a * A $$(aa, j) + (\<Sum>l\<leftarrow>ls. a * A $$ (l, j)) + A $$ (i, j)"
    using Cons.hyps assms(1) assms(2) Cons.prems(3) Cons.prems(4)
    by (metis (mono_tags, lifting) ab_semigroup_add_class.add_ac(1) list.set_intros(2))
  finally show "(add_multiple_rows a i (aa # ls) A) $$ (i, j) =
      (\<Sum>l\<leftarrow>(aa #ls). a * A $$ (l, j)) + A $$ (i, j)"
    by simp
qed

lemma add_multiple_rows_index_eq_bounds:
  assumes "i < dim_row A" and "j < dim_col A" and "i < low \<or> i \<ge> up" and "up \<le> dim_row A"
  shows "add_multiple_rows a i [low..<up] A $$ (i,j) = (\<Sum>l=low..<up. a * A $$(l,j)) + A$$(i,j)"
proof -
  have notin: "i \<notin> set [low..<up]" using assms(3) by auto
  have "\<And> l . l \<in> set [low..<up] \<Longrightarrow> l < dim_row A" using assms(4) by auto
  thus ?thesis  using add_multiple_rows_index_eq[of i A j "[low..<up]"]
      sum_set_upt_eq_sum_list[of "\<lambda> l. a * A $$(l,j)" low up]  notin assms(1) assms(2) by simp
qed

lemma add_multiple_cols_dim [simp]:
  "dim_row (add_multiple_cols a k ls A) = dim_row A"
  "dim_col (add_multiple_cols a k ls A) = dim_col A"
  by (induct ls) simp_all

lemma add_multiple_cols_index_unchanged [simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> k \<noteq> j \<Longrightarrow> add_multiple_cols a k ls A $$ (i,j) = A $$(i,j)"
  by (induct ls) (simp_all)

lemma add_multiple_cols_index_eq:
  assumes "i < dim_row A" and "j < dim_col A" and "j \<notin> set ls" and "\<And> l . l \<in> set ls \<Longrightarrow> l < dim_col A"
  shows "add_multiple_cols a j ls A $$ (i,j) = (\<Sum>l\<leftarrow>ls. a * A $$(i,l)) + A$$(i,j)"
  using assms
proof (induct ls)
  case Nil
  then show ?case by simp
next
  case (Cons aa ls)
  then have ne: "j \<noteq> aa"
    by auto
  have lt: "aa < dim_col A" using assms
    by (simp add: Cons.prems(4))
  have "(add_multiple_cols a j (aa # ls) A) $$ (i, j) = (addcol a j aa (add_multiple_cols a j ls A)) $$ (i, j)"
    by simp
  also have "... = a * add_multiple_cols a j ls A $$ (i, aa) + (add_multiple_cols a j ls A) $$ (i, j)"
    using assms index_mat_addcol by simp
  also have "... = a * A $$(i, aa) + (add_multiple_cols a j ls A) $$ (i, j)"
    using lt ne by (simp add: assms(1))
  also have "... = a * A $$(i, aa) + (\<Sum>l\<leftarrow>ls. a * A $$ (i, l)) + A $$ (i, j)"
    using Cons.hyps assms(1) assms(2)  Cons.prems(3) Cons.prems(4)
    by (metis (mono_tags, lifting) ab_semigroup_add_class.add_ac(1)  list.set_intros(2))
  finally show ?case by simp
qed

lemma add_multiple_cols_index_eq_bounds:
  assumes "i < dim_row A" and "j < dim_col A" and "j < low \<or> j \<ge> up" and "up \<le> dim_col A"
  shows "add_multiple_cols a j [low..<up] A $$ (i,j) = (\<Sum>l=low..<up. a * A $$(i,l)) + A$$(i,j)"
proof -
  have notin: "j \<notin> set [low..<up]" using assms(3) by auto
  have "\<And> l . l \<in> set [low..<up] \<Longrightarrow> l < dim_col A" using assms(4) by auto
  thus ?thesis using add_multiple_cols_index_eq[of i A j "[low..<up]" a]
      sum_set_upt_eq_sum_list[of "\<lambda> l. a * A $$(i,l)" low up] notin assms(1) assms(2) by simp
qed

lemma add_row_to_multiple_dim [simp]:
  "dim_row (add_row_to_multiple a ks l A) = dim_row A"
  "dim_col (add_row_to_multiple a ks l A) = dim_col A"
  by (induct ks) simp_all

lemma add_row_to_multiple_index_unchanged [simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> i \<notin> set ks \<Longrightarrow> add_row_to_multiple a ks l A $$ (i,j) = A $$(i,j)"
  by (induct ks) simp_all

lemma add_row_to_multiple_index_unchanged_bound:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> i < low \<Longrightarrow> i \<ge> up \<Longrightarrow>
    add_row_to_multiple a [low..<up] l A $$ (i,j) = A $$(i,j)"
  by simp

lemma add_row_to_multiple_index_change:
  assumes "i < dim_row A" and "j < dim_col A" and "i \<in> set ks" and "distinct ks" and "l \<notin> set ks"
    and "l < dim_row A"
  shows "add_row_to_multiple a ks l A $$ (i,j) = (a * A$$(l, j)) + A$$(i,j)"
  using assms
proof (induct ks)
  case Nil
  then show ?case by simp
next
  case (Cons aa ls)
  then have lnotin: "l \<notin> set ls" using assms by simp
  then show ?case
  proof (cases "i = aa")
    case True
    then have inotin: "i \<notin> set ls" using assms
      using Cons.prems(4) by fastforce
    have "add_row_to_multiple a (aa # ls) l A $$ (i, j) =
        (addrow a aa l (add_row_to_multiple a ls l A)) $$ (i, j)" by simp
    also have "... = (a * ((add_row_to_multiple a ls l A) $$ (l,j)) +
        ((add_row_to_multiple a ls l A) $$ (i,j)))"
      using True assms(1) assms(2) by auto
    also have "... = a* A $$ (l, j) + ((add_row_to_multiple a ls l A) $$ (i,j))"
      using assms lnotin by simp
    finally have "add_row_to_multiple a (aa # ls) l A $$ (i, j) = a* A $$ (l,j) + A $$ (i, j)"
      using inotin assms by simp
    then show ?thesis by simp
  next
    case False
    then have iin: "i \<in> set ls" using assms
      by (meson Cons.prems(3) set_ConsD)
    have "add_row_to_multiple a (aa # ls) l A $$ (i, j) = (addrow a aa l (add_row_to_multiple a ls l A)) $$ (i, j)"
      by simp
    also have "... =  ((add_row_to_multiple a ls l A) $$ (i,j))"
      using False assms by auto
    finally have "add_row_to_multiple a (aa # ls) l A $$ (i, j) =  a * A $$ (l, j) + A $$ (i, j)"
      using Cons.hyps by (metis Cons.prems(4) assms(1) assms(2) assms(6) distinct.simps(2) iin lnotin)
    then show ?thesis by simp
  qed
qed

lemma add_row_to_multiple_index_change_bounds:
  assumes "i < dim_row A" and "j < dim_col A" and "i \<ge> low" and "i < up"  and "l < low \<or> l \<ge> up"
    and "l < dim_row A"
  shows "add_row_to_multiple a [low..<up] l A $$ (i,j) = (a * A$$(l, j)) + A$$(i,j)"
proof -
  have d: "distinct [low..<up]" by simp
  have iin: "i \<in> set [low..<up]" using assms by auto
  have lnin: "l \<notin> set [low..<up]" using assms by auto
  thus ?thesis
    using add_row_to_multiple_index_change d iin assms by blast
qed

lemma add_col_to_multiple_dim [simp]:
  "dim_row (add_col_to_multiple a ks l A) = dim_row A"
  "dim_col (add_col_to_multiple a ks l A) = dim_col A"
  by (induct ks) simp_all

lemma add_col_to_multiple_index_unchanged [simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> j \<notin> set ks \<Longrightarrow> add_col_to_multiple a ks l A $$ (i,j) = A $$(i,j)"
  by (induct ks) simp_all

lemma add_col_to_multiple_index_unchanged_bound:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> j < low \<Longrightarrow> j \<ge> up \<Longrightarrow>
    add_col_to_multiple a [low..<up] l A $$ (i,j) = A $$(i,j)"
  by simp

lemma add_col_to_multiple_index_change:
  assumes "i < dim_row A" and "j < dim_col A" and "j \<in> set ks" and "distinct ks" and "l \<notin> set ks"
    and "l < dim_col A"
  shows "add_col_to_multiple a ks l A $$ (i,j) = (a * A$$(i, l)) + A$$(i,j)"
  using assms
proof (induct ks)
  case Nil
  then show ?case by simp
next
  case (Cons aa ls)
  then have lnotin: "l \<notin> set ls" using assms by simp
  then show ?case
  proof (cases "j = aa")
    case True
    then have inotin: "j \<notin> set ls" using assms
      using Cons.prems(4) by fastforce
    have "add_col_to_multiple a (aa # ls) l A $$ (i, j) =
        (addcol a aa l (add_col_to_multiple a ls l A)) $$ (i, j)" by simp
    also have "... = (a * ((add_col_to_multiple a ls l A) $$ (i,l)) +
        ((add_col_to_multiple a ls l A) $$ (i,j)))"
      using True assms(1) assms(2) by auto
    also have "... = a* A $$ (i, l) + ((add_col_to_multiple a ls l A) $$ (i,j))"
      using assms lnotin by simp
    finally have "add_col_to_multiple a (aa # ls) l A $$ (i, j) = a* A $$ (i,l) + A $$ (i, j)"
      using inotin assms by simp
    then show ?thesis by simp
  next
    case False
    then have iin: "j \<in> set ls" using assms
      by (meson Cons.prems(3) set_ConsD)
    have "add_col_to_multiple a (aa # ls) l A $$ (i, j) =
        (addcol a aa l (add_col_to_multiple a ls l A)) $$ (i, j)" by simp
    also have "... =  ((add_col_to_multiple a ls l A) $$ (i,j))"
      using False assms by auto
    finally have "add_col_to_multiple a (aa # ls) l A $$ (i, j) =  a * A $$ (i, l) + A $$ (i, j)"
      using Cons.hyps by (metis Cons.prems(4) assms(1) assms(2) assms(6) distinct.simps(2) iin lnotin)
    then show ?thesis by simp
  qed
qed

lemma add_col_to_multiple_index_change_bounds:
  assumes "i < dim_row A" and "j < dim_col A" and "j \<ge> low" and "j < up"  and "l < low \<or> l \<ge> up"
    and "l < dim_col A"
  shows "add_col_to_multiple a [low..<up] l A $$ (i,j) = (a * A$$(i, l)) + A$$(i,j)"
proof -
  have d: "distinct [low..<up]" by simp
  have jin: "j \<in> set [low..<up]" using assms by auto
  have lnin: "l \<notin> set [low..<up]" using assms by auto
  thus ?thesis
    using add_col_to_multiple_index_change d jin assms by blast
qed

text \<open> Operations specifically on 1st row/column \<close>

lemma add_first_row_to_multiple_index:
  assumes "i < dim_row M" and "j < dim_col M"
  shows "i = 0 \<Longrightarrow> (add_row_to_multiple a [1..<dim_row M] 0 M) $$ (i, j) = M $$ (i, j)"
  and "i \<noteq> 0 \<Longrightarrow> (add_row_to_multiple a [1..<dim_row M] 0 M) $$ (i, j) = (a * M$$(0, j)) + M$$(i,j)"
  using assms add_row_to_multiple_index_change_bounds[of i "M" j 1 "dim_row M" 0 "a"] by (simp,linarith)

lemma add_all_cols_to_first:
  assumes "i < dim_row (M)"
  assumes "j < dim_col (M)"
  shows "j \<noteq> 0 \<Longrightarrow> add_multiple_cols 1 0 [1..<dim_col M] M $$ (i, j)  = M $$ (i, j)"
  and "j = 0 \<Longrightarrow> add_multiple_cols 1 0 [1..<dim_col M] M $$ (i, j) = (\<Sum>l = 1..<dim_col M.  M $$(i,l)) + M$$(i,0)"
  using assms add_multiple_cols_index_eq_bounds[of "i" "M" "j" "1" "dim_col M" "1"] assms by (simp_all)

text \<open>Lemmas on the determinant of the matrix under extended row/column operations \<close>

lemma add_row_to_multiple_carrier:
  "A \<in> carrier_mat n n \<Longrightarrow> add_row_to_multiple a ks l A \<in> carrier_mat n n"
  by (metis add_row_to_multiple_dim(1) add_row_to_multiple_dim(2) carrier_matD(1) carrier_matD(2) carrier_matI)

lemma add_col_to_multiple_carrier:
  "A \<in> carrier_mat n n \<Longrightarrow> add_col_to_multiple a ks l A \<in> carrier_mat n n"
  by (metis add_col_to_multiple_dim carrier_matD(1) carrier_matD(2) carrier_matI)

lemma add_multiple_rows_carrier:
  "A \<in> carrier_mat n n \<Longrightarrow> add_multiple_rows a k ls A \<in> carrier_mat n n"
  by (metis add_multiple_rows_dim carrier_matD(1) carrier_matD(2) carrier_matI)

lemma add_multiple_cols_carrier:
  "A \<in> carrier_mat n n \<Longrightarrow> add_multiple_cols a k ls A \<in> carrier_mat n n"
  by (metis add_multiple_cols_dim carrier_matD(1) carrier_matD(2) carrier_matI)

lemma add_row_to_multiple_det:
  assumes "l \<notin> set ks" and "l < n" and "A \<in> carrier_mat n n"
  shows "det (add_row_to_multiple a ks l A) = det A"
  using assms
proof (induct ks)
  case Nil
  then show ?case by simp
next
  case (Cons aa ks)
  have ne: "aa \<noteq> l"
    using Cons.prems(1) by auto
  have "det (add_row_to_multiple a (aa # ks) l A) = det (addrow a aa l (add_row_to_multiple a ks l A))"
    by simp
  also have "... = det (add_row_to_multiple a ks l A)"
    by (meson det_addrow add_row_to_multiple_carrier ne assms)
  finally have "det (add_row_to_multiple a (aa # ks) l A) = det A"
    using Cons.hyps assms by (metis Cons.prems(1) list.set_intros(2))
  then show ?case by simp
qed

lemma add_col_to_multiple_det:
  assumes "l \<notin> set ks" and "l < n" and "A \<in> carrier_mat n n"
  shows "det (add_col_to_multiple a ks l A) = det A"
  using assms
proof (induct ks)
  case Nil
  then show ?case by simp
next
  case (Cons aa ks)
  have ne: "aa \<noteq> l"
    using Cons.prems(1) by auto
  have "det (add_col_to_multiple a (aa # ks) l A) = det (addcol a aa l (add_col_to_multiple a ks l A))"
    by simp
  also have "... = det (add_col_to_multiple a ks l A)"
    by (meson det_addcol add_col_to_multiple_carrier ne assms)
  finally have "det (add_col_to_multiple a (aa # ks) l A) = det A"
    using Cons.hyps assms by (metis Cons.prems(1) list.set_intros(2))
  then show ?case by simp
qed

lemma add_multiple_cols_det:
  assumes "k \<notin> set ls" and "\<And>l. l \<in> set ls \<Longrightarrow> l < n" and "A \<in> carrier_mat n n"
  shows "det (add_multiple_cols a k ls A) = det A"
  using assms
proof (induct ls)
  case Nil
  then show ?case by simp
next
  case (Cons aa ls)
  have ne: "aa \<noteq> k"
    using Cons.prems(1) by auto
  have "det (add_multiple_cols a k (aa # ls) A) = det (addcol a k aa (add_multiple_cols a k ls A))"
    by simp
  also have "... = det (add_multiple_cols a k ls A)"
    using det_addcol add_multiple_cols_carrier ne assms by (metis Cons.prems(2) list.set_intros(1))
  finally have "det (add_multiple_cols a k (aa # ls) A) = det A"
    using Cons.hyps assms by (metis Cons.prems(1) Cons.prems(2) list.set_intros(2))
  then show ?case by simp
qed

lemma add_multiple_rows_det:
  assumes "k \<notin> set ls" and "\<And>l. l \<in> set ls \<Longrightarrow> l < n" and "A \<in> carrier_mat n n"
  shows "det (add_multiple_rows a k ls A) = det A"
  using assms
proof (induct ls)
  case Nil
  then show ?case by simp
next
  case (Cons aa ls)
  have ne: "aa \<noteq> k"
    using Cons.prems(1) by auto
  have "det (add_multiple_rows a k (aa # ls) A) = det (addrow a k aa (add_multiple_rows a k ls A))"
    by simp
  also have "... = det (add_multiple_rows a k ls A)"
    using det_addrow add_multiple_rows_carrier ne assms by (metis Cons.prems(2) list.set_intros(1))
  finally have "det (add_multiple_rows a k (aa # ls) A) = det A"
    using Cons.hyps assms by (metis Cons.prems(1) Cons.prems(2) list.set_intros(2))
  then show ?case by simp
qed

subsection \<open>Rank and Linear Independence\<close>

abbreviation "rank v M \<equiv> vec_space.rank v M"

text \<open>Basic lemma: the rank of the multiplication of two matrices will be less than the minimum
of the individual ranks of those matrices. This directly follows from an existing lemmas in the
linear algebra library which show independently that the resulting matrices rank is less than either
the right or left matrix rank in the product \<close>
lemma rank_mat_mult_lt_min_rank_factor:
  fixes A :: "'a::{conjugatable_ordered_field} mat"
  assumes "A \<in> carrier_mat n m"
  assumes "B \<in> carrier_mat m nc"
  shows "rank n (A * B) \<le> min (rank n A) (rank m B)"
proof -
  have 1: "rank n (A * B) \<le> (rank n A)"
    using assms(1) assms(2) vec_space.rank_mat_mul_right by blast
  have "rank n (A* B) \<le> rank m B"
    by (meson assms(1) assms(2) rank_mat_mul_left)
  thus ?thesis using 1 by simp
qed

text \<open>Rank Argument 1: Given two a $x \times y$ matrix $M$ where $MM^T$ has rank x, $x \le y$\<close>
lemma rank_argument:
  fixes M :: "('c :: {conjugatable_ordered_field}) mat"
  assumes "M \<in> carrier_mat x y"
  assumes "vec_space.rank x (M* M\<^sup>T) = x"
  shows "x \<le> y"
proof -
  let ?B = "(M * M\<^sup>T)"
  have Mt_car: "M\<^sup>T \<in> carrier_mat y x" using assms by simp
  have b_car: "?B \<in> carrier_mat x x"
    using transpose_carrier_mat assms by simp
  then have "rank x ?B \<le> min (rank x M) (rank y M\<^sup>T)"
    using rank_mat_mult_lt_min_rank_factor Mt_car b_car assms(1) by blast
  thus ?thesis using le_trans vec_space.rank_le_nc
    by (metis assms(1) assms(2) min.bounded_iff)
qed

text \<open>Generalise the rank argument to use the determinant. If the determinant of the matrix
is non-zero, than it's rank must be equal to $x$. This removes the need for someone to use
facts on rank in their proofs. \<close>
lemma rank_argument_det:
  fixes M :: "('c :: {conjugatable_ordered_field}) mat"
  assumes "M \<in> carrier_mat x y"
  assumes "det (M* M\<^sup>T) \<noteq> 0"
  shows "x \<le> y"
proof -
  let ?B = "(M * M\<^sup>T)"
  have Mt_car: "M\<^sup>T \<in> carrier_mat y x" using assms by simp
  have b_car: "?B \<in> carrier_mat x x"
    using transpose_carrier_mat assms by simp
  then have b_rank: "vec_space.rank x ?B = x"
    using vec_space.low_rank_det_zero assms(2) by blast
  then have "rank x ?B \<le> min (rank x M) (rank y M\<^sup>T)"
    using rank_mat_mult_lt_min_rank_factor Mt_car b_car assms(1) by blast
  thus ?thesis using le_trans vec_space.rank_le_nc
    by (metis assms(1) b_rank min.bounded_iff)
qed

end

author: isabelle-prover

repo: mirror-afp-devel


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

datatype Bin = One | ZeroAnd "Bin" | OneAnd "Bin"

fun s :: "Bin => Bin" where
"s (One) = ZeroAnd One"
| "s (ZeroAnd xs) = OneAnd xs"
| "s (OneAnd ys) = ZeroAnd (s ys)"

fun plus :: "Bin => Bin => Bin" where
"plus (One) y = s y"
| "plus (ZeroAnd z) (One) = s (ZeroAnd z)"
| "plus (ZeroAnd z) (ZeroAnd ys) = ZeroAnd (plus z ys)"
| "plus (ZeroAnd z) (OneAnd xs) = OneAnd (plus z xs)"
| "plus (OneAnd x2) (One) = s (OneAnd x2)"
| "plus (OneAnd x2) (ZeroAnd zs) = OneAnd (plus x2 zs)"
| "plus (OneAnd x2) (OneAnd ys2) = ZeroAnd (s (plus x2 ys2))"

fun times :: "Bin => Bin => Bin" where
"times (One) y = y"
| "times (ZeroAnd xs1) y = ZeroAnd (times xs1 y)"
| "times (OneAnd xs12) y = plus (ZeroAnd (times xs12 y)) y"

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

end


text:
\<^marker>\<open>creator "Kevin Kappelmann"\<close>
paragraph \<open>Order Equivalence\<close>
theory Transport_Compositions_Agree_Order_Equivalence
  imports
    Transport_Compositions_Agree_Monotone
begin

context transport_comp_agree
begin

subparagraph \<open>Unit\<close>
text \<open>Inflationary\<close>

lemma inflationary_on_unitI:
  assumes mono_l1: "([P] \<Rrightarrow>\<^sub>m P') l1"
  and mono_r1: "((\<le>\<^bsub>R1\<^esub>) \<Rrightarrow>\<^sub>m (\<le>\<^bsub>L1\<^esub>)) r1"
  and inflationary_unit1: "inflationary_on P (\<le>\<^bsub>L1\<^esub>) \<eta>\<^sub>1"
  and trans_L1: "transitive (\<le>\<^bsub>L1\<^esub>)"
  and inflationary_unit2: "inflationary_on P' (\<le>\<^bsub>L2\<^esub>) \<eta>\<^sub>2"
  and L2_le_R1: "\<And>x. P x \<Longrightarrow> l1 x \<le>\<^bsub>L2\<^esub> r2 (l x) \<Longrightarrow> l1 x \<le>\<^bsub>R1\<^esub> r2 (l x)"
  shows "inflationary_on P (\<le>\<^bsub>L\<^esub>) \<eta>"
proof (rule inflationary_onI)
  fix x assume "P x"
  with mono_l1 have "P' (l1 x)" by blast
  with inflationary_unit2 have "l1 x \<le>\<^bsub>L2\<^esub> r2 (l x)" by auto
  with L2_le_R1 \<open>P x\<close> have "l1 x \<le>\<^bsub>R1\<^esub> r2 (l x)" by blast
  with mono_r1 have "\<eta>\<^sub>1 x \<le>\<^bsub>L1\<^esub> \<eta> x" by auto
  moreover from inflationary_unit1 \<open>P x\<close> have "x \<le>\<^bsub>L1\<^esub> \<eta>\<^sub>1 x" by auto
  ultimately show "x \<le>\<^bsub>L\<^esub> \<eta> x" using trans_L1 by blast
qed

corollary inflationary_on_in_field_unitI:
  assumes "((\<le>\<^bsub>L1\<^esub>) \<Rrightarrow>\<^sub>m (\<le>\<^bsub>L2\<^esub>)) l1"
  and "((\<le>\<^bsub>R1\<^esub>) \<Rrightarrow>\<^sub>m (\<le>\<^bsub>L1\<^esub>)) r1"
  and "inflationary_on (in_field (\<le>\<^bsub>L1\<^esub>)) (\<le>\<^bsub>L1\<^esub>) \<eta>\<^sub>1"
  and "transitive (\<le>\<^bsub>L1\<^esub>)"
  and "inflationary_on (in_field (\<le>\<^bsub>L2\<^esub>)) (\<le>\<^bsub>L2\<^esub>) \<eta>\<^sub>2"
  and "\<And>x. in_field (\<le>\<^bsub>L1\<^esub>) x \<Longrightarrow> l1 x \<le>\<^bsub>L2\<^esub> r2 (l x) \<Longrightarrow> l1 x \<le>\<^bsub>R1\<^esub> r2 (l x)"
  shows "inflationary_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>) \<eta>"
  using assms by (intro inflationary_on_unitI dep_mono_wrt_predI) auto

text \<open>Deflationary\<close>

context
begin

interpretation inv :
  transport_comp_agree "(\<ge>\<^bsub>L1\<^esub>)" "(\<ge>\<^bsub>R1\<^esub>)" l1 r1 "(\<ge>\<^bsub>L2\<^esub>)" "(\<ge>\<^bsub>R2\<^esub>)" l2 r2
  rewrites "\<And>R S. (R\<inverse> \<Rrightarrow>\<^sub>m S\<inverse>) \<equiv> (R \<Rrightarrow>\<^sub>m S)"
  and "\<And>R. inflationary_on P R\<inverse> \<equiv> deflationary_on P R"
  and "\<And>R. transitive R\<inverse> \<equiv> transitive R"
  and "\<And>R. in_field R\<inverse> \<equiv> in_field R"
  by simp_all

lemma deflationary_on_in_field_unitI:
  assumes "((\<le>\<^bsub>L1\<^esub>) \<Rrightarrow>\<^sub>m (\<le>\<^bsub>L2\<^esub>)) l1"
  and "((\<le>\<^bsub>R1\<^esub>) \<Rrightarrow>\<^sub>m (\<le>\<^bsub>L1\<^esub>)) r1"
  and "deflationary_on (in_field (\<le>\<^bsub>L1\<^esub>)) (\<le>\<^bsub>L1\<^esub>) \<eta>\<^sub>1"
  and "transitive (\<le>\<^bsub>L1\<^esub>)"
  and "deflationary_on (in_field (\<le>\<^bsub>L2\<^esub>)) (\<le>\<^bsub>L2\<^esub>) \<eta>\<^sub>2"
  and "\<And>x. in_field (\<le>\<^bsub>L1\<^esub>) x \<Longrightarrow> r2 (l x) \<le>\<^bsub>L2\<^esub> l1 x \<Longrightarrow> r2 (l x) \<le>\<^bsub>R1\<^esub> l1 x"
  shows "deflationary_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>) \<eta>"
  using assms by (intro inv.inflationary_on_in_field_unitI[simplified rel_inv_iff_rel])
  auto

end

text \<open>Relational Equivalence\<close>

corollary rel_equivalence_on_in_field_unitI:
  assumes "((\<le>\<^bsub>L1\<^esub>) \<Rrightarrow>\<^sub>m (\<le>\<^bsub>L2\<^esub>)) l1"
  and "((\<le>\<^bsub>R1\<^esub>) \<Rrightarrow>\<^sub>m (\<le>\<^bsub>L1\<^esub>)) r1"
  and "rel_equivalence_on (in_field (\<le>\<^bsub>L1\<^esub>)) (\<le>\<^bsub>L1\<^esub>) \<eta>\<^sub>1"
  and "transitive (\<le>\<^bsub>L1\<^esub>)"
  and "rel_equivalence_on (in_field (\<le>\<^bsub>L2\<^esub>)) (\<le>\<^bsub>L2\<^esub>) \<eta>\<^sub>2"
  and "\<And>x. in_field (\<le>\<^bsub>L1\<^esub>) x \<Longrightarrow> l1 x \<le>\<^bsub>L2\<^esub> r2 (l x) \<Longrightarrow> l1 x \<le>\<^bsub>R1\<^esub> r2 (l x)"
  and "\<And>x. in_field (\<le>\<^bsub>L1\<^esub>) x \<Longrightarrow> r2 (l x) \<le>\<^bsub>L2\<^esub> l1 x \<Longrightarrow> r2 (l x) \<le>\<^bsub>R1\<^esub> l1 x"
  shows "rel_equivalence_on (in_field (\<le>\<^bsub>L\<^esub>)) (\<le>\<^bsub>L\<^esub>) \<eta>"
  using assms by (intro rel_equivalence_onI
    inflationary_on_in_field_unitI deflationary_on_in_field_unitI)
  auto

subparagraph \<open>Counit\<close>

text \<open>Corresponding lemmas for the counit can be obtained by flipping the
interpretation of the locale.\<close>

subparagraph \<open>Order Equivalence\<close>

interpretation flip : transport_comp_agree R2 L2 r2 l2 R1 L1 r1 l1
  rewrites "flip.g1.unit \<equiv> \<epsilon>\<^sub>2" and "flip.g2.unit \<equiv> \<epsilon>\<^sub>1" and "flip.unit \<equiv> \<epsilon>"
  by (simp_all only: g1.flip_unit_eq_counit g2.flip_unit_eq_counit flip_unit_eq_counit)

lemma order_equivalenceI:
  assumes "((\<le>\<^bsub>L1\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R1\<^esub>)) l1 r1"
  and "transitive (\<le>\<^bsub>L1\<^esub>)"
  and "((\<le>\<^bsub>L2\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R2\<^esub>)) l2 r2"
  and "transitive (\<le>\<^bsub>R2\<^esub>)"
  and "\<And>x y. x \<le>\<^bsub>L1\<^esub> y \<Longrightarrow> l1 x \<le>\<^bsub>R1\<^esub> l1 y \<Longrightarrow> l1 x \<le>\<^bsub>L2\<^esub> l1 y"
  and "\<And>x y. x \<le>\<^bsub>R2\<^esub> y \<Longrightarrow> r2 x \<le>\<^bsub>L2\<^esub> r2 y \<Longrightarrow> r2 x \<le>\<^bsub>R1\<^esub> r2 y"
  and "\<And>x. in_field (\<le>\<^bsub>L1\<^esub>) x \<Longrightarrow> l1 x \<le>\<^bsub>L2\<^esub> r2 (l x) \<Longrightarrow> l1 x \<le>\<^bsub>R1\<^esub> r2 (l x)"
  and "\<And>x. in_field (\<le>\<^bsub>L1\<^esub>) x \<Longrightarrow> r2 (l x) \<le>\<^bsub>L2\<^esub> l1 x \<Longrightarrow> r2 (l x) \<le>\<^bsub>R1\<^esub> l1 x"
  and "\<And>x. in_field (\<le>\<^bsub>R2\<^esub>) x \<Longrightarrow> r2 x \<le>\<^bsub>R1\<^esub> l1 (r x) \<Longrightarrow> r2 x \<le>\<^bsub>L2\<^esub> l1 (r x)"
  and "\<And>x. in_field (\<le>\<^bsub>R2\<^esub>) x \<Longrightarrow> l1 (r x) \<le>\<^bsub>R1\<^esub> r2 x \<Longrightarrow> l1 (r x) \<le>\<^bsub>L2\<^esub> r2 x"
  shows "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R\<^esub>)) l r"
  using assms by (intro order_equivalenceI rel_equivalence_on_in_field_unitI
    flip.rel_equivalence_on_in_field_unitI
    mono_wrt_rel_leftI flip.mono_wrt_rel_leftI dep_mono_wrt_relI)
  (auto elim!: g1.order_equivalenceE g2.order_equivalenceE)

end

context transport_comp_same
begin

lemma order_equivalenceI:
  assumes "((\<le>\<^bsub>L1\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R1\<^esub>)) l1 r1"
  and "transitive (\<le>\<^bsub>L1\<^esub>)"
  and "((\<le>\<^bsub>R1\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R2\<^esub>)) l2 r2"
  and "transitive (\<le>\<^bsub>R2\<^esub>)"
  shows "((\<le>\<^bsub>L\<^esub>) \<equiv>\<^sub>o (\<le>\<^bsub>R\<^esub>)) l r"
  using assms by (rule order_equivalenceI) auto

end

end

author: kappelmann

repo: transport-isabelle


text:
theory Exercises1 imports Main begin

lemma "A \<or> B \<longrightarrow> B \<or> A"
  apply(rule impI)
  apply(erule disjE)
   apply(rule disjI2)
   apply(assumption)
  apply(rule disjI1)
  apply(assumption)
  done

lemma "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C \<rbrakk> \<Longrightarrow> A \<longrightarrow> C"
  apply(rule impI)
  apply(erule impE)
   apply(assumption)
  apply(erule impE)
   apply(assumption)
  apply(assumption)
  done

text {*
  use constdefs to define a new constant @{text or} that
  defines @{text "\<or>"} by conjunction and negation
*}

definition or :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
"or a b == \<not>(\<not>a \<and> \<not>b)"

thm notI notE

lemma "A \<or> B \<Longrightarrow> or A B"
  apply (unfold or_def)
  apply(rule notI)
  apply(erule disjE)
   apply(erule conjE)
   apply(erule notE)
   apply(assumption)
  apply(erule conjE)
  apply(erule notE)
  apply(erule notE)
  apply(assumption)
  done

thm ccontr notI notE

lemma "or A B \<Longrightarrow> A \<or> B"
  apply(unfold or_def)
  apply(rule ccontr)
  apply(erule notE)
  apply(rule conjI)
   apply(rule notI)
   apply(erule notE)
   apply(rule disjI1)
   apply(assumption)
  apply(rule notI)
  apply(erule notE)
  apply(rule disjI2)
  apply(assumption)
  done

thm allI allE exI exE impI impE

lemma "(\<exists>a. \<forall>b. P a b) \<longrightarrow> (\<forall>d. \<exists>c. P c d)"
  apply(rule impI)
  apply(rule allI)

lemma "((\<exists>x. P x) \<longrightarrow> Q) \<longrightarrow> (\<forall>x. P x \<longrightarrow> Q)"
oops

lemma "\<exists>x. (P x \<longrightarrow> (\<forall>x. P x))"
oops

end

author: zchn

repo: isabelle-practice


text:
theory Exe2p7
  imports Main
begin

datatype 'a tree2 = Tip 'a | Node "'a tree2" 'a "'a tree2"

fun mirror :: "'a tree2 \<Rightarrow> 'a tree2" where
"mirror (Tip a) = Tip a" |
"mirror (Node l n r) = Node (mirror r) n (mirror l)"

fun pre_order :: "'a tree2 \<Rightarrow> 'a list" where
"pre_order (Tip a) = [a]" |
"pre_order (Node l n r) = n # (pre_order l) @ (pre_order r)"

fun post_order :: "'a tree2 \<Rightarrow> 'a list" where
"post_order (Tip a) = [a]" |
"post_order (Node l n r) = (post_order l) @ (post_order r) @ [n]"

lemma pre_m_rev_post : "pre_order (mirror t) = rev (post_order t)"
  apply(induction t)
   apply(auto)
  done

end