# 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 "a♯T" and "x♯T"
by (nominal_induct T rule: ty.strong_induct)

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);x♯M⟧ ⟹ (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);b≠a⟧ ⟹ (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)"
| "x♯y ⟹ (AndL1 (x).M y)[d⊢c>e] = AndL1 (x).(M[d⊢c>e]) y"
| "x♯y ⟹ (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 ```