1 theory Term5

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "Rsp" "../Attic/Prove"

     3 begin

     4 

     5 atom_decl name

     6 

     7 datatype rtrm5 =

     8   rVr5 "name"

     9 | rAp5 "rtrm5" "rtrm5"

    10 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"

    11 and rlts =

    12   rLnil

    13 | rLcons "name" "rtrm5" "rlts"

    14 

    15 primrec

    16   rbv5

    17 where

    18   "rbv5 rLnil = {}"

    19 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"

    20 

    21 

    22 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term5.rtrm5") 2 *}

    23 print_theorems

    24 

    25 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term5.rtrm5")

    26   [[[], [], [(SOME (@{term rbv5}, false), 0, 1)]], [[], []]] [(@{term rbv5}, 1, [[], [0, 2]])] *}

    27 print_theorems

    28 

    29 notation

    30   alpha_rtrm5 ("_ \<approx>5 _" [100, 100] 100) and

    31   alpha_rlts ("_ \<approx>l _" [100, 100] 100)

    32 thm alpha_rtrm5_alpha_rlts_alpha_rbv5.intros

    33 

    34 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_inj}, []), (build_alpha_inj @{thms alpha_rtrm5_alpha_rlts_alpha_rbv5.intros} @{thms rtrm5.distinct rtrm5.inject rlts.distinct rlts.inject} @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} ctxt)) ctxt)) *}

    35 thm alpha5_inj

    36 

    37 lemma rbv5_eqvt[eqvt]:

    38   "pi \<bullet> (rbv5 x) = rbv5 (pi \<bullet> x)"

    39   apply (induct x)

    40   apply (simp_all add: eqvts atom_eqvt)

    41   done

    42 

    43 lemma fv_rtrm5_rlts_eqvt[eqvt]:

    44   "pi \<bullet> (fv_rtrm5 x) = fv_rtrm5 (pi \<bullet> x)"

    45   "pi \<bullet> (fv_rlts l) = fv_rlts (pi \<bullet> l)"

    46   "pi \<bullet> (fv_rbv5 l) = fv_rbv5 (pi \<bullet> l)"

    47   apply (induct x and l)

    48   apply (simp_all add: eqvts atom_eqvt)

    49   done

    50 

    51 local_setup {*

    52 (fn ctxt => snd (Local_Theory.note ((@{binding alpha5_eqvt}, []),

    53 build_alpha_eqvts [@{term alpha_rtrm5}, @{term alpha_rlts}, @{term alpha_rbv5}] (fn _ => alpha_eqvt_tac  @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} ctxt 1) ctxt) ctxt)) *}

    54 print_theorems

    55 

    56 lemma alpha5_equivp:

    57   "equivp alpha_rtrm5"

    58   "equivp alpha_rlts"

    59   sorry

    60 

    61 quotient_type

    62   trm5 = rtrm5 / alpha_rtrm5

    63 and

    64   lts = rlts / alpha_rlts

    65   by (auto intro: alpha5_equivp)

    66 

    67 local_setup {*

    68 (fn ctxt => ctxt

    69  |> snd o (Quotient_Def.quotient_lift_const ("Vr5", @{term rVr5}))

    70  |> snd o (Quotient_Def.quotient_lift_const ("Ap5", @{term rAp5}))

    71  |> snd o (Quotient_Def.quotient_lift_const ("Lt5", @{term rLt5}))

    72  |> snd o (Quotient_Def.quotient_lift_const ("Lnil", @{term rLnil}))

    73  |> snd o (Quotient_Def.quotient_lift_const ("Lcons", @{term rLcons}))

    74  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm5", @{term fv_rtrm5}))

    75  |> snd o (Quotient_Def.quotient_lift_const ("fv_lts", @{term fv_rlts}))

    76  |> snd o (Quotient_Def.quotient_lift_const ("fv_bv5", @{term fv_rbv5}))

    77  |> snd o (Quotient_Def.quotient_lift_const ("bv5", @{term rbv5}))

    78  |> snd o (Quotient_Def.quotient_lift_const ("alpha_bv5", @{term alpha_rbv5})))

    79 *}

    80 print_theorems

    81 

    82 lemma alpha5_rfv:

    83   "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)"

    84   "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))"

    85   "(alpha_rbv5 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)"

    86   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts)

    87   apply(simp_all)

    88   apply(simp add: alpha_gen)

    89   done

    90 

    91 lemma bv_list_rsp:

    92   shows "x \<approx>l y \<Longrightarrow> rbv5 x = rbv5 y"

    93   apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))

    94   apply(simp_all)

    95   apply(clarify)

    96   apply simp

    97   done

    98 

    99 lemma alpha_rbv5_rsp: "xa \<approx>l y \<Longrightarrow> xb \<approx>l ya \<Longrightarrow> alpha_rbv5 xa xb = alpha_rbv5 y ya"

   100   apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))

   101   apply (erule_tac[!] alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))

   102   apply (simp_all)

   103   defer defer (* should follow from distinctness *)

   104   apply clarify

   105   apply (simp add: alpha5_inj)

   106   sorry (* should be true? *)

   107 

   108 lemma [quot_respect]:

   109   "(alpha_rlts ===> op =) fv_rlts fv_rlts"

   110   "(alpha_rlts ===> op =) fv_rbv5 fv_rbv5"

   111   "(alpha_rtrm5 ===> op =) fv_rtrm5 fv_rtrm5"

   112   "(alpha_rlts ===> op =) rbv5 rbv5"

   113   "(op = ===> alpha_rtrm5) rVr5 rVr5"

   114   "(alpha_rtrm5 ===> alpha_rtrm5 ===> alpha_rtrm5) rAp5 rAp5"

   115   "(alpha_rlts ===> alpha_rtrm5 ===> alpha_rtrm5) rLt5 rLt5"

   116   "(op = ===> alpha_rtrm5 ===> alpha_rlts ===> alpha_rlts) rLcons rLcons"

   117   "(op = ===> alpha_rtrm5 ===> alpha_rtrm5) permute permute"

   118   "(op = ===> alpha_rlts ===> alpha_rlts) permute permute"

   119   "(alpha_rlts ===> alpha_rlts ===> op =) alpha_rbv5 alpha_rbv5"

   120   apply (simp_all add: alpha5_inj alpha5_rfv alpha5_eqvt bv_list_rsp alpha_rbv5_rsp)

   121   apply (clarify)

   122   apply (rule conjI)

   123   apply (erule alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts(2))

   124   apply (simp_all add: alpha5_inj)

   125   apply clarify

   126   apply (rule_tac x="0" in exI) apply (simp add: fresh_star_def fresh_zero_perm alpha_gen alpha5_rfv)

   127 done

   128 

   129 lemma

   130   shows "(alpha_rlts ===> op =) rbv5 rbv5"

   131   by (simp add: bv_list_rsp)

   132 

   133 lemmas trm5_lts_inducts = rtrm5_rlts.inducts[quot_lifted]

   134 

   135 instantiation trm5 and lts :: pt

   136 begin

   137 

   138 quotient_definition

   139   "permute_trm5 :: perm \<Rightarrow> trm5 \<Rightarrow> trm5"

   140 is

   141   "permute :: perm \<Rightarrow> rtrm5 \<Rightarrow> rtrm5"

   142 

   143 quotient_definition

   144   "permute_lts :: perm \<Rightarrow> lts \<Rightarrow> lts"

   145 is

   146   "permute :: perm \<Rightarrow> rlts \<Rightarrow> rlts"

   147 

   148 instance by default

   149   (simp_all add: permute_rtrm5_permute_rlts_zero[quot_lifted] permute_rtrm5_permute_rlts_append[quot_lifted])

   150 

   151 end

   152 

   153 lemmas permute_trm5_lts = permute_rtrm5_permute_rlts.simps[quot_lifted]

   154 lemmas bv5[simp] = rbv5.simps[quot_lifted]

   155 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted]

   156 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted]

   157 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]

   158 

   159 lemma lets_bla:

   160   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) \<noteq> (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))"

   161 apply (simp only: alpha5_INJ)

   162 apply (simp only: bv5)

   163 apply simp

   164 done

   165 

   166 lemma lets_ok:

   167   "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))"

   168 apply (simp add: alpha5_INJ)

   169 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)

   170 apply (simp_all add: alpha_gen)

   171 apply (simp add: permute_trm5_lts fresh_star_def)

   172 apply (metis flip_at_simps(1) supp_at_base supp_eqvt)

   173 done

   174 

   175 lemma lets_ok3:

   176   "x \<noteq> y \<Longrightarrow>

   177    (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>

   178    (Lt5 (Lcons y (Ap5 (Vr5 x) (Vr5 y)) (Lcons x (Vr5 x) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"

   179 apply (simp add: permute_trm5_lts alpha_gen alpha5_INJ)

   180 done

   181 

   182 

   183 lemma lets_not_ok1:

   184   "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) =

   185    (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"

   186 apply (simp add: alpha5_INJ alpha_gen)

   187 apply (rule_tac x="0::perm" in exI)

   188 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts)

   189 apply auto

   190 done

   191 

   192 lemma distinct_helper:

   193   shows "\<not>(rVr5 x \<approx>5 rAp5 y z)"

   194   apply auto

   195   apply (erule alpha_rtrm5.cases)

   196   apply (simp_all only: rtrm5.distinct)

   197   done

   198 

   199 lemma distinct_helper2:

   200   shows "(Vr5 x) \<noteq> (Ap5 y z)"

   201   by (lifting distinct_helper)

   202 

   203 lemma lets_nok:

   204   "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>

   205    (Lt5 (Lcons x (Ap5 (Vr5 z) (Vr5 z)) (Lcons y (Vr5 z) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq>

   206    (Lt5 (Lcons y (Vr5 z) (Lcons x (Ap5 (Vr5 z) (Vr5 z)) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))"

   207 apply (simp only: alpha5_INJ(3) alpha5_INJ(5) alpha_gen permute_trm5_lts fresh_star_def)

   208 apply (simp add: distinct_helper2 alpha5_INJ permute_trm5_lts)

   209 done

   210 

   211 end