1604
+ − 1 theory ExLetRec
2041
+ − 2 imports "../NewParser"
1603
+ − 3 begin
+ − 4
1685
+ − 5
1603
+ − 6 text {* example 3 or example 5 from Terms.thy *}
+ − 7
+ − 8 atom_decl name
+ − 9
2091
+ − 10 ML {* val _ = cheat_equivp := true *}
+ − 11
1603
+ − 12 nominal_datatype trm =
+ − 13 Vr "name"
+ − 14 | Ap "trm" "trm"
2041
+ − 15 | Lm x::"name" t::"trm" bind_set x in t
+ − 16 | Lt a::"lts" t::"trm" bind "bn a" in a t
1603
+ − 17 and lts =
+ − 18 Lnil
+ − 19 | Lcons "name" "trm" "lts"
+ − 20 binder
+ − 21 bn
+ − 22 where
1685
+ − 23 "bn Lnil = []"
+ − 24 | "bn (Lcons x t l) = (atom x) # (bn l)"
1603
+ − 25
+ − 26 thm trm_lts.fv
+ − 27 thm trm_lts.eq_iff
+ − 28 thm trm_lts.bn
+ − 29 thm trm_lts.perm
+ − 30 thm trm_lts.induct
+ − 31 thm trm_lts.distinct
1685
+ − 32 thm trm_lts.supp
1603
+ − 33 thm trm_lts.fv[simplified trm_lts.supp]
+ − 34
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35 equivariance alpha_trm_raw
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 36
1603
+ − 37 (* why is this not in HOL simpset? *)
+ − 38 lemma set_sub: "{a, b} - {b} = {a} - {b}"
+ − 39 by auto
+ − 40
+ − 41 lemma lets_bla:
+ − 42 "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
+ − 43 apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base)
+ − 44 done
1603
+ − 45
+ − 46 lemma lets_ok:
+ − 47 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
+ − 48 apply (simp add: trm_lts.eq_iff)
+ − 49 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
2101
+ − 50 apply (simp_all add: alphas fresh_star_def eqvts supp_at_base)
1603
+ − 51 done
+ − 52
+ − 53 lemma lets_ok3:
+ − 54 "x \<noteq> y \<Longrightarrow>
+ − 55 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 56 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 57 apply (simp add: alphas trm_lts.eq_iff)
+ − 58 done
+ − 59
+ − 60
+ − 61 lemma lets_not_ok1:
+ − 62 "x \<noteq> y \<Longrightarrow>
+ − 63 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 64 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 65 apply (simp add: alphas trm_lts.eq_iff)
+ − 66 done
+ − 67
+ − 68 lemma lets_nok:
+ − 69 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow>
+ − 70 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
+ − 71 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))"
+ − 72 apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
+ − 73 done
+ − 74
1685
+ − 75 lemma lets_ok4:
+ − 76 "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+ − 77 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
2041
+ − 78 apply (simp add: alphas trm_lts.eq_iff supp_at_base)
1685
+ − 79 apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+ − 80 apply (simp add: atom_eqvt fresh_star_def)
+ − 81 done
1603
+ − 82
+ − 83 end
+ − 84
+ − 85
+ − 86