theory Classical
imports "../NewParser"
begin

(* example from my Urban's PhD *)

(* 
  alpha_trm_raw is incorrectly defined, therefore the equivalence proof
  does not go through; below the correct definition is given
*)

atom_decl name
atom_decl coname

ML {* val _ = cheat_equivp := true *}

nominal_datatype trm =
   Ax "name" "coname"
|  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"              bind n in t1, bind c in t2
|  AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname"  bind c1 in t1, bind c2 in t2
|  AndL1 n::"name" t::"trm" "name"                              bind n in t
|  AndL2 n::"name" t::"trm" "name"                              bind n in t
|  ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name"        bind c in t1, bind n in t2
|  ImpR c::"coname" n::"name" t::"trm" "coname"                 bind n c in t


thm trm.fv
thm trm.eq_iff
thm trm.bn
thm trm.perm
thm trm.induct
thm trm.distinct
thm trm.fv[simplified trm.supp]

(* correct alpha definition *)

inductive
  alpha
where
  "\<lbrakk>name = namea; coname = conamea\<rbrakk> \<Longrightarrow> 
  alpha (Ax_raw name coname) (Ax_raw namea conamea)"
| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a); 
    \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a)\<rbrakk> \<Longrightarrow>
   alpha (Cut_raw coname1 trm_raw1 coname2 trm_raw2)
         (Cut_raw coname1a trm_raw1a coname2a trm_raw2a)"
| "\<lbrakk>\<exists>pi. ({atom coname1}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom coname1a}, trm_raw1a);
    \<exists>pia. ({atom coname2}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom coname2a}, trm_raw2a);
    coname3 = coname3a\<rbrakk> \<Longrightarrow>
   alpha (AndR_raw coname1 trm_raw1 coname2 trm_raw2 coname3)
         (AndR_raw coname1a trm_raw1a coname2a trm_raw2a coname3a)"
| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
    name2 = name2a\<rbrakk> \<Longrightarrow>
   alpha (AndL1_raw name1 trm_raw name2) (AndL1_raw name1a trm_rawa name2a)"
| "\<lbrakk>\<exists>pi. ({atom name1}, trm_raw) \<approx>gen alpha fv_trm_raw pi ({atom name1a}, trm_rawa);
     name2 = name2a\<rbrakk> \<Longrightarrow>
   alpha (AndL2_raw name1 trm_raw name2) (AndL2_raw name1a trm_rawa name2a)"
| "\<lbrakk>\<exists>pi. ({atom coname}, trm_raw1) \<approx>gen alpha fv_trm_raw pi ({atom conamea}, trm_raw1a);
    \<exists>pia. ({atom name1}, trm_raw2) \<approx>gen alpha fv_trm_raw pia ({atom name1a}, trm_raw2a);
    name2 = name2a\<rbrakk> \<Longrightarrow>
   alpha (ImpL_raw coname trm_raw1 name1 trm_raw2 name2)
         (ImpL_raw conamea trm_raw1a name1a trm_raw2a name2a)"
| "\<lbrakk>\<exists>pi.({atom name} \<union> {atom coname1}, trm_raw) \<approx>gen alpha fv_trm_raw pi  
        ({atom namea} \<union> {atom coname1a}, trm_rawa); coname2 = coname2a\<rbrakk> \<Longrightarrow>
   alpha (ImpR_raw coname1 name trm_raw coname2)
         (ImpR_raw coname1a namea trm_rawa coname2a)"

thm alpha.intros

equivariance alpha

thm eqvts_raw


end