--- a/Quot/Nominal/LFex.thy	Wed Feb 24 09:58:44 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 10:08:54 2010 +0100
@@ -92,19 +92,19 @@
 *)
 
 primrec
-    rfv_rkind :: "rkind \<Rightarrow> atom set"
-and rfv_rty   :: "rty \<Rightarrow> atom set"
-and rfv_rtrm  :: "rtrm \<Rightarrow> atom set"
+    fv_rkind :: "rkind \<Rightarrow> atom set"
+and fv_rty   :: "rty \<Rightarrow> atom set"
+and fv_rtrm  :: "rtrm \<Rightarrow> atom set"
 where
-  "rfv_rkind (Type) = {}"
-| "rfv_rkind (KPi A x K) = (rfv_rty A) \<union> ((rfv_rkind K) - {atom x})"
-| "rfv_rty (TConst i) = {atom i}"
-| "rfv_rty (TApp A M) = (rfv_rty A) \<union> (rfv_rtrm M)"
-| "rfv_rty (TPi A x B) = (rfv_rty A) \<union> ((rfv_rty B) - {atom x})"
-| "rfv_rtrm (Const i) = {atom i}"
-| "rfv_rtrm (Var x) = {atom x}"
-| "rfv_rtrm (App M N) = (rfv_rtrm M) \<union> (rfv_rtrm N)"
-| "rfv_rtrm (Lam A x M) = (rfv_rty A) \<union> ((rfv_rtrm M) - {atom x})"
+  "fv_rkind (Type) = {}"
+| "fv_rkind (KPi A x K) = (fv_rty A) \<union> ((fv_rkind K) - {atom x})"
+| "fv_rty (TConst i) = {atom i}"
+| "fv_rty (TApp A M) = (fv_rty A) \<union> (fv_rtrm M)"
+| "fv_rty (TPi A x B) = (fv_rty A) \<union> ((fv_rty B) - {atom x})"
+| "fv_rtrm (Const i) = {atom i}"
+| "fv_rtrm (Var x) = {atom x}"
+| "fv_rtrm (App M N) = (fv_rtrm M) \<union> (fv_rtrm N)"
+| "fv_rtrm (Lam A x M) = (fv_rty A) \<union> ((fv_rtrm M) - {atom x})"
 
 inductive
     arkind :: "rkind \<Rightarrow> rkind \<Rightarrow> bool" ("_ \<approx>ki _" [100, 100] 100)
@@ -112,25 +112,25 @@
 and artrm  :: "rtrm \<Rightarrow> rtrm \<Rightarrow> bool"   ("_ \<approx>tr _" [100, 100] 100)
 where
   a1: "(Type) \<approx>ki (Type)"
-| a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
+| a2: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K'))\<rbrakk> \<Longrightarrow> (KPi A a K) \<approx>ki (KPi A' b K')"
 | a3: "i = j \<Longrightarrow> (TConst i) \<approx>rty (TConst j)"
 | a4: "\<lbrakk>A \<approx>rty A'; M \<approx>tr M'\<rbrakk> \<Longrightarrow> (TApp A M) \<approx>rty (TApp A' M')"
-| a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (TPi A' b B')"
+| a5: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))\<rbrakk> \<Longrightarrow> (TPi A a B) \<approx>rty (TPi A' b B')"
 | a6: "i = j \<Longrightarrow> (Const i) \<approx>tr (Const j)"
 | a7: "x = y \<Longrightarrow> (Var x) \<approx>tr (Var y)"
 | a8: "\<lbrakk>M \<approx>tr M'; N \<approx>tr N'\<rbrakk> \<Longrightarrow> (App M N) \<approx>tr (App M' N')"
-| a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
+| a9: "\<lbrakk>A \<approx>rty A'; \<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))\<rbrakk> \<Longrightarrow> (Lam A a M) \<approx>tr (Lam A' b M')"
 
 lemma arkind_arty_artrm_inj:
   "(Type) \<approx>ki (Type) = True"
-  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind rfv_rkind pi ({atom b}, K')))"
+  "((KPi A a K) \<approx>ki (KPi A' b K')) = ((A \<approx>rty A') \<and> (\<exists>pi. ({atom a}, K) \<approx>gen arkind fv_rkind pi ({atom b}, K')))"
   "(TConst i) \<approx>rty (TConst j) = (i = j)"
   "(TApp A M) \<approx>rty (TApp A' M') = (A \<approx>rty A' \<and> M \<approx>tr M')"
-  "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty rfv_rty pi ({atom b}, B'))))"
+  "((TPi A a B) \<approx>rty (TPi A' b B')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, B) \<approx>gen arty fv_rty pi ({atom b}, B'))))"
   "(Const i) \<approx>tr (Const j) = (i = j)"
   "(Var x) \<approx>tr (Var y) = (x = y)"
   "(App M N) \<approx>tr (App M' N') = (M \<approx>tr M' \<and> N \<approx>tr N')"
-  "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm rfv_rtrm pi ({atom b}, M'))))"
+  "((Lam A a M) \<approx>tr (Lam A' b M')) = ((A \<approx>rty A') \<and> (\<exists>pi. (({atom a}, M) \<approx>gen artrm fv_rtrm pi ({atom b}, M'))))"
 apply -
 apply (simp add: arkind_arty_artrm.intros)
 
@@ -160,9 +160,9 @@
 done
 
 lemma rfv_eqvt[eqvt]:
-  "((pi\<bullet>rfv_rkind t1) = rfv_rkind (pi\<bullet>t1))"
-  "((pi\<bullet>rfv_rty t2) = rfv_rty (pi\<bullet>t2))"
-  "((pi\<bullet>rfv_rtrm t3) = rfv_rtrm (pi\<bullet>t3))"
+  "((pi\<bullet>fv_rkind t1) = fv_rkind (pi\<bullet>t1))"
+  "((pi\<bullet>fv_rty t2) = fv_rty (pi\<bullet>t2))"
+  "((pi\<bullet>fv_rtrm t3) = fv_rtrm (pi\<bullet>t3))"
 apply(induct t1 and t2 and t3 rule: rkind_rty_rtrm.inducts)
 apply(simp_all add:  union_eqvt Diff_eqvt)
 apply(simp_all add: permute_set_eq atom_eqvt)
@@ -331,24 +331,24 @@
 
 (* FIXME: print out a warning if the type contains a liftet type, like rkind \<Rightarrow> name set *)
 quotient_definition
-   "fv_rkind :: RKIND \<Rightarrow> atom set"
+   "fv_kind :: RKIND \<Rightarrow> atom set"
 is
-  "rfv_rkind"
+  "fv_rkind"
 
 quotient_definition
-   "fv_rty :: RTY \<Rightarrow> atom set"
+   "fv_ty :: RTY \<Rightarrow> atom set"
 is
-  "rfv_rty"
+  "fv_rty"
 
 quotient_definition
-   "fv_rtrm :: RTRM \<Rightarrow> atom set"
+   "fv_trm :: RTRM \<Rightarrow> atom set"
 is
-  "rfv_rtrm"
+  "fv_rtrm"
 
 lemma alpha_rfv:
-  shows "(t \<approx>ki s \<longrightarrow> rfv_rkind t = rfv_rkind s) \<and>
-     (t1 \<approx>rty s1 \<longrightarrow> rfv_rty t1 = rfv_rty s1) \<and>
-     (t2 \<approx>tr s2 \<longrightarrow> rfv_rtrm t2 = rfv_rtrm s2)"
+  shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>
+     (t1 \<approx>rty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
+     (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"
   apply(rule arkind_arty_artrm.induct)
   apply(simp_all add: alpha_gen)
   done
@@ -398,14 +398,14 @@
   apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
   done
 
-lemma rfv_rty_rsp[quot_respect]: 
-  "(arty ===> op =) rfv_rty rfv_rty"
+lemma fv_rty_rsp[quot_respect]: 
+  "(arty ===> op =) fv_rty fv_rty"
   by (simp add: alpha_rfv)
-lemma rfv_rkind_rsp[quot_respect]:
-  "(arkind ===> op =) rfv_rkind rfv_rkind"
+lemma fv_rkind_rsp[quot_respect]:
+  "(arkind ===> op =) fv_rkind fv_rkind"
   by (simp add: alpha_rfv)
-lemma rfv_rtrm_rsp[quot_respect]:
-  "(artrm ===> op =) rfv_rtrm rfv_rtrm"
+lemma fv_rtrm_rsp[quot_respect]:
+  "(artrm ===> op =) fv_rtrm fv_rtrm"
   by (simp add: alpha_rfv)
 
 thm rkind_rty_rtrm.induct
@@ -458,7 +458,7 @@
 
 lemmas RKIND_RTY_RTRM_INJECT = arkind_arty_artrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
-lemmas fv_rkind_rty_rtrm = rfv_rkind_rfv_rty_rfv_rtrm.simps[quot_lifted]
+lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
 
 lemmas fv_eqvt = rfv_eqvt[quot_lifted]
 
@@ -515,12 +515,12 @@
 done
 
 lemma supp_fv:
- "supp t1 = fv_rkind t1"
- "supp t2 = fv_rty t2"
- "supp t3 = fv_rtrm t3"
+ "supp t1 = fv_kind t1"
+ "supp t2 = fv_ty t2"
+ "supp t3 = fv_trm t3"
 apply(induct t1 and t2 and t3 rule: RKIND_RTY_RTRM_inducts)
 apply (simp_all add: supp_rkind_rty_rtrm_easy)
-apply (simp_all add: fv_rkind_rty_rtrm)
+apply (simp_all add: fv_kind_ty_trm)
 apply(subgoal_tac "supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)")
 apply(simp add: supp_Abs Set.Un_commute)
 apply(simp (no_asm) add: supp_def)
@@ -565,7 +565,7 @@
  "supp (APP M N) = supp M \<union> supp N"
  "supp (LAM A x M) = supp A \<union> (supp M - {atom x})"
 apply (simp_all only: supp_rkind_rty_rtrm_easy)
-apply (simp_all only: supp_fv fv_rkind_rty_rtrm)
+apply (simp_all only: supp_fv fv_kind_ty_trm)
 done
 
 end