1 theory Term3

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

     3 begin

     4 

     5 atom_decl name

     6 

     7 section {*** lets with many assignments ***}

     8 

     9 datatype rtrm3 =

    10   rVr3 "name"

    11 | rAp3 "rtrm3" "rtrm3"

    12 | rLm3 "name" "rtrm3" --"bind (name) in (trm3)"

    13 | rLt3 "rassigns" "rtrm3" --"bind (bv3 assigns) in (trm3)"

    14 and rassigns =

    15   rANil

    16 | rACons "name" "rtrm3" "rassigns"

    17 

    18 (* to be given by the user *)

    19 primrec 

    20   bv3

    21 where

    22   "bv3 rANil = {}"

    23 | "bv3 (rACons x t as) = {atom x} \<union> (bv3 as)"

    24 

    25 setup {* snd o define_raw_perms ["rtrm3", "rassigns"] ["Term3.rtrm3", "Term3.rassigns"] *}

    26 

    27 local_setup {* snd o define_fv_alpha "Term3.rtrm3"

    28   [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [(SOME @{term bv3}, 0)]]],

    29    [[], [[], [], []]]] *}

    30 print_theorems

    31 

    32 notation

    33   alpha_rtrm3 ("_ \<approx>3 _" [100, 100] 100) and

    34   alpha_rassigns ("_ \<approx>3a _" [100, 100] 100)

    35 thm alpha_rtrm3_alpha_rassigns.intros

    36 

    37 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_inj}, []), (build_alpha_inj @{thms alpha_rtrm3_alpha_rassigns.intros} @{thms rtrm3.distinct rtrm3.inject rassigns.distinct rassigns.inject} @{thms alpha_rtrm3.cases alpha_rassigns.cases} ctxt)) ctxt)) *}

    38 thm alpha3_inj

    39 

    40 lemma alpha3_eqvt:

    41   "t \<approx>3 s \<Longrightarrow> (pi \<bullet> t) \<approx>3 (pi \<bullet> s)"

    42   "a \<approx>3a b \<Longrightarrow> (pi \<bullet> a) \<approx>3a (pi \<bullet> b)"

    43 sorry

    44 

    45 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha3_equivp}, []),

    46   (build_equivps [@{term alpha_rtrm3}, @{term alpha_rassigns}] @{thm rtrm3_rassigns.induct} @{thm alpha_rtrm3_alpha_rassigns.induct} @{thms rtrm3.inject rassigns.inject} @{thms alpha3_inj} @{thms rtrm3.distinct rassigns.distinct} @{thms alpha_rtrm3.cases alpha_rassigns.cases} @{thms alpha3_eqvt} ctxt)) ctxt)) *}

    47 thm alpha3_equivp

    48 

    49 quotient_type

    50   trm3 = rtrm3 / alpha_rtrm3

    51 and

    52   assigns = rassigns / alpha_rassigns

    53   by (rule alpha3_equivp(1)) (rule alpha3_equivp(2))

    54 

    55 end