1 header {* Constant definitions *}

     2 

     3 theory Consts imports Utils begin

     4 

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

     6 where

     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"

     9 

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

    11   by auto

    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 

    17 lemma Lam_U:

    18   assumes "x \<noteq> y" "y \<noteq> z" "x \<noteq> z"

    19   shows "Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. Var z"

    20         "Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. Var y"

    21         "Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. Var x"

    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)

    23   apply (intro impI conjI)

    24   apply (metis assms)+

    25   done

    26 

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

    28   by (induct m)

    29      (auto simp add: lam.supp supp_at_base Umn.simps le_Suc_eq)

    30 

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

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

    33 

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

    35   using supp_U1 supp_U2

    36   by blast

    37 

    38 lemma U_eqvt:

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

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

    41 

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

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

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

    45 

    46 lemma VAR_APP_Abs:

    47   "x \<noteq> e \<Longrightarrow> VAR = \<integral>x. \<integral>e. (Var e \<cdot> Umn 2 2 \<cdot> Var x \<cdot> Var 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)"

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

    50   unfolding VAR_def APP_def Abs_def

    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)

    52      (auto simp only: cx_cy_cz cx_cy_cz[symmetric])

    53 

    54 lemma VAR_app:

    55   "VAR \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"

    56   by (rule lam2_fast_app[OF VAR_APP_Abs(1)]) simp_all

    57 

    58 lemma APP_app:

    59   "APP \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"

    60   by (rule lam3_fast_app[OF VAR_APP_Abs(2)]) (simp_all)

    61 

    62 lemma Abs_app:

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

    64   by (rule lam2_fast_app[OF VAR_APP_Abs(3)]) simp_all

    65 

    66 lemma supp_VAR_APP_Abs[simp]:

    67   "supp VAR = {}" "supp APP = {}" "supp Abs = {}"

    68   by (simp_all add: VAR_def APP_def Abs_def lam.supp supp_at_base) blast+

    69 

    70 lemma VAR_APP_Abs_eqvt[eqvt]:

    71   "p \<bullet> VAR = VAR" "p \<bullet> APP = APP" "p \<bullet> Abs = Abs"

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

    73 

    74 nominal_primrec

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

    76 where

    77   "\<lbrace>Var x\<rbrace> = VAR \<cdot> (Var x)"

    78 | Ap: "\<lbrace>M \<cdot> N\<rbrace> = APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"

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

    80 proof auto

    81   fix x :: lam and 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"

    83   then show "P"

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

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

    86 next

    87   fix x :: name and M and xa :: name and Ma

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

    89     "eqvt_at Numeral_sumC M"

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

    91     apply -

    92     apply (erule Abs_lst1_fcb)

    93     apply (simp_all add: Abs_fresh_iff)

    94     apply (erule fresh_eqvt_at)

    95     apply (simp_all add: finite_supp Abs1_eq_iff eqvt_at_def)

    96     done

    97 next

    98   show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def

    99     by (rule, perm_simp, rule)

   100 qed

   101 

   102 termination (eqvt) by lexicographic_order

   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 :: "name \<Rightarrow> lam list \<Rightarrow> lam" where

   114   "app_lst n [] = Var n"

   115 | "app_lst n (h # t) = (app_lst n t) \<cdot> 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="name" 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 (eqvt) by lexicographic_order

   148 

   149 lemma ltgt_eq_iff[simp]:

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

   151 proof auto

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

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

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

   155 qed

   156 

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

   158 proof -

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

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

   161   then show ?thesis

   162   apply (subst Ltgt.simps)

   163   apply (simp add: fresh_Cons fresh_Nil)

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

   165   done

   166 qed

   167 

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

   169 proof -

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

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

   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

   173   show ?thesis using *

   174     apply (subst Ltgt.simps)

   175   apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim)

   176   apply auto[1]

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

   178   done

   179 qed

   180 

   181 lemma supp_ltgt[simp]:

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

   183 proof -

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

   185   show ?thesis using *

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

   187 qed

   188 

   189 lemma fresh_ltgt[simp]:

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

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

   192   by (simp_all add: fresh_def supp_Cons supp_Nil supp_Pair)

   193 

   194 lemma Ltgt1_subst[simp]:

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

   196 proof -

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

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

   199   then show ?thesis

   200     apply (subst Ltgt.simps)

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

   202     apply (subst Ltgt.simps)

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

   204     apply (simp add: a)

   205     done

   206 qed

   207 

   208 lemma U_app:

   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"

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

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

   212 

   213 definition "F1 \<equiv> \<integral>cx. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var cx))"

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

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

   216 

   217 

   218 lemma Lam_F:

   219   "F1 = \<integral>x. (APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var x))"

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

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

   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)

   223      (auto simp add: cx_cy_cz cx_cy_cz[symmetric])

   224 

   225 lemma supp_F[simp]:

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

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

   228      blast+

   229 

   230 lemma F_eqvt[eqvt]:

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

   232   by (rule_tac [!] perm_supp_eq)

   233      (simp_all add: fresh_star_def fresh_def)

   234 

   235 lemma F_app:

   236   "F1 \<cdot> A \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> A)"

   237   "F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"

   238   by (rule lam1_fast_app, rule Lam_F, simp_all)

   239      (rule lam3_fast_app, rule Lam_F, simp_all)

   240 

   241 lemma F3_app:

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

   243   shows "F3 \<cdot> A \<cdot> B \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> Var x))))"

   244 proof -

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

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

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

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

   249   have **:

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

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

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

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

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

   255   show ?thesis

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

   257     apply (rule b3) apply (rule b5) apply (rule bI)

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

   259     apply (rule b3) apply (rule bI)

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

   261     apply (rule b1)

   262     done

   263 qed

   264 

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

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

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

   268 lemma Lam_A:

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

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

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

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

   273      auto

   274 

   275 lemma supp_A[simp]:

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

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

   278 

   279 lemma A_app:

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

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

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

   283   apply (rule lam2_fast_app, rule Lam_A, simp_all)

   284   apply (rule lam3_fast_app, rule Lam_A, simp_all)

   285   apply (rule lam2_fast_app, rule Lam_A, simp_all)

   286   done

   287 

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

   289 

   290 lemma supp_Num[simp]:

   291   "supp Num = {}"

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

   293 

   294 end