# HG changeset patch # User Cezary Kaliszyk # Date 1268055064 -3600 # Node ID e72d9d9eada309bf4a12eb73c586d2fb8bf7a465 # Parent 1e811e3424f3abecef2ce62931a8f6e6b441ef59 Term5 written as nominal_datatype is the recursive let. diff -r 1e811e3424f3 -r e72d9d9eada3 Nominal/Fv.thy --- a/Nominal/Fv.thy Mon Mar 08 11:25:57 2010 +0100 +++ b/Nominal/Fv.thy Mon Mar 08 14:31:04 2010 +0100 @@ -58,6 +58,12 @@ body. *) +ML {* +fun is_atom thy typ = + Sign.of_sort thy (typ, @{sort at}) +*} + + (* Like map2, only if the second list is empty passes empty lists insted of error *) ML {* fun map2i _ [] [] = [] diff -r 1e811e3424f3 -r e72d9d9eada3 Nominal/Term5a.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Nominal/Term5a.thy Mon Mar 08 14:31:04 2010 +0100 @@ -0,0 +1,38 @@ +theory Term5 +imports "Parser" +begin + +atom_decl name + +ML {* restricted_nominal := 2 *} + +nominal_datatype trm5 = + Vr5 "name" +| Ap5 "trm5" "trm5" +| Lt5 l::"lts" t::"trm5" bind "bv5 l" in t +and lts = + Lnil +| Lcons "name" "trm5" "lts" +binder + bv5 +where + "bv5 Lnil = {}" +| "bv5 (Lcons n t ltl) = {atom n} \ (bv5 ltl)" + +lemma lets_ok: + "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" +apply (simp add: trm5_lts_inject) +apply (rule_tac x="(x \ y)" in exI) +apply (simp_all add: alpha_gen) +apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn) +done + +lemma lets_nok: + "x \ y \ (Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) \ (Lt5 (Lcons y (Vr5 x) Lnil) (Vr5 y))" +apply (simp only: trm5_lts_inject not_ex) +apply (rule allI) +apply (simp add: alpha_gen) +apply (simp add: trm5_lts_perm fresh_star_def trm5_lts_fv trm5_lts_bn trm5_lts_inject) +done + +end