--- a/src/HOL/Nominal/Examples/Class.thy Tue Jan 31 18:19:36 2006 +0100
+++ b/src/HOL/Nominal/Examples/Class.thy Wed Feb 01 01:03:41 2006 +0100
@@ -3,16 +3,43 @@
imports "../nominal"
begin
+section {* Term-Calculus from Urban's PhD *}
+
atom_decl name coname
-section {* Term-Calculus from my PHD *}
+nominal_datatype trm =
+ Ax "name" "coname"
+ | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut <_>._ (_)._" [100,100,100,100] 100)
+ | NotR "\<guillemotleft>name\<guillemotright>trm" "coname" ("NotR (_)._ _" [100,100,100] 100)
+ | NotL "\<guillemotleft>coname\<guillemotright>trm" "name" ("NotL <_>._ _" [100,100,100] 100)
+ | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
+ | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL1 (_)._ _" [100,100,100] 100)
+ | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL2 (_)._ _" [100,100,100] 100)
+ | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR1 <_>._ _" [100,100,100] 100)
+ | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR2 <_>._ _" [100,100,100] 100)
+ | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("OrL (_)._ (_)._ _" [100,100,100,100,100] 100)
+ | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR (_).<_>._ _" [100,100,100,100] 100)
+ | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 100)
+
+
+text {* Induction principles *}
-nominal_datatype trm = Ax "name" "coname"
- | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR [_].[_]._ _" [100,100,100,100] 100)
- | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name"("ImpL [_]._ [_]._ _" [100,100,100,100,100] 100)
- | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut [_]._ [_]._" [100,100,100,100] 100)
+thm trm.induct_weak --"weak"
+thm trm.induct --"strong"
+thm trm.induct' --"strong with explicit context (rarely needed)"
+
+text {* named terms *}
+
+nominal_datatype ntrm = N "\<guillemotleft>name\<guillemotright>trm" ("N (_)._" [100,100] 100)
+
+text {* conamed terms *}
-thm trm.induct
-thm trm.inducts
-thm trm.induct'
+nominal_datatype ctrm = C "\<guillemotleft>coname\<guillemotright>trm" ("C <_>._" [100,100] 100)
+
+text {* We should now define the two forms of substitition :o( *}
+consts
+ substn :: "trm \<Rightarrow> name \<Rightarrow> ctrm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
+ substc :: "trm \<Rightarrow> coname \<Rightarrow> ntrm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
+
+text {* does not work yet *}
\ No newline at end of file