diff -r 0062c9e5c842 -r 28b264299590 LFex.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/LFex.thy	Fri Nov 06 19:26:08 2009 +0100
@@ -0,0 +1,175 @@
+theory LFex
+imports Nominal QuotMain
+begin
+
+atom_decl name id
+
+nominal_datatype kind = 
+    Type
+  | KPi "ty" "name" "kind"
+and ty =  
+    TConst "id"
+  | TApp "ty" "trm"
+  | TPi "ty" "name" "ty"
+and trm = 
+    Const "id"
+  | Var "name"
+  | App "trm" "trm"
+  | Lam "ty" "name" "trm" 
+
+function
+    fv_kind :: "kind \<Rightarrow> name set"
+and fv_ty   :: "ty \<Rightarrow> name set"
+and fv_trm  :: "trm \<Rightarrow> name set"
+where
+  "fv_kind (Type) = {}"
+| "fv_kind (KPi A x K) = (fv_ty A) \<union> ((fv_kind K) - {x})"
+| "fv_ty (TConst i) = {}"
+| "fv_ty (TApp A M) = (fv_ty A) \<union> (fv_trm M)"
+| "fv_ty (TPi A x B) = (fv_ty A) \<union> ((fv_ty B) - {x})"
+| "fv_trm (Const i) = {}"
+| "fv_trm (Var x) = {x}"
+| "fv_trm (App M N) = (fv_trm M) \<union> (fv_trm N)"
+| "fv_trm (Lam A x M) = (fv_ty A) \<union> ((fv_trm M) - {x})"
+sorry
+
+termination fv_kind sorry
+
+inductive
+    akind :: "kind \<Rightarrow> kind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
+and aty   :: "ty \<Rightarrow> ty \<Rightarrow> bool"     ("_ \<approx>ty _" [100, 100] 100)
+and atrm  :: "trm \<Rightarrow> trm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
+where
+  a1:  "(Type) \<approx>ki (Type)"
+| a21: "\<lbrakk>A \<approx>ty A'; K \<approx>ki K'\<rbrakk> \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x K')"
+| a22: "\<lbrakk>A \<approx>ty A'; K \<approx>ki ([(x,x')]\<bullet>K'); x \<notin> (fv_ty A'); x \<notin> ((fv_kind K') - {x'})\<rbrakk> 
+        \<Longrightarrow> (KPi A x K) \<approx>ki (KPi A' x' K')"
+| a3:  "i = j \<Longrightarrow> (TConst i) \<approx>ty (TConst j)"
+| a4:  "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>ty (TApp A' M')"
+| a51: "\<lbrakk>A \<approx>ty A'; B \<approx>ty B'\<rbrakk> \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x B')"
+| a52: "\<lbrakk>A \<approx>ty A'; B \<approx>ty ([(x,x')]\<bullet>B'); x \<notin> (fv_ty B'); x \<notin> ((fv_ty B') - {x'})\<rbrakk> 
+        \<Longrightarrow> (TPi A x B) \<approx>ty (TPi A' x' B')"
+| a6:  "i = j \<Longrightarrow> (Const i) \<approx>trm (Const j)"
+| a7:  "x = y \<Longrightarrow> (Var x) \<approx>trm (Var y)"
+| a8:  "\<lbrakk>M \<approx>trm M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
+| a91: "\<lbrakk>A \<approx>ty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x M')"
+| a92: "\<lbrakk>A \<approx>ty A'; M \<approx>tr ([(x,x')]\<bullet>M'); x \<notin> (fv_ty B'); x \<notin> ((fv_trm M') - {x'})\<rbrakk> 
+        \<Longrightarrow> (Lam A x M) \<approx>tr (Lam A' x' M')"
+
+lemma al_refl:
+  fixes K::"kind" 
+  and   A::"ty"
+  and   M::"trm"
+  shows "K \<approx>ki K"
+  and   "A \<approx>ty A"
+  and   "M \<approx>tr M"
+  apply(induct K and A and M rule: kind_ty_trm.inducts)
+  apply(auto intro: akind_aty_atrm.intros)
+  done
+
+lemma alpha_EQUIVs:
+  shows "EQUIV akind"
+  and   "EQUIV aty"
+  and   "EQUIV atrm"
+sorry
+
+quotient KIND = kind / akind
+  by (rule alpha_EQUIVs)
+
+quotient TY = ty / aty
+   and   TRM = trm / atrm
+  by (auto intro: alpha_EQUIVs)
+
+print_quotients
+
+quotient_def 
+  TYP :: "KIND"
+where
+  "TYP \<equiv> Type"
+
+quotient_def 
+  KPI :: "TY \<Rightarrow> name \<Rightarrow> KIND \<Rightarrow> KIND"
+where
+  "KPI \<equiv> KPi"
+
+quotient_def 
+  TCONST :: "id \<Rightarrow> TY"
+where
+  "TCONST \<equiv> TConst"
+
+quotient_def 
+  TAPP :: "TY \<Rightarrow> TRM \<Rightarrow> TY"
+where
+  "TAPP \<equiv> TApp"
+
+quotient_def 
+  TPI :: "TY \<Rightarrow> name \<Rightarrow> TY \<Rightarrow> TY"
+where
+  "TPI \<equiv> TPi"
+
+(* FIXME: does not work with CONST *)
+quotient_def 
+  CONS :: "id \<Rightarrow> TRM"
+where
+  "CONS \<equiv> Const"
+
+quotient_def 
+  VAR :: "name \<Rightarrow> TRM"
+where
+  "VAR \<equiv> Var"
+
+quotient_def 
+  APP :: "TRM \<Rightarrow> TRM \<Rightarrow> TRM"
+where
+  "APP \<equiv> App"
+
+quotient_def 
+  LAM :: "TY \<Rightarrow> name \<Rightarrow> TRM \<Rightarrow> TRM"
+where
+  "LAM \<equiv> Lam"
+
+thm TYP_def
+thm KPI_def
+thm TCONST_def
+thm TAPP_def
+thm TPI_def
+thm VAR_def
+thm CONS_def
+thm APP_def
+thm LAM_def
+
+(* FIXME: print out a warning if the type contains a liftet type, like kind \<Rightarrow> name set *)
+quotient_def 
+  FV_kind :: "KIND \<Rightarrow> name set"
+where
+  "FV_kind \<equiv> fv_kind"
+
+quotient_def 
+  FV_ty :: "TY \<Rightarrow> name set"
+where
+  "FV_ty \<equiv> fv_ty"
+
+quotient_def 
+  FV_trm :: "TRM \<Rightarrow> name set"
+where
+  "FV_trm \<equiv> fv_trm"
+
+thm FV_kind_def
+thm FV_ty_def
+thm FV_trm_def
+
+(* FIXME: does not work yet *)
+(*
+overloading
+    perm_kind \<equiv> "perm :: 'x prm \<Rightarrow> KIND \<Rightarrow> KIND"   (unchecked)
+    perm_ty   \<equiv> "perm :: 'x prm \<Rightarrow> TY \<Rightarrow> TY"       (unchecked)
+    perm_trm  \<equiv> "perm :: 'x prm \<Rightarrow> TRM \<Rightarrow> TRM"     (unchecked) 
+begin
+
+quotient_def 
+  perm_kind :: "'x prm \<Rightarrow> KIND \<Rightarrow> KIND"
+where
+  "perm_kind \<equiv> (perm::'x prm \<Rightarrow> KIND \<Rightarrow> KIND)"
+end
+*)
+