--- 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 = {}"