1 theory Term8

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

     3 begin

     4 

     5 atom_decl name

     6 

     7 datatype rfoo8 =

     8   Foo0 "name"

     9 | Foo1 "rbar8" "rfoo8" --"bind bv(bar) in foo"

    10 and rbar8 =

    11   Bar0 "name"

    12 | Bar1 "name" "name" "rbar8" --"bind second name in b"

    13 

    14 primrec

    15   rbv8

    16 where

    17   "rbv8 (Bar0 x) = {}"

    18 | "rbv8 (Bar1 v x b) = {atom v}"

    19 

    20 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term8.rfoo8") 2 *}

    21 print_theorems

    22 

    23 local_setup {* snd o define_fv_alpha (Datatype.the_info @{theory} "Term8.rfoo8") [

    24   [[[]], [[], [(SOME @{term rbv8}, 0)]]], [[[]], [[], [(NONE, 1)], [(NONE, 1)]]]] *}

    25 notation

    26   alpha_rfoo8 ("_ \<approx>f' _" [100, 100] 100) and

    27   alpha_rbar8 ("_ \<approx>b' _" [100, 100] 100)

    28 thm alpha_rfoo8_alpha_rbar8.intros

    29 

    30 

    31 inductive

    32   alpha8f :: "rfoo8 \<Rightarrow> rfoo8 \<Rightarrow> bool" ("_ \<approx>f _" [100, 100] 100)

    33 and

    34   alpha8b :: "rbar8 \<Rightarrow> rbar8 \<Rightarrow> bool" ("_ \<approx>b _" [100, 100] 100)

    35 where

    36   a1: "a = b \<Longrightarrow> (Foo0 a) \<approx>f (Foo0 b)"

    37 | a2: "a = b \<Longrightarrow> (Bar0 a) \<approx>b (Bar0 b)"

    38 | a3: "b1 \<approx>b b2 \<Longrightarrow> (\<exists>pi. (((rbv8 b1), t1) \<approx>gen alpha8f fv_rfoo8 pi ((rbv8 b2), t2))) \<Longrightarrow> Foo1 b1 t1 \<approx>f Foo1 b2 t2"

    39 | a4: "v1 = v2 \<Longrightarrow> (\<exists>pi. (({atom x1}, t1) \<approx>gen alpha8b fv_rbar8 pi ({atom x2}, t2))) \<Longrightarrow> Bar1 v1 x1 t1 \<approx>b Bar1 v2 x2 t2"

    40 

    41 lemma "(alpha8b ===> op =) rbv8 rbv8"

    42   apply simp apply clarify

    43   apply (erule alpha8f_alpha8b.inducts(2))

    44   apply (simp_all)

    45 done

    46 

    47 lemma fv_rbar8_rsp_hlp: "x \<approx>b y \<Longrightarrow> fv_rbar8 x = fv_rbar8 y"

    48   apply (erule alpha8f_alpha8b.inducts(2))

    49   apply (simp_all add: alpha_gen)

    50 done

    51 lemma "(alpha8b ===> op =) fv_rbar8 fv_rbar8"

    52   apply simp apply clarify apply (simp add: fv_rbar8_rsp_hlp)

    53 done

    54 

    55 lemma "(alpha8f ===> op =) fv_rfoo8 fv_rfoo8"

    56   apply simp apply clarify

    57   apply (erule alpha8f_alpha8b.inducts(1))

    58   apply (simp_all add: alpha_gen fv_rbar8_rsp_hlp)

    59 done

    60 

    61 end