theory SingleLet+ −
imports "../NewParser"+ −
begin+ −
+ −
atom_decl name+ −
+ −
declare [[STEPS = 12]]+ −
+ −
+ −
nominal_datatype trm =+ −
Var "name"+ −
| App "trm" "trm"+ −
| Lam x::"name" t::"trm" bind_set x in t+ −
| Let a::"assg" t::"trm" bind_set "bn a" in t+ −
| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2+ −
| Bar x::"name" y::"name" t::"trm" bind y x in t x y+ −
| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 + −
and assg =+ −
As "name" "name" "trm" "name"+ −
binder+ −
bn::"assg \<Rightarrow> atom set"+ −
where+ −
"bn (As x y t z) = {atom x}"+ −
+ −
+ −
lemma+ −
shows "alpha_trm_raw x x"+ −
and "alpha_assg_raw y y"+ −
and "alpha_bn_raw y y"+ −
apply(induct rule: trm_raw_assg_raw.inducts)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(rule refl)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(assumption)+ −
apply(assumption)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(rule_tac x="0" in exI)+ −
apply(rule alpha_gen_refl)+ −
apply(assumption)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(rule_tac x="0" in exI)+ −
apply(rule alpha_gen_refl)+ −
apply(assumption)+ −
apply(assumption)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(rule_tac x="0" in exI)+ −
apply(rule alpha_gen_refl)+ −
apply(simp only: prod_alpha_def split_conv prod_rel.simps)+ −
apply(simp)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(rule_tac x="0" in exI)+ −
apply(rule alpha_gen_refl)+ −
apply(simp only: prod_alpha_def split_conv prod_rel.simps)+ −
apply(simp)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(rule refl)+ −
apply(rule refl)+ −
apply(assumption)+ −
apply(rule refl)+ −
apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)+ −
apply(rule refl)+ −
apply(assumption)+ −
apply(rule refl)+ −
done+ −
+ −
+ −
+ −
thm trm_assg.fv+ −
thm trm_assg.supp+ −
thm trm_assg.eq_iff+ −
thm trm_assg.bn+ −
thm trm_assg.perm+ −
thm trm_assg.induct+ −
thm trm_assg.inducts+ −
thm trm_assg.distinct+ −
ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}+ −
+ −
(* TEMPORARY+ −
thm trm_assg.fv[simplified trm_assg.supp(1-2)]+ −
*)+ −
+ −
end+ −
+ −
+ −
+ −