equal
deleted
inserted
replaced
1 theory LetRec2 |
1 theory LetRec2 |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
|
6 |
6 |
7 |
7 nominal_datatype trm = |
8 nominal_datatype trm = |
8 Vr "name" |
9 Vr "name" |
9 | Ap "trm" "trm" |
10 | Ap "trm" "trm" |
10 | Lm x::"name" t::"trm" bind (set) x in t |
11 | Lm x::"name" t::"trm" bind (set) x in t |
17 where |
18 where |
18 "bn Lnil = []" |
19 "bn Lnil = []" |
19 | "bn (Lcons x t l) = (atom x) # (bn l)" |
20 | "bn (Lcons x t l) = (atom x) # (bn l)" |
20 |
21 |
21 |
22 |
22 thm trm_lts.fv |
23 thm trm_lts.fv_defs |
23 thm trm_lts.eq_iff |
24 thm trm_lts.eq_iff |
24 thm trm_lts.bn |
25 thm trm_lts.bn_defs |
25 thm trm_lts.perm |
26 thm trm_lts.perm_simps |
26 thm trm_lts.induct |
27 thm trm_lts.induct |
27 thm trm_lts.distinct |
28 thm trm_lts.distinct |
28 thm trm_lts.supp |
|
29 thm trm_lts.fv[simplified trm_lts.supp] |
|
30 |
29 |
31 |
30 |
32 (* why is this not in HOL simpset? *) |
31 (* why is this not in HOL simpset? *) |
33 (* |
32 (* |
34 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
33 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
73 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" |
72 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" |
74 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
73 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
75 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
74 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
76 apply (simp add: atom_eqvt fresh_star_def) |
75 apply (simp add: atom_eqvt fresh_star_def) |
77 done |
76 done |
78 |
77 *) |
79 end |
78 end |
80 |
79 |
81 |
80 |
82 |
81 |