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 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+ −
+ −
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+ −
+ −
declare permute_trm_raw.simps[eqvt]+ −
declare alpha_gen_eqvt[eqvt]+ −
+ −
equivariance alpha+ −
thm eqvts_raw+ −
+ −
+ −
end+ −
+ −
+ −
+ −