1 theory Term2

     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 single assignments ***}

     8 

     9 datatype rtrm2 =

    10   rVr2 "name"

    11 | rAp2 "rtrm2" "rtrm2"

    12 | rLm2 "name" "rtrm2" --"bind (name) in (rtrm2)"

    13 | rLt2 "rassign" "rtrm2" --"bind (bv2 rassign) in (rtrm2)"

    14 and rassign =

    15   rAs "name" "rtrm2"

    16 

    17 (* to be given by the user *)

    18 primrec

    19   rbv2

    20 where

    21   "rbv2 (rAs x t) = {atom x}"

    22 

    23 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term2.rtrm2") 2 *}

    24 

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

    26   [[[],

    27     [],

    28     [(NONE, 0, 1)],

    29     [(SOME @{term rbv2}, 0, 1)]],

    30    [[]]] *}

    31 

    32 notation

    33   alpha_rtrm2 ("_ \<approx>2 _" [100, 100] 100) and

    34   alpha_rassign ("_ \<approx>2b _" [100, 100] 100)

    35 thm alpha_rtrm2_alpha_rassign.intros

    36 

    37 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha2_inj}, []), (build_alpha_inj @{thms alpha_rtrm2_alpha_rassign.intros} @{thms rtrm2.distinct rtrm2.inject rassign.distinct rassign.inject} @{thms alpha_rtrm2.cases alpha_rassign.cases} ctxt)) ctxt)) *}

    38 thm alpha2_inj

    39 

    40 lemma alpha2_eqvt:

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

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

    43 sorry

    44 

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

    46   (build_equivps [@{term alpha_rtrm2}, @{term alpha_rassign}] @{thm rtrm2_rassign.induct} @{thm alpha_rtrm2_alpha_rassign.induct} @{thms rtrm2.inject rassign.inject} @{thms alpha2_inj} @{thms rtrm2.distinct rassign.distinct} @{thms alpha_rtrm2.cases alpha_rassign.cases} @{thms alpha2_eqvt} ctxt)) ctxt)) *}

    47 thm alpha2_equivp

    48 

    49 local_setup  {* define_quotient_type 

    50   [(([], @{binding trm2}, NoSyn), (@{typ rtrm2}, @{term alpha_rtrm2})),

    51    (([], @{binding assign}, NoSyn), (@{typ rassign}, @{term alpha_rassign}))]

    52   ((rtac @{thm alpha2_equivp(1)} 1) THEN (rtac @{thm alpha2_equivp(2)}) 1) *}

    53 

    54 local_setup {*

    55 (fn ctxt => ctxt

    56  |> snd o (Quotient_Def.quotient_lift_const ("Vr2", @{term rVr2}))

    57  |> snd o (Quotient_Def.quotient_lift_const ("Ap2", @{term rAp2}))

    58  |> snd o (Quotient_Def.quotient_lift_const ("Lm2", @{term rLm2}))

    59  |> snd o (Quotient_Def.quotient_lift_const ("Lt2", @{term rLt2}))

    60  |> snd o (Quotient_Def.quotient_lift_const ("As", @{term rAs}))

    61  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm2", @{term fv_rtrm2}))

    62  |> snd o (Quotient_Def.quotient_lift_const ("bv2", @{term rbv2})))

    63 *}

    64 print_theorems

    65 

    66 local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]

    67   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}

    68 local_setup {* snd o prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]

    69   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}

    70 local_setup {* snd o prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]

    71   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

    72 local_setup {* snd o prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]

    73   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

    74 local_setup {* snd o prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]

    75   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}

    76 local_setup {* snd o prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]

    77   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *}

    78 local_setup {* snd o prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]

    79   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}

    80 

    81 end