# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1324449838 -32400
# Node ID c95afd0dc594878bc586be265f2bc3406a2c5e62
# Parent  3750c08f627e5da9ec214ba6952d9bcd2a5f599a
SFT: Rename Lambda to LambdaTerms, rename constants to match Lambda, remove smt proofs.

diff -r 3750c08f627e -r c95afd0dc594 Nominal/Ex/SFT/Consts.thy
--- a/Nominal/Ex/SFT/Consts.thy	Wed Dec 21 14:25:05 2011 +0900
+++ b/Nominal/Ex/SFT/Consts.thy	Wed Dec 21 15:43:58 2011 +0900
@@ -4,77 +4,82 @@
 
 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"
 where
-  [simp del]: "Umn 0 n = \<integral>(cn 0). V (cn n)"
+  [simp del]: "Umn 0 n = \<integral>(cn 0). Var (cn n)"
 | [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n"
 
 lemma [simp]: "2 = Suc 1"
   by auto
 
+lemma split_lemma:
+  "(a = b \<and> X) \<or> (a \<noteq> b \<and> Y) \<longleftrightarrow> (a = b \<longrightarrow> X) \<and> (a \<noteq> b \<longrightarrow> Y)"
+  by blast
+
 lemma Lam_U:
-  "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. V z"
-  "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. V y"
-  "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. V x"
-  apply (simp_all add: Umn.simps Abs1_eq_iff lam.fresh fresh_at_base flip_def[symmetric] Umn.simps)
-  apply (smt Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+
+  assumes "x \<noteq> y" "y \<noteq> z" "x \<noteq> z"
+  shows "Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. Var z"
+        "Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. Var y"
+        "Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. Var x"
+  apply (simp_all add: Umn.simps Abs1_eq_iff lam.fresh fresh_at_base flip_def[symmetric] Umn.simps cnd permute_flip_at assms assms[symmetric] split_lemma)
+  apply (intro impI conjI)
+  apply (metis assms)+
   done
 
-lemma a: "n \<le> m \<Longrightarrow> atom (cn n) \<notin> supp (Umn m n)"
-  apply (induct m)
-  apply (auto simp add: lam.supp supp_at_base Umn.simps)
-  by smt
+lemma supp_U1: "n \<le> m \<Longrightarrow> atom (cn n) \<notin> supp (Umn m n)"
+  by (induct m)
+     (auto simp add: lam.supp supp_at_base Umn.simps le_Suc_eq)
 
-lemma b: "supp (Umn m n) \<subseteq> {atom (cn n)}"
+lemma supp_U2: "supp (Umn m n) \<subseteq> {atom (cn n)}"
   by (induct m) (auto simp add: lam.supp supp_at_base Umn.simps)
 
 lemma supp_U[simp]: "n \<le> m \<Longrightarrow> supp (Umn m n) = {}"
-  using a b
+  using supp_U1 supp_U2
   by blast
 
 lemma U_eqvt:
   "n \<le> m \<Longrightarrow> p \<bullet> (Umn m n) = Umn m n"
   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
 
-definition Var where "Var \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> (Umn 2 2) \<cdot> V cx \<cdot> V cy)"
-definition "App \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (V cz \<cdot> Umn 2 1 \<cdot> V cx \<cdot> V cy \<cdot> V cz)"
-definition "Abs \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> Umn 2 0 \<cdot> V cx \<cdot> V cy)"
+definition VAR where "VAR \<equiv> \<integral>cx. \<integral>cy. (Var cy \<cdot> (Umn 2 2) \<cdot> Var cx \<cdot> Var cy)"
+definition "APP \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (Var cz \<cdot> Umn 2 1 \<cdot> Var cx \<cdot> Var cy \<cdot> Var cz)"
+definition "Abs \<equiv> \<integral>cx. \<integral>cy. (Var cy \<cdot> Umn 2 0 \<cdot> Var cx \<cdot> Var cy)"
 
-lemma Var_App_Abs:
-  "x \<noteq> e \<Longrightarrow> Var = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 2 \<cdot> V x \<cdot> V e)"
-  "e \<noteq> x \<Longrightarrow> e \<noteq> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> App = \<integral>x. \<integral>y. \<integral>e. (V e \<cdot> Umn 2 1 \<cdot> V x \<cdot> V y \<cdot> V e)"
-  "x \<noteq> e \<Longrightarrow> Abs = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 0 \<cdot> V x \<cdot> V e)"
-  unfolding Var_def App_def Abs_def
-  by (simp_all add: Abs1_eq_iff lam.fresh flip_def[symmetric] U_eqvt fresh_def lam.supp supp_at_base)
-     (smt cx_cy_cz permute_flip_at Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+
+lemma VAR_APP_Abs:
+  "x \<noteq> e \<Longrightarrow> VAR = \<integral>x. \<integral>e. (Var e \<cdot> Umn 2 2 \<cdot> Var x \<cdot> Var e)"
+  "e \<noteq> x \<Longrightarrow> e \<noteq> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> APP = \<integral>x. \<integral>y. \<integral>e. (Var e \<cdot> Umn 2 1 \<cdot> Var x \<cdot> Var y \<cdot> Var e)"
+  "x \<noteq> e \<Longrightarrow> Abs = \<integral>x. \<integral>e. (Var e \<cdot> Umn 2 0 \<cdot> Var x \<cdot> Var e)"
+  unfolding VAR_def APP_def Abs_def
+  by (simp_all add: Abs1_eq_iff lam.fresh flip_def[symmetric] U_eqvt fresh_def lam.supp supp_at_base split_lemma permute_flip_at)
+     (auto simp only: cx_cy_cz cx_cy_cz[symmetric])
 
-lemma Var_app:
-  "Var \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"
-  by (rule lam2_fast_app) (simp_all add: Var_App_Abs)
+lemma VAR_app:
+  "VAR \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"
+  by (rule lam2_fast_app[OF VAR_APP_Abs(1)]) simp_all
 
-lemma App_app:
-  "App \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"
-  by (rule lam3_fast_app[OF Var_App_Abs(2)]) (simp_all)
+lemma APP_app:
+  "APP \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"
+  by (rule lam3_fast_app[OF VAR_APP_Abs(2)]) (simp_all)
 
 lemma Abs_app:
   "Abs \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 0 \<cdot> x \<cdot> e"
-  by (rule lam2_fast_app) (simp_all add: Var_App_Abs)
+  by (rule lam2_fast_app[OF VAR_APP_Abs(3)]) simp_all
 
-lemma supp_Var_App_Abs[simp]:
-  "supp Var = {}" "supp App = {}" "supp Abs = {}"
-  by (simp_all add: Var_def App_def Abs_def lam.supp supp_at_base) blast+
+lemma supp_VAR_APP_Abs[simp]:
+  "supp VAR = {}" "supp APP = {}" "supp Abs = {}"
+  by (simp_all add: VAR_def APP_def Abs_def lam.supp supp_at_base) blast+
 
-lemma Var_App_Abs_eqvt[eqvt]:
-  "p \<bullet> Var = Var" "p \<bullet> App = App" "p \<bullet> Abs = Abs"
+lemma VAR_APP_Abs_eqvt[eqvt]:
+  "p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs"
   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
 
 nominal_primrec
   Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)
 where
-  "\<lbrace>V x\<rbrace> = Var \<cdot> (V x)"
-| Ap: "\<lbrace>M \<cdot> N\<rbrace> = App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"
+  "\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)"
+| Ap: "\<lbrace>M \<cdot> N\<rbrace> = APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"
 | "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)"
 proof auto
   fix x :: lam and P
-  assume "\<And>xa. x = V xa \<Longrightarrow> P" "\<And>M N. x = M \<cdot> N \<Longrightarrow> P" "\<And>xa M. x = \<integral> xa. M \<Longrightarrow> P"
+  assume "\<And>xa. x = Var xa \<Longrightarrow> P" "\<And>M N. x = M \<cdot> N \<Longrightarrow> P" "\<And>xa M. x = \<integral> xa. M \<Longrightarrow> P"
   then show "P"
     by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)
        (auto simp add: Abs1_eq_iff fresh_star_def)[3]
@@ -106,8 +111,8 @@
   unfolding fresh_def by simp
 
 fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where
-  "app_lst n [] = V n"
-| "app_lst n (h # t) = Ap (app_lst n t) h"
+  "app_lst n [] = Var n"
+| "app_lst n (h # t) = (app_lst n t) \<cdot> h"
 
 lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)"
   by (induct ts arbitrary: t p) (simp_all add: eqvts)
@@ -164,7 +169,7 @@
 proof -
   obtain x :: var 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: "V x \<cdot> M \<cdot> N \<cdot> P [x ::= R] \<approx> R \<cdot> M \<cdot> N \<cdot> P" using b1 by simp
+  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 *
     apply (subst Ltgt.simps)
   apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim)
@@ -205,18 +210,17 @@
   by (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U, simp_all)
      (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U[simplified], simp_all)+
 
-definition "F1 \<equiv> \<integral>cx. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V cx))"
-definition "F2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V cz \<cdot> V cx))) \<cdot> (V cz \<cdot> V cy))"
-definition "F3 \<equiv> \<integral>cx. \<integral>cy. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>cz. (V cy \<cdot> (V cx \<cdot> V cz)))))"
+definition "F1 \<equiv> \<integral>cx. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var cx))"
+definition "F2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. ((APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Var cz \<cdot> Var cx))) \<cdot> (Var cz \<cdot> Var cy))"
+definition "F3 \<equiv> \<integral>cx. \<integral>cy. (APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>cz. (Var cy \<cdot> (Var cx \<cdot> Var cz)))))"
 
 
 lemma Lam_F:
-  "F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))"
-  "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V c \<cdot> V a))) \<cdot> (V c \<cdot> V b))"
-  "a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (V b \<cdot> (V a \<cdot> V x)))))"
-  apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base)
-  apply (smt cx_cy_cz permute_flip_at)+
-  done
+  "F1 = \<integral>x. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var x))"
+  "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Var c \<cdot> Var a))) \<cdot> (Var c \<cdot> Var b))"
+  "a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (Var b \<cdot> (Var a \<cdot> Var x)))))"
+  by (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base VAR_APP_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base split_lemma permute_flip_at)
+     (auto simp add: cx_cy_cz cx_cy_cz[symmetric])
 
 lemma supp_F[simp]:
   "supp F1 = {}" "supp F2 = {}" "supp F3 = {}"
@@ -229,14 +233,14 @@
      (simp_all add: fresh_star_def fresh_def)
 
 lemma F_app:
-  "F1 \<cdot> A \<approx> App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> A)"
-  "F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"
+  "F1 \<cdot> A \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> A)"
+  "F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"
   by (rule lam1_fast_app, rule Lam_F, simp_all)
      (rule lam3_fast_app, rule Lam_F, simp_all)
 
 lemma F3_app:
   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> V x))))"
+  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
@@ -258,16 +262,15 @@
     done
 qed
 
-definition Lam_A1_pre : "A1 \<equiv> \<integral>cx. \<integral>cy. (F1 \<cdot> V cx)"
-definition Lam_A2_pre : "A2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (F2 \<cdot> V cx \<cdot> V cy \<cdot> \<guillemotleft>[V cz]\<guillemotright>)"
-definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> V cx \<cdot> \<guillemotleft>[V cy]\<guillemotright>)"
+definition Lam_A1_pre : "A1 \<equiv> \<integral>cx. \<integral>cy. (F1 \<cdot> Var cx)"
+definition Lam_A2_pre : "A2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (F2 \<cdot> Var cx \<cdot> Var cy \<cdot> \<guillemotleft>[Var cz]\<guillemotright>)"
+definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> Var cx \<cdot> \<guillemotleft>[Var cy]\<guillemotright>)"
 lemma Lam_A:
-  "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)"
-  "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> V a \<cdot> V b \<cdot> \<guillemotleft>[V c]\<guillemotright>)"
-  "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)"
-  apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base F_eqvt Ltgt.eqvt)
-  apply (smt cx_cy_cz permute_flip_at)+
-  done
+  "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> Var x)"
+  "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> Var a \<cdot> Var b \<cdot> \<guillemotleft>[Var c]\<guillemotright>)"
+  "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> Var a \<cdot> \<guillemotleft>[Var b]\<guillemotright>)"
+  by (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base VAR_APP_Abs_eqvt Numeral.eqvt flip_def[symmetric] fresh_at_base F_eqvt Ltgt.eqvt split_lemma permute_flip_at cx_cy_cz cx_cy_cz[symmetric])
+     auto
 
 lemma supp_A[simp]:
   "supp A1 = {}" "supp A2 = {}" "supp A3 = {}"
diff -r 3750c08f627e -r c95afd0dc594 Nominal/Ex/SFT/Lambda.thy
--- a/Nominal/Ex/SFT/Lambda.thy	Wed Dec 21 14:25:05 2011 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-header {* Definition of Lambda terms and convertibility *}
-
-theory Lambda imports "../../Nominal2" begin
-
-lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"
-  unfolding fresh_def by blast
-
-atom_decl var
-
-nominal_datatype lam =
-  V "var"
-| Ap "lam" "lam" (infixl "\<cdot>" 98)
-| Lm x::"var" l::"lam"  binds x in l ("\<integral> _. _" [97, 97] 99)
-
-nominal_primrec
-  subst :: "lam \<Rightarrow> var \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
-where
-  "(V x)[y ::= s] = (if x = y then s else (V 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
-  assume "\<And>x y s. a = V 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"
-  then show "P"
-    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
-  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"
-  then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)"
-    apply -
-    apply (erule Abs_lst1_fcb)
-    apply(simp (no_asm) add: Abs_fresh_iff)
-    apply(drule_tac a="atom xa" in fresh_eqvt_at)
-    apply(simp add: finite_supp)
-    apply(simp_all add: fresh_Pair_elim Abs_fresh_iff Abs1_eq_iff)
-    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
-    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa")
-    apply(simp add: atom_eqvt eqvt_at_def)
-    apply(rule perm_supp_eq, simp add: supp_swap fresh_star_def fresh_Pair)+
-    done
-next
-  show "eqvt subst_graph" unfolding eqvt_def subst_graph_def
-    by (rule, perm_simp, rule)
-qed
-
-termination (eqvt) by lexicographic_order
-
-lemma forget[simp]:
-  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
-  by (nominal_induct t avoiding: x s rule: lam.strong_induct)
-     (auto simp add: lam.fresh fresh_at_base)
-
-lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t"
-  by (simp add: fresh_def)
-
-lemma subst_id[simp]: "M [x ::= V x] = M"
-  by (rule_tac lam="M" and c="x" in lam.strong_induct)
-     (simp_all add: fresh_star_def lam.fresh fresh_Pair)
-
-inductive
-  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<approx>" 80)
-where
-  bI: "(\<integral>x. M) \<cdot> N \<approx> M[x ::= N]"
-| b1: "M \<approx> M"
-| b2: "M \<approx> N \<Longrightarrow> N \<approx> M"
-| b3: "M \<approx> N \<Longrightarrow> N \<approx> L \<Longrightarrow> M \<approx> L"
-| b4: "M \<approx> N \<Longrightarrow> Z \<cdot> M \<approx> Z \<cdot> N"
-| b5: "M \<approx> N \<Longrightarrow> M \<cdot> Z \<approx> N \<cdot> Z"
-| b6: "M \<approx> N \<Longrightarrow> \<integral>x. M \<approx> \<integral>x. N"
-
-lemmas [trans] = b3
-equivariance beta
-
-end
diff -r 3750c08f627e -r c95afd0dc594 Nominal/Ex/SFT/LambdaTerms.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/SFT/LambdaTerms.thy	Wed Dec 21 15:43:58 2011 +0900
@@ -0,0 +1,83 @@
+header {* Definition of Lambda terms and convertibility *}
+
+theory LambdaTerms imports "../../Nominal2" begin
+
+lemma [simp]: "supp x = {} \<Longrightarrow> y \<sharp> x"
+  unfolding fresh_def by blast
+
+atom_decl var
+
+nominal_datatype lam =
+  Var "var"
+| App "lam" "lam"
+| Lam x::"var" 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)
+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
+  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"
+  then show "P"
+    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
+  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"
+  then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)"
+    apply -
+    apply (erule Abs_lst1_fcb)
+    apply(simp (no_asm) add: Abs_fresh_iff)
+    apply(drule_tac a="atom xa" in fresh_eqvt_at)
+    apply(simp add: finite_supp)
+    apply(simp_all add: fresh_Pair_elim Abs_fresh_iff Abs1_eq_iff)
+    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
+    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa")
+    apply(simp add: atom_eqvt eqvt_at_def)
+    apply(rule perm_supp_eq, simp add: supp_swap fresh_star_def fresh_Pair)+
+    done
+next
+  show "eqvt subst_graph" unfolding eqvt_def subst_graph_def
+    by (rule, perm_simp, rule)
+qed
+
+termination (eqvt) by lexicographic_order
+
+lemma forget[simp]:
+  shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t"
+  by (nominal_induct t avoiding: x s rule: lam.strong_induct)
+     (auto simp add: lam.fresh fresh_at_base)
+
+lemma forget_closed[simp]: "supp t = {} \<Longrightarrow> t[x ::= s] = t"
+  by (simp add: fresh_def)
+
+lemma subst_id[simp]: "M [x ::= Var x] = M"
+  by (rule_tac lam="M" and c="x" in lam.strong_induct)
+     (simp_all add: fresh_star_def lam.fresh fresh_Pair)
+
+inductive
+  beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<approx>" 80)
+where
+  bI: "(\<integral>x. M) \<cdot> N \<approx> M[x ::= N]"
+| b1: "M \<approx> M"
+| b2: "M \<approx> N \<Longrightarrow> N \<approx> M"
+| b3: "M \<approx> N \<Longrightarrow> N \<approx> L \<Longrightarrow> M \<approx> L"
+| b4: "M \<approx> N \<Longrightarrow> Z \<cdot> M \<approx> Z \<cdot> N"
+| b5: "M \<approx> N \<Longrightarrow> M \<cdot> Z \<approx> N \<cdot> Z"
+| b6: "M \<approx> N \<Longrightarrow> \<integral>x. M \<approx> \<integral>x. N"
+
+lemmas [trans] = b3
+equivariance beta
+
+end
diff -r 3750c08f627e -r c95afd0dc594 Nominal/Ex/SFT/Theorem.thy
--- a/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 14:25:05 2011 +0900
+++ b/Nominal/Ex/SFT/Theorem.thy	Wed Dec 21 15:43:58 2011 +0900
@@ -8,31 +8,31 @@
 lemma Num:
   shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>"
 proof (induct M rule: lam.induct)
-  case (V n)
-  have "Num \<cdot> \<lbrace>V n\<rbrace> = Num \<cdot> (Var \<cdot> V n)" by simp
-  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Var \<cdot> V n)" by simp
-  also have "... \<approx> Var \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
-  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 2 \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Var_app .
-  also have "... \<approx> A1 \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
-  also have "... \<approx> F1 \<cdot> V n" using A_app(1) .
-  also have "... \<approx> App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V n)" using F_app(1) .
-  also have "... = \<lbrace>\<lbrace>V n\<rbrace>\<rbrace>" by simp
-  finally show "Num \<cdot> \<lbrace>V n\<rbrace> \<approx> \<lbrace>\<lbrace>V n\<rbrace>\<rbrace>".
+  case (Var n)
+  have "Num \<cdot> \<lbrace>Var n\<rbrace> = Num \<cdot> (VAR \<cdot> Var n)" by simp
+  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (VAR \<cdot> Var n)" by simp
+  also have "... \<approx> VAR \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
+  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 2 \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using VAR_app .
+  also have "... \<approx> A1 \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
+  also have "... \<approx> F1 \<cdot> Var n" using A_app(1) .
+  also have "... \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var n)" using F_app(1) .
+  also have "... = \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>" by simp
+  finally show "Num \<cdot> \<lbrace>Var n\<rbrace> \<approx> \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>".
 next
-  case (Ap M N)
+  case (App M N)
   assume IH: "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" "Num \<cdot> \<lbrace>N\<rbrace> \<approx> \<lbrace>\<lbrace>N\<rbrace>\<rbrace>"
-  have "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> = Num \<cdot> (App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
-  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
-  also have "... \<approx> App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
-  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 1 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using App_app .
+  have "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> = Num \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
+  also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp
+  also have "... \<approx> APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app .
+  also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 1 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using APP_app .
   also have "... \<approx> A2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
   also have "... \<approx> F2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> Num" using A_app(2) by simp
-  also have "... \<approx> App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (Num \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) .
-  also have "... \<approx> App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using IH by simp
+  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Num \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) .
+  also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using IH by simp
   also have "... \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>" using IH by simp
   finally show "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>".
 next
-  case (Lm x P)
+  case (Lam x P)
   assume IH: "Num \<cdot> \<lbrace>P\<rbrace> \<approx> \<lbrace>\<lbrace>P\<rbrace>\<rbrace>"
   have "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> = Num \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp
   also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp
@@ -41,9 +41,9 @@
   also have "... \<approx> A3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp
   also have "... \<approx> F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" using A_app(3) .
   also have "... = F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Num" by simp
-  also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> V x)))" by (rule F3_app) simp_all
-  also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp
-  also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>\<lbrace>P\<rbrace>\<rbrace>)" using IH by simp
+  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Var x)))" by (rule F3_app) simp_all
+  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp
+  also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>\<lbrace>P\<rbrace>\<rbrace>)" using IH by simp
   also have "... = \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" by simp
   finally show "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> \<approx> \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" .
 qed
@@ -56,12 +56,12 @@
   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
-  def W \<equiv> "\<integral>x. (F \<cdot> (App \<cdot> V x \<cdot> (Num \<cdot> V x)))"
+  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 ..
-  also have "... = (\<integral>x. (F \<cdot> (App \<cdot> V x \<cdot> (Num \<cdot> V x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def ..
-  also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp
-  also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp
+  also have "... = (\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def ..
+  also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp
+  also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp
   also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp
   also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def ..
   finally show ?thesis by blast
diff -r 3750c08f627e -r c95afd0dc594 Nominal/Ex/SFT/Utils.thy
--- a/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 14:25:05 2011 +0900
+++ b/Nominal/Ex/SFT/Utils.thy	Wed Dec 21 15:43:58 2011 +0900
@@ -1,9 +1,9 @@
 header {* Utilities for defining constants and functions *}
 
-theory Utils imports Lambda begin
+theory Utils imports LambdaTerms begin
 
 lemma beta_app:
-  "(\<integral> x. M) \<cdot> V x \<approx> M"
+  "(\<integral> x. M) \<cdot> Var x \<approx> M"
   by (rule b3, rule bI)
      (simp add: b1)
 
@@ -72,7 +72,7 @@
     done
   qed
 
-definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''Lambda.var'' []) n)"
+definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''LambdaTerms.var'' []) n)"
 
 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n"
   unfolding cn_def using Abs_var_inject by simp