New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
theory Classical+ −
imports "../Nominal2"+ −
begin+ −
+ −
(* example from Urban's PhD *)+ −
+ −
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.distinct+ −
thm trm.induct+ −
thm trm.exhaust+ −
thm trm.strong_exhaust+ −
thm trm.strong_exhaust[simplified]+ −
thm trm.fv_defs+ −
thm trm.bn_defs+ −
thm trm.perm_simps+ −
thm trm.eq_iff+ −
thm trm.fv_bn_eqvt+ −
thm trm.size_eqvt+ −
thm trm.supp+ −
thm trm.supp[simplified]+ −
+ −
+ −
+ −
+ −
end+ −
+ −
+ −
+ −