Isabelle/ZF proof of consistency of STLC

STLC.thy

theory Scratch
  imports ZF
begin

consts ty :: "i" 
datatype "ty" 
  = TyNat 
  | TyBool
  | TyArr ("τ ∈ ty", "υ ∈ ty") 

consts tySem :: "i⇒i"
primrec
  "tySem(TyNat)       = nat"
  "tySem(TyBool)      = bool"
  "tySem(TyArr(τ, υ)) = tySem(τ) → tySem(υ)"

definition sTy :: i where
  "sTy = ⋃  { tySem(x). x∈ty }"

consts ctx :: "i" 
datatype "ctx" 
  = CtxEmpty 
  | CtxCons ("τ ∈ ty", "Γ ∈ ctx") 

consts ctxSem :: "i⇒i"
primrec
  "ctxSem(CtxEmpty)      = {0}"
  "ctxSem(CtxCons(τ, Γ)) = ctxSem(Γ) × tySem(τ)"

definition sCtx :: i where
  "sCtx = ⋃ { ctxSem(x). x∈ctx }"

consts ref :: "i" 
inductive 
  domains "ref" ⊆ "ctx × nat × ty" 
  intros 
    RefHere: "⟦ Γ ∈ ctx; τ ∈ ty ⟧
         ⟹ < CtxCons(τ, Γ), 0, τ > ∈ ref"
    RefThere: "⟦ <Γ, n, τ> ∈ ref; υ ∈ ty; n ∈ nat ⟧
          ⟹ < CtxCons(υ, Γ), succ(n), τ > ∈ ref"
  type_intros ctx.intros nat_typechecks ty.intros


definition lookupCtx :: "[i,i] ⇒ i" where
  "lookupCtx(n, γ) ≡ snd(nat_rec(n, γ, λ n rec. fst(rec)))"

lemma lookupCtx_0 [simp]:
  "lookupCtx(0, <γ , t>) = t"
  using lookupCtx_def nat_rec_0
  by auto

lemma nat_rec_proj :
  assumes nnat: "n ∈ nat"
  shows "fst(nat_rec(n, ⟨γ, t⟩, λn. fst))
         = nat_rec(n, γ, λn . fst)"
using nnat
proof (induct n rule: nat_induct)
  case 0
  then show ?case
    using nat_rec_0
    by auto
  case succ
  then show ?case
    using nat_rec_succ
    by auto
qed

lemma lookupCtx_cons [simp]:
  assumes nnat: "n ∈ nat"
  shows "lookupCtx(succ(n), <γ, t>) = lookupCtx(n, γ)"
using nnat
proof (induct n rule: nat_induct)
  case 0
  then show ?case
    using lookupCtx_def nat_rec_0 nat_rec_succ
    by auto
  case succ
  then show ?case
    using lookupCtx_def nat_rec_succ nat_rec_proj
    by auto
qed

lemma lookupCtx_sound: 
  assumes wref: "<Γ, n, τ> ∈ ref"
  assumes γsem: "γ ∈ ctxSem(Γ)"
  shows "lookupCtx(n, γ) ∈ tySem(τ)"
using wref γsem
proof (induct arbitrary: γ rule: ref.induct)
  case RefHere
  then show ?case
    by auto
next
  case RefThere
  then show ?case
    by auto
qed

consts tm :: "i" 
datatype "tm" 
  = TmVar ("n ∈ nat") 
  | TmLam ("dom ∈ ty", "body ∈ tm") 
  | TmApp ("fun ∈ tm", "arg ∈ tm") 
  | TmInt ("i ∈ nat")
  | TmBool ("b ∈ bool")
  | TmIte ("g ∈ tm", "t ∈ tm", "e ∈ tm")
  | TmWeak ("t ∈ tm") 

consts
  tmSem :: "i ⇒ i"
primrec
  "tmSem(TmVar(n))       = (λγ∈sCtx. lookupCtx(n, γ))"
  "tmSem(TmLam(τ, body)) = (λγ∈sCtx. λt∈tySem(τ). tmSem(body) ` <γ, t>)"
  "tmSem(TmApp(f, a))    = (λγ∈sCtx. (tmSem(f) ` γ) ` (tmSem(a) ` γ))"
  "tmSem(TmInt(i))       = (λγ∈sCtx. i)"
  "tmSem(TmBool(b))      = (λγ∈sCtx. b)"
  "tmSem(TmIte(g, t, e)) = (λγ∈sCtx. cond(tmSem(g)` γ, tmSem(t)` γ, tmSem(e)` γ))"
  "tmSem(TmWeak(t))      = (λγ∈sCtx. tmSem(t) ` fst(γ))"

definition sTm :: i where
  "sTm = ⋃ { tmSem(x). x∈tm }"

consts wt :: "i" inductive
  domains "wt" ⊆ "ctx × tm × ty"
  intros
    WtVar: "⟦ Γ ∈ ctx; n ∈ nat; τ ∈ ty; < Γ, n, τ > ∈ ref ⟧
       ⟹ < Γ, TmVar(n), τ > ∈ wt"
    WtLam: "⟦ Γ ∈ ctx; τ ∈ ty; < CtxCons(τ, Γ), body, υ > ∈ wt ⟧
       ⟹ < Γ, TmLam(τ, body), TyArr(τ, υ) > ∈ wt"
    WtApp: "⟦ Γ ∈ ctx; υ ∈ ty; < Γ, fun, TyArr(τ, υ) > ∈ wt; < Γ, arg, τ > ∈ wt ⟧
       ⟹ < Γ, TmApp(fun, arg), υ > ∈ wt"
    WtInt: "⟦ Γ ∈ ctx; i ∈ nat ⟧
       ⟹ < Γ, TmInt(i), TyNat > ∈ wt"
    WtBool: "⟦ Γ ∈ ctx; b ∈ bool ⟧
        ⟹ < Γ, TmBool(b), TyBool > ∈ wt"
    WtIte: "⟦Γ ∈ ctx; τ ∈ ty; <Γ, g, TyBool> ∈ wt; <Γ, t, τ> ∈ wt; <Γ, e, τ> ∈ wt⟧
       ⟹ <Γ, TmIte(g, t, e), τ> ∈ wt"
    WtWeak: "⟦Γ ∈ ctx; υ ∈ ty; < Γ, t, τ > ∈ wt⟧
       ⟹ <CtxCons(υ, Γ), TmWeak(t), τ> ∈ wt"
  type_intros ctx.intros tm.intros ty.intros ref.intros

lemma ctxSemSub:
  assumes Γctx: "Γ ∈ ctx"
  shows "ctxSem(Γ) ⊆ sCtx"
using Γctx
  unfolding sCtx_def
  by auto
  
lemma tmSem_const:
  assumes typTm: "<Γ, t, τ> ∈ wt"
  assumes gammaC: "γ ∈ ctxSem(Γ)"
  shows "tmSem(t) ` γ  ∈ tySem(τ)"
using typTm gammaC
proof(induct arbitrary: γ rule: wt.induct)
  case (WtVar Γ' τ' n)
  have "γ ∈ sCtx"
    using WtVar(1) WtVar(5) ctxSemSub
    by auto
  then show ?case
    using WtVar(4) WtVar(5) lookupCtx_sound
    by auto
next
  case (WtLam Γ' τ' υ body)
  have "γ ∈ sCtx"
    and "⋀ t. t ∈ tySem(τ') ⟹ tmSem(body) ` <γ, t> ∈ tySem(υ)"
    using WtLam(4) WtLam(5) WtLam(1) ctxSemSub
    by auto
  then show ?case
    using lam_type
    by auto
next
  case (WtApp Γ' τ' υ a f)
  have "γ ∈ sCtx"
   and "tmSem(f) ` γ ∈ tySem(τ') → tySem(υ)"
   and "tmSem(a) ` γ ∈ tySem(τ')"
    using WtApp(6) WtApp(7) WtApp(4) ctxSemSub WtApp(1)
    by auto
  then show ?case
    by auto
next
  case (WtInt Γ' i)
  have "γ ∈ sCtx"
    using WtInt(1) WtInt(3) ctxSemSub
    by auto
  then show ?case
    using WtInt(2)
    by auto
next
  case (WtBool Γ' b)
  have "γ ∈ sCtx"
    using WtBool(1) WtBool(3) ctxSemSub
    by auto
  then show ?case
    using WtBool(2)
    by auto
next
  case (WtIte Γ' τ' e g t)
  have "γ ∈ sCtx"
   and "tmSem(g) ` γ ∈ bool"
   and "tmSem(t) ` γ ∈ tySem(τ')"
   and "tmSem(e) ` γ ∈ tySem(τ')"
    using WtIte(1) WtIte(9) ctxSemSub WtIte(4) WtIte(6) WtIte(8)
    by auto
  then show ?case
    by auto
next
  case (WtWeak Γ' τ' υ t)
  have cctx: "CtxCons(υ, Γ') ∈ ctx"
    using WtWeak(2) WtWeak(1)
    by auto
  have "γ ∈ sCtx"
   and "fst(γ) ∈ ctxSem(Γ')"
    using cctx WtWeak(5) ctxSemSub[where Γ="CtxCons(υ, Γ')"]
    by auto
  then show ?case
    using WtWeak(4)
    by auto
qed