1 theory LamEx

     2 imports Nominal QuotMain

     3 begin

     4 

     5 atom_decl name

     6 

     7 nominal_datatype rlam =

     8   rVar "name"

     9 | rApp "rlam" "rlam"

    10 | rLam "name" "rlam"

    11 

    12 inductive 

    13   alpha :: "rlam \<Rightarrow> rlam \<Rightarrow> bool" ("_ \<approx> _" [100, 100] 100)

    14 where

    15   a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)"

    16 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"

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

    18 

    19 quotient lam = rlam / alpha

    20 sorry

    21 

    22 local_setup {*

    23   make_const_def @{binding Var} @{term "rVar"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>

    24   make_const_def @{binding App} @{term "rApp"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd #>

    25   make_const_def @{binding Lam} @{term "rLam"} NoSyn @{typ "rlam"} @{typ "lam"} #> snd

    26 *}

    27 

    28 lemma real_alpha:

    29   assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"

    30   shows "Lam a t = Lam b s"

    31 sorry