# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324450062 -32400
# Node ID 5e74bd87bcda558bc9b23daf1151a0d3cb685bbd
# Parent  c95afd0dc594878bc586be265f2bc3406a2c5e62
SFT/LambdaTerms: rename 'var' to 'name' to match Lambda.

diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/Consts.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -84,7 +84,7 @@
     by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)
        (auto simp add: Abs1_eq_iff fresh_star_def)[3]
 next
-  fix x :: var and M and xa :: var and Ma
+  fix x :: name and M and xa :: name and Ma
   assume "[[atom x]]lst. M = [[atom xa]]lst. Ma"
     "eqvt_at Numeral_sumC M"
   then show "[[atom x]]lst. Numeral_sumC M = [[atom xa]]lst. Numeral_sumC Ma"
@@ -110,7 +110,7 @@
   "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y"
   unfolding fresh_def by simp
 
-fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where
+fun app_lst :: "name \<Rightarrow> lam list \<Rightarrow> lam" where
   "app_lst n [] = Var n"
 | "app_lst n (h # t) = (app_lst n t) \<cdot> h"
 
@@ -134,7 +134,7 @@
   [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))"
   unfolding eqvt_def Ltgt_graph_def
   apply (rule, perm_simp, rule, rule)
-  apply (rule_tac x="x" and ?'a="var" in obtain_fresh)
+  apply (rule_tac x="x" and ?'a="name" in obtain_fresh)
   apply (simp_all add: Abs1_eq_iff lam.fresh swap_fresh_fresh fresh_at_base)
   apply (simp add: eqvts swap_fresh_fresh)
   apply (case_tac "x = xa")
@@ -149,14 +149,14 @@
 lemma ltgt_eq_iff[simp]:
   "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"
 proof auto
-  obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto
+  obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto
   then have *: "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
   then show "(\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright>) \<Longrightarrow> (M = N)" by (simp add: Abs1_eq_iff app_lst_rev_eq_iff Ltgt.simps)
 qed
 
 lemma Ltgt1_app: "\<guillemotleft>[M]\<guillemotright> \<cdot> N \<approx> N \<cdot> M"
 proof -
-  obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto
+  obtain x :: name where "atom x \<sharp> (M, N)" using obtain_fresh by auto
   then have "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
   then show ?thesis
   apply (subst Ltgt.simps)
@@ -167,7 +167,7 @@
 
 lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P"
 proof -
-  obtain x :: var where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
+  obtain x :: name where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
   then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all
   then have s: "Var x \<cdot> M \<cdot> N \<cdot> P [x ::= R] \<approx> R \<cdot> M \<cdot> N \<cdot> P" using b1 by simp
   show ?thesis using *
@@ -181,7 +181,7 @@
 lemma supp_ltgt[simp]:
   "supp \<guillemotleft>t\<guillemotright> = supp t"
 proof -
-  obtain x :: var where *:"atom x \<sharp> t" using obtain_fresh by auto
+  obtain x :: name where *:"atom x \<sharp> t" using obtain_fresh by auto
   show ?thesis using *
   by (simp_all add: Ltgt.simps lam.supp supp_at_base supp_Nil supp_app_lst supp_rev fresh_def)
 qed
@@ -194,7 +194,7 @@
 lemma Ltgt1_subst[simp]:
   "\<guillemotleft>[M]\<guillemotright> [y ::= A] = \<guillemotleft>[M [y ::= A]]\<guillemotright>"
 proof -
-  obtain x :: var where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast
+  obtain x :: name where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast
   have "x \<noteq> y" using a[simplified fresh_Pair fresh_at_base] by simp
   then show ?thesis
     apply (subst Ltgt.simps)
@@ -242,8 +242,8 @@
   assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *)
   shows "F3 \<cdot> A \<cdot> B \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> Var x))))"
 proof -
-  obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
-  obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
+  obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
+  obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
   have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z"
     using b c by (simp_all add: fresh_Pair fresh_at_base) blast+
   have **:
diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/LambdaTerms.thy
--- a/Nominal/Ex/SFT/LambdaTerms.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/LambdaTerms.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -5,25 +5,25 @@
 lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"
   unfolding fresh_def by blast
 
-atom_decl var
+atom_decl name
 
 nominal_datatype lam =
-  Var "var"
+  Var "name"
 | App "lam" "lam"
-| Lam x::"var" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
+| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
 notation
   App (infixl "\<cdot>" 98) and
   Lam ("\<integral> _. _" [97, 97] 99)
 
 nominal_primrec
-  subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
   "(Var x)[y ::= s] = (if x = y then s else (Var x))"
 | "(t1 \<cdot> t2)[y ::= s] = (t1[y ::= s]) \<cdot> (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (\<integral>x. t)[y ::= s] = \<integral>x.(t[y ::= s])"
 proof auto
-  fix a b :: lam and aa :: var and P
+  fix a b :: lam and aa :: name and P
   assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P"
     "\<And>t1 t2 y s. a = t1 \<cdot> t2 \<and> aa = y \<and> b = s \<Longrightarrow> P"
     "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = \<integral> x. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P"
@@ -31,7 +31,7 @@
     by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
        (blast, blast, simp add: fresh_star_def)
 next
-  fix x :: var and t and xa :: var and ya sa ta
+  fix x :: name and t and xa :: name and ya sa ta
   assume *: "eqvt_at subst_sumC (t, ya, sa)"
     "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)"
     "[[atom x]]lst. t = [[atom xa]]lst. ta"
diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/Theorem.thy
--- a/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -55,7 +55,7 @@
   fixes F :: lam
   shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>"
 proof -
-  obtain x :: var where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
+  obtain x :: name where [simp]:"atom x \<sharp> F" using obtain_fresh by blast
   def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))"
   def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>"
   have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def ..
diff -r c95afd0dc594 -r 5e74bd87bcda Nominal/Ex/SFT/Utils.thy
--- a/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 15:43:58 2011 +0900
+++ b/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 15:47:42 2011 +0900
@@ -12,7 +12,7 @@
       and su: "\<And>x. atom x \<sharp> A \<Longrightarrow> F (V x) [x ::= A] = F A"
   shows "L \<cdot> A \<approx> F A"
 proof -
-  obtain x :: var where a: "atom x \<sharp> A" using obtain_fresh by blast
+  obtain x :: name where a: "atom x \<sharp> A" using obtain_fresh by blast
   show ?thesis
     by (simp add: leq[of x], rule b3, rule bI, simp add: su b1 a)
 qed
@@ -23,9 +23,9 @@
        x \<noteq> y \<Longrightarrow> F (V x) (V y) [x ::= A] [y ::= B] = F A B"
   shows "L \<cdot> A \<cdot> B \<approx> F A B"
 proof -
-  obtain x :: var where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast
-  obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
-  obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
+  obtain x :: name where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast
+  obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
+  obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
   have *: "x \<noteq> y" "x \<noteq> z" "y \<noteq> z"
     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
   have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
@@ -51,9 +51,9 @@
       ((F (V x) (V y) (V z))[x ::= A] [y ::= B] [z ::= C] = F A B C)"
   shows "L \<cdot> A \<cdot> B \<cdot> C \<approx> F A B C"
 proof -
-  obtain x :: var where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast
-  obtain y :: var where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast
-  obtain z :: var where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast
+  obtain x :: name where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast
+  obtain y :: name where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast
+  obtain z :: name where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast
   have *: "x \<noteq> y" "y \<noteq> z" "z \<noteq> x"
     using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+
   have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
@@ -72,14 +72,14 @@
     done
   qed
 
-definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''LambdaTerms.var'' []) n)"
+definition cn :: "nat \<Rightarrow> name" where "cn n \<equiv> Abs_name (Atom (Sort ''LambdaTerms.name'' []) n)"
 
 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n"
-  unfolding cn_def using Abs_var_inject by simp
+  unfolding cn_def using Abs_name_inject by simp
 
-definition cx :: var where "cx \<equiv> cn 0"
-definition cy :: var where "cy \<equiv> cn 1"
-definition cz :: var where "cz \<equiv> cn 2"
+definition cx :: name where "cx \<equiv> cn 0"
+definition cy :: name where "cy \<equiv> cn 1"
+definition cz :: name where "cz \<equiv> cn 2"
 
 lemma cx_cy_cz[simp]:
   "cx \<noteq> cy" "cx \<noteq> cz" "cz \<noteq> cy"