equal
deleted
inserted
replaced
25 thm trm_assn.perm_simps |
25 thm trm_assn.perm_simps |
26 thm trm_assn.induct |
26 thm trm_assn.induct |
27 thm trm_assn.inducts |
27 thm trm_assn.inducts |
28 thm trm_assn.distinct |
28 thm trm_assn.distinct |
29 thm trm_assn.supp |
29 thm trm_assn.supp |
30 |
30 thm trm_assn.fresh |
31 |
31 |
32 lemma supp_fresh_eq: |
|
33 assumes "supp x = supp y" |
|
34 shows "a \<sharp> x \<longleftrightarrow> a \<sharp> y" |
|
35 using assms by (simp add: fresh_def) |
|
36 |
|
37 lemma supp_not_in: |
|
38 assumes "x = y" |
|
39 shows "a \<notin> x \<longleftrightarrow> a \<notin> y" |
|
40 using assms |
|
41 by (simp add: fresh_def) |
|
42 |
|
43 lemmas freshs = |
|
44 trm_assn.supp(1)[THEN supp_not_in, folded fresh_def] |
|
45 trm_assn.supp(2)[THEN supp_not_in, simplified, folded fresh_def] |
|
46 trm_assn.supp(3)[THEN supp_not_in, folded fresh_def] |
|
47 trm_assn.supp(4)[THEN supp_not_in, folded fresh_def] |
|
48 trm_assn.supp(5)[THEN supp_not_in, simplified, folded fresh_def] |
|
49 trm_assn.supp(6)[THEN supp_not_in, simplified, folded fresh_def] |
|
50 |
32 |
51 lemma fin_bn: |
33 lemma fin_bn: |
52 shows "finite (set (bn l))" |
34 shows "finite (set (bn l))" |
53 apply(induct l rule: trm_assn.inducts(2)) |
35 apply(induct l rule: trm_assn.inducts(2)) |
54 apply(simp_all) |
36 apply(simp_all) |
81 apply(assumption) |
63 apply(assumption) |
82 apply(assumption) |
64 apply(assumption) |
83 apply(simp) |
65 apply(simp) |
84 apply(rule test_trm_test_assn.intros) |
66 apply(rule test_trm_test_assn.intros) |
85 apply(assumption) |
67 apply(assumption) |
86 apply(simp add: freshs fresh_star_def) |
68 apply(simp add: trm_assn.fresh fresh_star_def) |
87 apply(simp) |
69 apply(simp) |
88 defer |
70 defer |
89 apply(simp) |
71 apply(simp) |
90 apply(rule test_trm_test_assn.intros) |
72 apply(rule test_trm_test_assn.intros) |
91 apply(simp) |
73 apply(simp) |
92 apply(rule test_trm_test_assn.intros) |
74 apply(rule test_trm_test_assn.intros) |
93 apply(assumption) |
75 apply(assumption) |
94 apply(assumption) |
76 apply(assumption) |
95 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst) |
77 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst) |
96 apply(rule eq_iffs(4)[THEN iffD2]) |
78 apply(rule trm_assn.eq_iff(4)[THEN iffD2]) |
97 defer |
79 defer |
98 apply(rule test_trm_test_assn.intros) |
80 apply(rule test_trm_test_assn.intros) |
99 prefer 3 |
81 prefer 3 |
|
82 apply(simp add: fresh_star_def trm_assn.fresh) |
100 thm freshs |
83 thm freshs |
101 --"HERE" |
84 --"HERE" |
102 |
85 |
103 thm supps |
86 thm supps |
104 apply(rule test_trm_test_assn.intros) |
87 apply(rule test_trm_test_assn.intros) |