Theory MonadicEquationalTheory

(*
Author: Alexander Katovsky
*)

section "Monadic Equational Theory"

theory MonadicEquationalTheory
imports Category Universe
begin

record ('t,'f) Signature = 
  BaseTypes :: "'t set" ("Tyı")
  BaseFunctions :: "'f set" ("Fnı")
  SigDom :: "'f  't" ("sDomı")
  SigCod :: "'f  't" ("sCodı")

locale Signature = 
  fixes S :: "('t,'f) Signature" (structure)
  assumes Domt: "f  Fn  sDom f  Ty"
  and     Codt: "f  Fn  sCod f  Ty"

definition funsignature_abbrev ("_  Sig _ : _  _" ) where
  "f  Sig S : A  B  f  (BaseFunctions S)  A  (BaseTypes S)  B  (BaseTypes S)  
                        (SigDom S f) = A  (SigCod S f) = B  Signature S"

lemma funsignature_abbrevE[elim]: 
"f  Sig S : A  B ; f  (BaseFunctions S) ; A  (BaseTypes S) ; B  (BaseTypes S) ; 
                        (SigDom S f) = A ; (SigCod S f) = B ; Signature S  R  R"
by (simp add: funsignature_abbrev_def)

datatype ('t,'f) Expression = ExprVar ("Vx") | ExprApp 'f "('t,'f) Expression" ("_ E@ _")
datatype ('t,'f) Language = Type 't (" _ Type") | Term 't "('t,'f) Expression" 't ("Vx : _  _ : _") | 
                            Equation 't "('t,'f) Expression" "('t,'f) Expression" 't ("Vx : _  __ : _")

inductive
  WellDefined :: "('t,'f) Signature  ('t,'f) Language  bool" ("Sig _  _") where
    WellDefinedTy: "A  BaseTypes S  Sig S   A Type"
  | WellDefinedVar: "Sig S   A Type  Sig S  (Vx : A   Vx : A)" 
  | WellDefinedFn: "Sig S  (Vx : A   e : B)  ; f  Sig S : B  C  Sig S  (Vx : A   (f E@ e) : C)"
  | WellDefinedEq: "Sig S  (Vx : A   e1 : B) ; Sig S  (Vx : A   e2 : B)  Sig S  (Vx : A  e1  e2 : B)"

lemmas WellDefined.intros [intro]
inductive_cases WellDefinedTyE [elim!]: "Sig S   A Type"
inductive_cases WellDefinedVarE [elim!]: "Sig S  (Vx : A   Vx : A)"
inductive_cases WellDefinedFnE [elim!]: "Sig S  (Vx : A   (f E@ e) : C)"
inductive_cases WellDefinedEqE [elim!]: "Sig S  (Vx : A  e1  e2 : B)"

lemma SigId: "Sig S  (Vx : A   Vx : B)  A = B"
apply(rule WellDefined.cases)
by simp+

lemma SigTyId: "Sig S  (Vx : A   Vx : A)  A  BaseTypes S"
apply(rule WellDefined.cases)
by auto

lemma (in Signature) SigTy: " B . Sig S  (Vx : A   e : B)  (A  BaseTypes S  B  BaseTypes S)"
proof(induct e)
  {
    fix B assume a: "Sig S  Vx : A  Vx : B"
    have "A = B" using a SigId[of S] by simp
    thus "A  Ty  B  Ty" using a by auto
  }
  {
    fix B f e assume ih: "B'. Sig S  (Vx : A  e : B')  A  Ty  B'  Ty"
    and a: "Sig S  (Vx : A  (f E@ e) : B)"
    from a obtain B' where f: "f  Sig S : B'  B" and "Sig S  (Vx : A  e : B')" by auto
    hence "A  Ty" using ih by auto
    moreover have "B  Ty" using f by (auto simp add: funsignature_abbrev_def Codt)
    ultimately show "A  Ty  B  Ty" by simp
  }
qed

(*An interpretation is an object, a morphism or a boolean*)
datatype ('o,'m) IType = IObj 'o | IMor 'm | IBool bool

record ('t,'f,'o,'m) Interpretation = 
  ISignature :: "('t,'f) Signature" ("iSı")
  ICategory  :: "('o,'m) Category"  ("iCı")
  ITypes     :: "'t  'o" ("Ty⟦_ı")
  IFunctions :: "'f  'm" ("Fn⟦_ı")

locale Interpretation = 
  fixes I :: "('t,'f,'o,'m) Interpretation" (structure)
  assumes ICat: "Category  iC"
  and     ISig: "Signature iS" 
  and     It  : "A  BaseTypes iS  Ty⟦A  Obj iC"
  and     If  : "(f  Sig iS : A  B)  Fn⟦f mapsiCTy⟦A to Ty⟦B"

inductive Interp  ("L⟦_ı  _") where
    InterpTy: "Sig iSI  A Type  
                       L⟦ A TypeI (IObj Ty⟦AI)"
  | InterpVar: "L⟦ A TypeI (IObj c)  
                       L⟦Vx : A   Vx : AI (IMor (Id iCIc))" 
  | InterpFn: "Sig iSI Vx : A   e : B ; 
               f  Sig iSI: B  C ; 
               L⟦Vx : A   e : BI (IMor g)  
               L⟦Vx : A   (f E@ e) : CI (IMor (g ;;ICategory IFn⟦fI))"
  | InterpEq: "L⟦Vx : A   e1 : BI (IMor g1) ; 
                L⟦Vx : A   e2 : BI (IMor g2)  
                L⟦Vx : A   e1  e2 : BI (IBool (g1 = g2))"

lemmas  Interp.intros [intro]
inductive_cases  InterpTyE [elim!]: "L⟦ A TypeI i"
inductive_cases  InterpVarE [elim!]: "L⟦Vx : A   Vx : AI i"
inductive_cases  InterpFnE [elim!]: "L⟦Vx : A   (f E@ e) : CI i"
inductive_cases  InterpEqE [elim!]: "L⟦Vx : A   e1  e2 : BI i"

lemma (in Interpretation) InterpEqEq[intro]: 
  "L⟦Vx : A   e1 : B  (IMor g) ; L⟦Vx : A   e2 : B  (IMor g)  L⟦Vx : A   e1  e2 : B  (IBool True)"
proof-
  assume a: "L⟦Vx : A   e1 : B  (IMor g)" and b: "L⟦Vx : A   e2 : B  (IMor g)"
  thus ?thesis using InterpEq[of I A e1 B g e2 g] by simp
qed

lemma (in Interpretation) InterpExprWellDefined:
"L⟦Vx : A  e : B  i  Sig iS  Vx : A   e : B"
apply (rule Interp.cases)
by auto

lemma (in Interpretation) WellDefined: "L⟦φ  i  Sig iS  φ"
apply(rule Interp.cases)
by (auto simp add: InterpExprWellDefined)

lemma (in Interpretation) Bool: "L⟦φ  (IBool i)   A B e d . φ = (Vx : A  e  d : B)"
apply(rule Interp.cases)
by auto

lemma (in Interpretation) FunctionalExpr:
"i j A B.L⟦Vx : A  e : B  i; L⟦Vx : A  e : B  j  i = j"
apply (induct e)
apply (rule Interp.cases)
apply auto
apply (auto simp add: funsignature_abbrev_def)
done

lemma (in Interpretation) Functional: "L⟦φ  i1 ; L⟦φ  i2  i1 = i2"
proof(induct φ)
  {
    fix t show "L⟦ t Type  i1 ; L⟦ t Type  i2  i1 = i2" by auto
  }
  {
    fix t1 t2 e 
    show "L⟦Vx : t1  e : t2  i1; L⟦Vx : t1  e : t2  i2  i1 = i2" by (simp add: FunctionalExpr)
  }
  {
    fix t1 t2 e1 e2 show "L⟦Vx : t1  e1  e2 : t2  i1; L⟦Vx : t1  e1  e2 : t2  i2  i1 = i2" 
    proof(auto)
      {
        fix f g h assume f1: "L⟦Vx : t1  e1 : t2  (IMor f)" and f2: "L⟦Vx : t1  e2 : t2  (IMor f)"
          and g1: "L⟦Vx : t1  e1 : t2  (IMor g)" and g2: "L⟦Vx : t1  e2 : t2  (IMor h)"
        have "f = g" using f1 g1 FunctionalExpr[of t1 e1 t2 "IMor f" "IMor g"] by simp
        moreover have "f = h" using f2 g2 FunctionalExpr[of t1 e2 t2 "IMor f" "IMor h"] by simp
        ultimately show "g = h" by simp
      }
      moreover 
      {
        fix f g h assume f1: "L⟦Vx : t1  e1 : t2  (IMor f)" and f2: "L⟦Vx : t1  e2 : t2  (IMor g)"
          and g1: "L⟦Vx : t1  e1 : t2  (IMor h)" and g2: "L⟦Vx : t1  e2 : t2  (IMor h)"
        have "f = h" using f1 g1 FunctionalExpr[of t1 e1 t2 "IMor f" "IMor h"] by simp
        moreover have "g = h" using f2 g2 FunctionalExpr[of t1 e2 t2 "IMor g" "IMor h"] by simp
        ultimately show "f = g" by simp
      }
    qed 
  }
qed

lemma (in Interpretation) MorphismsPreserved:
" B i . L⟦Vx : A   e : B  i   g . i = (IMor g)  (g mapsiCTy⟦A to Ty⟦B)"
proof(induct e)
  {
    fix B i assume a: "L⟦Vx : A  Vx : B  i" show " g. i = IMor g  g mapsiCTy⟦A to Ty⟦B"
    proof(rule exI[where ?x="Id iC Ty⟦A"], rule conjI)
      have sig: "Sig iS  Vx : A   Vx : B" using a by (simp add: InterpExprWellDefined) 
      hence aEqb: "A = B" by (simp add: SigId)
      have ty: "A  BaseTypes iS" using aEqb sig SigTyId by simp
      hence "L⟦Vx : A  Vx : A  (IMor (Id iC Ty⟦A))" by auto
      thus "i = IMor (Category.Id iC Ty⟦A)" using a aEqb Functional by simp
      show "(Id iC Ty⟦A) mapsiCTy⟦A to Ty⟦B" using aEqb ICat It[of A] Category.Cidm[of iC "Ty⟦A"] ty by simp
    qed
  }
  {
    fix f e B i assume a: " B i . L⟦Vx : A  e : B  i  g. i = IMor g  g mapsiCTy⟦A to Ty⟦B"
               and b: "L⟦Vx : A  f E@ e : B  i"
    show "g. i = IMor g  g mapsiCTy⟦A to Ty⟦B" using a b 
    proof-
      from b obtain g B' where g: "(Sig iS  Vx : A  e : B')  (f  Sig iS : B'  B)  (L⟦Vx : A  e : B'  (IMor g))"
        by auto
      from a have gmaps: "g mapsiCTy⟦A to Ty⟦B'" using g by auto
      have fmaps: "Fn⟦f mapsiCTy⟦B' to Ty⟦B" using g If by simp
      have "(g ;;iCFn⟦f) mapsiCTy⟦A to Ty⟦B" using ICat fmaps gmaps Category.Ccompt[of "iC" g] by simp
      moreover have "L⟦Vx : A  f E@ e : B  (IMor (g ;;iCFn⟦f))" using g by auto
      ultimately show ?thesis using b Functional exI[where ?x = "(g ;;iCFn⟦f)"] by simp
    qed
  }
qed

lemma (in Interpretation) Expr2Mor: "L⟦Vx : A   e : B  (IMor g)  (g mapsiCTy⟦A to Ty⟦B)"
proof-
  assume a: "L⟦Vx : A   e : B  (IMor g)"
  from MorphismsPreserved[of A e B "(IMor g)"] obtain g' where "(IMor g) = (IMor g')  (g' mapsiCTy⟦A to Ty⟦B)"
    using a by auto
  thus ?thesis by simp
qed

lemma (in Interpretation) WellDefinedExprInterp: " B . (Sig iS  Vx : A   e : B)  ( i . L⟦Vx : A   e : B  i)"
proof(induct e)
  {
    fix B assume sig: "(Sig iS  Vx : A   Vx : B)" show "i. L⟦Vx : A  Vx : B  i"
    proof-
      have aEqb: "A = B" using sig by (simp add: SigId)
      hence ty: "A  BaseTypes iS" using sig SigTyId by simp
      hence "L⟦Vx : A  Vx : A  (IMor (Id iC Ty⟦A))" by auto
      thus ?thesis using aEqb by auto
    qed
  }
  {
    fix f e B assume a: " B . (Sig iS  Vx : A   e : B)  ( i . L⟦Vx : A   e : B  i)"
      and b: "(Sig iS  Vx : A   f E@ e : B)"
    show " i . L⟦Vx : A   f E@ e : B  i"
    proof-
      from b obtain B' where B': "(Sig iS  (Vx : A   e : B'))  (f  Sig iS : B'  B)" by auto
      from B' a obtain i where i: "L⟦Vx : A   e : B'  i" by auto
      from MorphismsPreserved[of A e B' i] i obtain g where g: "i = (IMor g)" by auto
      thus ?thesis using B' i by auto
    qed
  }
qed

lemma (in Interpretation) Sig2Mor: assumes "(Sig iS  Vx : A   e : B)" shows " g . L⟦Vx : A   e : B  (IMor g)"
proof-
  from WellDefinedExprInterp[of A e B] assms obtain i where i: "L⟦Vx : A   e : B  i" by auto
  thus ?thesis using MorphismsPreserved[of A e B i] i by auto
qed

record ('t,'f) Axioms = 
  aAxioms :: "('t,'f) Language set" 
  aSignature :: "('t,'f) Signature" ("aSı")

locale Axioms = 
  fixes Ax :: "('t,'f) Axioms" (structure)
  assumes AxT: "(aAxioms Ax)  {(Vx : A  e1  e2 : B) | A B e1 e2 . Sig (aSignature Ax)  (Vx : A  e1  e2 : B)}"
  assumes AxSig: "Signature (aSignature Ax)"

primrec Subst :: "('t,'f) Expression  ('t,'f) Expression  ('t,'f) Expression" ("sub _ in _" [81,81] 81) where
  "(sub e in Vx) = e" | "sub e in (f E@ d) = (f E@ (sub e in d))"

lemma SubstXinE: "(sub Vx in e) = e"
by(induct e, auto simp add: Subst_def)

lemma SubstAssoc: "sub a in (sub b in c) = sub (sub a in b) in c"
by(induct c, (simp add: Subst_def)+)

lemma SubstWellDefined: " C . Sig S  (Vx : A  e : B); Sig S  (Vx : B  d : C)
        Sig S  (Vx : A  (sub e in d) : C)"
proof(induct d)
  {
    fix C assume a: "Sig S  Vx : A  e : B" and b: "Sig S  Vx : B  Vx : C"
    have BCeq: "B = C" using b SigId[of S] by simp
    thus "Sig S  Vx : A  sub e in Vx : C" using a by simp
  }
  {
    fix f d C assume ih: "B'. Sig S  Vx : A  e : B; Sig S  Vx : B  d : B'
             Sig S  Vx : A  sub e in d : B'" and a: "Sig S  Vx : A  e : B" 
    and b: "Sig S  Vx : B  f E@ d : C"
    from b obtain B' where B': "f  Sig S : B'  C" and d: "Sig S  Vx : B  d : B'" by auto
    hence "Sig S  Vx : A  sub e in d : B'" using ih a by simp
    hence "Sig S  Vx : A  f E@ (sub e in d) : C" using B' by auto
    thus "Sig S  Vx : A  (sub e in (f E@ d)) : C" by auto
  }
qed

inductive_set (in Axioms) Theory where
  Ax: "A  (aAxioms Ax)  A  Theory"
| Refl: "Sig (aSignature Ax)  (Vx : A  e : B)  (Vx : A  e  e : B)  Theory"
| Symm: "(Vx : A  e1  e2 : B)  Theory  (Vx : A  e2  e1 : B)  Theory" 
| Trans: "(Vx : A  e1  e2 : B)  Theory ; (Vx : A  e2  e3 : B)  Theory 
           (Vx : A  e1  e3 : B)  Theory"
| Congr: "(Vx : A  e1  e2 : B)  Theory ; f  Sig (aSignature Ax) : B  C  
           (Vx : A  (f E@ e1)  (f E@ e2) : C)  Theory"
| Subst: "Sig (aSignature Ax)  (Vx : A  e1 : B) ; (Vx : B  e2  e3 : C)  Theory 
           (Vx : A  (sub e1 in e2)  (sub e1 in e3) : C)  Theory"

lemma (in Axioms) Equiv2WellDefined: "φ  Theory  Sig aS  φ"
proof(rule Theory.induct,auto simp add: SubstWellDefined)
  {
    fix φ assume ax: "φ  aAxioms Ax"
    from AxT obtain A e1 e2 B where "Sig aS  Vx : A  e1  e2 : B" and "φ = Vx : A  e1  e2 : B" using ax by blast
    thus "Sig aS  φ" by simp    
  }
qed

lemma (in Axioms) Subst':
  " C . Sig aS  Vx : B  d : C ; (Vx : A  e1  e2 : B)  Theory  
  (Vx : A  (sub e1 in d)  (sub e2 in d) : C)  Theory"
proof(induct d)
  {
    fix C assume a: "Sig aS  Vx : B  Vx : C" and b: "(Vx : A  e1e2 : B)  Theory"
    have BCeq: "B = C" using a SigId[of aS B C] by simp
    thus "(Vx : A  (sub e1 in Vx)  (sub e2 in Vx) : C)  Theory" using b by (simp add: Subst_def)
  }
  {
    fix C f d assume ih: " B' . Sig aS  Vx : B  d : B'; (Vx : A  e1e2 : B)  Theory
       (Vx : A  (sub e1 in d)  (sub e2 in d) : B')  Theory" and wd: "Sig aS  Vx : B  f E@ d : C" and
      eq: "(Vx : A  e1  e2 : B)  Theory"
    from wd obtain B' where B': "f  Sig aS : B'  C" and d: "Sig aS  Vx : B  d : B'" by auto
    hence "(Vx : A  (sub e1 in d)  (sub e2 in d) : B')  Theory" using ih eq by simp
    hence "(Vx : A  f E@ (sub e1 in d)  f E@ (sub e2 in d) : C)  Theory" using B' by (simp add: Congr)
    thus "(Vx : A  (sub e1 in (f E@ d))  (sub e2 in (f E@ d)) : C)  Theory" by (simp add: Subst_def)
  }
qed

(*This is the diamond problem in multiple inheritance -- both Interpretation and Axioms share a Signature*)
locale Model = Interpretation I + Axioms Ax
  for I :: "('t,'f,'o,'m) Interpretation" (structure)
  and Ax :: "('t,'f) Axioms" +
  assumes AxSound: "φ  (aAxioms Ax)  L⟦φ  (IBool True)"
  and Seq[simp]: "(aSignature Ax) = iS"

lemma (in Interpretation) Equiv:
  assumes "L⟦Vx : A  e1  e2 : B  (IBool True)"
  shows " g . (L⟦Vx : A  e1 : B  (IMor g))  (L⟦Vx : A  e2 : B  (IMor g))"
proof-
  from assms Sig2Mor[of A e1 B] obtain g1 where g1: "L⟦Vx : A  e1 : B  (IMor g1)" by auto
  from assms Sig2Mor[of A e2 B] obtain g2 where g2: "L⟦Vx : A  e2 : B  (IMor g2)" by auto
  have "L⟦Vx : A  e1e2 : B  (IBool (g1 = g2))" using g1 g2 by auto
  hence "g1 = g2" using assms Functional[of "Vx : A  e1e2 : B" "(IBool True)" "IBool (g1=g2)"] by simp
  thus ?thesis using g1 g2 by auto
qed

lemma (in Interpretation) SubstComp: " h C . (L⟦Vx : A  e : B  (IMor g)) ; (L⟦Vx : B  d : C  (IMor h)) 
  (L⟦Vx : A  (sub e in d) : C  (IMor (g ;;iCh)))"
proof(induct d,auto)
  {
    fix h C assume a: "L⟦Vx : A  e : B  IMor g" and b: "L⟦Vx : B  Vx : C  (IMor h)"
    show "L⟦Vx : A  e : C  IMor (g ;;iCh)"
    proof-
      have beqc: "B = C" using b SigId[of iS B C] InterpExprWellDefined by simp
      have "L⟦Vx : B  Vx : B  (IMor (Id iC Ty⟦B))" using beqc b by auto
      hence h: "h = Id iC Ty⟦B" using b beqc by (auto simp add: Functional)
      have "g mapsiCTy⟦A to Ty⟦B" using a MorphismsPreserved by auto
      hence "g  Mor iC" and "codiCg = Ty⟦B" by auto
      hence "(g ;;iCh) = g" using h ICat Category.Cidr[of iC g] by simp
      thus ?thesis using beqc a by simp
    qed
  }
  {
    fix f d C' h C assume 
      i: " h C' . L⟦Vx : B  d : C'  IMor h  L⟦Vx : A  (sub e in d) : C'  (IMor (g ;;iCh))" and
      a: "L⟦Vx : A  e : B  IMor g" "f  Sig iS : C'  C" "L⟦Vx : B  d : C'  IMor h"
    show "L⟦Vx : A  f E@ (sub e in d) : C  (IMor (g ;;iC(h ;;iCFn⟦f)))"
    proof-
      have "L⟦Vx : A  (sub e in d) : C'  (IMor (g ;;iCh))" using i a by auto
      moreover hence "Sig iS  Vx : A  (sub e in d) : C'" using InterpExprWellDefined by simp
      ultimately have 1: "L⟦Vx : A  f E@ (sub e in d) : C  (IMor ((g ;;iCh) ;;iCFn⟦f))" using a(2) by auto
      have "g mapsiCTy⟦A to Ty⟦B" and "h mapsiCTy⟦B to Ty⟦C'" and "Fn⟦f mapsiCTy⟦C' to Ty⟦C"
        using a If Expr2Mor by simp+
      hence "g ≈>iCh" and "h ≈>iC(Fn⟦f)" using MapsToCompDef[of iC] by simp+
      hence "(g ;;iCh) ;;iCFn⟦f = g ;;iC(h ;;iCFn⟦f)" using ICat Category.Cassoc[of iC] by simp
      thus ?thesis using 1 by simp
    qed
  }
qed

lemma (in Model) Sound: "φ  Theory   L⟦φ  (IBool True)"
proof(rule Theory.induct, (simp_all add: AxSound)+)
  {
    fix A e B assume sig: "Sig iS  Vx : A  e : B" show "L⟦Vx : A  ee : B  (IBool True)"
    proof-
      from sig Sig2Mor[of A e B] obtain g where g: "L⟦Vx : A  e : B  (IMor g)" by auto
      thus ?thesis using InterpEq[of I A e B g e g] by simp
    qed
  }
  {
    fix A e1 e2 B assume a: "L⟦Vx : A  e1e2 : B  (IBool True)" show "L⟦Vx : A  e2e1 : B  (IBool True)"
    proof-
      from a obtain g where g1: "L⟦Vx : A  e1 : B  (IMor g)" and g2: "L⟦Vx : A  e2 : B  (IMor g)"
        using Equiv by auto
      thus ?thesis by auto
    qed
  }
  {
    fix A e1 e2 B e3 assume a: "L⟦Vx : A  e1e2 : B  (IBool True)" and b: "L⟦Vx : A  e2e3 : B  (IBool True)"
    show "L⟦Vx : A  e1e3 : B  (IBool True)"
    proof-
      from a obtain g where g1: "L⟦Vx : A  e1 : B  (IMor g)" and g2: "L⟦Vx : A  e2 : B  (IMor g)"
        using Equiv by auto
      from b obtain g' where g1': "L⟦Vx : A  e2 : B  (IMor g')" and g2': "L⟦Vx : A  e3 : B  (IMor g')"
        using Equiv by auto
      have eq: "g = g'" using g2 g1' using Functional by auto
      thus ?thesis using eq g1 g2' by auto
    qed
  }
  {
    fix A e1 e2 B f C assume a: "L⟦Vx : A  e1e2 : B  (IBool True)" and b: "f  Sig iS : B  C"
    show "L⟦Vx : A  (f E@ e1)  (f E@ e2) : C  (IBool True)"
    proof-
      from a obtain g where g1: "L⟦Vx : A  e1 : B  (IMor g)" and g2: "L⟦Vx : A  e2 : B  (IMor g)"
        using Equiv by auto      
      have s1: "Sig iS  Vx : A   e1 : B" and s2: "Sig iS  Vx : A   e2 : B" using g1 g2 InterpExprWellDefined by simp+
      have "L⟦Vx : A   (f E@ e1) : C  (IMor (g ;;iCFn⟦f))"
        and "L⟦Vx : A   (f E@ e2) : C  (IMor (g ;;iCFn⟦f))" using b g1 s1 g2 s2 by auto
      thus ?thesis using InterpEqEq[of A "(f E@ e1)" C "(g ;;iCFn⟦f)"] by simp
    qed
  }
  {
    fix A e1 B e2 e3 C assume a: "Sig iS  (Vx : A  e1 : B)" and b: "L⟦Vx : B  e2e3 : C  (IBool True)"
    show "L⟦Vx : A  (sub e1 in e2)  (sub e1 in e3) : C  (IBool True)"
    proof-
      from b obtain g where g1: "L⟦Vx : B  e2 : C  (IMor g)" and g2: "L⟦Vx : B  e3 : C  (IMor g)"
        using Equiv by auto
      from a Sig2Mor[of A e1 B] obtain f where f: "L⟦Vx : A  e1 : B  (IMor f)" by auto
      have "L⟦Vx : A  (sub e1 in e2) : C  (IMor (f ;;iCg))" using SubstComp g1 f by simp
      moreover have "L⟦Vx : A  (sub e1 in e3) : C  (IMor (f ;;iCg))" using SubstComp g2 f by simp
      ultimately show ?thesis using InterpEqEq by simp
    qed
  }
qed

record ('t,'f) TermEquivClT = 
  TDomain :: 't
  TExprSet :: "('t,'f) Expression set"
  TCodomain :: 't

locale ZFAxioms = Ax : Axioms Ax for Ax :: "(ZF,ZF) Axioms" (structure) +
  assumes     fnzf: "BaseFunctions (aSignature Ax)  range explode"

lemma [simp]: "ZFAxioms T  Axioms T" by (simp add: ZFAxioms_def)

(*(tree depth, rule number, components)*)
primrec Expr2ZF :: "(ZF,ZF) Expression  ZF" where
    Expr2ZFVx: "Expr2ZF Vx = ZFTriple (nat2Nat 0) (nat2Nat 0) Empty" 
  | Expr2ZFfe: "Expr2ZF (f E@ e) = ZFTriple (SucNat (ZFTFst (Expr2ZF e)))
                                 (nat2Nat 1)
                                 (Opair f (Expr2ZF e))"

definition ZF2Expr :: "ZF  (ZF,ZF) Expression" where
  "ZF2Expr = inv Expr2ZF"

definition "ZFDepth = Nat2nat o ZFTFst"
definition "ZFType = Nat2nat o ZFTSnd"
definition "ZFData = ZFTThd"

lemma Expr2ZFType0: "ZFType (Expr2ZF e) = 0  e = Vx"
by(cases e,auto simp add: ZFType_def ZFTSnd Elem_Empty_Nat Elem_SucNat_Nat ZFSucNeq0)

lemma ZFDepthInNat: "Elem (ZFTFst (Expr2ZF e)) Nat"
by(induct e, auto simp add:  ZFTFst HOLZF.Elem_Empty_Nat Elem_SucNat_Nat)

lemma Expr2ZFType1: "ZFType (Expr2ZF e) = 1  
   f e' . e = (f E@ e')  (Suc (ZFDepth (Expr2ZF e'))) = (ZFDepth (Expr2ZF e))"
by(cases e,auto simp add: ZFType_def ZFTSnd ZFDepth_def ZFTFst ZFZero ZFDepthInNat Nat2nat_SucNat)

lemma Expr2ZFDepth0: "ZFDepth (Expr2ZF e) = 0  ZFType (Expr2ZF e) = 0"
by(cases e, auto simp add: ZFDepth_def ZFTFst ZFType_def ZFTSnd ZFSucNeq0 ZFDepthInNat)

lemma Expr2ZFDepthSuc: "ZFDepth (Expr2ZF e) = Suc n  ZFType (Expr2ZF e) = 1"
by(cases e, auto simp add: ZFDepth_def ZFTFst ZFType_def ZFTSnd ZFSucZero ZFSucNeq0 ZFZero)

lemma Expr2Data: "ZFData (Expr2ZF (f E@ e)) = Opair f (Expr2ZF e)"
by(auto simp add: ZFData_def ZFTThd)

lemma Expr2ZFinj: "inj Expr2ZF"
proof(auto simp add: inj_on_def)
  have a: " n e d . n = ZFDepth (Expr2ZF e) ; Expr2ZF e = Expr2ZF d  e = d"
  proof-
    fix n show " e d . n = ZFDepth (Expr2ZF e) ; Expr2ZF e = Expr2ZF d  e = d"
    proof(induct n)
      {
        fix e d assume a: "0 = ZFDepth (Expr2ZF e)" and b: "Expr2ZF e = Expr2ZF d"
        have "0 = ZFDepth (Expr2ZF d)" using a b by simp 
        hence "e = Vx" and "d = Vx" using a by (simp add: Expr2ZFDepth0 Expr2ZFType0)+
        thus "e = d" by simp
      }
      {
        fix n e d assume ih: " e' d' . n = ZFDepth (Expr2ZF e') ; Expr2ZF e' = Expr2ZF d'  e' = d'"
          and a: "Suc n = ZFDepth (Expr2ZF e)" and b: "Expr2ZF e = Expr2ZF d"
        have "ZFType (Expr2ZF e) = 1" and "ZFType (Expr2ZF d) = 1" using a b Expr2ZFDepthSuc[of e n] by simp+
        from this Expr2ZFType1[of e] Expr2ZFType1[of d] obtain fe fd e' d' 
          where e: "e = (fe E@ e')  (Suc (ZFDepth (Expr2ZF e'))) = (ZFDepth (Expr2ZF e))" and
          d: "d = (fd E@ d')  (Suc (ZFDepth (Expr2ZF d'))) = (ZFDepth (Expr2ZF d))" by auto
        hence "Suc (ZFDepth (Expr2ZF e')) = Suc n" using a by simp
        hence ne: "(ZFDepth (Expr2ZF e')) = n" by (rule Suc_inject)
        have edat: "ZFData (Expr2ZF e) = Opair fe (Expr2ZF e')" using e Expr2Data by simp
        have ddat: "ZFData (Expr2ZF d) = Opair fd (Expr2ZF d')" using d Expr2Data by simp
        have fd_eq_fe: "fe = fd" and "(Expr2ZF e') = (Expr2ZF d')" using edat ddat Opair b by auto
        hence "e' = d'" using ne ih by auto
        thus "e = d" using e d fd_eq_fe by auto
      }
    qed
  qed
  fix e d show "Expr2ZF e = Expr2ZF d  e = d" using a by auto
qed

definition "TermEquivClGen T A e B  {e' . (Vx : A  e'  e : B)  Axioms.Theory T}"
definition "TermEquivCl' T A e B   TDomain = A , TExprSet = TermEquivClGen T A e B , TCodomain = B"

definition m2ZF :: "(ZF,ZF) TermEquivClT  ZF" where
  "m2ZF t  ZFTriple (TDomain t) (implode (Expr2ZF ` (TExprSet t))) (TCodomain t)"

definition ZF2m :: "(ZF,ZF) Axioms  ZF  (ZF,ZF) TermEquivClT" where
  "ZF2m T  inv_into {TermEquivCl' T A e B | A e B . True} m2ZF"

lemma TDomain: "TDomain (TermEquivCl' T A e B) = A" by (simp add: TermEquivCl'_def)
lemma TCodomain: "TCodomain (TermEquivCl' T A e B) = B" by (simp add: TermEquivCl'_def)

primrec WellFormedToSet :: "(ZF,ZF) Signature  nat  (ZF,ZF) Expression set" where
  WFS0: "WellFormedToSet S 0 = {Vx}"
| WFSS: "WellFormedToSet S (Suc n) = (WellFormedToSet S n) 
                { f E@ e | f e . f  BaseFunctions S  e  (WellFormedToSet S n)}"

lemma WellFormedToSetInRangeExplode: "ZFAxioms T  (Expr2ZF ` (WellFormedToSet aSTn))  range explode"
proof((induct n),(simp add: WellFormedToSet_def SingletonInRangeExplode))
  fix n assume zfx: "ZFAxioms T" and ih: "ZFAxioms T  Expr2ZF ` WellFormedToSet aSTn  range explode"
  hence a: "Expr2ZF ` WellFormedToSet aSTn  range explode" by simp
  have "Expr2ZF ` { f E@ e | f e . f  BaseFunctions aST e  (WellFormedToSet aSTn)}
    = (λ (f, ze) . Expr2ZF (f E@ (ZF2Expr ze))) ` ((BaseFunctions aST) × Expr2ZF ` (WellFormedToSet aSTn))"
  proof (auto simp add: image_Collect image_def ZF2Expr_def Expr2ZFinj)
    fix f e
    assume f: "f  BaseFunctions aST⇙" and e: "e  WellFormedToSet aSTn"
    show " x  BaseFunctions aST.y. ( x  WellFormedToSet aSTn. y = Expr2ZF x) 
      ZFTriple (SucNat (ZFTFst (Expr2ZF e))) (SucNat Empty) (Opair f (Expr2ZF e)) =
      ZFTriple (SucNat (ZFTFst (Expr2ZF (inv Expr2ZF y)))) (SucNat Empty) (Opair x (Expr2ZF (inv Expr2ZF y)))"
      apply(rule bexI[where ?x = f], rule exI[where ?x = "Expr2ZF e"])
      apply (auto simp add: Expr2ZFinj f e)
      done
    show "x. (f e. x = f E@ e  f  (BaseFunctions aST)  e  WellFormedToSet aSTn) 
              ZFTriple (SucNat (ZFTFst (Expr2ZF e))) (SucNat Empty) (Opair f (Expr2ZF e)) = Expr2ZF x"
      apply(rule exI[where ?x = "f E@ e"])
      apply (auto simp add: f e)
      done
  qed
  moreover have "(BaseFunctions aST)  range explode" using zfx ZFAxioms.fnzf by simp 
  ultimately have "Expr2ZF ` { f E@ e | f e . f  BaseFunctions aST e  (WellFormedToSet aSTn)}  range explode"
    using a ZFProdFnInRangeExplode by simp
  moreover have "Expr2ZF ` WellFormedToSet aST(Suc n) = (Expr2ZF ` (WellFormedToSet aSTn)) 
                (Expr2ZF  ` { f E@ e | f e . f  BaseFunctions aST e  (WellFormedToSet aSTn)})" by auto
  ultimately show "Expr2ZF ` WellFormedToSet aST(Suc n)  range explode" using ZFUnionInRangeExplode a by simp
qed

lemma WellDefinedToWellFormedSet: " B . (Sig S  (Vx : A  e : B))  n. e  WellFormedToSet S n"
proof(induct e)
  {
    fix B assume "Sig S  Vx : A  Vx : B"
    show "n. Vx  WellFormedToSet S n" by (rule exI[of _ 0], auto)
  }
  {
    fix f e B assume ih: "B'. Sig S  Vx : A  e : B'  n. e  WellFormedToSet S n"
      and "Sig S  Vx : A  (f E@ e) : B"
    from this obtain B' where "Sig S  (Vx : A  e : B')" and f: "f  Sig S : B'  B" by auto
    from this obtain n where a: "e  WellFormedToSet S n" using ih by auto
    have ff: "f  BaseFunctions S" using f by auto
    show "n. (f E@ e)  WellFormedToSet S n" by(rule exI[of _ "Suc n"], auto simp add: a ff)
  }
qed

lemma TermSetInSet: "ZFAxioms T  Expr2ZF ` (TermEquivClGen T A e B)  range explode"
proof-
  assume zfax: "ZFAxioms T"
  have "(TermEquivClGen T A e B)  {e' . (Sig aST (Vx : A  e' : B))}"
  proof(auto simp add: TermEquivClGen_def)
    fix x assume "Vx : A  xe : B  Axioms.Theory T" 
    hence "Sig aST Vx : A  xe : B" by (auto simp add: Axioms.Equiv2WellDefined zfax)
    thus "Sig aST Vx : A  x : B" by auto
  qed
  also have "...  ( n . (WellFormedToSet aSTn))" by (auto simp add: WellDefinedToWellFormedSet)
  finally have "Expr2ZF ` (TermEquivClGen T A e B)  Expr2ZF ` ( n . (WellFormedToSet aSTn))" by auto
  also have "... = ( n . (Expr2ZF ` (WellFormedToSet aSTn)))" by auto
  finally have "Expr2ZF ` (TermEquivClGen T A e B)  ( n . (Expr2ZF ` (WellFormedToSet aSTn)))" by auto
  moreover have "( n . (Expr2ZF ` (WellFormedToSet aSTn)))  range explode" 
    using zfax ZFUnionNatInRangeExplode WellFormedToSetInRangeExplode by auto
  ultimately show ?thesis using  ZFSubsetRangeExplode[of 
    "( n . (Expr2ZF ` (WellFormedToSet aSTn)))" "Expr2ZF ` (TermEquivClGen T A e B)"] by simp
qed

lemma m2ZFinj_on: "ZFAxioms T  inj_on m2ZF {TermEquivCl' T A e B | A e B . True}"
apply(auto simp only: inj_on_def m2ZF_def)
apply(drule ZFTriple)
apply(auto simp add: TDomain TCodomain implode_def)
apply(simp add: TermEquivCl'_def)
apply(drule inv_into_injective)
apply(auto simp add: TermSetInSet inj_image_eq_iff Expr2ZFinj)
done

lemma ZF2m: "ZFAxioms T  ZF2m T (m2ZF (TermEquivCl' T A e B)) = (TermEquivCl' T A e B)"
proof-
  assume zfax: "ZFAxioms T"
  let ?A = "{TermEquivCl' T A e B | A e B . True}" and ?x = "TermEquivCl' T A e B"
  have "?x  ?A" by auto
  thus ?thesis using m2ZFinj_on[of T] inv_into_f_f zfax by (simp add:  ZF2m_def )
qed

definition TermEquivCl ("[_,_,_]ı") where "[A,e,B]T m2ZF (TermEquivCl' T A e B)"

definition "CLDomain T  TDomain o ZF2m T"
definition "CLCodomain T  TCodomain o ZF2m T"

definition "CanonicalComp T f g  
  THE h .  e e' . h = [CLDomain T f,sub e in e',CLCodomain T g]T  
  f = [CLDomain T f,e,CLCodomain T f]T g = [CLDomain T g,e',CLCodomain T g]T⇙"

lemma CLDomain: "ZFAxioms T  CLDomain T [A,e,B]T= A"  by (simp add: TermEquivCl_def CLDomain_def ZF2m TDomain)
lemma CLCodomain: "ZFAxioms T  CLCodomain T [A,e,B]T= B"  by (simp add: TermEquivCl_def CLCodomain_def ZF2m TCodomain)

lemma Equiv2Cl: assumes "Axioms T" and "(Vx : A  e  d : B)  Axioms.Theory T" shows  "[A,e,B]T= [A,d,B]T⇙"
proof-
  have "{e'. (Vx : A  e'e : B)  Axioms.Theory T} = {e'. (Vx : A  e'd : B)  Axioms.Theory T}"
    using assms by(blast intro: Axioms.Trans Axioms.Symm)
  thus ?thesis by(auto simp add: TermEquivCl_def TermEquivCl'_def TermEquivClGen_def)
qed

lemma Cl2Equiv: 
  assumes axt: "ZFAxioms T" and sa: "Sig aST (Vx : A  e : B)" and cl: "[A,e,B]T= [A,d,B]T⇙"
  shows "(Vx : A  e  d : B)  Axioms.Theory T"
proof-
  have "ZF2m T (m2ZF (TermEquivCl' T A e B)) = ZF2m T (m2ZF (TermEquivCl' T A d B))" using cl by (simp add: TermEquivCl_def)
  hence a:"TermEquivCl' T A e B = TermEquivCl' T A d B" using assms by (simp add: ZF2m)
  have "(Vx : A  e  e : B)  Axioms.Theory T" using axt sa Axioms.Refl[of T] by simp
  hence "e  TermEquivClGen T A e B" by (simp add: TermEquivClGen_def)
  hence "e  TermEquivClGen T A d B" using a by (simp add: TermEquivCl'_def)
  thus ?thesis by (simp add: TermEquivClGen_def)
qed 

lemma CanonicalCompWellDefined: 
  assumes zaxt: "ZFAxioms T" and "Sig aST (Vx : A  d : B)" and "Sig aST (Vx : B  d' : C)" 
  shows "CanonicalComp T [A,d,B]T[B,d',C]T= [A,sub d in d',C]T⇙"
proof((simp only: zaxt CanonicalComp_def CLDomain CLCodomain),(rule the_equality),
    (rule exI[of _ d], rule exI[of _ d'], auto))
  fix e e' assume de: "[A,d,B]T= [A,e,B]T⇙" and de': "[B,d',C]T= [B,e',C]T⇙"
  have axt: "Axioms T" using assms by simp
  have a: "(Vx : A  d  e : B)  Axioms.Theory T" using assms de Cl2Equiv by simp
  hence sa: "(Vx : A  (sub d in d')  (sub e in d') : C)  Axioms.Theory T" 
    using assms Axioms.Subst'[of T] by simp
  have b: "(Vx : B  d' e' : C)  Axioms.Theory T" using assms de' Cl2Equiv by simp
  have "Sig aST (Vx : A  d  e : B)" using a axt Axioms.Equiv2WellDefined[of T] by simp
  hence "Sig aST (Vx : A  e : B)" by auto
  hence "(Vx : A  (sub e in d')  (sub e in e') : C)  Axioms.Theory T" using b Axioms.Subst[of T] axt by simp
  hence "(Vx : A  (sub e in e')  (sub d in d') : C)  Axioms.Theory T" using sa axt
    by (blast intro: Axioms.Symm[of T] Axioms.Trans[of T])
  thus "[A,sub e in e',C]T= [A,sub d in d',C]T⇙" using zaxt Equiv2Cl by simp
qed

definition "CanonicalCat' T  
  Obj = BaseTypes (aST), 
  Mor = {[A,e,B]T| A e B . Sig aST (Vx : A  e : B)}, 
  Dom = CLDomain T, 
  Cod = CLCodomain T, 
  Id  = (λ A . [A,Vx,A]T), 
  Comp = CanonicalComp T
  "

definition "CanonicalCat T  MakeCat (CanonicalCat' T)"

lemma CanonicalCat'MapsTo: 
  assumes "f mapsCanonicalCat' TX to Y" and zx: "ZFAxioms T"
  shows " ef . f = [X,ef,Y]T Sig (aSignature T)  (Vx : X  ef : Y)"
proof-
  have fm: "f  Mor (CanonicalCat' T)" and fd: "Dom (CanonicalCat' T) f = X" and fc: "Cod (CanonicalCat' T) f = Y"
    using assms by auto
  from fm obtain ef A B where ef: "f = [A,ef,B]T⇙" and efsig: "Sig (aSignature T)  (Vx : A  ef : B)" 
    by (auto simp add: CanonicalCat'_def)
  have "A = X" and "B = Y" using fd fc ef zx CLDomain[of T] CLCodomain[of T]  by (simp add: CanonicalCat'_def)+
  thus ?thesis using ef efsig by auto
qed

lemma CanonicalCatCat': "ZFAxioms T  Category_axioms (CanonicalCat' T)"
proof(auto simp only: Category_axioms_def)
  have obj: "objCanonicalCat' T= BaseTypes (aSignature T)" by (simp add: CanonicalCat'_def)
  assume zx: "ZFAxioms T"
  hence axt: "Axioms T" by simp
  {
    fix f assume a: "f  morCanonicalCat' T⇙" 
    from a obtain A e B where f: "f = [A,e,B]T⇙" and fwd: "Sig (aSignature T)  (Vx : A  e : B)"
      by (auto simp add: CanonicalCat'_def)
    have domf: "domCanonicalCat' Tf = CLDomain T f" and codf: "codCanonicalCat' Tf = CLCodomain T f" 
      by (simp add: CanonicalCat'_def)+
    have absig: "A  TyaSignature T B  TyaSignature T⇙" using fwd Signature.SigTy[of "(aSignature T)"] Axioms.AxSig axt
      by auto
    have Awd: "Sig (aSignature T)  (Vx : A  Vx : A)" and Bwd: "Sig (aSignature T)  (Vx : B  Vx : B)" 
      using absig by auto
    show "domCanonicalCat' Tf  objCanonicalCat' T⇙" using domf f obj CLDomain[of T A e B] absig zx
      by simp
    show "codCanonicalCat' Tf  objCanonicalCat' T⇙" using codf f obj CLCodomain[of T A e B] absig zx
      by simp
    have idA: "Id (CanonicalCat' T) A = [A,Vx,A]T⇙" and idB: "Id (CanonicalCat' T) B = [B,Vx,B]T⇙" 
      by (simp add: CanonicalCat'_def)+
    have "(Id (CanonicalCat' T) (domCanonicalCat' Tf)) ;;CanonicalCat' Tf = [A, sub Vx in e, B]T⇙" 
      using f domf CLDomain[of T A e B] idA axt CanonicalCompWellDefined[of T] Awd fwd zx
      by (simp add: CanonicalCat'_def)
    thus "(Id (CanonicalCat' T) (domCanonicalCat' Tf)) ;;CanonicalCat' Tf = f" using f SubstXinE[of e] by simp
    have "f ;;CanonicalCat' T(Id (CanonicalCat' T) (codCanonicalCat' Tf)) = [A, sub e in Vx, B]T⇙" 
      using f codf CLCodomain[of T A e B] idB axt CanonicalCompWellDefined[of T] Bwd fwd zx
      by (simp add: CanonicalCat'_def)
    thus "f ;;CanonicalCat' T(Id (CanonicalCat' T) (codCanonicalCat' Tf)) = f" using f Subst_def by simp
  }
  {
    fix X assume a: "X  objCanonicalCat' T⇙"
    have "X  BaseTypes (aSignature T)" using a by (simp add: CanonicalCat'_def)
    hence b: "Sig (aSignature T)  (Vx : X  Vx : X)" by auto
    show "Id (CanonicalCat' T) X mapsCanonicalCat' TX to X"
      apply(rule MapsToI)
      apply(auto simp add: CanonicalCat'_def CLDomain CLCodomain zx)
      apply(rule exI)+
      apply(auto simp add: b)
      done
  }
  {
    fix f g h assume a: "f ≈>CanonicalCat' Tg" and b: "g ≈>CanonicalCat' Th"
    from a b have fm: "f  Mor (CanonicalCat' T)" and gm: "g  Mor (CanonicalCat' T)" 
      and hm: "h  Mor (CanonicalCat' T)" and fg: "Cod (CanonicalCat' T) f = Dom (CanonicalCat' T) g" 
      and gh: "Cod (CanonicalCat' T) g = Dom (CanonicalCat' T) h" by auto
    from fm obtain A ef B where f: "f = [A,ef,B]T⇙" and fwd: "Sig (aSignature T)  (Vx : A  ef : B)"
      by (auto simp add: CanonicalCat'_def)
    from gm obtain B' eg C where g: "g = [B',eg,C]T⇙" and gwd: "Sig (aSignature T)  (Vx : B'  eg : C)"
      by (auto simp add: CanonicalCat'_def)
    from hm obtain C' eh D where h: "h = [C',eh,D]T⇙" and hwd: "Sig (aSignature T)  (Vx : C'  eh : D)"
      by (auto simp add: CanonicalCat'_def)
    from fg have Beq: "B = B'" using f g zx CLCodomain[of T A ef B] CLDomain[of T B' eg C] by (simp add: CanonicalCat'_def)
    from gh have Ceq: "C = C'" using g h zx CLCodomain[of T B' eg C] CLDomain[of T C' eh D] by (simp add: CanonicalCat'_def)
    have "CanonicalComp T (CanonicalComp T f g) h = CanonicalComp T f (CanonicalComp T g h)"
    proof-
      have "(CanonicalComp T f g) = [A,sub ef in eg,C]T⇙" 
        using axt fwd gwd Beq zx CanonicalCompWellDefined[of T A ef B eg C] f g by simp
      moreover have "Sig aST Vx : A  sub ef in eg : C" using fwd gwd SubstWellDefined Beq by simp
      ultimately have a: "CanonicalComp T (CanonicalComp T f g) h = [A,(sub (sub ef in eg) in eh),D]T⇙"
        using CanonicalCompWellDefined[of T A "sub ef in eg" C eh D] axt hwd h Beq Ceq zx by simp
      have "(CanonicalComp T g h) = [B,sub eg in eh,D]T⇙"
        using axt gwd hwd Ceq Beq CanonicalCompWellDefined[of T B eg C eh D] g h zx by simp
      moreover have "Sig aST Vx : B  sub eg in eh : D" using gwd hwd SubstWellDefined Beq Ceq by simp
      ultimately have b: "CanonicalComp T f (CanonicalComp T g h) = [A,(sub ef in (sub eg in eh)),D]T⇙"
        using CanonicalCompWellDefined[of T A ef B "sub eg in eh" D] axt fwd f zx by simp
      show ?thesis using a b by (simp add: SubstAssoc)
    qed
    thus "(f ;;CanonicalCat' Tg) ;;CanonicalCat' Th = f ;;CanonicalCat' T(g ;;CanonicalCat' Th)"
      by(simp add: CanonicalCat'_def)
  }
  {
    fix f X Y g Z assume a: "f mapsCanonicalCat' TX to Y" and b: "g mapsCanonicalCat' TY to Z"
    from a CanonicalCat'MapsTo[of T f X Y] obtain ef 
      where f: "f = [X,ef,Y]T⇙" and fwd: "Sig (aSignature T)  (Vx : X  ef : Y)" using zx by auto
    from b CanonicalCat'MapsTo[of T g Y Z] obtain eg
      where g: "g = [Y,eg,Z]T⇙" and gwd: "Sig (aSignature T)  (Vx : Y  eg : Z)" using zx by auto
    have fg: "CanonicalComp T f g = [X,sub ef in eg,Z]T⇙" 
      using CanonicalCompWellDefined[of T X ef Y eg Z] f g fwd gwd zx by simp
    have fgwd: "Sig (aSignature T)  (Vx : X  sub ef in eg : Z)" 
      using fwd gwd SubstWellDefined[of "aST⇙"] by simp
    have "(CanonicalComp T f g) mapsCanonicalCat' TX to Z"
    proof(rule MapsToI)
      show "Dom (CanonicalCat' T) (CanonicalComp T f g) = X" 
        using fg CLDomain[of T] zx by (simp add: CanonicalCat'_def)
      show "CanonicalComp T f g  Mor (CanonicalCat' T)" using fg fgwd by (auto simp add: CanonicalCat'_def)
      show "Cod (CanonicalCat' T) (CanonicalComp T f g) = Z" 
        using fg CLCodomain[of T] zx by (simp add: CanonicalCat'_def)
    qed
    thus "f ;;CanonicalCat' Tg mapsCanonicalCat' TX to Z" by (simp add: CanonicalCat'_def)
  }
qed

lemma CanonicalCatCat: "ZFAxioms T  Category (CanonicalCat T)"
by (simp add: CanonicalCat_def CanonicalCatCat' MakeCat)

definition CanonicalInterpretation where 
"CanonicalInterpretation T  
  ISignature = aSignature T,
  ICategory  = CanonicalCat T,
  ITypes     = λ A . A,
  IFunctions = λ f . [SigDom (aSignature T) f, f E@ Vx, SigCod (aSignature T) f]T"

abbreviation "CI T  CanonicalInterpretation T"

lemma CIObj: "Obj (CanonicalCat T) = BaseTypes (aSignature T)"
by (simp add: MakeCat_def CanonicalCat_def CanonicalCat'_def)

lemma CIMor: "ZFAxioms T  [A,e,B]T Mor (CanonicalCat T) = Sig (aSignature T)  (Vx : A  e : B)"
proof(auto simp add: MakeCat_def CanonicalCat_def CanonicalCat'_def)
  fix A' e' B' assume zx: "ZFAxioms T" and b: "[A,e,B]T= [A',e',B']T⇙" and c: "Sig aST Vx : A'  e' : B'"
  have "CLDomain T [A,e,B]T= CLDomain T [A',e',B']T⇙" 
    and "CLCodomain T [A,e,B]T= CLCodomain T [A',e',B']T⇙" using b by simp+
  hence "A = A'" and "B = B'" by (simp add: CLDomain CLCodomain zx)+
  hence "(Vx : A  e'  e : B)  Axioms.Theory T" using zx b c Cl2Equiv[of T A e' B e] by simp
  hence "Sig aST (Vx : A  e'  e : B)" using Axioms.Equiv2WellDefined[of T] zx by simp
  thus "Sig aST Vx : A  e : B" by auto
qed

lemma CIDom: "ZFAxioms T ; [A,e,B]T Mor(CanonicalCat T)   Dom (CanonicalCat T) [A,e,B]T= A"
proof-
  assume "[A,e,B]T Mor(CanonicalCat T)" and "ZFAxioms T"
  thus "Dom (CanonicalCat T) [A,e,B]T= A" 
    by (simp add: CLDomain MakeCatMor CanonicalCat_def MakeCat_def CanonicalCat'_def)
qed

lemma CICod: "ZFAxioms T ; [A,e,B]T Mor(CanonicalCat T)  Cod (CanonicalCat T) [A,e,B]T= B"
proof-
  assume "[A,e,B]T Mor(CanonicalCat T)" and "ZFAxioms T"
  thus "Cod (CanonicalCat T) [A,e,B]T= B" 
    by (simp add: CLCodomain MakeCatMor CanonicalCat_def MakeCat_def CanonicalCat'_def)
qed

lemma CIId: "A  BaseTypes (aSignature T)  Id (CanonicalCat T) A = [A,Vx,A]T⇙"
by(simp add: MakeCat_def CanonicalCat_def CanonicalCat'_def)

lemma CIComp: 
  assumes "ZFAxioms T" and "Sig (aSignature T)  (Vx : A  e : B)" and "Sig (aSignature T)  (Vx : B  d : C)"
  shows "[A,e,B]T;;CanonicalCat T[B,d,C]T= [A,sub e in d,C]T⇙"
proof-
  have "[A,e,B]T≈>CanonicalCat' T[B,d,C]T⇙"
  proof(rule CompDefinedI)
    show "[A,e,B]T Mor (CanonicalCat' T)" and "[B,d,C]T Mor (CanonicalCat' T)"
      using assms by (auto simp add:  CanonicalCat'_def)
    have "codCanonicalCat' T[A,e,B]T= B" using assms by (simp add: CanonicalCat'_def CLCodomain)
    moreover have "domCanonicalCat' T[B,d,C]T= B" using assms by (simp add: CanonicalCat'_def CLDomain)
    ultimately show "codCanonicalCat' T[A,e,B]T= domCanonicalCat' T[B,d,C]T⇙" by simp
  qed
  hence "[A,e,B]T;;CanonicalCat T[B,d,C]T= [A,e,B]T;;CanonicalCat' T[B,d,C]T⇙"
    by (auto simp add: MakeCatComp CanonicalCat_def)
  thus "[A,e,B]T;;CanonicalCat T[B,d,C]T= [A, sub e in d, C]T⇙" 
    using CanonicalCompWellDefined[of T] assms by (simp add: CanonicalCat'_def)
qed

lemma [simp]: "ZFAxioms T  Category iCCI T⇙" by(simp add: CanonicalInterpretation_def CanonicalCatCat[of T])
lemma [simp]: "ZFAxioms T  Signature iSCI T⇙" by(simp add: CanonicalInterpretation_def Axioms.AxSig)

lemma CIInterpretation: "ZFAxioms T  Interpretation (CI T)"
proof(auto simp only: Interpretation_def)
  assume xt: "ZFAxioms T"
  show "Category iCCI T⇙" and "Signature iSCI T⇙" using xt by simp+
  {
    fix A assume "A  BaseTypes (iSCI T)" thus "Ty⟦ACI T Obj (iCCI T)"
      by(simp add: CanonicalInterpretation_def CIObj[of T])
  }
  {
    fix f A B assume a: "f  Sig iSCI T: A  B"
    hence "[sDomISignature (CI T)f,f E@ Vx,sCodISignature (CI T)f]T morCanonicalCat T⇙"
      using xt by(auto simp add: CanonicalInterpretation_def CIMor)
    thus "Fn⟦fCI TmapsICategory (CI T)Ty⟦ACI Tto Ty⟦BCI T⇙" using a xt
      by(auto simp add: CanonicalInterpretation_def MapsTo_def funsignature_abbrev_def CIDom CICod)
  }
qed

lemma CIInterp2Mor: "ZFAxioms T  ( B . Sig iSCI T (Vx : A  e : B)   L⟦Vx : A  e : BCI T (IMor [A, e, B]T))"
proof(induct e)
  assume xt: "ZFAxioms T"
  {
    fix B assume a: "Sig iSCI T Vx : A  Vx : B" 
    have aeqb: "A = B" using a SigId[of "iSCI T⇙" A B] Interpretation.InterpExprWellDefined[of "CI T"] by simp
    moreover have bt: "A  BaseTypes iSCI T⇙" using a SigTyId aeqb by simp
    ultimately have b: "L⟦Vx : A  Vx : BCI T (IMor (Id iCCI TTy⟦ACI T))" by auto
    have "Ty⟦ACI T= A" by (simp add: CanonicalInterpretation_def)
    hence "(Id iCCI TTy⟦ACI T) = [A,Vx,A]T⇙" using bt CIId by(simp add: CanonicalInterpretation_def)
    thus "L⟦Vx : A  Vx : BCI T (IMor [A,Vx,B]T)" using aeqb b by simp
  }
  {
    fix f e B assume ih: "B'. ZFAxioms T ; Sig iSCI T (Vx : A  e : B')  (L⟦Vx : A  e : B'CI T (IMor [A,e,B']T))"
    and a: "Sig iSCI T Vx : A  f E@ e : B"
    from a obtain B' where sig: "Sig iSCI T (Vx : A  e : B')" and f: "f  Sig iSCI T: B'  B" by auto 
    hence "L⟦Vx : A  e : B'CI T (IMor [A,e,B']T)" using ih xt by auto
    hence b: "L⟦Vx : A  f E@ e : BCI T (IMor ([A,e,B']T;;ICategory (CI T)Fn⟦fCI T))" using sig f by auto
    have "[A,e,B']T;;ICategory (CI T)Fn⟦fCI T= [A,f E@ e,B]T⇙" 
    proof-
      have aa: "Fn⟦fCI T= [B', f E@ Vx, B]T⇙" using f by (simp add: CanonicalInterpretation_def funsignature_abbrev_def)
      have "Sig iSCI T Vx : A  e : B'" and "Sig iSCI T Vx : B'  f E@ Vx : B"  using sig f by auto
      hence "[A,e,B']T;;ICategory (CI T)[B', f E@ Vx, B]T= [A, sub e in (f E@ Vx), B]T⇙" 
        using CIComp[of T] xt by (simp add: CanonicalInterpretation_def)
      moreover have "sub e in (f E@ Vx) = f E@ e" by (auto simp add: Subst_def)
      ultimately show ?thesis using aa by simp
    qed
    thus "L⟦Vx : A  f E@ e : BCI T (IMor [A,f E@ e,B]T)" using b by simp
  }
qed

lemma CIModel: "ZFAxioms T  Model (CI T) T"
proof(auto simp add: Model_def Model_axioms_def )
  assume xt: "ZFAxioms T"
  have axt: "Axioms T" using xt by simp
  show ii: "Interpretation (CI T)" using xt by (simp add: CIInterpretation)
  show aeq: "aST= iSCI T⇙" by (simp add: CanonicalInterpretation_def)
  {
    fix φ assume a: "φ  aAxioms T"
    from a Axioms.AxT obtain A B e d where φ: "φ = Vx : A  e  d : B" and sig: "Sig aST Vx : A  e  d : B" 
      using axt by blast
    have "Sig aST Vx : A  e : B" using sig by auto
    hence e: "L⟦Vx : A  e : BCI T (IMor [A, e, B]T)" using aeq CIInterp2Mor xt by simp
    have "Sig aST Vx : A  d : B" using sig by auto
    hence d: "L⟦Vx : A  d : BCI T (IMor [A, d, B]T)" using aeq CIInterp2Mor xt by simp
    have "φ  Axioms.Theory T" using a axt by (simp add: Axioms.Theory.Ax)
    hence "[A, e, B]T= [A, d, B]T⇙" using φ Equiv2Cl axt by simp
    thus "L⟦φCI T (IBool True)" using e d φ ii InterpEq[of "CI T" A e B "[A, e, B]T⇙" d "[A, d, B]T⇙"] by simp
  }
qed

lemma CIComplete: assumes "ZFAxioms T" and "L⟦φCI T (IBool True)" shows "φ  Axioms.Theory T"
proof-
  have ii: "Interpretation (CI T)" using assms by (simp add: CIInterpretation)
  hence aeq: "aST= iSCI T⇙" by (simp add: CanonicalInterpretation_def)
  from Interpretation.Bool[of "CI T" φ True] obtain A B e d where φ: "φ = (Vx : A  e  d : B)" using ii assms by auto
  from Interpretation.Equiv[of "CI T" A e d B] obtain g 
    where g1: "L⟦Vx : A  e : BCI T (IMor g)" 
    and   g2: "L⟦Vx : A  d : BCI T (IMor g)" using ii φ assms by auto
  have ewd: "Sig iSCI T (Vx : A  e : B)" and dwd: "Sig iSCI T (Vx : A  d : B)" 
    using g1 g2 Interpretation.InterpExprWellDefined[of "CI T"] ii by simp+
  have ie: "L⟦Vx : A  e : BCI T (IMor [A, e, B]T)" using ewd CIInterp2Mor assms by simp
  have id: "L⟦Vx : A  d : BCI T (IMor [A, d, B]T)" using dwd CIInterp2Mor assms by simp
  have "[A, e, B]T= g" 
    using g1 ie ii Interpretation.Functional[of "CI T" "Vx : A  e : B" "IMor [A, e, B]T⇙" "IMor g"] by simp
  moreover have "[A, d, B]T= g" 
    using g2 id ii Interpretation.Functional[of "CI T" "Vx : A  d : B" "IMor [A, d, B]T⇙" "IMor g"] by simp
  ultimately have "[A, e, B]T= [A, d, B]T⇙" by simp
  thus ?thesis using φ ewd Cl2Equiv aeq assms by simp
qed

lemma Complete: 
  assumes "ZFAxioms T" 
  and " (I :: (ZF,ZF,ZF,ZF) Interpretation) . Model I T  (L⟦φI (IBool True))" 
  shows "φ  Axioms.Theory T"
proof-
  have "Model (CI T) T" using assms CIModel by simp
  thus ?thesis using CIComplete[of T φ] assms by auto
qed

end