1 header {* Constant definitions *}

     2 theory Consts imports Utils Lambda begin

     3 

     4 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"

     5 where

     6   [simp del]: "Umn 0 n = \<integral>(cn 0). V (cn n)"

     7 | [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n"

     8 

     9 lemma [simp]: "2 = Suc 1"

    10   by auto

    11 

    12 lemma Lam_U:

    13   "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. V z"

    14   "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. V y"

    15   "x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. V x"

    16   apply (simp_all add: Umn.simps Abs1_eq_iff lam.fresh fresh_at_base flip_def[symmetric] Umn.simps)

    17   apply (smt Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+

    18   done

    19 

    20 lemma a: "n \<le> m \<Longrightarrow> atom (cn n) \<notin> supp (Umn m n)"

    21   apply (induct m)

    22   apply (auto simp add: lam.supp supp_at_base Umn.simps)

    23   by smt

    24 

    25 lemma b: "supp (Umn m n) \<subseteq> {atom (cn n)}"

    26   by (induct m) (auto simp add: lam.supp supp_at_base Umn.simps)

    27 

    28 lemma supp_U[simp]: "n \<le> m \<Longrightarrow> supp (Umn m n) = {}"

    29   using a b

    30   by blast

    31 

    32 lemma U_eqvt:

    33   "n \<le> m \<Longrightarrow> p \<bullet> (Umn m n) = Umn m n"

    34   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)

    35 

    36 definition Var where "Var \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> (Umn 2 2) \<cdot> V cx \<cdot> V cy)"

    37 definition "App \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (V cz \<cdot> Umn 2 1 \<cdot> V cx \<cdot> V cy \<cdot> V cz)"

    38 definition "Abs \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> Umn 2 0 \<cdot> V cx \<cdot> V cy)"

    39 

    40 lemma Var_App_Abs:

    41   "x \<noteq> e \<Longrightarrow> Var = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 2 \<cdot> V x \<cdot> V e)"

    42   "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)"

    43   "x \<noteq> e \<Longrightarrow> Abs = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 0 \<cdot> V x \<cdot> V e)"

    44   unfolding Var_def App_def Abs_def

    45   by (simp_all add: Abs1_eq_iff lam.fresh flip_def[symmetric] U_eqvt fresh_def lam.supp supp_at_base)

    46      (smt cx_cy_cz permute_flip_at Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+

    47 

    48 lemma Var_app:

    49   "Var \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"

    50   by (rule lam2_fast_app) (simp_all add: Var_App_Abs)

    51 

    52 lemma App_app:

    53   "App \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"

    54   by (rule lam3_fast_app[OF Var_App_Abs(2)]) (simp_all)

    55 

    56 lemma Abs_app:

    57   "Abs \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 0 \<cdot> x \<cdot> e"

    58   by (rule lam2_fast_app) (simp_all add: Var_App_Abs)

    59 

    60 lemma supp_Var_App_Abs[simp]:

    61   "supp Var = {}" "supp App = {}" "supp Abs = {}"

    62   by (simp_all add: Var_def App_def Abs_def lam.supp supp_at_base) blast+

    63 

    64 lemma Var_App_Abs_eqvt[eqvt]:

    65   "p \<bullet> Var = Var" "p \<bullet> App = App" "p \<bullet> Abs = Abs"

    66   by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)

    67 

    68 nominal_primrec

    69   Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)

    70 where

    71   "\<lbrace>V x\<rbrace> = Var \<cdot> (V x)"

    72 | Ap: "\<lbrace>M \<cdot> N\<rbrace> = App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"

    73 | "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)"

    74 proof auto

    75   fix x :: lam and P

    76   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"

    77   then show "P"

    78     by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)

    79        (auto simp add: Abs1_eq_iff fresh_star_def)[3]

    80 next

    81   fix x :: var and M and xa :: var and Ma

    82   assume "[[atom x]]lst. M = [[atom xa]]lst. Ma"

    83     "eqvt_at Numeral_sumC M"

    84   then show "[[atom x]]lst. Numeral_sumC M = [[atom xa]]lst. Numeral_sumC Ma"

    85     apply -

    86     apply (erule Abs_lst1_fcb)

    87     apply (simp_all add: Abs_fresh_iff)

    88     apply (erule fresh_eqvt_at)

    89     apply (simp_all add: finite_supp Abs1_eq_iff eqvt_at_def)

    90     done

    91 next

    92   show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def

    93     by (rule, perm_simp, rule)

    94 qed

    95 

    96 termination

    97   by (relation "measure (\<lambda>(t). size t)")

    98      (simp_all add: lam.size)

    99 

   100 lemma numeral_eqvt[eqvt]: "p \<bullet> \<lbrace>x\<rbrace> = \<lbrace>p \<bullet> x\<rbrace>"

   101   by (induct x rule: lam.induct)

   102      (simp_all add: Var_App_Abs_eqvt)

   103 

   104 lemma supp_numeral[simp]:

   105   "supp \<lbrace>x\<rbrace> = supp x"

   106   by (induct x rule: lam.induct)

   107      (simp_all add: lam.supp)

   108 

   109 lemma fresh_numeral[simp]:

   110   "x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y"

   111   unfolding fresh_def by simp

   112 

   113 fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where

   114   "app_lst n [] = V n"

   115 | "app_lst n (h # t) = Ap (app_lst n t) h"

   116 

   117 lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)"

   118   by (induct ts arbitrary: t p) (simp_all add: eqvts)

   119 

   120 lemma supp_app_lst: "supp (app_lst x l) = {atom x} \<union> supp l"

   121   apply (induct l)

   122   apply (simp_all add: supp_Nil lam.supp supp_at_base supp_Cons)

   123   by blast

   124 

   125 lemma app_lst_eq_iff: "app_lst n M = app_lst n N \<Longrightarrow> M = N"

   126   by (induct M N rule: list_induct2') simp_all

   127 

   128 lemma app_lst_rev_eq_iff: "app_lst n (rev M) = app_lst n (rev N) \<Longrightarrow> M = N"

   129   by (drule app_lst_eq_iff) simp

   130 

   131 nominal_primrec

   132   Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000)

   133 where

   134   [simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))"

   135   unfolding eqvt_def Ltgt_graph_def

   136   apply (rule, perm_simp, rule, rule)

   137   apply (rule_tac x="x" and ?'a="var" in obtain_fresh)

   138   apply (simp_all add: Abs1_eq_iff lam.fresh swap_fresh_fresh fresh_at_base)

   139   apply (simp add: eqvts swap_fresh_fresh)

   140   apply (case_tac "x = xa")

   141   apply simp_all

   142   apply (subgoal_tac "eqvt app_lst")

   143   apply (erule fresh_fun_eqvt_app2)

   144   apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)

   145   done

   146 

   147 termination

   148   by (relation "measure (\<lambda>t. size t)")

   149      (simp_all add: lam.size)

   150 

   151 lemma ltgt_eqvt[eqvt]:

   152   "p \<bullet> \<guillemotleft>t\<guillemotright> = \<guillemotleft>p \<bullet> t\<guillemotright>"

   153 proof -

   154   obtain x :: var where "atom x \<sharp> (t, p \<bullet> t)" using obtain_fresh by auto

   155   then have *: "atom x \<sharp> t" "atom x \<sharp> (p \<bullet> t)" using fresh_Pair by simp_all

   156   then show ?thesis using *[unfolded fresh_def]

   157     apply (simp add: Abs1_eq_iff lam.fresh app_lst_eqvt Ltgt.simps)

   158     apply (case_tac "p \<bullet> x = x")

   159     apply (simp_all add: eqvts)

   160     apply rule

   161     apply (subst swap_fresh_fresh)

   162     apply (simp_all add: fresh_at_base_permute_iff fresh_def[symmetric] fresh_at_base)

   163     apply (subgoal_tac "eqvt app_lst")

   164     apply (erule fresh_fun_eqvt_app2)

   165     apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)

   166     done

   167 qed

   168 

   169 lemma ltgt_eq_iff[simp]:

   170   "\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"

   171 proof auto

   172   obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto

   173   then have *: "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all

   174   then show "(\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright>) \<Longrightarrow> (M = N)" by (simp add: Abs1_eq_iff app_lst_rev_eq_iff Ltgt.simps)

   175 qed

   176 

   177 lemma Ltgt1_app: "\<guillemotleft>[M]\<guillemotright> \<cdot> N \<approx> N \<cdot> M"

   178 proof -

   179   obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto

   180   then have "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all

   181   then show ?thesis

   182   apply (subst Ltgt.simps)

   183   apply (simp add: fresh_Cons fresh_Nil)

   184   apply (rule b3, rule bI, simp add: b1)

   185   done

   186 qed

   187 

   188 lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P"

   189 proof -

   190   obtain x :: var where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto

   191   then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all

   192   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

   193   show ?thesis using *

   194     apply (subst Ltgt.simps)

   195   apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim)

   196   apply auto[1]

   197   apply (rule b3, rule bI, simp add: b1)

   198   done

   199 qed

   200 

   201 lemma supp_ltgt[simp]:

   202   "supp \<guillemotleft>t\<guillemotright> = supp t"

   203 proof -

   204   obtain x :: var where *:"atom x \<sharp> t" using obtain_fresh by auto

   205   show ?thesis using *

   206   by (simp_all add: Ltgt.simps lam.supp supp_at_base supp_Nil supp_app_lst supp_rev fresh_def)

   207 qed

   208 

   209 lemma fresh_ltgt[simp]:

   210   "x \<sharp> \<guillemotleft>[y]\<guillemotright> = x \<sharp> y"

   211   "x \<sharp> \<guillemotleft>[t,r,s]\<guillemotright> = x \<sharp> (t,r,s)"

   212   by (simp_all add: fresh_def supp_Cons supp_Nil supp_Pair)

   213 

   214 lemma Ltgt1_subst[simp]:

   215   "\<guillemotleft>[M]\<guillemotright> [y ::= A] = \<guillemotleft>[M [y ::= A]]\<guillemotright>"

   216 proof -

   217   obtain x :: var where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast

   218   have "x \<noteq> y" using a[simplified fresh_Pair fresh_at_base] by simp

   219   then show ?thesis

   220     apply (subst Ltgt.simps)

   221     using a apply (simp add: fresh_Nil fresh_Cons fresh_Pair_elim)

   222     apply (subst Ltgt.simps)

   223     using a apply (simp add: fresh_Pair_elim fresh_Nil fresh_Cons)

   224     apply (simp add: a)

   225     done

   226 qed

   227 

   228 lemma U_app:

   229   "\<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"

   230   by (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U, simp_all)

   231      (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U[simplified], simp_all)+

   232 

   233 definition "F1 \<equiv> \<integral>cx. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V cx))"

   234 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))"

   235 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)))))"

   236 

   237 

   238 lemma Lam_F:

   239   "F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))"

   240   "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))"

   241   "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)))))"

   242   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)

   243   apply (smt cx_cy_cz permute_flip_at)+

   244   done

   245 

   246 lemma supp_F[simp]:

   247   "supp F1 = {}" "supp F2 = {}" "supp F3 = {}"

   248   by (simp_all add: F1_def F2_def F3_def lam.supp supp_at_base)

   249      blast+

   250 

   251 lemma F_eqvt[eqvt]:

   252   "p \<bullet> F1 = F1" "p \<bullet> F2 = F2" "p \<bullet> F3 = F3"

   253   by (rule_tac [!] perm_supp_eq)

   254      (simp_all add: fresh_star_def fresh_def)

   255 

   256 lemma F_app:

   257   "F1 \<cdot> A \<approx> App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> A)"

   258   "F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"

   259   by (rule lam1_fast_app, rule Lam_F, simp_all)

   260      (rule lam3_fast_app, rule Lam_F, simp_all)

   261 

   262 lemma F3_app:

   263   assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *)

   264   shows "F3 \<cdot> A \<cdot> B \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> V x))))"

   265 proof -

   266   obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast

   267   obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast

   268   have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z"

   269     using b c by (simp_all add: fresh_Pair fresh_at_base) blast+

   270   have **:

   271     "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"

   272     "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y"

   273     "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A"

   274     "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B"

   275     using b c f by (simp_all add: fresh_Pair fresh_at_base) blast+

   276   show ?thesis

   277     apply (simp add: Lam_F(3)[of y z x] * *[symmetric])

   278     apply (rule b3) apply (rule b5) apply (rule bI)

   279     apply (simp add: ** fresh_Pair * *[symmetric])

   280     apply (rule b3) apply (rule bI)

   281     apply (simp add: ** fresh_Pair * *[symmetric])

   282     apply (rule b1)

   283     done

   284 qed

   285 

   286 definition Lam_A1_pre : "A1 \<equiv> \<integral>cx. \<integral>cy. (F1 \<cdot> V cx)"

   287 definition Lam_A2_pre : "A2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (F2 \<cdot> V cx \<cdot> V cy \<cdot> \<guillemotleft>[V cz]\<guillemotright>)"

   288 definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> V cx \<cdot> \<guillemotleft>[V cy]\<guillemotright>)"

   289 lemma Lam_A:

   290   "x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)"

   291   "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>)"

   292   "a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)"

   293   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)

   294   apply (smt cx_cy_cz permute_flip_at)+

   295   done

   296 

   297 lemma supp_A[simp]:

   298   "supp A1 = {}" "supp A2 = {}" "supp A3 = {}"

   299   by (auto simp add: Lam_A1_pre Lam_A2_pre Lam_A3_pre lam.supp supp_at_base supp_Cons supp_Nil)

   300 

   301 lemma A_app:

   302   "A1 \<cdot> A \<cdot> B \<approx> F1 \<cdot> A"

   303   "A2 \<cdot> A \<cdot> B \<cdot> C \<approx> F2 \<cdot> A \<cdot> B \<cdot> \<guillemotleft>[C]\<guillemotright>"

   304   "A3 \<cdot> A \<cdot> B \<approx> F3 \<cdot> A \<cdot> \<guillemotleft>[B]\<guillemotright>"

   305   apply (rule lam2_fast_app, rule Lam_A, simp_all)

   306   apply (rule lam3_fast_app, rule Lam_A, simp_all)

   307   apply (rule lam2_fast_app, rule Lam_A, simp_all)

   308   done

   309 

   310 definition "Num \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>"

   311 

   312 lemma supp_Num[simp]:

   313   "supp Num = {}"

   314   by (auto simp only: Num_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil)

   315 

   316 end