--- a/src/HOL/Nominal/Examples/Type_Preservation.thy Wed Jun 11 18:15:36 2008 +0200
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Thu Jun 12 09:37:13 2008 +0200
@@ -1,7 +1,17 @@
+(* $Id$ *)
+
theory Type_Preservation
imports Nominal
begin
+text {*
+
+ This theory shows how to prove the type preservation
+ property for the simply-typed lambda-calculus and
+ beta-reduction.
+
+*}
+
atom_decl name
nominal_datatype lam =
@@ -58,7 +68,7 @@
where
"\<Gamma>\<^isub>1 \<subseteq> \<Gamma>\<^isub>2 \<equiv> \<forall>x. x \<in> set \<Gamma>\<^isub>1 \<longrightarrow> x \<in> set \<Gamma>\<^isub>2"
-text {* Validity of typing contexts *}
+text {* Validity of Typing Contexts *}
inductive
valid :: "(name\<times>ty) list \<Rightarrow> bool"
@@ -92,7 +102,7 @@
using a1 a2 a3
by (induct) (auto simp add: fresh_set fresh_prod fresh_atm)
-text {* typing relation *}
+text {* Typing Relation *}
inductive
typing :: "ctx \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _")
@@ -159,7 +169,7 @@
using a b
by (auto intro: type_substitution_aux[where \<Delta>="[]",simplified])
-text {* Beta reduction *}
+text {* Beta Reduction *}
inductive
"beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _")