Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/SFT/Consts.thy
changeset 3087 c95afd0dc594
parent 2984 1b39ba5db2c1
child 3088 5e74bd87bcda
equal deleted inserted replaced
3086:3750c08f627e 3087:c95afd0dc594 
     2 
     2 
     3 theory Consts imports Utils begin
 
     3 theory Consts imports Utils begin
 
     4 
     4 
     5 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"
 
     5 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"
 
     6 where
 
     6 where
 
     7   [simp del]: "Umn 0 n = \<integral>(cn 0). V (cn n)"
 
     7   [simp del]: "Umn 0 n = \<integral>(cn 0). Var (cn n)"
 
     8 | [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n"
 
     8 | [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n"
 
     9 
     9 
    10 lemma [simp]: "2 = Suc 1"
 
    10 lemma [simp]: "2 = Suc 1"
 
    11   by auto
 
    11   by auto
 
    12 
    12 
       
    13 lemma split_lemma:
 
       
    14   "(a = b \<and> X) \<or> (a \<noteq> b \<and> Y) \<longleftrightarrow> (a = b \<longrightarrow> X) \<and> (a \<noteq> b \<longrightarrow> Y)"
 
       
    15   by blast
 
       
    16 
    13 lemma Lam_U:
 
    17 lemma Lam_U:
 
    14   "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. V z"
 
    18   assumes "x \<noteq> y" "y \<noteq> z" "x \<noteq> z"
 
    15   "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. V y"
 
    19   shows "Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. Var z"
 
    16   "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. V x"
 
    20         "Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. Var y"
 
    17   apply (simp_all add: Umn.simps Abs1_eq_iff lam.fresh fresh_at_base flip_def[symmetric] Umn.simps)
 
    21         "Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. Var x"
 
    18   apply (smt Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+
 
    22   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)
 
    19   done
 
    23   apply (intro impI conjI)
 
    20 
    24   apply (metis assms)+
 
    21 lemma a: "n \<le> m \<Longrightarrow> atom (cn n) \<notin> supp (Umn m n)"
 
    25   done
 
    22   apply (induct m)
 
    26 
    23   apply (auto simp add: lam.supp supp_at_base Umn.simps)
 
    27 lemma supp_U1: "n \<le> m \<Longrightarrow> atom (cn n) \<notin> supp (Umn m n)"
 
    24   by smt
 
    28   by (induct m)
 
    25 
    29      (auto simp add: lam.supp supp_at_base Umn.simps le_Suc_eq)
 
    26 lemma b: "supp (Umn m n) \<subseteq> {atom (cn n)}"
 
    30 
       
    31 lemma supp_U2: "supp (Umn m n) \<subseteq> {atom (cn n)}"
 
    27   by (induct m) (auto simp add: lam.supp supp_at_base Umn.simps)
 
    32   by (induct m) (auto simp add: lam.supp supp_at_base Umn.simps)
 
    28 
    33 
    29 lemma supp_U[simp]: "n \<le> m \<Longrightarrow> supp (Umn m n) = {}"
 
    34 lemma supp_U[simp]: "n \<le> m \<Longrightarrow> supp (Umn m n) = {}"
 
    30   using a b
 
    35   using supp_U1 supp_U2
 
    31   by blast
 
    36   by blast
 
    32 
    37 
    33 lemma U_eqvt:
 
    38 lemma U_eqvt:
 
    34   "n \<le> m \<Longrightarrow> p \<bullet> (Umn m n) = Umn m n"
 
    39   "n \<le> m \<Longrightarrow> p \<bullet> (Umn m n) = Umn m n"
 
    35   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
 
    40   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
 
    36 
    41 
    37 definition Var where "Var \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> (Umn 2 2) \<cdot> V cx \<cdot> V cy)"
 
    42 definition VAR where "VAR \<equiv> \<integral>cx. \<integral>cy. (Var cy \<cdot> (Umn 2 2) \<cdot> Var cx \<cdot> Var cy)"
 
    38 definition "App \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (V cz \<cdot> Umn 2 1 \<cdot> V cx \<cdot> V cy \<cdot> V cz)"
 
    43 definition "APP \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (Var cz \<cdot> Umn 2 1 \<cdot> Var cx \<cdot> Var cy \<cdot> Var cz)"
 
    39 definition "Abs \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> Umn 2 0 \<cdot> V cx \<cdot> V cy)"
 
    44 definition "Abs \<equiv> \<integral>cx. \<integral>cy. (Var cy \<cdot> Umn 2 0 \<cdot> Var cx \<cdot> Var cy)"
 
    40 
    45 
    41 lemma Var_App_Abs:
 
    46 lemma VAR_APP_Abs:
 
    42   "x \<noteq> e \<Longrightarrow> Var = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 2 \<cdot> V x \<cdot> V e)"
 
    47   "x \<noteq> e \<Longrightarrow> VAR = \<integral>x. \<integral>e. (Var e \<cdot> Umn 2 2 \<cdot> Var x \<cdot> Var e)"
 
    43   "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)"
 
    48   "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)"
 
    44   "x \<noteq> e \<Longrightarrow> Abs = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 0 \<cdot> V x \<cdot> V e)"
 
    49   "x \<noteq> e \<Longrightarrow> Abs = \<integral>x. \<integral>e. (Var e \<cdot> Umn 2 0 \<cdot> Var x \<cdot> Var e)"
 
    45   unfolding Var_def App_def Abs_def
 
    50   unfolding VAR_def APP_def Abs_def
 
    46   by (simp_all add: Abs1_eq_iff lam.fresh flip_def[symmetric] U_eqvt fresh_def lam.supp supp_at_base)
 
    51   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)
 
    47      (smt cx_cy_cz permute_flip_at Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+
 
    52      (auto simp only: cx_cy_cz cx_cy_cz[symmetric])
 
    48 
    53 
    49 lemma Var_app:
 
    54 lemma VAR_app:
 
    50   "Var \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"
 
    55   "VAR \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"
 
    51   by (rule lam2_fast_app) (simp_all add: Var_App_Abs)
 
    56   by (rule lam2_fast_app[OF VAR_APP_Abs(1)]) simp_all
 
    52 
    57 
    53 lemma App_app:
 
    58 lemma APP_app:
 
    54   "App \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"
 
    59   "APP \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"
 
    55   by (rule lam3_fast_app[OF Var_App_Abs(2)]) (simp_all)
 
    60   by (rule lam3_fast_app[OF VAR_APP_Abs(2)]) (simp_all)
 
    56 
    61 
    57 lemma Abs_app:
 
    62 lemma Abs_app:
 
    58   "Abs \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 0 \<cdot> x \<cdot> e"
 
    63   "Abs \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 0 \<cdot> x \<cdot> e"
 
    59   by (rule lam2_fast_app) (simp_all add: Var_App_Abs)
 
    64   by (rule lam2_fast_app[OF VAR_APP_Abs(3)]) simp_all
 
    60 
    65 
    61 lemma supp_Var_App_Abs[simp]:
 
    66 lemma supp_VAR_APP_Abs[simp]:
 
    62   "supp Var = {}" "supp App = {}" "supp Abs = {}"
 
    67   "supp VAR = {}" "supp APP = {}" "supp Abs = {}"
 
    63   by (simp_all add: Var_def App_def Abs_def lam.supp supp_at_base) blast+
 
    68   by (simp_all add: VAR_def APP_def Abs_def lam.supp supp_at_base) blast+
 
    64 
    69 
    65 lemma Var_App_Abs_eqvt[eqvt]:
 
    70 lemma VAR_APP_Abs_eqvt[eqvt]:
 
    66   "p \<bullet> Var = Var" "p \<bullet> App = App" "p \<bullet> Abs = Abs"
 
    71   "p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs"
 
    67   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
 
    72   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
 
    68 
    73 
    69 nominal_primrec
 
    74 nominal_primrec
 
    70   Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)
 
    75   Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)
 
    71 where
 
    76 where
 
    72   "\<lbrace>V x\<rbrace> = Var \<cdot> (V x)"
 
    77   "\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)"
 
    73 | Ap: "\<lbrace>M \<cdot> N\<rbrace> = App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"
 
    78 | Ap: "\<lbrace>M \<cdot> N\<rbrace> = APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"
 
    74 | "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)"
 
    79 | "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)"
 
    75 proof auto
 
    80 proof auto
 
    76   fix x :: lam and P
 
    81   fix x :: lam and P
 
    77   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"
 
    82   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"
 
    78   then show "P"
 
    83   then show "P"
 
    79     by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)
 
    84     by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)
 
    80        (auto simp add: Abs1_eq_iff fresh_star_def)[3]
 
    85        (auto simp add: Abs1_eq_iff fresh_star_def)[3]
 
    81 next
 
    86 next
 
    82   fix x :: var and M and xa :: var and Ma
 
    87   fix x :: var and M and xa :: var and Ma
 
   104 lemma fresh_numeral[simp]:
 
   109 lemma fresh_numeral[simp]:
 
   105   "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y"
 
   110   "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y"
 
   106   unfolding fresh_def by simp
 
   111   unfolding fresh_def by simp
 
   107 
   112 
   108 fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where
 
   113 fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where
 
   109   "app_lst n [] = V n"
 
   114   "app_lst n [] = Var n"
 
   110 | "app_lst n (h # t) = Ap (app_lst n t) h"
 
   115 | "app_lst n (h # t) = (app_lst n t) \<cdot> h"
 
   111 
   116 
   112 lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)"
 
   117 lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)"
 
   113   by (induct ts arbitrary: t p) (simp_all add: eqvts)
 
   118   by (induct ts arbitrary: t p) (simp_all add: eqvts)
 
   114 
   119 
   115 lemma supp_app_lst: "supp (app_lst x l) = {atom x} \<union> supp l"
 
   120 lemma supp_app_lst: "supp (app_lst x l) = {atom x} \<union> supp l"
 
   162 
   167 
   163 lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P"
 
   168 lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P"
 
   164 proof -
 
   169 proof -
 
   165   obtain x :: var where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
 
   170   obtain x :: var where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
 
   166   then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all
 
   171   then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all
 
   167   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
 
   172   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
 
   168   show ?thesis using *
 
   173   show ?thesis using *
 
   169     apply (subst Ltgt.simps)
 
   174     apply (subst Ltgt.simps)
 
   170   apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim)
 
   175   apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim)
 
   171   apply auto[1]
 
   176   apply auto[1]
 
   172   apply (rule b3, rule bI, simp add: b1)
 
   177   apply (rule b3, rule bI, simp add: b1)
 
   203 lemma U_app:
 
   208 lemma U_app:
 
   204   "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 2 \<approx> A" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 1 \<approx> B" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 0 \<approx> C"
 
   209   "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 2 \<approx> A" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 1 \<approx> B" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 0 \<approx> C"
 
   205   by (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U, simp_all)
 
   210   by (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U, simp_all)
 
   206      (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U[simplified], simp_all)+
 
   211      (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U[simplified], simp_all)+
 
   207 
   212 
   208 definition "F1 \<equiv> \<integral>cx. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V cx))"
 
   213 definition "F1 \<equiv> \<integral>cx. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var cx))"
 
   209 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))"
 
   214 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))"
 
   210 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)))))"
 
   215 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)))))"
 
   211 
   216 
   212 
   217 
   213 lemma Lam_F:
 
   218 lemma Lam_F:
 
   214   "F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))"
 
   219   "F1 = \<integral>x. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var x))"
 
   215   "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))"
 
   220   "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))"
 
   216   "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)))))"
 
   221   "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)))))"
 
   217   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)
 
   222   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)
 
   218   apply (smt cx_cy_cz permute_flip_at)+
 
   223      (auto simp add: cx_cy_cz cx_cy_cz[symmetric])
 
   219   done
 
       
   220 
   224 
   221 lemma supp_F[simp]:
 
   225 lemma supp_F[simp]:
 
   222   "supp F1 = {}" "supp F2 = {}" "supp F3 = {}"
 
   226   "supp F1 = {}" "supp F2 = {}" "supp F3 = {}"
 
   223   by (simp_all add: F1_def F2_def F3_def lam.supp supp_at_base)
 
   227   by (simp_all add: F1_def F2_def F3_def lam.supp supp_at_base)
 
   224      blast+
 
   228      blast+
 
   227   "p \<bullet> F1 = F1" "p \<bullet> F2 = F2" "p \<bullet> F3 = F3"
 
   231   "p \<bullet> F1 = F1" "p \<bullet> F2 = F2" "p \<bullet> F3 = F3"
 
   228   by (rule_tac [!] perm_supp_eq)
 
   232   by (rule_tac [!] perm_supp_eq)
 
   229      (simp_all add: fresh_star_def fresh_def)
 
   233      (simp_all add: fresh_star_def fresh_def)
 
   230 
   234 
   231 lemma F_app:
 
   235 lemma F_app:
 
   232   "F1 \<cdot> A \<approx> App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> A)"
 
   236   "F1 \<cdot> A \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> A)"
 
   233   "F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"
 
   237   "F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"
 
   234   by (rule lam1_fast_app, rule Lam_F, simp_all)
 
   238   by (rule lam1_fast_app, rule Lam_F, simp_all)
 
   235      (rule lam3_fast_app, rule Lam_F, simp_all)
 
   239      (rule lam3_fast_app, rule Lam_F, simp_all)
 
   236 
   240 
   237 lemma F3_app:
 
   241 lemma F3_app:
 
   238   assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *)
 
   242   assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *)
 
   239   shows "F3 \<cdot> A \<cdot> B \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> V x))))"
 
   243   shows "F3 \<cdot> A \<cdot> B \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> Var x))))"
 
   240 proof -
 
   244 proof -
 
   241   obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
 
   245   obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
 
   242   obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
 
   246   obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
 
   243   have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z"
 
   247   have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z"
 
   244     using b c by (simp_all add: fresh_Pair fresh_at_base) blast+
 
   248     using b c by (simp_all add: fresh_Pair fresh_at_base) blast+
 
   256     apply (simp add: ** fresh_Pair * *[symmetric])
 
   260     apply (simp add: ** fresh_Pair * *[symmetric])
 
   257     apply (rule b1)
 
   261     apply (rule b1)
 
   258     done
 
   262     done
 
   259 qed
 
   263 qed
 
   260 
   264 
   261 definition Lam_A1_pre : "A1 \<equiv> \<integral>cx. \<integral>cy. (F1 \<cdot> V cx)"
 
   265 definition Lam_A1_pre : "A1 \<equiv> \<integral>cx. \<integral>cy. (F1 \<cdot> Var cx)"
 
   262 definition Lam_A2_pre : "A2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (F2 \<cdot> V cx \<cdot> V cy \<cdot> \<guillemotleft>[V cz]\<guillemotright>)"
 
   266 definition Lam_A2_pre : "A2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (F2 \<cdot> Var cx \<cdot> Var cy \<cdot> \<guillemotleft>[Var cz]\<guillemotright>)"
 
   263 definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> V cx \<cdot> \<guillemotleft>[V cy]\<guillemotright>)"
 
   267 definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> Var cx \<cdot> \<guillemotleft>[Var cy]\<guillemotright>)"
 
   264 lemma Lam_A:
 
   268 lemma Lam_A:
 
   265   "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)"
 
   269   "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> Var x)"
 
   266   "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>)"
 
   270   "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>)"
 
   267   "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)"
 
   271   "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> Var a \<cdot> \<guillemotleft>[Var b]\<guillemotright>)"
 
   268   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)
 
   272   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])
 
   269   apply (smt cx_cy_cz permute_flip_at)+
 
   273      auto
 
   270   done
 
       
   271 
   274 
   272 lemma supp_A[simp]:
 
   275 lemma supp_A[simp]:
 
   273   "supp A1 = {}" "supp A2 = {}" "supp A3 = {}"
 
   276   "supp A1 = {}" "supp A2 = {}" "supp A3 = {}"
 
   274   by (auto simp add: Lam_A1_pre Lam_A2_pre Lam_A3_pre lam.supp supp_at_base supp_Cons supp_Nil)
 
   277   by (auto simp add: Lam_A1_pre Lam_A2_pre Lam_A3_pre lam.supp supp_at_base supp_Cons supp_Nil)
 
   275 
   278
nominal2