2436
+ − 1 theory LetRec2
2454
+ − 2 imports "../Nominal2"
1603
+ − 3 begin
+ − 4
+ − 5 atom_decl name
+ − 6
+ − 7 nominal_datatype trm =
3029
+ − 8 Var "name"
+ − 9 | App "trm" "trm"
+ − 10 | Lam x::"name" t::"trm" binds x in t
+ − 11 | Let as::"assn" t::"trm" binds "bn as" in t
+ − 12 | Let_rec as::"assn" t::"trm" binds "bn as" in as t
+ − 13 and assn =
+ − 14 ANil
+ − 15 | ACons "name" "trm" "assn"
1603
+ − 16 binder
+ − 17 bn
+ − 18 where
3029
+ − 19 "bn (ANil) = []"
+ − 20 | "bn (ACons x t as) = (atom x) # (bn as)"
1603
+ − 21
3029
+ − 22 thm trm_assn.eq_iff
+ − 23 thm trm_assn.supp
2436
+ − 24
3065
+ − 25 ML {*
+ − 26 @{term Trueprop} ;
+ − 27 @{const_name HOL.eq}
+ − 28 *}
+ − 29
3029
+ − 30 thm trm_assn.fv_defs
+ − 31 thm trm_assn.eq_iff
+ − 32 thm trm_assn.bn_defs
+ − 33 thm trm_assn.perm_simps
+ − 34 thm trm_assn.induct
+ − 35 thm trm_assn.distinct
1603
+ − 36
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 37
2561
+ − 38
+ − 39 section {* Tests *}
+ − 40
+ − 41
1603
+ − 42 (* why is this not in HOL simpset? *)
2436
+ − 43 (*
1603
+ − 44 lemma set_sub: "{a, b} - {b} = {a} - {b}"
+ − 45 by auto
+ − 46
+ − 47 lemma lets_bla:
+ − 48 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
2101
+ − 49 apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)
+ − 50 done
1603
+ − 51
+ − 52 lemma lets_ok:
+ − 53 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+ − 54 apply (simp add: trm_lts.eq_iff)
+ − 55 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
2101
+ − 56 apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)
1603
+ − 57 done
+ − 58
+ − 59 lemma lets_ok3:
+ − 60 "x \<noteq> y \<Longrightarrow>
+ − 61 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 62 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 63 apply (simp add: alphas trm_lts.eq_iff)
+ − 64 done
+ − 65
+ − 66
+ − 67 lemma lets_not_ok1:
+ − 68 "x \<noteq> y \<Longrightarrow>
+ − 69 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 70 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 71 apply (simp add: alphas trm_lts.eq_iff)
+ − 72 done
+ − 73
+ − 74 lemma lets_nok:
+ − 75 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ − 76 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 77 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 78 apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+ − 79 done
+ − 80
1685
+ − 81 lemma lets_ok4:
+ − 82 "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+ − 83 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
2041
+ − 84 apply (simp add: alphas trm_lts.eq_iff supp_at_base)
1685
+ − 85 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 86 apply (simp add: atom_eqvt fresh_star_def)
+ − 87 done
2438
abafea9b39bb
corrected bug with fv-function generation (that was the problem with recursive binders)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 88 *)
1603
+ − 89 end
+ − 90
+ − 91
+ − 92