attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
theory Classicalimports "../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 nameatom_decl conamenominal_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 tthm trm.fvthm trm.eq_iffthm trm.bnthm trm.permthm trm.inductthm trm.distinctthm trm.fv[simplified trm.supp](* correct alpha definition *)inductive alphawhere "\<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.introsdeclare permute_trm_raw.simps[eqvt]declare alpha_gen_eqvt[eqvt]equivariance alphathm eqvts_rawend