7 thm abs_fresh(1)

     7 datatype rlam =

     8 

     9 nominal_datatype rlam =

    14 print_theorems

    12 fun

    15 

    16 function

    22 sorry

    18 

    23 

    19 overloading

    24 termination rfv sorry

    20   perm_rlam    \<equiv> "perm :: 'x prm \<Rightarrow> rlam \<Rightarrow> rlam"   (unchecked)

    21 begin

    22 

    23 fun

    24   perm_rlam

    25 where

    26   "perm_rlam pi (rVar a) = rVar (pi \<bullet> a)"

    27 | "perm_rlam pi (rApp t1 t2) = rApp (perm_rlam pi t1) (perm_rlam pi t2)"

    28 | "perm_rlam pi (rLam a t) = rLam (pi \<bullet> a) (perm_rlam pi t)"

    29 

    30 end

    31 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"

    37 | a3: "\<lbrakk>t \<approx> ([(a,b)] \<bullet> s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"

    32 

    38 

    33 print_theorems

    39 lemma helper:

    40   fixes t::"rlam"

    41   and   a::"name"

    42   shows "[(a, a)] \<bullet> t = t"

    43 by (induct t)

    44    (auto simp add: calc_atm)

    42   apply(subst pt_swap_bij'')

    53   apply(simp add: helper)

    43   apply(rule pt_name_inst)

    44   apply(rule at_name_inst)

    45   apply(simp)

    54   apply(rule alpha_equivp)

    62   by (rule alpha_equivp)

    55   done

    63 

    56 

    57 print_quotients

   100 (* lemmas that need to lift *)

   105 (* lemmas that need to be lifted *)

   101 lemma pi_var_com:

   106 lemma pi_var_eqvt1:

   102   fixes pi::"'x prm"

   107   fixes pi::"'x prm"

   103   shows "(pi\<bullet>rVar a) \<approx> rVar (pi\<bullet>a)"

   108   shows "(pi \<bullet> rVar a) \<approx> rVar (pi \<bullet> a)"

   104   sorry

   109   by (simp add: alpha_refl)

   105 

   110 

   106 lemma pi_app_com:

   111 lemma pi_var_eqvt2:

   107   fixes pi::"'x prm"

   112   fixes pi::"'x prm"

   108   shows "(pi\<bullet>rApp t1 t2) \<approx> rApp (pi\<bullet>t1) (pi\<bullet>t2)"

   113   shows "(pi \<bullet> rVar a) = rVar (pi \<bullet> a)"

   109   sorry

   114   by (simp)

   110 

   115 

   111 lemma pi_lam_com:

   116 lemma pi_app_eqvt1:

   112   fixes pi::"'x prm"

   117   fixes pi::"'x prm"

   113   shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"

   118   shows "(pi \<bullet> rApp t1 t2) \<approx> rApp (pi \<bullet> t1) (pi \<bullet> t2)"

   114   sorry

   119   by (simp add: alpha_refl)

   115 

   120 

   121 lemma pi_app_eqvt2:

   122   fixes pi::"'x prm"

   123   shows "(pi \<bullet> rApp t1 t2) = rApp (pi \<bullet> t1) (pi \<bullet> t2)"

   124   by (simp)

   125 

   126 lemma pi_lam_eqvt1:

   127   fixes pi::"'x prm"

   128   shows "(pi \<bullet> rLam a t) \<approx> rLam (pi \<bullet> a) (pi \<bullet> t)"

   129   by (simp add: alpha_refl)

   130 

   131 lemma pi_lam_eqvt2:

   132   fixes pi::"'x prm"

   133   shows "(pi \<bullet> rLam a t) = rLam (pi \<bullet> a) (pi \<bullet> t)"

   134   by (simp add: alpha)

   139 by (auto intro:a1)

   158 by (auto intro: a1)

   142 by (auto intro:a2)

   161 by (auto intro: a2)

   147   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)

   166   apply(simp add: helper)

   148   apply(rule sym)

   167   apply(simp)

   149   apply(rule trans)

   168   done

   150   apply(rule pt_name3)

   169 

   151   apply(rule at_ds1[OF at_name_inst])

   170 lemma rfv_rsp[quot_respect]: 

   152   apply(simp add: pt_name1)

   171   "(alpha ===> op =) rfv rfv"

   153   apply(assumption)

   154   apply(simp add: abs_fresh)

   155   done

   156 

   157 lemma rfv_rsp[quot_respect]: "(alpha ===> op =) rfv rfv"

   167 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"

   181 lemma pi_var1:

   168 apply (lifting pi_var_com)

   182   fixes pi::"'x prm"

   169 done

   183   shows "pi \<bullet> Var a = Var (pi \<bullet> a)"

   170 

   184   by (lifting pi_var_eqvt1)

   171 lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"

   185 

   172 apply (lifting pi_app_com)

   186 lemma pi_var2:

   173 done

   187   fixes pi::"'x prm"

   174 

   188   shows "pi \<bullet> Var a = Var (pi \<bullet> a)"

   175 lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"

   189   by (lifting pi_var_eqvt2)

   176 apply (lifting pi_lam_com)

   190 

   177 done

   191 

   178 

   192 lemma pi_app: 

   179 lemma fv_var: "fv (Var (a\<Colon>name)) = {a}"

   193   fixes pi::"'x prm"

   180 apply (lifting rfv_var)

   194   shows "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)"

   181 done

   195   by (lifting pi_app_eqvt2)

   182 

   196 

   183 lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"

   197 lemma pi_lam: 

   184 apply (lifting rfv_app)

   198   fixes pi::"'x prm"

   185 done

   199   shows "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)"

   186 

   200   by (lifting pi_lam_eqvt2)

   187 lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"

   201 

   188 apply (lifting rfv_lam)

   202 lemma fv_var: 

   189 done

   203   shows "fv (Var a) = {a}"

   190 

   204   by  (lifting rfv_var)

   191 lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"

   205 

   192 apply (lifting a1)

   206 lemma fv_app: 

   193 done

   207   shows "fv (App t1 t2) = fv t1 \<union> fv t2"

   194 

   208   by (lifting rfv_app)

   195 lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"

   209 

   196 apply (lifting a2)

   210 lemma fv_lam: 

   197 done

   211   shows "fv (Lam a t) = fv t - {a}"

   198 

   212   by (lifting rfv_lam)

   199 lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"

   213 

   200 apply (lifting a3)

   214 lemma a1: 

   201 done

   215   "a = b \<Longrightarrow> Var a = Var b"

   202 

   216   by  (lifting a1)

   203 lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;

   217 

   204      \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;

   218 lemma a2: 

   205      \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>

   219   "\<lbrakk>x = xa; xb = xc\<rbrakk> \<Longrightarrow> App x xb = App xa xc"

   220   by  (lifting a2)

   221 

   222 lemma a3: 

   223   "\<lbrakk>x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"

   224   by  (lifting a3)

   225 

   226 lemma alpha_cases: 

   227   "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;

   228     \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;

   229     \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>

   207 apply (lifting alpha.cases)

   231   by (lifting alpha.cases)

   208 done

   232 

   209 

   233 lemma alpha_induct: 

   210 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);

   234   "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);

   211      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);

   235     \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);

   212      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.

   236      \<And>x a b xa.

   215 apply (lifting alpha.induct)

   239   by (lifting alpha.induct)

   216 done

   240 

   217 

   241 lemma var_inject: 

   218 lemma var_inject: "(Var a = Var b) = (a = b)"

   242   "(Var a = Var b) = (a = b)"

   219 apply (lifting rvar_inject)

   243   by (lifting rvar_inject)

   220 done

   244 

   221 

   245 lemma lam_induct:

   222 lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);

   246   "\<lbrakk>\<And>name. P (Var name); 

   223               \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"

   247     \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);

   224 apply (lifting rlam.induct)

   248     \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"

   225 done

   249   by (lifting rlam.induct)

   230   apply(simp add: pi_var)

   254   apply(simp add: pi_var2)

   236   shows "(a\<sharp>(Var b)) = (a\<sharp>b)"

   260   shows "(a \<sharp> (Var b)) = (a \<sharp> b)"