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