text:
(*  Title:      HOL/Proofs/Lambda/WeakNorm.thy
    Author:     Stefan Berghofer
    Copyright   2003 TU Muenchen
*)

section \<open>Weak normalization for simply-typed lambda calculus\<close>

theory WeakNorm
imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
  "~~/src/HOL/Library/Code_Target_Int"
begin

text \<open>
Formalization by Stefan Berghofer. Partly based on a paper proof by
Felix Joachimski and Ralph Matthes @{cite "Matthes-Joachimski-AML"}.
\<close>

subsection \<open>Main theorems\<close>

lemma norm_list:
  assumes f_compat: "\<And>t t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<Longrightarrow> f t \<rightarrow>\<^sub>\<beta>\<^sup>* f t'"
  and f_NF: "\<And>t. NF t \<Longrightarrow> NF (f t)"
  and uNF: "NF u" and uT: "e \<turnstile> u : T"
  shows "\<And>Us. e\<langle>i:T\<rangle> \<tturnstile> as : Us \<Longrightarrow>
    listall (\<lambda>t. \<forall>e T' u i. e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow>
      NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')) as \<Longrightarrow>
    \<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) as \<rightarrow>\<^sub>\<beta>\<^sup>*
      Var j \<degree>\<degree> map f as' \<and> NF (Var j \<degree>\<degree> map f as')"
  (is "\<And>Us. _ \<Longrightarrow> listall ?R as \<Longrightarrow> \<exists>as'. ?ex Us as as'")
proof (induct as rule: rev_induct)
  case (Nil Us)
  with Var_NF have "?ex Us [] []" by simp
  thus ?case ..
next
  case (snoc b bs Us)
  have "e\<langle>i:T\<rangle> \<tturnstile> bs  @ [b] : Us" by fact
  then obtain Vs W where Us: "Us = Vs @ [W]"
    and bs: "e\<langle>i:T\<rangle> \<tturnstile> bs : Vs" and bT: "e\<langle>i:T\<rangle> \<turnstile> b : W"
    by (rule types_snocE)
  from snoc have "listall ?R bs" by simp
  with bs have "\<exists>bs'. ?ex Vs bs bs'" by (rule snoc)
  then obtain bs' where bsred: "Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> map f bs'"
    and bsNF: "NF (Var j \<degree>\<degree> map f bs')" for j
    by iprover
  from snoc have "?R b" by simp
  with bT and uNF and uT have "\<exists>b'. b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b' \<and> NF b'"
    by iprover
  then obtain b' where bred: "b[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* b'" and bNF: "NF b'"
    by iprover
  from bsNF [of 0] have "listall NF (map f bs')"
    by (rule App_NF_D)
  moreover have "NF (f b')" using bNF by (rule f_NF)
  ultimately have "listall NF (map f (bs' @ [b']))"
    by simp
  hence "\<And>j. NF (Var j \<degree>\<degree> map f (bs' @ [b']))" by (rule NF.App)
  moreover from bred have "f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>* f b'"
    by (rule f_compat)
  with bsred have
    "\<And>j. (Var j \<degree>\<degree> map (\<lambda>t. f (t[u/i])) bs) \<degree> f (b[u/i]) \<rightarrow>\<^sub>\<beta>\<^sup>*
     (Var j \<degree>\<degree> map f bs') \<degree> f b'" by (rule rtrancl_beta_App)
  ultimately have "?ex Us (bs @ [b]) (bs' @ [b'])" by simp
  thus ?case ..
qed

lemma subst_type_NF:
  "\<And>t e T u i. NF t \<Longrightarrow> e\<langle>i:U\<rangle> \<turnstile> t : T \<Longrightarrow> NF u \<Longrightarrow> e \<turnstile> u : U \<Longrightarrow> \<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
  (is "PROP ?P U" is "\<And>t e T u i. _ \<Longrightarrow> PROP ?Q t e T u i U")
proof (induct U)
  fix T t
  let ?R = "\<lambda>t. \<forall>e T' u i.
    e\<langle>i:T\<rangle> \<turnstile> t : T' \<longrightarrow> NF u \<longrightarrow> e \<turnstile> u : T \<longrightarrow> (\<exists>t'. t[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t')"
  assume MI1: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T1"
  assume MI2: "\<And>T1 T2. T = T1 \<Rightarrow> T2 \<Longrightarrow> PROP ?P T2"
  assume "NF t"
  thus "\<And>e T' u i. PROP ?Q t e T' u i T"
  proof induct
    fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
    {
      case (App ts x e1 T'1 u1 i1)
      assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
      then obtain Us
        where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
        and argsT: "e\<langle>i:T\<rangle> \<tturnstile> ts : Us"
        by (rule var_app_typesE)
      from nat_eq_dec show "\<exists>t'. (Var x \<degree>\<degree> ts)[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
      proof
        assume eq: "x = i"
        show ?thesis
        proof (cases ts)
          case Nil
          with eq have "(Var x \<degree>\<degree> [])[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* u" by simp
          with Nil and uNF show ?thesis by simp iprover
        next
          case (Cons a as)
          with argsT obtain T'' Ts where Us: "Us = T'' # Ts"
            by (cases Us) (rule FalseE, simp)
          from varT and Us have varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : T'' \<Rightarrow> Ts \<Rrightarrow> T'"
            by simp
          from varT eq have T: "T = T'' \<Rightarrow> Ts \<Rrightarrow> T'" by cases auto
          with uT have uT': "e \<turnstile> u : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by simp
          from argsT Us Cons have argsT': "e\<langle>i:T\<rangle> \<tturnstile> as : Ts" by simp
          from argsT Us Cons have argT: "e\<langle>i:T\<rangle> \<turnstile> a : T''" by simp
          from argT uT refl have aT: "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
          from App and Cons have "listall ?R as" by simp (iprover dest: listall_conj2)
          with lift_preserves_beta' lift_NF uNF uT argsT'
          have "\<exists>as'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
            Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as' \<and>
            NF (Var j \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by (rule norm_list)
          then obtain as' where
            asred: "Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as \<rightarrow>\<^sub>\<beta>\<^sup>*
              Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as'"
            and asNF: "NF (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')" by iprover
          from App and Cons have "?R a" by simp
          with argT and uNF and uT have "\<exists>a'. a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a' \<and> NF a'"
            by iprover
          then obtain a' where ared: "a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* a'" and aNF: "NF a'" by iprover
          from uNF have "NF (lift u 0)" by (rule lift_NF)
          hence "\<exists>u'. lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u' \<and> NF u'" by (rule app_Var_NF)
          then obtain u' where ured: "lift u 0 \<degree> Var 0 \<rightarrow>\<^sub>\<beta>\<^sup>* u'" and u'NF: "NF u'"
            by iprover
          from T and u'NF have "\<exists>ua. u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua \<and> NF ua"
          proof (rule MI1)
            have "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 \<degree> Var 0 : Ts \<Rrightarrow> T'"
            proof (rule typing.App)
              from uT' show "e\<langle>0:T''\<rangle> \<turnstile> lift u 0 : T'' \<Rightarrow> Ts \<Rrightarrow> T'" by (rule lift_type)
              show "e\<langle>0:T''\<rangle> \<turnstile> Var 0 : T''" by (rule typing.Var) simp
            qed
            with ured show "e\<langle>0:T''\<rangle> \<turnstile> u' : Ts \<Rrightarrow> T'" by (rule subject_reduction')
            from ared aT show "e \<turnstile> a' : T''" by (rule subject_reduction')
            show "NF a'" by fact
          qed
          then obtain ua where uared: "u'[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" and uaNF: "NF ua"
            by iprover
          from ared have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* (lift u 0 \<degree> Var 0)[a'/0]"
            by (rule subst_preserves_beta2')
          also from ured have "(lift u 0 \<degree> Var 0)[a'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u'[a'/0]"
            by (rule subst_preserves_beta')
          also note uared
          finally have "(lift u 0 \<degree> Var 0)[a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" .
          hence uared': "u \<degree> a[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* ua" by simp
          from T asNF _ uaNF have "\<exists>r. (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r \<and> NF r"
          proof (rule MI2)
            have "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as : T'"
            proof (rule list_app_typeI)
              show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 : Ts \<Rrightarrow> T'" by (rule typing.Var) simp
              from uT argsT' have "e \<tturnstile> map (\<lambda>t. t[u/i]) as : Ts"
                by (rule substs_lemma)
              hence "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift t 0) (map (\<lambda>t. t[u/i]) as) : Ts"
                by (rule lift_types)
              thus "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<tturnstile> map (\<lambda>t. lift (t[u/i]) 0) as : Ts"
                by (simp_all add: o_def)
            qed
            with asred show "e\<langle>0:Ts \<Rrightarrow> T'\<rangle> \<turnstile> Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as' : T'"
              by (rule subject_reduction')
            from argT uT refl have "e \<turnstile> a[u/i] : T''" by (rule subst_lemma)
            with uT' have "e \<turnstile> u \<degree> a[u/i] : Ts \<Rrightarrow> T'" by (rule typing.App)
            with uared' show "e \<turnstile> ua : Ts \<Rrightarrow> T'" by (rule subject_reduction')
          qed
          then obtain r where rred: "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r"
            and rnf: "NF r" by iprover
          from asred have
            "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
            (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0]"
            by (rule subst_preserves_beta')
          also from uared' have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>*
            (Var 0 \<degree>\<degree> map (\<lambda>t. lift t 0) as')[ua/0]" by (rule subst_preserves_beta2')
          also note rred
          finally have "(Var 0 \<degree>\<degree> map (\<lambda>t. lift (t[u/i]) 0) as)[u \<degree> a[u/i]/0] \<rightarrow>\<^sub>\<beta>\<^sup>* r" .
          with rnf Cons eq show ?thesis
            by (simp add: o_def) iprover
        qed
      next
        assume neq: "x \<noteq> i"
        from App have "listall ?R ts" by (iprover dest: listall_conj2)
        with uNF uT argsT
        have "\<exists>ts'. \<forall>j. Var j \<degree>\<degree> map (\<lambda>t. t[u/i]) ts \<rightarrow>\<^sub>\<beta>\<^sup>* Var j \<degree>\<degree> ts' \<and>
          NF (Var j \<degree>\<degree> ts')" (is "\<exists>ts'. ?ex ts'")
          by (rule norm_list [of "\<lambda>t. t", simplified])
        then obtain ts' where NF: "?ex ts'" ..
        from nat_le_dec show ?thesis
        proof
          assume "i < x"
          with NF show ?thesis by simp iprover
        next
          assume "\<not> (i < x)"
          with NF neq show ?thesis by (simp add: subst_Var) iprover
        qed
      qed
    next
      case (Abs r e1 T'1 u1 i1)
      assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
      then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle>  \<turnstile> r : S" by (rule abs_typeE) simp
      moreover have "NF (lift u 0)" using \<open>NF u\<close> by (rule lift_NF)
      moreover have "e\<langle>0:R\<rangle> \<turnstile> lift u 0 : T" using uT by (rule lift_type)
      ultimately have "\<exists>t'. r[lift u 0/Suc i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" by (rule Abs)
      thus "\<exists>t'. Abs r[u/i] \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'"
        by simp (iprover intro: rtrancl_beta_Abs NF.Abs)
    }
  qed
qed

\<comment> \<open>A computationally relevant copy of @{term "e \<turnstile> t : T"}\<close>
inductive rtyping :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile>\<^sub>R _ : _" [50, 50, 50] 50)
  where
    Var: "e x = T \<Longrightarrow> e \<turnstile>\<^sub>R Var x : T"
  | Abs: "e\<langle>0:T\<rangle> \<turnstile>\<^sub>R t : U \<Longrightarrow> e \<turnstile>\<^sub>R Abs t : (T \<Rightarrow> U)"
  | App: "e \<turnstile>\<^sub>R s : T \<Rightarrow> U \<Longrightarrow> e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile>\<^sub>R (s \<degree> t) : U"

lemma rtyping_imp_typing: "e \<turnstile>\<^sub>R t : T \<Longrightarrow> e \<turnstile> t : T"
  apply (induct set: rtyping)
  apply (erule typing.Var)
  apply (erule typing.Abs)
  apply (erule typing.App)
  apply assumption
  done

theorem type_NF:
  assumes "e \<turnstile>\<^sub>R t : T"
  shows "\<exists>t'. t \<rightarrow>\<^sub>\<beta>\<^sup>* t' \<and> NF t'" using assms
proof induct
  case Var
  show ?case by (iprover intro: Var_NF)
next
  case Abs
  thus ?case by (iprover intro: rtrancl_beta_Abs NF.Abs)
next
  case (App e s T U t)
  from App obtain s' t' where
    sred: "s \<rightarrow>\<^sub>\<beta>\<^sup>* s'" and "NF s'"
    and tred: "t \<rightarrow>\<^sub>\<beta>\<^sup>* t'" and tNF: "NF t'" by iprover
  have "\<exists>u. (Var 0 \<degree> lift t' 0)[s'/0] \<rightarrow>\<^sub>\<beta>\<^sup>* u \<and> NF u"
  proof (rule subst_type_NF)
    have "NF (lift t' 0)" using tNF by (rule lift_NF)
    hence "listall NF [lift t' 0]" by (rule listall_cons) (rule listall_nil)
    hence "NF (Var 0 \<degree>\<degree> [lift t' 0])" by (rule NF.App)
    thus "NF (Var 0 \<degree> lift t' 0)" by simp
    show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 \<degree> lift t' 0 : U"
    proof (rule typing.App)
      show "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> Var 0 : T \<Rightarrow> U"
        by (rule typing.Var) simp
      from tred have "e \<turnstile> t' : T"
        by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
      thus "e\<langle>0:T \<Rightarrow> U\<rangle> \<turnstile> lift t' 0 : T"
        by (rule lift_type)
    qed
    from sred show "e \<turnstile> s' : T \<Rightarrow> U"
      by (rule subject_reduction') (rule rtyping_imp_typing, rule App.hyps)
    show "NF s'" by fact
  qed
  then obtain u where ured: "s' \<degree> t' \<rightarrow>\<^sub>\<beta>\<^sup>* u" and unf: "NF u" by simp iprover
  from sred tred have "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* s' \<degree> t'" by (rule rtrancl_beta_App)
  hence "s \<degree> t \<rightarrow>\<^sub>\<beta>\<^sup>* u" using ured by (rule rtranclp_trans)
  with unf show ?case by iprover
qed

subsection \<open>Extracting the program\<close>

declare NF.induct [ind_realizer]
declare rtranclp.induct [ind_realizer irrelevant]
declare rtyping.induct [ind_realizer]
lemmas [extraction_expand] = conj_assoc listall_cons_eq

extract type_NF

lemma rtranclR_rtrancl_eq: "rtranclpR r a b = r\<^sup>*\<^sup>* a b"
  apply (rule iffI)
  apply (erule rtranclpR.induct)
  apply (rule rtranclp.rtrancl_refl)
  apply (erule rtranclp.rtrancl_into_rtrancl)
  apply assumption
  apply (erule rtranclp.induct)
  apply (rule rtranclpR.rtrancl_refl)
  apply (erule rtranclpR.rtrancl_into_rtrancl)
  apply assumption
  done

lemma NFR_imp_NF: "NFR nf t \<Longrightarrow> NF t"
  apply (erule NFR.induct)
  apply (rule NF.intros)
  apply (simp add: listall_def)
  apply (erule NF.intros)
  done

text_raw \<open>
\begin{figure}
\renewcommand{\isastyle}{\scriptsize\it}%
@{thm [display,eta_contract=false,margin=100] subst_type_NF_def}
\renewcommand{\isastyle}{\small\it}%
\caption{Program extracted from \<open>subst_type_NF\<close>}
\label{fig:extr-subst-type-nf}
\end{figure}

\begin{figure}
\renewcommand{\isastyle}{\scriptsize\it}%
@{thm [display,margin=100] subst_Var_NF_def}
@{thm [display,margin=100] app_Var_NF_def}
@{thm [display,margin=100] lift_NF_def}
@{thm [display,eta_contract=false,margin=100] type_NF_def}
\renewcommand{\isastyle}{\small\it}%
\caption{Program extracted from lemmas and main theorem}
\label{fig:extr-type-nf}
\end{figure}
\<close>

text \<open>
The program corresponding to the proof of the central lemma, which
performs substitution and normalization, is shown in Figure
\ref{fig:extr-subst-type-nf}. The correctness
theorem corresponding to the program \<open>subst_type_NF\<close> is
@{thm [display,margin=100] subst_type_NF_correctness
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
where \<open>NFR\<close> is the realizability predicate corresponding to
the datatype \<open>NFT\<close>, which is inductively defined by the rules
\pagebreak
@{thm [display,margin=90] NFR.App [of ts nfs x] NFR.Abs [of nf t]}

The programs corresponding to the main theorem \<open>type_NF\<close>, as
well as to some lemmas, are shown in Figure \ref{fig:extr-type-nf}.
The correctness statement for the main function \<open>type_NF\<close> is
@{thm [display,margin=100] type_NF_correctness
  [simplified rtranclR_rtrancl_eq Collect_mem_eq, no_vars]}
where the realizability predicate \<open>rtypingR\<close> corresponding to the
computationally relevant version of the typing judgement is inductively
defined by the rules
@{thm [display,margin=100] rtypingR.Var [no_vars]
  rtypingR.Abs [of ty, no_vars] rtypingR.App [of ty e s T U ty' t]}
\<close>

subsection \<open>Generating executable code\<close>

instantiation NFT :: default
begin

definition "default = Dummy ()"

instance ..

end

instantiation dB :: default
begin

definition "default = dB.Var 0"

instance ..

end

instantiation prod :: (default, default) default
begin

definition "default = (default, default)"

instance ..

end

instantiation list :: (type) default
begin

definition "default = []"

instance ..

end

instantiation "fun" :: (type, default) default
begin

definition "default = (\<lambda>x. default)"

instance ..

end

definition int_of_nat :: "nat \<Rightarrow> int" where
  "int_of_nat = of_nat"

text \<open>
  The following functions convert between Isabelle's built-in {\tt term}
  datatype and the generated {\tt dB} datatype. This allows to
  generate example terms using Isabelle's parser and inspect
  normalized terms using Isabelle's pretty printer.
\<close>

ML \<open>
val nat_of_integer = @{code nat} o @{code int_of_integer};

fun dBtype_of_typ (Type ("fun", [T, U])) =
      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
  | dBtype_of_typ (TFree (s, _)) = (case raw_explode s of
        ["'", a] => @{code Atom} (nat_of_integer (ord a - 97))
      | _ => error "dBtype_of_typ: variable name")
  | dBtype_of_typ _ = error "dBtype_of_typ: bad type";

fun dB_of_term (Bound i) = @{code dB.Var} (nat_of_integer i)
  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
  | dB_of_term _ = error "dB_of_term: bad term";

fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
      Abs ("x", T, term_of_dB (T :: Ts) U dBt)
  | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code integer_of_nat} n)
  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
      let val t = term_of_dB' Ts dBt
      in case fastype_of1 (Ts, t) of
          Type ("fun", [T, _]) => t $ term_of_dB Ts T dBu
        | _ => error "term_of_dB: function type expected"
      end
  | term_of_dB' _ _ = error "term_of_dB: term not in normal form";

fun typing_of_term Ts e (Bound i) =
      @{code Var} (e, nat_of_integer i, dBtype_of_typ (nth Ts i))
  | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
          dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
          typing_of_term Ts e t, typing_of_term Ts e u)
      | _ => error "typing_of_term: function type expected")
  | typing_of_term Ts e (Abs (_, T, t)) =
      let val dBT = dBtype_of_typ T
      in @{code Abs} (e, dBT, dB_of_term t,
        dBtype_of_typ (fastype_of1 (T :: Ts, t)),
        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
      end
  | typing_of_term _ _ _ = error "typing_of_term: bad term";

fun dummyf _ = error "dummy";

val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct1));
val ct1' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct1) dB1);

val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (Thm.term_of ct2));
val ct2' = Thm.cterm_of @{context} (term_of_dB [] (Thm.typ_of_cterm ct2) dB2);
\<close>

end

repo: jormungand


text:
section \<open> UTP Expressions \<close>

theory utp_expr
imports
  utp_var
begin

subsection \<open> Expression type \<close>

purge_notation BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")

text \<open> Before building the predicate model, we will build a model of expressions that generalise
  alphabetised predicates. Expressions are represented semantically as mapping from
  the alphabet @{typ "'\<alpha>"} to the expression's type @{typ "'a"}. This general model will allow us to unify
  all constructions under one type. The majority definitions in the file are given using
  the \emph{lifting} package~\<^cite>\<open>"Huffman13"\<close>, which allows us to reuse much of the existing
  library of HOL functions. \<close>

typedef ('t, '\<alpha>) uexpr = "UNIV :: ('\<alpha> \<Rightarrow> 't) set" ..

setup_lifting type_definition_uexpr

notation Rep_uexpr ("\<lbrakk>_\<rbrakk>\<^sub>e")
notation Abs_uexpr ("mk\<^sub>e")

lemma uexpr_eq_iff:
  "e = f \<longleftrightarrow> (\<forall> b. \<lbrakk>e\<rbrakk>\<^sub>e b = \<lbrakk>f\<rbrakk>\<^sub>e b)"
  using Rep_uexpr_inject[of e f, THEN sym] by (auto)

text \<open> The term @{term "\<lbrakk>e\<rbrakk>\<^sub>e b"} effectively refers to the semantic interpretation of the expression
  under the state-space valuation (or variables binding) @{term b}. It can be used, in concert
  with the lifting package, to interpret UTP constructs to their HOL equivalents. We create some
  theorem sets to store such transfer theorems. \<close>

named_theorems uexpr_defs and ueval and lit_simps and lit_norm

subsection \<open> Core expression constructs \<close>

text \<open> A variable expression corresponds to the lens $get$ function associated with a variable.
  Specifically, given a lens the expression always returns that portion of the state-space
  referred to by the lens. \<close>

lift_definition var :: "('t \<Longrightarrow> '\<alpha>) \<Rightarrow> ('t, '\<alpha>) uexpr" is lens_get .

text \<open> A literal is simply a constant function expression, always returning the same value
  for any binding. \<close>

lift_definition lit :: "'t \<Rightarrow> ('t, '\<alpha>) uexpr" ("\<guillemotleft>_\<guillemotright>") is "\<lambda> v b. v" .

text \<open> We define lifting for unary, binary, ternary, and quaternary expression constructs, that
  simply take a HOL function with correct number of arguments and apply it function to all possible
  results of the expressions. \<close>

lift_definition uop :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a, '\<alpha>) uexpr \<Rightarrow> ('b, '\<alpha>) uexpr"
  is "\<lambda> f e b. f (e b)" .
lift_definition bop ::
  "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, '\<alpha>) uexpr \<Rightarrow> ('b, '\<alpha>) uexpr \<Rightarrow> ('c, '\<alpha>) uexpr"
  is "\<lambda> f u v b. f (u b) (v b)" .
lift_definition trop ::
  "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd) \<Rightarrow> ('a, '\<alpha>) uexpr \<Rightarrow> ('b, '\<alpha>) uexpr \<Rightarrow> ('c, '\<alpha>) uexpr \<Rightarrow> ('d, '\<alpha>) uexpr"
  is "\<lambda> f u v w b. f (u b) (v b) (w b)" .
lift_definition qtop ::
  "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'd \<Rightarrow> 'e) \<Rightarrow>
   ('a, '\<alpha>) uexpr \<Rightarrow> ('b, '\<alpha>) uexpr \<Rightarrow> ('c, '\<alpha>) uexpr \<Rightarrow> ('d, '\<alpha>) uexpr \<Rightarrow>
   ('e, '\<alpha>) uexpr"
  is "\<lambda> f u v w x b. f (u b) (v b) (w b) (x b)" .

text \<open> We also define a UTP expression version of function ($\lambda$) abstraction, that takes
  a function producing an expression and produces an expression producing a function. \<close>

lift_definition ulambda :: "('a \<Rightarrow> ('b, '\<alpha>) uexpr) \<Rightarrow> ('a \<Rightarrow> 'b, '\<alpha>) uexpr"
is "\<lambda> f A x. f x A" .

text \<open> We set up syntax for the conditional. This is effectively an infix version of
  if-then-else where the condition is in the middle. \<close>

definition uIf :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
[uexpr_defs]: "uIf = If"

abbreviation cond ::
  "('a,'\<alpha>) uexpr \<Rightarrow> (bool, '\<alpha>) uexpr \<Rightarrow> ('a,'\<alpha>) uexpr \<Rightarrow> ('a,'\<alpha>) uexpr"
  ("(3_ \<triangleleft> _ \<triangleright>/ _)" [52,0,53] 52)
where "P \<triangleleft> b \<triangleright> Q \<equiv> trop uIf b P Q"

text \<open> UTP expression is equality is simply HOL equality lifted using the @{term bop} binary
  expression constructor. \<close>

definition eq_upred :: "('a, '\<alpha>) uexpr \<Rightarrow> ('a, '\<alpha>) uexpr \<Rightarrow> (bool, '\<alpha>) uexpr" (infixl "=\<^sub>u" 50)
where [uexpr_defs]: "eq_upred x y = bop HOL.eq x y"

text \<open> A literal is the expression @{term "\<guillemotleft>v\<guillemotright>"}, where @{term v} is any HOL term. Actually, the
  literal construct is very versatile and also allows us to refer to HOL variables within UTP
  expressions, and has a variety of other uses. It can therefore also be considered as a kind
  of quotation mechanism.

  We also set up syntax for UTP variable expressions. \<close>

syntax
  "_uuvar" :: "svar \<Rightarrow> logic" ("_")

translations
  "_uuvar x" == "CONST var x"

text \<open> Since we already have a parser for variables, we can directly reuse it and simply apply
  the @{term var} expression construct to lift the resulting variable to an expression. \<close>

subsection \<open> Type class instantiations \<close>

text \<open> Isabelle/HOL of course provides a large hierarchy of type classes that provide constructs
  such as numerals and the arithmetic operators. Fortunately we can directly make use of these
  for UTP expressions, and thus we now perform a long list of appropriate instantiations. We
  first lift the core arithemtic constants and operators using a mixture of literals, unary, and binary
  expression constructors. \<close>

instantiation uexpr :: (zero, type) zero
begin
  definition zero_uexpr_def [uexpr_defs]: "0 = lit 0"
instance ..
end

instantiation uexpr :: (one, type) one
begin
  definition one_uexpr_def [uexpr_defs]: "1 = lit 1"
instance ..

end

instantiation uexpr :: (plus, type) plus
begin
  definition plus_uexpr_def [uexpr_defs]: "u + v = bop (+) u v"
instance ..
end

instance uexpr :: (semigroup_add, type) semigroup_add
  by (intro_classes) (simp add: plus_uexpr_def zero_uexpr_def, transfer, simp add: add.assoc)+

text \<open> The following instantiation sets up numerals. This will allow us to have Isabelle number
  representations (i.e. 3,7,42,198 etc.) to UTP expressions directly. \<close>

instance uexpr :: (numeral, type) numeral
  by (intro_classes, simp add: plus_uexpr_def, transfer, simp add: add.assoc)

text \<open> We can also define the order relation on expressions. Now, unlike the previous group and ring
  constructs, the order relations @{term "(\<le>)"} and @{term "(\<le>)"} return a @{type bool} type.
  This order is not therefore the lifted order which allows us to compare the valuation of two
  expressions, but rather the order on expressions themselves. Notably, this instantiation will
  later allow us to talk about predicate refinements and complete lattices. \<close>

instantiation uexpr :: (ord, type) ord
begin
  lift_definition less_eq_uexpr :: "('a, 'b) uexpr \<Rightarrow> ('a, 'b) uexpr \<Rightarrow> bool"
  is "\<lambda> P Q. (\<forall> A. P A \<le> Q A)" .
  definition less_uexpr :: "('a, 'b) uexpr \<Rightarrow> ('a, 'b) uexpr \<Rightarrow> bool"
  where [uexpr_defs]: "less_uexpr P Q = (P \<le> Q \<and> \<not> Q \<le> P)"
instance ..
end

text \<open> UTP expressions whose return type is a partial ordered type, are also partially ordered
  as the following instantiation demonstrates. \<close>

instance uexpr :: (order, type) order
proof
  fix x y z :: "('a, 'b) uexpr"
  show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by (simp add: less_uexpr_def)
  show "x \<le> x" by (transfer, auto)
  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
    by (transfer, blast intro:order.trans)
  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
    by (transfer, rule ext, simp add: eq_iff)
qed

subsection \<open> Syntax translations \<close>

text \<open> The follows a large number of translations that lift HOL functions to UTP expressions
  using the various expression constructors defined above. Much of the time we try to keep
  the HOL syntax but add a "u" subscript. \<close>

text \<open> This operator allows us to get the characteristic set of a type. Essentially this is
  @{term "UNIV"}, but it retains the type syntactically for pretty printing. \<close>

definition set_of :: "'a itself \<Rightarrow> 'a set" where
[uexpr_defs]: "set_of t = UNIV"

text \<open> We add new non-terminals for UTP tuples and maplets. \<close>

nonterminal utuple_args and umaplet and umaplets

syntax \<comment> \<open> Core expression constructs \<close>
  "_ucoerce"    :: "logic \<Rightarrow> type \<Rightarrow> logic" (infix ":\<^sub>u" 50)
  "_ulambda"    :: "pttrn \<Rightarrow> logic \<Rightarrow> logic" ("\<lambda> _ \<bullet> _" [0, 10] 10)
  "_ulens_ovrd" :: "logic \<Rightarrow> logic \<Rightarrow> salpha \<Rightarrow> logic" ("_ \<oplus> _ on _" [85, 0, 86] 86)
  "_ulens_get"  :: "logic \<Rightarrow> svar \<Rightarrow> logic" ("_:_" [900,901] 901)
  "_umem"       :: "('a, '\<alpha>) uexpr \<Rightarrow> ('a set, '\<alpha>) uexpr \<Rightarrow> (bool, '\<alpha>) uexpr" (infix "\<in>\<^sub>u" 50)

translations
  "\<lambda> x \<bullet> p" == "CONST ulambda (\<lambda> x. p)"
  "x :\<^sub>u 'a" == "x :: ('a, _) uexpr"
  "_ulens_ovrd f g a" => "CONST bop (CONST lens_override a) f g"
  "_ulens_ovrd f g a" <= "CONST bop (\<lambda>x y. CONST lens_override x1 y1 a) f g"
  "_ulens_get x y" == "CONST uop (CONST lens_get y) x"
  "x \<in>\<^sub>u A" == "CONST bop (\<in>) x A"

syntax \<comment> \<open> Tuples \<close>
  "_utuple"     :: "('a, '\<alpha>) uexpr \<Rightarrow> utuple_args \<Rightarrow> ('a * 'b, '\<alpha>) uexpr" ("(1'(_,/ _')\<^sub>u)")
  "_utuple_arg"  :: "('a, '\<alpha>) uexpr \<Rightarrow> utuple_args" ("_")
  "_utuple_args" :: "('a, '\<alpha>) uexpr => utuple_args \<Rightarrow> utuple_args"     ("_,/ _")
  "_uunit"      :: "('a, '\<alpha>) uexpr" ("'(')\<^sub>u")
  "_ufst"       :: "('a \<times> 'b, '\<alpha>) uexpr \<Rightarrow> ('a, '\<alpha>) uexpr" ("\<pi>\<^sub>1'(_')")
  "_usnd"       :: "('a \<times> 'b, '\<alpha>) uexpr \<Rightarrow> ('b, '\<alpha>) uexpr" ("\<pi>\<^sub>2'(_')")

translations
  "()\<^sub>u"      == "\<guillemotleft>()\<guillemotright>"
  "(x, y)\<^sub>u"  == "CONST bop (CONST Pair) x y"
  "_utuple x (_utuple_args y z)" == "_utuple x (_utuple_arg (_utuple y z))"
  "\<pi>\<^sub>1(x)"    == "CONST uop CONST fst x"
  "\<pi>\<^sub>2(x)"    == "CONST uop CONST snd x"

syntax \<comment> \<open> Orders \<close>
  "_uless"      :: "logic \<Rightarrow> logic \<Rightarrow> logic" (infix "<\<^sub>u" 50)
  "_uleq"       :: "logic \<Rightarrow> logic \<Rightarrow> logic" (infix "\<le>\<^sub>u" 50)
  "_ugreat"     :: "logic \<Rightarrow> logic \<Rightarrow> logic" (infix ">\<^sub>u" 50)
  "_ugeq"       :: "logic \<Rightarrow> logic \<Rightarrow> logic" (infix "\<ge>\<^sub>u" 50)

translations
  "x <\<^sub>u y"   == "CONST bop (<) x y"
  "x \<le>\<^sub>u y"   == "CONST bop (\<le>) x y"
  "x >\<^sub>u y"   => "y <\<^sub>u x"
  "x \<ge>\<^sub>u y"   => "y \<le>\<^sub>u x"

subsection \<open> Evaluation laws for expressions \<close>

text \<open> The following laws show how to evaluate the core expressions constructs in terms of which
  the above definitions are defined. Thus, using these theorems together, we can convert any UTP
  expression into a pure HOL expression. All these theorems are marked as \emph{ueval} theorems
  which can be used for evaluation. \<close>

lemma lit_ueval [ueval]: "\<lbrakk>\<guillemotleft>x\<guillemotright>\<rbrakk>\<^sub>eb = x"
  by (transfer, simp)

lemma var_ueval [ueval]: "\<lbrakk>var x\<rbrakk>\<^sub>eb = get\<^bsub>x\<^esub> b"
  by (transfer, simp)

lemma uop_ueval [ueval]: "\<lbrakk>uop f x\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb)"
  by (transfer, simp)

lemma bop_ueval [ueval]: "\<lbrakk>bop f x y\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb) (\<lbrakk>y\<rbrakk>\<^sub>eb)"
  by (transfer, simp)

lemma trop_ueval [ueval]: "\<lbrakk>trop f x y z\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb) (\<lbrakk>y\<rbrakk>\<^sub>eb) (\<lbrakk>z\<rbrakk>\<^sub>eb)"
  by (transfer, simp)

lemma qtop_ueval [ueval]: "\<lbrakk>qtop f x y z w\<rbrakk>\<^sub>eb = f (\<lbrakk>x\<rbrakk>\<^sub>eb) (\<lbrakk>y\<rbrakk>\<^sub>eb) (\<lbrakk>z\<rbrakk>\<^sub>eb) (\<lbrakk>w\<rbrakk>\<^sub>eb)"
  by (transfer, simp)

subsection \<open> Misc laws \<close>

text \<open> We also prove a few useful algebraic and expansion laws for expressions. \<close>

lemma uop_const [simp]: "uop id u = u"
  by (transfer, simp)

lemma bop_const_1 [simp]: "bop (\<lambda>x y. y) u v = v"
  by (transfer, simp)

lemma bop_const_2 [simp]: "bop (\<lambda>x y. x) u v = u"
  by (transfer, simp)

lemma uexpr_fst [simp]: "\<pi>\<^sub>1((e, f)\<^sub>u) = e"
  by (transfer, simp)

lemma uexpr_snd [simp]: "\<pi>\<^sub>2((e, f)\<^sub>u) = f"
  by (transfer, simp)

subsection \<open> Literalise tactics \<close>

text \<open> The following tactic converts literal HOL expressions to UTP expressions and vice-versa
        via a collection of simplification rules. The two tactics are called "literalise", which
        converts UTP to expressions to HOL expressions -- i.e. it pushes them into literals --
        and unliteralise that reverses this. We collect the equations in a theorem attribute
        called "lit\_simps". \<close>

lemma lit_fun_simps [lit_simps]:
  "\<guillemotleft>i x y z u\<guillemotright> = qtop i \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright> \<guillemotleft>z\<guillemotright> \<guillemotleft>u\<guillemotright>"
  "\<guillemotleft>h x y z\<guillemotright> = trop h \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright> \<guillemotleft>z\<guillemotright>"
  "\<guillemotleft>g x y\<guillemotright> = bop g \<guillemotleft>x\<guillemotright> \<guillemotleft>y\<guillemotright>"
  "\<guillemotleft>f x\<guillemotright> = uop f \<guillemotleft>x\<guillemotright>"
  by (transfer, simp)+

text \<open> The following two theorems also set up interpretation of numerals, meaning a UTP numeral
  can always be converted to a HOL numeral. \<close>

lemma numeral_uexpr_rep_eq [ueval]: "\<lbrakk>numeral x\<rbrakk>\<^sub>e b = numeral x"
  apply (induct x)
    apply (simp add: lit.rep_eq one_uexpr_def)
   apply (simp add: bop.rep_eq numeral_Bit0 plus_uexpr_def)
  apply (simp add: bop.rep_eq lit.rep_eq numeral_code(3) one_uexpr_def plus_uexpr_def)
  done

lemma numeral_uexpr_simp: "numeral x = \<guillemotleft>numeral x\<guillemotright>"
  by (simp add: uexpr_eq_iff numeral_uexpr_rep_eq lit.rep_eq)

lemma lit_zero [lit_simps]: "\<guillemotleft>0\<guillemotright> = 0" by (simp add:uexpr_defs)
lemma lit_one [lit_simps]: "\<guillemotleft>1\<guillemotright> = 1" by (simp add: uexpr_defs)
lemma lit_plus [lit_simps]: "\<guillemotleft>x + y\<guillemotright> = \<guillemotleft>x\<guillemotright> + \<guillemotleft>y\<guillemotright>" by (simp add: uexpr_defs, transfer, simp)
lemma lit_numeral [lit_simps]: "\<guillemotleft>numeral n\<guillemotright> = numeral n" by (simp add: numeral_uexpr_simp)

text \<open> In general unliteralising converts function applications to corresponding expression
  liftings. Since some operators, like + and *, have specific operators we also have to
  use @{thm uexpr_defs} in reverse to correctly interpret these. Moreover, numerals must be handled
  separately by first simplifying them and then converting them into UTP expression numerals;
  hence the following two simplification rules. \<close>

lemma lit_numeral_1: "uop numeral x = Abs_uexpr (\<lambda>b. numeral (\<lbrakk>x\<rbrakk>\<^sub>e b))"
  by (simp add: uop_def)

lemma lit_numeral_2: "Abs_uexpr (\<lambda> b. numeral v) = numeral v"
  by (metis lit.abs_eq lit_numeral)

method literalise = (unfold lit_simps[THEN sym])
method unliteralise = (unfold lit_simps uexpr_defs[THEN sym];
                     (unfold lit_numeral_1 ; (unfold uexpr_defs ueval); (unfold lit_numeral_2))?)+

text \<open> The following tactic can be used to evaluate literal expressions. It first literalises UTP
  expressions, that is pushes as many operators into literals as possible. Then it tries to simplify,
  and final unliteralises at the end. \<close>

method uexpr_simp uses simps = ((literalise)?, simp add: lit_norm simps, (unliteralise)?)

(* Example *)

lemma "(1::(int, '\<alpha>) uexpr) + \<guillemotleft>2\<guillemotright> = 4 \<longleftrightarrow> \<guillemotleft>3\<guillemotright> = 4"
  apply (literalise)
  apply (uexpr_simp) oops

end

author: isabelle-prover

repo: mirror-afp-devel


text:
subsection \<open>Single step relations\<close>

subsubsection \<open>Registers\<close>

theory SingleStepRegister
  imports RegisterMachineSimulation
begin

lemma single_step_add:
  fixes c :: configuration
    and p :: program
    and l :: register
    and t a :: nat

defines "cs \<equiv> fst (steps c p t)"

assumes is_val: "is_valid_initial c p a"
    and l: "l < length tape"

shows "(\<Sum>R+ p l (\<lambda>k. S c p k t))
        = (if isadd (p!cs) \<and> l = modifies (p!cs) then 1 else 0)"
proof -
  have ic: "c = (0, snd c)"
    using is_val by (auto simp add: is_valid_initial_def) (metis prod.collapse)

  have add_if: "(\<Sum>k = 0..length p-1. if isadd (p ! k) \<and> modifies (p ! cs) = modifies (p ! k)
                                      then S c p k t else 0)
              = (\<Sum>k = 0..length p-1. if k=cs then
              if isadd (p ! k) \<and> modifies (p ! cs) = modifies (p ! k) then S c p k t else 0 else 0)"
    apply (rule sum.cong)
    using S_unique cs_def by auto

  have bound: "fst (steps c p t) \<le> length p - 1" using is_val ic p_contains[of "c" "p" "a" "t"]
    by (auto simp add: dual_order.strict_implies_order)

  thus ?thesis using S_unique add_if
    apply (auto simp add: sum_radd.simps add_if S_def cs_def)
    by (smt S_def sum.cong)
qed

lemma single_step_sub:
  fixes c :: configuration
    and p :: program
    and l :: register
    and t a :: nat

defines "cs \<equiv> fst (steps c p t)"

assumes is_val: "is_valid_initial c p a"

shows "(\<Sum>R- p l (\<lambda>k. Z c p l t * S c p k t))
        = (if issub (p!cs) \<and> l = modifies (p!cs) then Z c p l t else 0)"
proof -
  have "fst c = 0" using is_val by (auto simp add: is_valid_initial_def)
  hence ic: "c = (0, snd c)" by (metis prod.collapse)

  have bound: "cs \<le> length p - 1" using is_val ic p_contains[of "c" "p" "a" "t"]
    by (auto simp add: dual_order.strict_implies_order cs_def)

  have sub_if: "(\<Sum>k = 0..length p-1. if issub (p ! k) \<and> modifies (p ! cs) = modifies (p ! k)
                                    then 1 * (if cs = k then (Suc 0) else 0) else 0)
               =(\<Sum>k = 0..length p-1. if k = cs then
                                      (if issub (p ! k) \<and> modifies (p ! cs) = modifies (p ! k)
                                       then (Suc 0) * (if cs = k then (Suc 0) else 0)
                                    else 0) else 0)"
    apply (rule sum.cong) using cs_def by auto

  show ?thesis using bound sub_if
    apply (auto simp add: sum_rsub.simps cs_def Z_def S_def R_def)
    by (metis One_nat_def cs_def)
qed

lemma lm04_06_one_step_relation_register_old:
  fixes l::register
    and ic::configuration
    and p::program

  defines "s \<equiv> fst ic"
      and "tape \<equiv> snd ic"

  defines "m \<equiv> length p"
      and "tape' \<equiv> snd (step ic p)"

  assumes is_val: "is_valid ic p"
      and l: \<open>l < length tape\<close>

  shows "(tape'!l) = (tape!l) + (if isadd (p!s) \<and> l = modifies (p!s) then 1 else 0)
                              - Z ic p l 0 * (if issub (p!s) \<and> l = modifies (p!s) then 1 else 0)"
proof -
  show ?thesis
    using l
    apply (cases \<open>p!s\<close>)
    apply (auto simp: assms(1-4) step_def update_def)
    using nth_digit_0 by (auto simp add: Z_def R_def)
qed

(* [T] 4.6 *)
lemma lm04_06_one_step_relation_register:
  fixes l :: register
    and c :: configuration
    and p :: program
    and t :: nat
    and a :: nat

defines "r \<equiv> R c p"
defines "s \<equiv> S c p"

assumes is_val: "is_valid_initial c p a"
    and l: "l < length (snd c)"

  shows "r l (Suc t) = r l t + (\<Sum>R+ p l (\<lambda>k. s k t))
                             - (\<Sum>R- p l (\<lambda>k. (Z c p l t) * s k t))"
proof -
  define cs where "cs \<equiv> fst (steps c p t)"

  have add: "(\<Sum>R+ p l (\<lambda>k. s k t))
      = (if isadd (p!cs) \<and> l = modifies (p!cs) then 1 else 0)"
    using single_step_add[of "c" "p" "a" "l" "snd c" "t"] is_val l s_def cs_def by auto

  have sub: "(\<Sum>R- p l (\<lambda>k. Z c p l t * s k t))
         = (if issub (p!cs) \<and> l = modifies (p!cs) then Z c p l t else 0)"
    using single_step_sub is_val l s_def cs_def Z_def R_def by auto

  have lhs: "r l (Suc t) = snd (steps c p (Suc t)) ! l"
    by (simp add: r_def R_def del: steps.simps)

  have rhs: "r l t = snd (steps c p t) ! l"
    by (simp add: r_def R_def del: steps.simps)

  have valid_time: "is_valid (steps c p t) p" using steps_is_valid_invar is_val
    by (auto simp add: is_valid_initial_def)

  have l_time: "l < length (snd (steps c p t))" using l steps_tape_length_invar by auto

  from lhs rhs have "r l (Suc t) = r l t + (if isadd (p!cs) \<and> l = modifies (p!cs) then 1 else 0)
                            - (if issub (p!cs) \<and> l = modifies (p!cs) then Z c p l t else 0)"
    using l_time valid_time lm04_06_one_step_relation_register_old steps.simps cs_def nth_digit_0
    Z_def R_def by auto

  thus ?thesis using add sub by simp
qed

end


text:
theory fmap_functions
  imports Main
    "~~/src/HOL/Library/Finite_Map"
begin

section {* Finite maps *}

text {* To keep out model executable, we use finite maps.
In this theory, we extend the standard library with additional syntax and functions. *}

abbreviation lookupsyntax ("_ .[_]"[25,25]25) where
"m.[x] \<equiv> fmlookup m x"

abbreviation lookupsyntax2 ("_ ![_]"[25,25]25) where
"m![x] \<equiv> the (fmlookup m x)"

definition fmap_entries :: "('k, 'v) fmap \<Rightarrow> ('k\<times>'v) set" where
"fmap_entries m \<equiv> (\<lambda>k. (k, m![k])) ` fmdom' m"

lemma fmap_entries_forall[code_abbrev]: "fmpred P m \<longleftrightarrow> (\<forall>(k,v)\<in>fmap_entries m. P k v)"
  apply (auto simp add: fmap_entries_def)
  apply (meson fmdom'_notI fmpredD option.exhaust_sel)
  by (metis fmdom'I fmpredI option.sel)

lemma fmap_entries_exists[code_abbrev]: "(\<not>fmpred (\<lambda>k v. \<not>P k v) m) \<longleftrightarrow> (\<exists>(k,v)\<in>fmap_entries m. P k v)"
  by (subst fmap_entries_forall, auto)

end

author: peterzeller

repo: ref-crdt


text:
(* ---------------------------------------------------------------------------- *)
subsection \<open>Vectors and Matrices in $\mathbb{C}^2$\<close>
(* ---------------------------------------------------------------------------- *)

text \<open>Representing vectors and matrices of arbitrary dimensions pose a challenge in formal theorem
proving \cite{harrison05}, but we only need to consider finite dimension spaces $\mathbb{C}^2$ and
$\mathbb{R}^3$.\<close>

theory Matrices
imports More_Complex Linear_Systems Quadratic
begin

(* ---------------------------------------------------------------------------- *)
subsubsection \<open>Vectors in $\mathbb{C}^2$\<close>
(* ---------------------------------------------------------------------------- *)

text \<open>Type of complex vector\<close>

type_synonym complex_vec = "complex \<times> complex"

definition vec_zero :: "complex_vec" where
  [simp]: "vec_zero = (0, 0)"

text \<open>Vector scalar multiplication\<close>

fun mult_sv :: "complex \<Rightarrow> complex_vec \<Rightarrow> complex_vec" (infixl "*\<^sub>s\<^sub>v" 100) where
  "k *\<^sub>s\<^sub>v (x, y) = (k*x, k*y)"

lemma fst_mult_sv [simp]:
  shows "fst (k *\<^sub>s\<^sub>v v) = k * fst v"
  by (cases v) simp

lemma snd_mult_sv [simp]:
  shows "snd (k *\<^sub>s\<^sub>v v) = k * snd v"
  by (cases v) simp

lemma mult_sv_mult_sv [simp]:
  shows "k1 *\<^sub>s\<^sub>v (k2 *\<^sub>s\<^sub>v v) = (k1*k2) *\<^sub>s\<^sub>v v"
  by (cases v) simp

lemma one_mult_sv [simp]:
  shows "1 *\<^sub>s\<^sub>v v =  v"
  by (cases v) simp

lemma mult_sv_ex_id1 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> k *\<^sub>s\<^sub>v v = v"
  by (rule_tac x=1 in exI, simp)

lemma mult_sv_ex_id2 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> v = k *\<^sub>s\<^sub>v v"
  by (rule_tac x=1 in exI, simp)

text \<open>Scalar product of two vectors\<close>

fun mult_vv :: "complex \<times> complex \<Rightarrow> complex \<times> complex \<Rightarrow> complex" (infixl "*\<^sub>v\<^sub>v" 100) where
 "(x, y) *\<^sub>v\<^sub>v (a, b) = x*a + y*b"

lemma mult_vv_commute:
  shows "v1 *\<^sub>v\<^sub>v v2 = v2 *\<^sub>v\<^sub>v v1"
  by (cases v1, cases v2) auto

lemma mult_vv_scale_sv1:
  shows "(k *\<^sub>s\<^sub>v v1) *\<^sub>v\<^sub>v v2 = k * (v1 *\<^sub>v\<^sub>v v2)"
  by (cases v1, cases v2) (auto simp add: field_simps)

lemma mult_vv_scale_sv2:
  shows "v1 *\<^sub>v\<^sub>v (k *\<^sub>s\<^sub>v v2) = k * (v1 *\<^sub>v\<^sub>v v2)"
  by (cases v1, cases v2) (auto simp add: field_simps)

text \<open>Conjugate vector\<close>

fun vec_map where
 "vec_map f (x, y) = (f x, f y)"

definition vec_cnj where
  "vec_cnj = vec_map cnj"

lemma vec_cnj_vec_cnj [simp]:
  shows "vec_cnj (vec_cnj v) = v"
  by (cases v) (simp add: vec_cnj_def)

lemma cnj_mult_vv:
  shows "cnj (v1 *\<^sub>v\<^sub>v v2) = (vec_cnj v1) *\<^sub>v\<^sub>v (vec_cnj v2)"
  by (cases v1, cases v2) (simp add: vec_cnj_def)

lemma vec_cnj_sv [simp]:
  shows "vec_cnj (k *\<^sub>s\<^sub>v A) = cnj k *\<^sub>s\<^sub>v vec_cnj A"
  by (cases A) (auto simp add: vec_cnj_def)

lemma scalsquare_vv_zero:
  shows "(vec_cnj v) *\<^sub>v\<^sub>v v = 0 \<longleftrightarrow> v = vec_zero"
  apply (cases v)
  apply (auto simp add: vec_cnj_def field_simps complex_mult_cnj_cmod power2_eq_square)
   apply (simp only: cor_add[symmetric] cor_mult[symmetric] of_real_eq_0_iff, simp)+
  done

(* ---------------------------------------------------------------------------- *)
subsubsection \<open>Matrices in $\mathbb{C}^2$\<close>
(* ---------------------------------------------------------------------------- *)

text \<open>Type of complex matrices\<close>

type_synonym complex_mat = "complex \<times> complex \<times> complex \<times> complex"

text \<open>Matrix scalar multiplication\<close>

fun mult_sm :: "complex \<Rightarrow> complex_mat \<Rightarrow> complex_mat" (infixl "*\<^sub>s\<^sub>m" 100) where
  "k *\<^sub>s\<^sub>m (a, b, c, d) = (k*a, k*b, k*c, k*d)"

lemma mult_sm_distribution [simp]:
  shows "k1 *\<^sub>s\<^sub>m (k2 *\<^sub>s\<^sub>m A) = (k1*k2) *\<^sub>s\<^sub>m A"
  by (cases A) auto

lemma mult_sm_neutral [simp]:
  shows "1 *\<^sub>s\<^sub>m A = A"
  by (cases A) auto

lemma mult_sm_inv_l:
  assumes "k \<noteq> 0" and "k *\<^sub>s\<^sub>m A = B"
  shows "A = (1/k) *\<^sub>s\<^sub>m B"
  using assms
  by auto

lemma mult_sm_ex_id1 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> k *\<^sub>s\<^sub>m M = M"
  by (rule_tac x=1 in exI, simp)

lemma mult_sm_ex_id2 [simp]:
  shows "\<exists> k::complex. k \<noteq> 0 \<and> M = k *\<^sub>s\<^sub>m M"
  by (rule_tac x=1 in exI, simp)

text \<open>Matrix addition and subtraction\<close>

definition mat_zero :: "complex_mat" where [simp]: "mat_zero = (0, 0, 0, 0)"

fun mat_plus :: "complex_mat \<Rightarrow> complex_mat \<Rightarrow> complex_mat" (infixl "+\<^sub>m\<^sub>m" 100) where
  "mat_plus (a1, b1, c1, d1) (a2, b2, c2, d2) = (a1+a2, b1+b2, c1+c2, d1+d2)"

fun mat_minus :: "complex_mat \<Rightarrow> complex_mat \<Rightarrow> complex_mat" (infixl "-\<^sub>m\<^sub>m" 100) where
  "mat_minus (a1, b1, c1, d1) (a2, b2, c2, d2) = (a1-a2, b1-b2, c1-c2, d1-d2)"

fun mat_uminus :: "complex_mat \<Rightarrow> complex_mat" where
  "mat_uminus (a, b, c, d) = (-a, -b, -c, -d)"

lemma nonzero_mult_real:
  assumes "A \<noteq> mat_zero" and "k \<noteq> 0"
  shows "k *\<^sub>s\<^sub>m A \<noteq> mat_zero"
  using assms
  by (cases A) simp

text \<open>Matrix multiplication.\<close>

fun mult_mm :: "complex_mat \<Rightarrow> complex_mat \<Rightarrow> complex_mat" (infixl "*\<^sub>m\<^sub>m" 100) where
  "(a1, b1, c1, d1) *\<^sub>m\<^sub>m (a2, b2, c2, d2) =
   (a1*a2 + b1*c2, a1*b2 + b1*d2, c1*a2+d1*c2, c1*b2+d1*d2)"

lemma mult_mm_assoc:
  shows "A *\<^sub>m\<^sub>m (B *\<^sub>m\<^sub>m C) = (A *\<^sub>m\<^sub>m B) *\<^sub>m\<^sub>m C"
  by (cases A, cases B, cases C) (auto simp add: field_simps)

lemma mult_assoc_5:
  shows "A *\<^sub>m\<^sub>m (B *\<^sub>m\<^sub>m C *\<^sub>m\<^sub>m D) *\<^sub>m\<^sub>m E = (A *\<^sub>m\<^sub>m B) *\<^sub>m\<^sub>m C *\<^sub>m\<^sub>m (D *\<^sub>m\<^sub>m E)"
  by (simp only: mult_mm_assoc)

lemma mat_zero_r [simp]:
  shows "A *\<^sub>m\<^sub>m mat_zero = mat_zero"
  by (cases A) simp

lemma mat_zero_l [simp]:
  shows "mat_zero *\<^sub>m\<^sub>m A = mat_zero"
  by (cases A) simp

definition eye :: "complex_mat" where
  [simp]: "eye = (1, 0, 0, 1)"

lemma mat_eye_l:
  shows "eye *\<^sub>m\<^sub>m A = A"
  by (cases A) auto

lemma mat_eye_r:
  shows "A *\<^sub>m\<^sub>m eye = A"
  by (cases A) auto

lemma mult_mm_sm [simp]:
  shows "A *\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m B) = k *\<^sub>s\<^sub>m (A *\<^sub>m\<^sub>m B)"
  by (cases A, cases B) (simp add: field_simps)

lemma mult_sm_mm [simp]:
  shows "(k *\<^sub>s\<^sub>m A) *\<^sub>m\<^sub>m B = k *\<^sub>s\<^sub>m (A *\<^sub>m\<^sub>m B)"
  by (cases A, cases B) (simp add: field_simps)

lemma mult_sm_eye_mm [simp]:
  shows "k *\<^sub>s\<^sub>m eye *\<^sub>m\<^sub>m A = k *\<^sub>s\<^sub>m A"
  by (cases A) simp

text \<open>Matrix determinant\<close>

fun mat_det where "mat_det (a, b, c, d) = a*d - b*c"

lemma mat_det_mult [simp]:
  shows "mat_det (A *\<^sub>m\<^sub>m B) = mat_det A * mat_det B"
  by (cases A, cases B) (auto simp add: field_simps)

lemma mat_det_mult_sm [simp]:
  shows "mat_det (k *\<^sub>s\<^sub>m A) = (k*k) * mat_det A"
  by (cases A) (auto simp add: field_simps)

text \<open>Matrix inverse\<close>

fun mat_inv :: "complex_mat \<Rightarrow> complex_mat" where
  "mat_inv (a, b, c, d) = (1/(a*d - b*c)) *\<^sub>s\<^sub>m (d, -b, -c, a)"

lemma mat_inv_r:
  assumes "mat_det A \<noteq> 0"
  shows "A *\<^sub>m\<^sub>m (mat_inv A) = eye"
  using assms
proof (cases A, auto simp add: field_simps)
  fix a b c d :: complex
  assume "a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))"
  hence "(a*d - b*c)*(a*d - b*c) = 0"
    by (auto simp add: field_simps)
  hence *: "a*d - b*c = 0"
    by auto
  assume "a*d \<noteq> b*c"
  with * show False
    by auto
qed

lemma mat_inv_l:
  assumes "mat_det A \<noteq> 0"
  shows "(mat_inv A) *\<^sub>m\<^sub>m A  = eye"
  using assms
proof (cases A, auto simp add: field_simps)
  fix a b c d :: complex
  assume "a * (a * (d * d)) + b * (b * (c * c)) = a * (b * (c * (d * 2)))"
  hence "(a*d - b*c)*(a*d - b*c) = 0"
    by (auto simp add: field_simps)
  hence *: "a*d - b*c = 0"
    by auto
  assume "a*d \<noteq> b*c"
  with * show False
    by auto
qed

lemma mat_det_inv:
  assumes "mat_det A \<noteq> 0"
  shows "mat_det (mat_inv A) = 1 / mat_det A"
proof-
  have "mat_det eye = mat_det A * mat_det (mat_inv A)"
    using mat_inv_l[OF assms, symmetric]
    by simp
  thus ?thesis
    using assms
    by (simp add: field_simps)
qed

lemma mult_mm_inv_l:
  assumes "mat_det A \<noteq> 0" and "A *\<^sub>m\<^sub>m B = C"
  shows "B = mat_inv A *\<^sub>m\<^sub>m C"
  using assms mat_eye_l[of B]
  by (auto simp add: mult_mm_assoc mat_inv_l)

lemma mult_mm_inv_r:
  assumes "mat_det B \<noteq> 0" and "A *\<^sub>m\<^sub>m B = C"
  shows "A = C *\<^sub>m\<^sub>m mat_inv B"
  using assms mat_eye_r[of A]
  by (auto simp add: mult_mm_assoc[symmetric] mat_inv_r)

lemma mult_mm_non_zero_l:
  assumes "mat_det A \<noteq> 0" and "B \<noteq> mat_zero"
  shows "A *\<^sub>m\<^sub>m B \<noteq> mat_zero"
  using assms mat_zero_r
  using mult_mm_inv_l[OF assms(1), of B mat_zero]
  by auto

lemma mat_inv_mult_mm:
  assumes "mat_det A \<noteq> 0" and "mat_det B \<noteq> 0"
  shows "mat_inv (A *\<^sub>m\<^sub>m B) = mat_inv B *\<^sub>m\<^sub>m mat_inv A"
  using assms
proof-
  have "(A *\<^sub>m\<^sub>m B) *\<^sub>m\<^sub>m (mat_inv B *\<^sub>m\<^sub>m mat_inv A) = eye"
    using assms
    by (metis mat_inv_r mult_mm_assoc mult_mm_inv_r)
  thus ?thesis
    using mult_mm_inv_l[of "A *\<^sub>m\<^sub>m B" "mat_inv B *\<^sub>m\<^sub>m mat_inv A" eye] assms mat_eye_r
    by simp
qed

lemma mult_mm_cancel_l:
  assumes "mat_det M \<noteq> 0"  "M *\<^sub>m\<^sub>m A = M *\<^sub>m\<^sub>m B"
  shows "A = B"
  using assms
  by (metis mult_mm_inv_l)

lemma mult_mm_cancel_r:
  assumes "mat_det M \<noteq> 0"  "A *\<^sub>m\<^sub>m M = B *\<^sub>m\<^sub>m M"
  shows "A = B"
  using assms
  by (metis mult_mm_inv_r)

lemma mult_mm_non_zero_r:
  assumes "A \<noteq> mat_zero" and "mat_det B \<noteq> 0"
  shows "A *\<^sub>m\<^sub>m B \<noteq> mat_zero"
  using assms mat_zero_l
  using mult_mm_inv_r[OF assms(2), of A mat_zero]
  by auto

lemma mat_inv_mult_sm:
  assumes "k \<noteq> 0"
  shows "mat_inv (k *\<^sub>s\<^sub>m A) = (1 / k) *\<^sub>s\<^sub>m mat_inv A"
proof-
  obtain a b c d where "A = (a, b, c, d)"
    by (cases A) auto
  thus ?thesis
    using assms
    by auto (subst mult.assoc[of k a "k*d"], subst mult.assoc[of k b "k*c"], subst right_diff_distrib[of k "a*(k*d)" "b*(k*c)", symmetric], simp, simp add: field_simps)+
qed

lemma mat_inv_inv [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "mat_inv (mat_inv M) = M"
proof-
  have "mat_inv M *\<^sub>m\<^sub>m M = eye"
    using mat_inv_l[OF assms]
    by simp
  thus ?thesis
    using assms mat_det_inv[of M]
    using mult_mm_inv_l[of "mat_inv M" M eye] mat_eye_r
    by (auto simp del: eye_def)
qed

text \<open>Matrix transpose\<close>

fun mat_transpose where
  "mat_transpose (a, b, c, d) = (a, c, b, d)"

lemma mat_t_mat_t [simp]:
  shows "mat_transpose (mat_transpose A) = A"
  by (cases A) auto

lemma mat_t_mult_sm [simp]:
  shows "mat_transpose (k *\<^sub>s\<^sub>m A) = k *\<^sub>s\<^sub>m (mat_transpose A)"
  by (cases A) simp

lemma mat_t_mult_mm [simp]:
  shows "mat_transpose (A *\<^sub>m\<^sub>m B) = mat_transpose B *\<^sub>m\<^sub>m mat_transpose A"
  by (cases A, cases B) auto

lemma mat_inv_transpose:
  shows "mat_transpose (mat_inv M) = mat_inv (mat_transpose M)"
  by (cases M) auto

lemma mat_det_transpose [simp]:
  fixes M :: "complex_mat"
  shows "mat_det (mat_transpose M) = mat_det M"
  by (cases M) auto

text \<open>Diagonal matrices definition\<close>

fun mat_diagonal where
 "mat_diagonal (A, B, C, D) = (B = 0 \<and> C = 0)"

text \<open>Matrix conjugate\<close>

fun mat_map where
 "mat_map f (a, b, c, d) = (f a, f b, f c, f d)"

definition mat_cnj where
  "mat_cnj = mat_map cnj"

lemma mat_cnj_cnj [simp]:
  shows "mat_cnj (mat_cnj A) = A"
  unfolding mat_cnj_def
  by (cases A) auto

lemma mat_cnj_sm [simp]:
  shows "mat_cnj (k *\<^sub>s\<^sub>m A) = cnj k *\<^sub>s\<^sub>m (mat_cnj A)"
  by (cases A) (simp add: mat_cnj_def)

lemma mat_det_cnj [simp]:
  shows "mat_det (mat_cnj A) = cnj (mat_det A)"
  by (cases A) (simp add: mat_cnj_def)

lemma nonzero_mat_cnj:
  shows "mat_cnj A = mat_zero \<longleftrightarrow> A = mat_zero"
  by (cases A) (auto simp add: mat_cnj_def)

lemma mat_inv_cnj:
  shows "mat_cnj (mat_inv M) = mat_inv (mat_cnj M)"
  unfolding mat_cnj_def
  by (cases M) auto

text \<open>Matrix adjoint - the conjugate traspose matrix ($A^* = \overline{A^t}$)\<close>

definition mat_adj where
  "mat_adj A = mat_cnj (mat_transpose A)"

lemma mat_adj_mult_mm [simp]:
  shows "mat_adj (A *\<^sub>m\<^sub>m B) = mat_adj B *\<^sub>m\<^sub>m mat_adj A"
  by (cases A, cases B) (auto simp add: mat_adj_def mat_cnj_def)

lemma mat_adj_mult_sm [simp]:
  shows "mat_adj (k *\<^sub>s\<^sub>m A) = cnj k *\<^sub>s\<^sub>m mat_adj A"
  by (cases A) (auto simp add: mat_adj_def mat_cnj_def)

lemma mat_det_adj:
  shows "mat_det (mat_adj A) = cnj (mat_det A)"
  by (cases A) (auto simp add: mat_adj_def mat_cnj_def)

lemma mat_transpose_mat_cnj:
  shows "mat_transpose (mat_cnj A) = mat_adj A"
  by (cases A)  (auto simp add: mat_adj_def mat_cnj_def)

lemma mat_adj_adj [simp]:
  shows "mat_adj (mat_adj A) = A"
  unfolding mat_adj_def
  by (subst mat_transpose_mat_cnj) (simp add: mat_adj_def)

lemma mat_adj_eye [simp]:
  shows "mat_adj eye = eye"
  by (auto simp add: mat_adj_def mat_cnj_def)

text \<open>Matrix trace\<close>

fun mat_trace where
  "mat_trace (a, b, c, d) = a + d"

text \<open>Multiplication of matrix and a vector\<close>

fun mult_mv :: "complex_mat \<Rightarrow> complex_vec \<Rightarrow> complex_vec" (infixl "*\<^sub>m\<^sub>v" 100)  where
  "(a, b, c, d) *\<^sub>m\<^sub>v (x, y) = (x*a + y*b, x*c + y*d)"

fun mult_vm :: "complex_vec \<Rightarrow> complex_mat \<Rightarrow> complex_vec" (infixl "*\<^sub>v\<^sub>m" 100) where
  "(x, y) *\<^sub>v\<^sub>m (a, b, c, d)  = (x*a + y*c, x*b + y*d)"

lemma eye_mv_l [simp]:
  shows "eye *\<^sub>m\<^sub>v v = v"
  by (cases v) simp

lemma mult_mv_mv [simp]:
  shows "B *\<^sub>m\<^sub>v (A *\<^sub>m\<^sub>v v) = (B *\<^sub>m\<^sub>m A) *\<^sub>m\<^sub>v v"
  by (cases v, cases A, cases B) (auto simp add: field_simps)

lemma mult_vm_vm [simp]:
  shows "(v *\<^sub>v\<^sub>m A) *\<^sub>v\<^sub>m B = v *\<^sub>v\<^sub>m (A *\<^sub>m\<^sub>m B)"
  by (cases v, cases A, cases B) (auto simp add: field_simps)

lemma mult_mv_inv:
  assumes "x =  A *\<^sub>m\<^sub>v y" and "mat_det A \<noteq> 0"
  shows "y = (mat_inv A) *\<^sub>m\<^sub>v x"
  using assms
  by (cases y) (simp add: mat_inv_l)

lemma mult_vm_inv:
  assumes "x =  y *\<^sub>v\<^sub>m A" and "mat_det A \<noteq> 0"
  shows "y = x *\<^sub>v\<^sub>m (mat_inv A) "
  using assms
  by (cases y) (simp add: mat_inv_r)

lemma mult_mv_cancel_l:
  assumes "mat_det A \<noteq> 0" and "A *\<^sub>m\<^sub>v v = A *\<^sub>m\<^sub>v v'"
  shows "v = v'"
  using assms
  using mult_mv_inv
  by blast

lemma mult_vm_cancel_r:
  assumes "mat_det A \<noteq> 0" and "v *\<^sub>v\<^sub>m A = v' *\<^sub>v\<^sub>m A"
  shows "v = v'"
  using assms
  using mult_vm_inv
  by blast

lemma vec_zero_l [simp]:
  shows "A *\<^sub>m\<^sub>v vec_zero = vec_zero"
  by (cases A) simp

lemma vec_zero_r [simp]:
  shows "vec_zero *\<^sub>v\<^sub>m A = vec_zero"
  by (cases A) simp

lemma mult_mv_nonzero:
  assumes "v \<noteq> vec_zero" and "mat_det A \<noteq> 0"
  shows "A *\<^sub>m\<^sub>v v \<noteq> vec_zero"
  apply (rule ccontr)
  using assms mult_mv_inv[of vec_zero A v] mat_inv_l vec_zero_l
  by auto

lemma mult_vm_nonzero:
  assumes "v \<noteq> vec_zero" and "mat_det A \<noteq> 0"
  shows "v *\<^sub>v\<^sub>m A \<noteq> vec_zero"
  apply (rule ccontr)
  using assms mult_vm_inv[of vec_zero v A] mat_inv_r vec_zero_r
  by auto

lemma mult_sv_mv:
  shows "k *\<^sub>s\<^sub>v (A *\<^sub>m\<^sub>v v) = (A *\<^sub>m\<^sub>v (k *\<^sub>s\<^sub>v v))"
  by (cases A, cases v) (simp add: field_simps)

lemma mult_mv_mult_vm:
  shows "A *\<^sub>m\<^sub>v x = x *\<^sub>v\<^sub>m (mat_transpose A)"
  by (cases A, cases x) auto

lemma mult_mv_vv:
  shows "A *\<^sub>m\<^sub>v v1 *\<^sub>v\<^sub>v v2 = v1 *\<^sub>v\<^sub>v (mat_transpose A *\<^sub>m\<^sub>v v2)"
  by (cases v1, cases v2, cases A) (auto simp add: field_simps)

lemma mult_vv_mv:
  shows "x *\<^sub>v\<^sub>v (A *\<^sub>m\<^sub>v y)  = (x *\<^sub>v\<^sub>m A) *\<^sub>v\<^sub>v y"
  by (cases x, cases y, cases A) (auto simp add: field_simps)

lemma vec_cnj_mult_mv:
  shows "vec_cnj (A *\<^sub>m\<^sub>v x) =  (mat_cnj A) *\<^sub>m\<^sub>v (vec_cnj x)"
  by (cases A, cases x) (auto simp add: vec_cnj_def mat_cnj_def)

lemma vec_cnj_mult_vm:
  shows "vec_cnj (v *\<^sub>v\<^sub>m A) = vec_cnj v *\<^sub>v\<^sub>m mat_cnj A"
  unfolding vec_cnj_def mat_cnj_def
  by (cases A, cases v, auto)

(* ---------------------------------------------------------------------------- *)
subsubsection \<open>Eigenvalues and eigenvectors\<close>
(* ---------------------------------------------------------------------------- *)

definition eigenpair where
  [simp]: "eigenpair k v H \<longleftrightarrow> v \<noteq> vec_zero \<and> H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v"

definition eigenval where
  [simp]: "eigenval k H \<longleftrightarrow> (\<exists> v. v \<noteq> vec_zero \<and> H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v)"

lemma eigen_equation:
  shows "eigenval k H \<longleftrightarrow> k\<^sup>2 - mat_trace H * k + mat_det H = 0" (is "?lhs \<longleftrightarrow> ?rhs")
proof-
  obtain A B C D where HH: "H = (A, B, C, D)"
    by (cases H) auto
  show ?thesis
  proof
    assume ?lhs
    then obtain v where "v \<noteq> vec_zero" "H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v"
      unfolding eigenval_def
      by blast
    obtain v1 v2 where vv: "v = (v1, v2)"
      by (cases v) auto
    from \<open>H *\<^sub>m\<^sub>v v = k *\<^sub>s\<^sub>v v\<close> have "(H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v v = vec_zero"
      using HH vv
      by (auto simp add: field_simps)
    hence "mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0"
      using \<open>v \<noteq> vec_zero\<close> vv HH
      using regular_homogenous_system[of "A - k" B C "D - k" v1 v2]
      unfolding det2_def
      by (auto simp add: field_simps)
    thus ?rhs
      using HH
      by (auto simp add: power2_eq_square field_simps)
  next
    assume ?rhs
    hence *: "mat_det (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) = 0"
      using HH
      by (auto simp add: field_simps power2_eq_square)
    show ?lhs
    proof (cases "H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye) = mat_zero")
      case True
      thus ?thesis
        using HH
        by (auto) (rule_tac x=1 in exI, simp)
    next
      case False
      hence "(A - k \<noteq> 0 \<or> B \<noteq> 0) \<or> (D - k \<noteq> 0 \<or> C \<noteq> 0)"
        using HH
        by auto
      thus ?thesis
      proof
        assume "A - k \<noteq> 0 \<or> B \<noteq> 0"
        hence "C * B + (D - k) * (k - A) = 0"
          using * singular_system[of "A-k" "D-k" B C "(0, 0)" 0 0  "(B, k-A)"] HH
          by (auto simp add: field_simps)
        hence  "(B, k-A) \<noteq> vec_zero" "(H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v (B, k-A) = vec_zero"
          using HH \<open>A - k \<noteq> 0 \<or> B \<noteq> 0\<close>
          by (auto simp add: field_simps)
        then obtain v where "v \<noteq> vec_zero \<and> (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v v = vec_zero"
          by blast
        thus ?thesis
          using HH
          unfolding eigenval_def
          by (rule_tac x="v" in exI) (case_tac v, simp add: field_simps)
      next
        assume "D - k \<noteq> 0 \<or> C \<noteq> 0"
        hence "C * B + (D - k) * (k - A) = 0"
          using * singular_system[of "D-k" "A-k" C B "(0, 0)" 0 0  "(C, k-D)"] HH
          by (auto simp add: field_simps)
        hence  "(k-D, C) \<noteq> vec_zero" "(H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v (k-D, C) = vec_zero"
          using HH \<open>D - k \<noteq> 0 \<or> C \<noteq> 0\<close>
          by (auto simp add: field_simps)
        then obtain v where "v \<noteq> vec_zero \<and> (H -\<^sub>m\<^sub>m (k *\<^sub>s\<^sub>m eye)) *\<^sub>m\<^sub>v v = vec_zero"
          by blast
        thus ?thesis
          using HH
          unfolding eigenval_def
          by (rule_tac x="v" in exI) (case_tac v, simp add: field_simps)
      qed
    qed
  qed
qed

(* ---------------------------------------------------------------------------- *)
subsubsection \<open>Bilinear and Quadratic forms, Congruence, and Similarity\<close>
(* ---------------------------------------------------------------------------- *)

text \<open>Bilinear forms\<close>

definition bilinear_form where
  [simp]: "bilinear_form v1 v2 H = (vec_cnj v1) *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v2"

lemma bilinear_form_scale_m:
  shows "bilinear_form v1 v2 (k *\<^sub>s\<^sub>m H) = k * bilinear_form v1 v2 H"
  by (cases v1, cases v2, cases H) (simp add: vec_cnj_def field_simps)

lemma bilinear_form_scale_v1:
  shows "bilinear_form (k *\<^sub>s\<^sub>v v1) v2 H = cnj k * bilinear_form v1 v2 H"
  by (cases v1, cases v2, cases H) (simp add: vec_cnj_def field_simps)

lemma bilinear_form_scale_v2:
  shows "bilinear_form  v1 (k *\<^sub>s\<^sub>v v2) H = k * bilinear_form v1 v2 H"
  by (cases v1, cases v2, cases H) (simp add: vec_cnj_def field_simps)

text \<open>Quadratic forms\<close>

definition quad_form where
  [simp]: "quad_form v H = (vec_cnj v) *\<^sub>v\<^sub>m H *\<^sub>v\<^sub>v v"

lemma quad_form_bilinear_form:
  shows "quad_form v H = bilinear_form v v H"
  by simp

lemma quad_form_scale_v:
  shows "quad_form (k *\<^sub>s\<^sub>v v) H = cor ((cmod k)\<^sup>2) * quad_form v H"
  using bilinear_form_scale_v1 bilinear_form_scale_v2
  by (simp add: complex_mult_cnj_cmod field_simps)

lemma quad_form_scale_m:
  shows "quad_form v (k *\<^sub>s\<^sub>m H) = k * quad_form v H"
  using bilinear_form_scale_m
  by simp

lemma cnj_quad_form [simp]:
  shows "cnj (quad_form z H) = quad_form z (mat_adj H)"
  by (cases H, cases z) (auto simp add: mat_adj_def mat_cnj_def vec_cnj_def field_simps)

text \<open>Matrix congruence\<close>

text \<open>Two matrices are congruent iff they represent the same quadratic form with respect to different
bases (for example if one circline can be transformed to another by a Möbius trasformation).\<close>

definition congruence where
  [simp]: "congruence M H \<equiv> mat_adj M *\<^sub>m\<^sub>m H *\<^sub>m\<^sub>m M"

lemma congruence_nonzero:
  assumes "H \<noteq> mat_zero" and "mat_det M \<noteq> 0"
  shows "congruence M H \<noteq> mat_zero"
  using assms
  unfolding congruence_def
  by (subst mult_mm_non_zero_r, subst mult_mm_non_zero_l) (auto simp add: mat_det_adj)

lemma congruence_congruence:
  shows "congruence M1 (congruence M2 H) = congruence (M2 *\<^sub>m\<^sub>m M1) H"
  unfolding congruence_def
  apply (subst mult_mm_assoc)
  apply (subst mult_mm_assoc)
  apply (subst mat_adj_mult_mm)
  apply (subst mult_mm_assoc)
  by simp

lemma congruence_eye [simp]:
  shows "congruence eye H = H"
  by (cases H) (simp add: mat_adj_def mat_cnj_def)

lemma congruence_congruence_inv [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "congruence M (congruence (mat_inv M) H) = H"
  using assms congruence_congruence[of M "mat_inv M" H]
  using mat_inv_l[of M] mat_eye_l mat_eye_r
  unfolding congruence_def
  by (simp del: eye_def)

lemma congruence_inv:
  assumes "mat_det M \<noteq> 0" and "congruence M H = H'"
  shows "congruence (mat_inv M) H' = H"
  using assms
  using \<open>mat_det M \<noteq> 0\<close> mult_mm_inv_l[of "mat_adj M" "H *\<^sub>m\<^sub>m M" "H'"]
  using mult_mm_inv_r[of M "H" "mat_inv (mat_adj M) *\<^sub>m\<^sub>m H'"]
  by (simp add: mat_det_adj mult_mm_assoc mat_adj_inv)

lemma congruence_scale_m [simp]:
  shows "congruence M (k *\<^sub>s\<^sub>m H) = k *\<^sub>s\<^sub>m (congruence M H)"
  by (cases M, cases H) (auto simp add: mat_adj_def mat_cnj_def field_simps)

lemma inj_congruence:
  assumes "mat_det M \<noteq> 0" and "congruence M H = congruence M H'"
  shows "H = H'"
proof-
  have "H *\<^sub>m\<^sub>m M = H' *\<^sub>m\<^sub>m M "
    using assms
    using mult_mm_cancel_l[of "mat_adj M" "H *\<^sub>m\<^sub>m M" "H' *\<^sub>m\<^sub>m M"]
    by (simp add: mat_det_adj mult_mm_assoc)
  thus ?thesis
    using assms
    using mult_mm_cancel_r[of "M" "H" "H'"]
    by simp
qed

lemma mat_det_congruence [simp]:
  "mat_det (congruence M H) = (cor ((cmod (mat_det M))\<^sup>2)) * mat_det H"
  using complex_mult_cnj_cmod[of "mat_det M"]
  by (auto simp add: mat_det_adj field_simps)

lemma det_sgn_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "sgn (mat_det (congruence M H)) = sgn (mat_det H)"
  using assms
  by (subst mat_det_congruence, auto simp add: sgn_mult power2_eq_square) (simp add: sgn_of_real)

lemma Re_det_sgn_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "sgn (Re (mat_det (congruence M H))) = sgn (Re (mat_det H))"
proof-
  have *: "Re (mat_det (congruence M H)) = (cmod (mat_det M))\<^sup>2 * Re (mat_det H)"
    by (subst mat_det_congruence, subst Re_mult_real, rule Im_complex_of_real) (subst Re_complex_of_real, simp)
  show ?thesis
    using assms
    by (subst *) (auto simp add: sgn_mult)
qed

text \<open>Transforming a matrix $H$ by a regular matrix $M$ preserves its bilinear and quadratic forms.\<close>

lemma bilinear_form_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "bilinear_form (M *\<^sub>m\<^sub>v v1) (M *\<^sub>m\<^sub>v v2) (congruence (mat_inv M) H) =
         bilinear_form v1 v2 H"
proof-
  have "mat_det (mat_adj M) \<noteq> 0"
    using assms
    by (simp add: mat_det_adj)
  show ?thesis
    unfolding bilinear_form_def congruence_def
    apply (subst mult_mv_mult_vm)
    apply (subst vec_cnj_mult_vm)
    apply (subst mat_adj_def[symmetric])
    apply (subst mult_vm_vm)
    apply (subst mult_vv_mv)
    apply (subst mult_vm_vm)
    apply (subst mat_adj_inv[OF \<open>mat_det M \<noteq> 0\<close>])
    apply (subst mult_assoc_5)
    apply (subst mat_inv_r[OF \<open>mat_det (mat_adj M) \<noteq> 0\<close>])
    apply (subst mat_inv_l[OF \<open>mat_det M \<noteq> 0\<close>])
    apply (subst mat_eye_l, subst mat_eye_r)
    by simp
qed

lemma quad_form_congruence [simp]:
  assumes "mat_det M \<noteq> 0"
  shows "quad_form (M *\<^sub>m\<^sub>v z) (congruence (mat_inv M) H) = quad_form z H"
  using bilinear_form_congruence[OF assms]
  by simp

text \<open>Similar matrices\<close>

text \<open>Two matrices are similar iff they represent the same linear operator with respect to (possibly)
different bases (e.g., if they represent the same Möbius transformation after changing the
coordinate system)\<close>

definition similarity where
  "similarity A M = mat_inv A *\<^sub>m\<^sub>m M *\<^sub>m\<^sub>m A"

lemma mat_det_similarity [simp]:
  assumes "mat_det A \<noteq> 0"
  shows "mat_det (similarity A M) = mat_det M"
  using assms
  unfolding similarity_def
  by (simp add: mat_det_inv)

lemma mat_trace_similarity [simp]:
  assumes "mat_det A \<noteq> 0"
  shows "mat_trace (similarity A M) = mat_trace M"
proof-
  obtain a b c d where AA: "A = (a, b, c, d)"
    by (cases A) auto
  obtain mA mB mC mD where MM: "M = (mA, mB, mC, mD)"
    by (cases M) auto
  have "mA * (a * d) / (a * d - b * c) + mD * (a * d) / (a * d - b * c) =
        mA + mD + mA * (b * c) / (a * d - b * c) + mD * (b * c) / (a * d - b * c)"
    using assms AA
    by (simp add: field_simps)
  thus ?thesis
    using AA MM
    by (simp add: field_simps similarity_def)
qed

lemma similarity_eye [simp]:
  shows "similarity eye M = M"
  unfolding similarity_def
  using mat_eye_l mat_eye_r
  by auto

lemma similarity_eye' [simp]:
  shows "similarity (1, 0, 0, 1) M = M"
  unfolding eye_def[symmetric]
  by (simp del: eye_def)

lemma similarity_comp [simp]:
  assumes "mat_det A1 \<noteq> 0" and "mat_det A2 \<noteq> 0"
  shows "similarity A1 (similarity A2 M) = similarity (A2*\<^sub>m\<^sub>mA1) M"
  using assms
  unfolding similarity_def
  by (simp add: mult_mm_assoc mat_inv_mult_mm)

lemma similarity_inv:
  assumes "similarity A M1 = M2" and "mat_det A \<noteq> 0"
  shows "similarity (mat_inv A) M2 = M1"
  using assms
  unfolding similarity_def
  by (metis mat_det_mult mult_mm_assoc mult_mm_inv_l mult_mm_inv_r mult_zero_left)

end

repo: PSL


text:
(*  Title:      HOL/TLA/Intensional.thy
    Author:     Stephan Merz
    Copyright:  1998 University of Munich
*)

section {* A framework for "intensional" (possible-world based) logics
  on top of HOL, with lifting of constants and functions *}

theory Intensional
imports Main
begin

class world

(** abstract syntax **)

type_synonym ('w,'a) expr = "'w => 'a"   (* intention: 'w::world, 'a::type *)
type_synonym 'w form = "('w, bool) expr"

consts
  Valid    :: "('w::world) form => bool"
  const    :: "'a => ('w::world, 'a) expr"
  lift     :: "['a => 'b, ('w::world, 'a) expr] => ('w,'b) expr"
  lift2    :: "['a => 'b => 'c, ('w::world,'a) expr, ('w,'b) expr] => ('w,'c) expr"
  lift3    :: "['a => 'b => 'c => 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] => ('w,'d) expr"

  (* "Rigid" quantification (logic level) *)
  RAll     :: "('a => ('w::world) form) => 'w form"       (binder "Rall " 10)
  REx      :: "('a => ('w::world) form) => 'w form"       (binder "Rex " 10)
  REx1     :: "('a => ('w::world) form) => 'w form"       (binder "Rex! " 10)

(** concrete syntax **)

nonterminal lift and liftargs

syntax
  ""            :: "id => lift"                          ("_")
  ""            :: "longid => lift"                      ("_")
  ""            :: "var => lift"                         ("_")
  "_applC"      :: "[lift, cargs] => lift"               ("(1_/ _)" [1000, 1000] 999)
  ""            :: "lift => lift"                        ("'(_')")
  "_lambda"     :: "[idts, 'a] => lift"                  ("(3%_./ _)" [0, 3] 3)
  "_constrain"  :: "[lift, type] => lift"                ("(_::_)" [4, 0] 3)
  ""            :: "lift => liftargs"                    ("_")
  "_liftargs"   :: "[lift, liftargs] => liftargs"        ("_,/ _")
  "_Valid"      :: "lift => bool"                        ("(|- _)" 5)
  "_holdsAt"    :: "['a, lift] => bool"                  ("(_ |= _)" [100,10] 10)

  (* Syntax for lifted expressions outside the scope of |- or |= *)
  "_LIFT"       :: "lift => 'a"                          ("LIFT _")

  (* generic syntax for lifted constants and functions *)
  "_const"      :: "'a => lift"                          ("(#_)" [1000] 999)
  "_lift"       :: "['a, lift] => lift"                  ("(_<_>)" [1000] 999)
  "_lift2"      :: "['a, lift, lift] => lift"            ("(_<_,/ _>)" [1000] 999)
  "_lift3"      :: "['a, lift, lift, lift] => lift"      ("(_<_,/ _,/ _>)" [1000] 999)

  (* concrete syntax for common infix functions: reuse same symbol *)
  "_liftEqu"    :: "[lift, lift] => lift"                ("(_ =/ _)" [50,51] 50)
  "_liftNeq"    :: "[lift, lift] => lift"                ("(_ ~=/ _)" [50,51] 50)
  "_liftNot"    :: "lift => lift"                        ("(~ _)" [40] 40)
  "_liftAnd"    :: "[lift, lift] => lift"                ("(_ &/ _)" [36,35] 35)
  "_liftOr"     :: "[lift, lift] => lift"                ("(_ |/ _)" [31,30] 30)
  "_liftImp"    :: "[lift, lift] => lift"                ("(_ -->/ _)" [26,25] 25)
  "_liftIf"     :: "[lift, lift, lift] => lift"          ("(if (_)/ then (_)/ else (_))" 10)
  "_liftPlus"   :: "[lift, lift] => lift"                ("(_ +/ _)" [66,65] 65)
  "_liftMinus"  :: "[lift, lift] => lift"                ("(_ -/ _)" [66,65] 65)
  "_liftTimes"  :: "[lift, lift] => lift"                ("(_ */ _)" [71,70] 70)
  "_liftDiv"    :: "[lift, lift] => lift"                ("(_ div _)" [71,70] 70)
  "_liftMod"    :: "[lift, lift] => lift"                ("(_ mod _)" [71,70] 70)
  "_liftLess"   :: "[lift, lift] => lift"                ("(_/ < _)"  [50, 51] 50)
  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ <= _)" [50, 51] 50)
  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ : _)" [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ ~: _)" [50, 51] 50)
  "_liftFinset" :: "liftargs => lift"                    ("{(_)}")
  (** TODO: syntax for lifted collection / comprehension **)
  "_liftPair"   :: "[lift,liftargs] => lift"                   ("(1'(_,/ _'))")
  (* infix syntax for list operations *)
  "_liftCons" :: "[lift, lift] => lift"                  ("(_ #/ _)" [65,66] 65)
  "_liftApp"  :: "[lift, lift] => lift"                  ("(_ @/ _)" [65,66] 65)
  "_liftList" :: "liftargs => lift"                      ("[(_)]")

  (* Rigid quantification (syntax level) *)
  "_ARAll"  :: "[idts, lift] => lift"                    ("(3! _./ _)" [0, 10] 10)
  "_AREx"   :: "[idts, lift] => lift"                    ("(3? _./ _)" [0, 10] 10)
  "_AREx1"  :: "[idts, lift] => lift"                    ("(3?! _./ _)" [0, 10] 10)
  "_RAll" :: "[idts, lift] => lift"                      ("(3ALL _./ _)" [0, 10] 10)
  "_REx"  :: "[idts, lift] => lift"                      ("(3EX _./ _)" [0, 10] 10)
  "_REx1" :: "[idts, lift] => lift"                      ("(3EX! _./ _)" [0, 10] 10)

translations
  "_const"        == "CONST const"
  "_lift"         == "CONST lift"
  "_lift2"        == "CONST lift2"
  "_lift3"        == "CONST lift3"
  "_Valid"        == "CONST Valid"
  "_RAll x A"     == "Rall x. A"
  "_REx x  A"     == "Rex x. A"
  "_REx1 x  A"    == "Rex! x. A"
  "_ARAll"        => "_RAll"
  "_AREx"         => "_REx"
  "_AREx1"        => "_REx1"

  "w |= A"        => "A w"
  "LIFT A"        => "A::_=>_"

  "_liftEqu"      == "_lift2 (op =)"
  "_liftNeq u v"  == "_liftNot (_liftEqu u v)"
  "_liftNot"      == "_lift (CONST Not)"
  "_liftAnd"      == "_lift2 (op &)"
  "_liftOr"       == "_lift2 (op | )"
  "_liftImp"      == "_lift2 (op -->)"
  "_liftIf"       == "_lift3 (CONST If)"
  "_liftPlus"     == "_lift2 (op +)"
  "_liftMinus"    == "_lift2 (op -)"
  "_liftTimes"    == "_lift2 (op *)"
  "_liftDiv"      == "_lift2 (op div)"
  "_liftMod"      == "_lift2 (op mod)"
  "_liftLess"     == "_lift2 (op <)"
  "_liftLeq"      == "_lift2 (op <=)"
  "_liftMem"      == "_lift2 (op :)"
  "_liftNotMem x xs"   == "_liftNot (_liftMem x xs)"
  "_liftFinset (_liftargs x xs)"  == "_lift2 (CONST insert) x (_liftFinset xs)"
  "_liftFinset x" == "_lift2 (CONST insert) x (_const {})"
  "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
  "_liftPair"     == "_lift2 (CONST Pair)"
  "_liftCons"     == "CONST lift2 (CONST Cons)"
  "_liftApp"      == "CONST lift2 (op @)"
  "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
  "_liftList x"   == "_liftCons x (_const [])"

  "w |= ~A"       <= "_liftNot A w"
  "w |= A & B"    <= "_liftAnd A B w"
  "w |= A | B"    <= "_liftOr A B w"
  "w |= A --> B"  <= "_liftImp A B w"
  "w |= u = v"    <= "_liftEqu u v w"
  "w |= ALL x. A"   <= "_RAll x A w"
  "w |= EX x. A"   <= "_REx x A w"
  "w |= EX! x. A"  <= "_REx1 x A w"

syntax (xsymbols)
  "_Valid"      :: "lift => bool"                        ("(\<turnstile> _)" 5)
  "_holdsAt"    :: "['a, lift] => bool"                  ("(_ \<Turnstile> _)" [100,10] 10)
  "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
  "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
  "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
  "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
  "_liftImp"    :: "[lift, lift] => lift"                (infixr "\<longrightarrow>" 25)
  "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
  "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
  "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)

syntax (HTML output)
  "_liftNeq"    :: "[lift, lift] => lift"                (infixl "\<noteq>" 50)
  "_liftNot"    :: "lift => lift"                        ("\<not> _" [40] 40)
  "_liftAnd"    :: "[lift, lift] => lift"                (infixr "\<and>" 35)
  "_liftOr"     :: "[lift, lift] => lift"                (infixr "\<or>" 30)
  "_RAll"       :: "[idts, lift] => lift"                ("(3\<forall>_./ _)" [0, 10] 10)
  "_REx"        :: "[idts, lift] => lift"                ("(3\<exists>_./ _)" [0, 10] 10)
  "_REx1"       :: "[idts, lift] => lift"                ("(3\<exists>!_./ _)" [0, 10] 10)
  "_liftLeq"    :: "[lift, lift] => lift"                ("(_/ \<le> _)" [50, 51] 50)
  "_liftMem"    :: "[lift, lift] => lift"                ("(_/ \<in> _)" [50, 51] 50)
  "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [50, 51] 50)

defs
  Valid_def:   "|- A    ==  ALL w. w |= A"

  unl_con:     "LIFT #c w  ==  c"
  unl_lift:    "lift f x w == f (x w)"
  unl_lift2:   "LIFT f<x, y> w == f (x w) (y w)"
  unl_lift3:   "LIFT f<x, y, z> w == f (x w) (y w) (z w)"

  unl_Rall:    "w |= ALL x. A x  ==  ALL x. (w |= A x)"
  unl_Rex:     "w |= EX x. A x   ==  EX x. (w |= A x)"
  unl_Rex1:    "w |= EX! x. A x  ==  EX! x. (w |= A x)"

subsection {* Lemmas and tactics for "intensional" logics. *}

lemmas intensional_rews [simp] =
  unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1

lemma inteq_reflection: "|- x=y  ==>  (x==y)"
  apply (unfold Valid_def unl_lift2)
  apply (rule eq_reflection)
  apply (rule ext)
  apply (erule spec)
  done

lemma intI [intro!]: "(!!w. w |= A) ==> |- A"
  apply (unfold Valid_def)
  apply (rule allI)
  apply (erule meta_spec)
  done

lemma intD [dest]: "|- A ==> w |= A"
  apply (unfold Valid_def)
  apply (erule spec)
  done

(** Lift usual HOL simplifications to "intensional" level. **)

lemma int_simps:
  "|- (x=x) = #True"
  "|- (~#True) = #False"  "|- (~#False) = #True"  "|- (~~ P) = P"
  "|- ((~P) = P) = #False"  "|- (P = (~P)) = #False"
  "|- (P ~= Q) = (P = (~Q))"
  "|- (#True=P) = P"  "|- (P=#True) = P"
  "|- (#True --> P) = P"  "|- (#False --> P) = #True"
  "|- (P --> #True) = #True"  "|- (P --> P) = #True"
  "|- (P --> #False) = (~P)"  "|- (P --> ~P) = (~P)"
  "|- (P & #True) = P"  "|- (#True & P) = P"
  "|- (P & #False) = #False"  "|- (#False & P) = #False"
  "|- (P & P) = P"  "|- (P & ~P) = #False"  "|- (~P & P) = #False"
  "|- (P | #True) = #True"  "|- (#True | P) = #True"
  "|- (P | #False) = P"  "|- (#False | P) = P"
  "|- (P | P) = P"  "|- (P | ~P) = #True"  "|- (~P | P) = #True"
  "|- (! x. P) = P"  "|- (? x. P) = P"
  "|- (~Q --> ~P) = (P --> Q)"
  "|- (P|Q --> R) = ((P-->R)&(Q-->R))"
  apply (unfold Valid_def intensional_rews)
  apply blast+
  done

declare int_simps [THEN inteq_reflection, simp]

lemma TrueW [simp]: "|- #True"
  by (simp add: Valid_def unl_con)

(* ======== Functions to "unlift" intensional implications into HOL rules ====== *)

ML {*
(* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
   |- F = G    becomes   F w = G w
   |- F --> G  becomes   F w --> G w
*)

fun int_unlift ctxt th =
  rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm intD} handle THM _ => th);

(* Turn  |- F = G  into meta-level rewrite rule  F == G *)
fun int_rewrite ctxt th =
  zero_var_indexes (rewrite_rule ctxt @{thms intensional_rews} (th RS @{thm inteq_reflection}))

(* flattening turns "-->" into "==>" and eliminates conjunctions in the
   antecedent. For example,

         P & Q --> (R | S --> T)    becomes   [| P; Q; R | S |] ==> T

   Flattening can be useful with "intensional" lemmas (after unlifting).
   Naive resolution with mp and conjI may run away because of higher-order
   unification, therefore the code is a little awkward.
*)
fun flatten t =
  let
    (* analogous to RS, but using matching instead of resolution *)
    fun matchres tha i thb =
      case Seq.chop 2 (Thm.biresolution NONE true [(false,tha)] i thb) of
          ([th],_) => th
        | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
        |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])

    (* match tha with some premise of thb *)
    fun matchsome tha thb =
      let fun hmatch 0 = raise THM("matchsome: no match", 0, [tha,thb])
            | hmatch n = matchres tha n thb handle THM _ => hmatch (n-1)
      in hmatch (nprems_of thb) end

    fun hflatten t =
        case (concl_of t) of
          Const _ $ (Const (@{const_name HOL.implies}, _) $ _ $ _) => hflatten (t RS mp)
        | _ => (hflatten (matchsome conjI t)) handle THM _ => zero_var_indexes t
  in
    hflatten t
  end

fun int_use ctxt th =
    case (concl_of th) of
      Const _ $ (Const (@{const_name Valid}, _) $ _) =>
              (flatten (int_unlift ctxt th) handle THM _ => th)
    | _ => th
*}

attribute_setup int_unlift =
  {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
attribute_setup int_rewrite =
  {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
attribute_setup int_use =
  {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}

lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
  by (simp add: Valid_def)

lemma Not_Rex: "|- (~ (? x. F x)) = (! x. ~ F x)"
  by (simp add: Valid_def)

end

author: Josh-Tilles

repo: isabelle


text:
(* Title: Linear_Bound_Argument.thy
   Author: Chelsea Edmonds
*)
section \<open>Linear Bound Argument - General \<close>
text \<open>Lemmas to enable general reasoning using the linear bound argument for combinatorial proofs.
Jukna \cite{juknaExtremalCombinatorics2011} presents a good overview of the mathematical background
this theory is based on and applications \<close>
theory Linear_Bound_Argument imports Incidence_Matrices Jordan_Normal_Form.DL_Rank
Jordan_Normal_Form.Ring_Hom_Matrix
begin

subsection \<open>Vec Space Extensions\<close>
text \<open>Simple extensions to the existing vector space locale on linear independence \<close>
context vec_space
begin
lemma lin_indpt_set_card_lt_dim:
  fixes A :: "'a vec set"
  assumes "A \<subseteq> carrier_vec n"
  assumes "lin_indpt A"
  shows "card A \<le> dim"
  using assms(1) assms(2) fin_dim li_le_dim(2) by blast

lemma lin_indpt_dim_col_lt_dim:
  fixes A :: "'a mat"
  assumes "A \<in> carrier_mat n nc"
  assumes "distinct (cols A)"
  assumes "lin_indpt (set (cols A))"
  shows "nc \<le> dim"
proof -
  have b: "card (set (cols A)) = dim_col A" using cols_length assms(2)
    by (simp add: distinct_card)
  have "set (cols A) \<subseteq> carrier_vec n" using assms(1) cols_dim by blast
  thus ?thesis using lin_indpt_set_card_lt_dim assms b by auto
qed

lemma lin_comb_imp_lin_dep_fin:
  fixes A :: "'a vec set"
  assumes "finite A"
  assumes "A \<subseteq> carrier_vec n"
  assumes "lincomb c A = 0\<^sub>v n"
  assumes "\<exists> a. a \<in> A \<and> c a \<noteq> 0"
  shows "lin_dep A"
  unfolding lin_dep_def using assms lincomb_as_lincomb_list_distinct sumlist_nth by auto

text \<open>While a trivial definition, this enables us to directly reference the definition outside
of a locale context, as @{term "lin_indpt"} is an inherited definition \<close>
definition lin_indpt_vs:: "'a vec set \<Rightarrow> bool" where
"lin_indpt_vs A \<longleftrightarrow> lin_indpt A"

lemma lin_comb_sum_lin_indpt:
  fixes A :: "'a vec list"
  assumes "set (A) \<subseteq> carrier_vec n"
  assumes "distinct A"
  assumes "\<And> f. lincomb_list (\<lambda>i. f (A ! i)) A = 0\<^sub>v n \<Longrightarrow> \<forall>v\<in> (set A). f v = 0"
  shows "lin_indpt (set A)"
  by (rule finite_lin_indpt2, auto simp add: assms lincomb_as_lincomb_list_distinct)

lemma lin_comb_mat_lin_indpt:
  fixes A :: "'a vec list"
  assumes "set (A) \<subseteq> carrier_vec n"
  assumes "distinct A"
  assumes "\<And> f. mat_of_cols n A *\<^sub>v vec (length A) (\<lambda>i. f (A ! i))  = 0\<^sub>v n \<Longrightarrow> \<forall>v\<in> (set A). f v = 0"
  shows "lin_indpt (set A)"
proof (rule lin_comb_sum_lin_indpt, auto simp add: assms)
  fix f v
  have "\<And> v. v \<in> set A \<Longrightarrow> dim_vec v = n"
    using assms by auto
  then show "lincomb_list (\<lambda>i. f (A ! i)) A = 0\<^sub>v n \<Longrightarrow> v \<in> set A \<Longrightarrow> f v = 0"
    using  lincomb_list_as_mat_mult[of A "(\<lambda>i. f (A ! i))"] assms(3)[of f] by auto
qed

lemma lin_comb_mat_lin_indpt_vs:
  fixes A :: "'a vec list"
  assumes "set (A) \<subseteq> carrier_vec n"
  assumes "distinct A"
  assumes "\<And> f. mat_of_cols n A *\<^sub>v vec (length A) (\<lambda>i. f (A ! i))  = 0\<^sub>v n \<Longrightarrow> \<forall>v\<in> (set A). f v = 0"
  shows "lin_indpt_vs (set A)"
  using lin_comb_mat_lin_indpt lin_indpt_vs_def assms by auto

end

subsection \<open>Linear Bound Argument Lemmas\<close>

text \<open>Three general representations of the linear bound argument, requiring a direct fact of
linear independence onthe rows of the vector space over either a set A of vectors, list xs of vectors
or a Matrix' columns \<close>
lemma lin_bound_arg_general_set:
  fixes A ::"('a :: {field})vec set"
  assumes "A \<subseteq> carrier_vec nr"
  assumes "vec_space.lin_indpt_vs nr A"
  shows "card A \<le> nr"
  using vec_space.lin_indpt_set_card_lt_dim[of "A" "nr"] vec_space.lin_indpt_vs_def[of nr A]
    vec_space.dim_is_n assms by metis

lemma lin_bound_arg_general_list:
  fixes xs ::"('a :: {field})vec list"
  assumes "distinct xs"
  assumes "(set xs) \<subseteq> carrier_vec nr"
  assumes "vec_space.lin_indpt_vs nr (set xs)"
  shows "length (xs) \<le> nr"
  using lin_bound_arg_general_set[of "set xs" nr] distinct_card assms
  by force

lemma lin_bound_arg_general:
  fixes A ::"('a :: {field}) mat"
  assumes "distinct (cols A)"
  assumes "A \<in> carrier_mat nr nc"
  assumes "vec_space.lin_indpt_vs nr (set (cols A))"
  shows "nc \<le> nr"
proof -
  have ss: "set (cols A) \<subseteq> carrier_vec nr" using assms cols_dim by blast
  have "length (cols A) = nc"
    using assms(2) cols_length by blast
  thus ?thesis using lin_bound_arg_general_list[of "cols A" "nr"] ss assms by simp
qed

text\<open>The linear bound argument lemma on a matrix requiring the lower level assumption on a linear
combination. This removes the need to directly refer to any aspect of the linear algebra libraries \<close>
lemma lin_bound_argument:
  fixes A :: "('a :: {field}) mat"
  assumes "distinct (cols A)"
  assumes "A \<in> carrier_mat nr nc"
  assumes "\<And> f. A *\<^sub>v vec nc (\<lambda>i. f (col A i)) = 0\<^sub>v nr \<Longrightarrow> \<forall>v\<in> (set (cols A)). f v = 0"
  shows "nc \<le> nr"
proof (intro lin_bound_arg_general[of "A" nr nc] vec_space.lin_comb_mat_lin_indpt_vs, simp_all add: assms)
  show "set (cols A) \<subseteq> carrier_vec nr" using assms cols_dim by blast
next
  have mA: "mat_of_cols nr (cols A) = A" using mat_of_cols_def assms by auto
  have "\<And> f. vec (dim_col A) (\<lambda>i. f (cols A ! i)) = vec nc (\<lambda>i. f (col A i))"
  proof (intro eq_vecI, simp_all add: assms)
    show "\<And>f i. i < nc \<Longrightarrow> vec (dim_col A) (\<lambda>i. f (cols A ! i)) $ i = f (col A i)"
      using assms(2) by force
    show "dim_col A = nc " using assms by simp
  qed
  then show "\<And>f. mat_of_cols nr (cols A) *\<^sub>v vec (dim_col A) (\<lambda>i. f (cols A ! i)) = 0\<^sub>v nr \<Longrightarrow>
      \<forall>v\<in>set (cols A). f v = 0"
    using mA assms(3) by metis
qed

text \<open>A further extension to present the linear combination directly as a sum. This manipulation from
vector product to a summation was found to commonly be repeated in proofs applying this rule \<close>
lemma lin_bound_argument2:
  fixes A :: "('a :: {field}) mat"
  assumes "distinct (cols A)"
  assumes "A \<in> carrier_mat nr nc"
  assumes "\<And> f. vec nr (\<lambda>i. \<Sum> j \<in> {0..<nc} . f (col A j) * (col A j) $ i) = 0\<^sub>v nr \<Longrightarrow>
    \<forall>v\<in> (set (cols A)). f v = 0"
  shows "nc \<le> nr"
proof (intro lin_bound_argument[of A nr nc], simp add: assms, simp add: assms)
  fix f
  have "A *\<^sub>v vec nc (\<lambda>i. f (col A i)) =
      vec (dim_row A) (\<lambda>i. \<Sum> j \<in> {0..<nc} . (row A i $ j) * f (col A j))"
    by (auto simp add: mult_mat_vec_def scalar_prod_def assms(2))
  also have "... = vec (dim_row A) (\<lambda>i. \<Sum> j \<in> {0..<nc} . f (col A j) * (col A j $ i))"
    using assms(2) by (intro eq_vecI, simp_all) (meson mult.commute)
  finally show "A *\<^sub>v vec nc (\<lambda>i. f (col A i)) = 0\<^sub>v nr \<Longrightarrow> \<forall>v\<in>set (cols A). f v = 0"
    using assms(3)[of f] assms(2) by fastforce
qed

end

author: cledmonds