Theory Class1

theory Class1
imports "HOL-Nominal.Nominal" 
begin

section ‹Term-Calculus from Urban's PhD›

atom_decl name coname

text ‹types›

no_notation not  ("NOT")

nominal_datatype ty =
    PR "string"
  | NOT  "ty"
  | AND  "ty" "ty"   ("_ AND _" [100,100] 100)
  | OR   "ty" "ty"   ("_ OR _" [100,100] 100)
  | IMP  "ty" "ty"   ("_ IMP _" [100,100] 100)

instantiation ty :: size
begin

nominal_primrec size_ty
where
  "size (PR s)     = (1::nat)"
| "size (NOT T)     = 1 + size T"
| "size (T1 AND T2) = 1 + size T1 + size T2"
| "size (T1 OR T2)  = 1 + size T1 + size T2"
| "size (T1 IMP T2) = 1 + size T1 + size T2"
by (rule TrueI)+

instance ..

end

lemma ty_cases:
  fixes T::ty
  shows "(s. T=PR s)  (T'. T=NOT T')  (S U. T=S OR U)  (S U. T=S AND U)  (S U. T=S IMP U)"
by (induct T rule:ty.induct) (auto)

lemma fresh_ty:
  fixes a::"coname"
  and   x::"name"
  and   T::"ty"
  shows "aT" and "xT"
by (nominal_induct T rule: ty.strong_induct)
   (auto simp add: fresh_string)

text ‹terms›

nominal_datatype trm = 
    Ax   "name" "coname"
  | Cut  "«coname»trm" "«name»trm"            ("Cut <_>._ (_)._" [100,100,100,100] 100)
  | NotR "«name»trm" "coname"                 ("NotR (_)._ _" [100,100,100] 100)
  | NotL "«coname»trm" "name"                 ("NotL <_>._ _" [100,100,100] 100)
  | AndR "«coname»trm" "«coname»trm" "coname" ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
  | AndL1 "«name»trm" "name"                  ("AndL1 (_)._ _" [100,100,100] 100)
  | AndL2 "«name»trm" "name"                  ("AndL2 (_)._ _" [100,100,100] 100)
  | OrR1 "«coname»trm" "coname"               ("OrR1 <_>._ _" [100,100,100] 100)
  | OrR2 "«coname»trm" "coname"               ("OrR2 <_>._ _" [100,100,100] 100)
  | OrL "«name»trm" "«name»trm" "name"        ("OrL (_)._ (_)._ _" [100,100,100,100,100] 100)
  | ImpR "«name»(«coname»trm)" "coname"       ("ImpR (_).<_>._ _" [100,100,100,100] 100)
  | ImpL "«coname»trm" "«name»trm" "name"     ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 100)

text ‹named terms›

nominal_datatype ntrm = Na "«name»trm" ("((_):_)" [100,100] 100)

text ‹conamed terms›

nominal_datatype ctrm = Co "«coname»trm" ("(<_>:_)" [100,100] 100)

text ‹renaming functions›

nominal_primrec (freshness_context: "(d::coname,e::coname)") 
  crename :: "trm  coname  coname  trm"  ("_[_⊢c>_]" [100,100,100] 100) 
where
  "(Ax x a)[d⊢c>e] = (if a=d then Ax x e else Ax x a)" 
| "a(d,e,N);xM  (Cut <a>.M (x).N)[d⊢c>e] = Cut <a>.(M[d⊢c>e]) (x).(N[d⊢c>e])" 
| "(NotR (x).M a)[d⊢c>e] = (if a=d then NotR (x).(M[d⊢c>e]) e else NotR (x).(M[d⊢c>e]) a)" 
| "a(d,e)  (NotL <a>.M x)[d⊢c>e] = (NotL <a>.(M[d⊢c>e]) x)" 
| "a(d,e,N,c);b(d,e,M,c);ba  (AndR <a>.M <b>.N c)[d⊢c>e] = 
          (if c=d then AndR <a>.(M[d⊢c>e]) <b>.(N[d ⊢c>e]) e else AndR <a>.(M[d⊢c>e]) <b>.(N[d⊢c>e]) c)" 
| "xy  (AndL1 (x).M y)[d⊢c>e] = AndL1 (x).(M[d⊢c>e]) y"
| "xy  (AndL2 (x).M y)[d⊢c>e] = AndL2 (x).(M[d⊢c>e]) y"
| "a(d,e,b)  (OrR1 <a>.M b)[d⊢c>e] = (if b=d then OrR1 <a>.(M[d⊢c>e]) e else OrR1 <a>.(M[d⊢c>e]) b)"
| "a(d,e,b)  (OrR2 <a>.M b)[d⊢c>e] = (if b=d then OrR2 <a>.(M[d⊢c>e]) e else