31 thm single_let.perm_simps |
31 thm single_let.perm_simps |
32 thm single_let.eq_iff |
32 thm single_let.eq_iff |
33 thm single_let.fv_bn_eqvt |
33 thm single_let.fv_bn_eqvt |
34 thm single_let.size_eqvt |
34 thm single_let.size_eqvt |
35 thm single_let.supports |
35 thm single_let.supports |
|
36 thm single_let.fsupp |
36 |
37 |
37 lemma test: |
38 |
38 "finite (supp (t::trm)) \<and> finite (supp (a::assg))" |
|
39 apply(rule single_let.induct) |
|
40 apply(rule supports_finite) |
|
41 apply(rule single_let.supports) |
|
42 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
43 apply(rule supports_finite) |
|
44 apply(rule single_let.supports) |
|
45 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
46 apply(rule supports_finite) |
|
47 apply(rule single_let.supports) |
|
48 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
49 apply(rule supports_finite) |
|
50 apply(rule single_let.supports) |
|
51 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
52 apply(rule supports_finite) |
|
53 apply(rule single_let.supports) |
|
54 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
55 apply(rule supports_finite) |
|
56 apply(rule single_let.supports) |
|
57 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
58 apply(rule supports_finite) |
|
59 apply(rule single_let.supports) |
|
60 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
61 apply(rule supports_finite) |
|
62 apply(rule single_let.supports) |
|
63 apply(simp only: finite_supp supp_Pair finite_Un, simp) |
|
64 done |
|
65 |
39 |
66 instantiation trm and assg :: fs |
40 instantiation trm and assg :: fs |
67 begin |
41 begin |
68 |
42 |
69 instance |
43 instance |
70 apply(default) |
44 apply(default) |
71 apply(simp_all add: test) |
45 apply(simp_all add: single_let.fsupp) |
72 done |
46 done |
73 |
47 |
74 end |
48 end |
75 |
49 |
76 |
50 |