47 | "b_fnclauses (S fc) = (b_fnclause fc)" |
47 | "b_fnclauses (S fc) = (b_fnclause fc)" |
48 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
48 | "b_fnclauses (ORs fc fcs) = (b_fnclause fc) \<union> (b_fnclauses fcs)" |
49 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
49 | "b_lrb (Clause fcs) = (b_fnclauses fcs)" |
50 | "b_fnclause (K x pat exp) = {atom x}" |
50 | "b_fnclause (K x pat exp) = {atom x}" |
51 |
51 |
|
52 |
|
53 |
|
54 thm fun_recs.perm_bn_alpha |
|
55 thm fun_recs.perm_bn_simps |
|
56 thm fun_recs.bn_finite |
|
57 thm fun_recs.inducts |
|
58 thm fun_recs.distinct |
|
59 thm fun_recs.induct |
|
60 thm fun_recs.inducts |
|
61 thm fun_recs.exhaust |
|
62 thm fun_recs.fv_defs |
|
63 thm fun_recs.bn_defs |
|
64 thm fun_recs.perm_simps |
|
65 thm fun_recs.eq_iff |
|
66 thm fun_recs.fv_bn_eqvt |
|
67 thm fun_recs.size_eqvt |
|
68 thm fun_recs.supports |
|
69 thm fun_recs.fsupp |
|
70 thm fun_recs.supp |
|
71 |
|
72 term alpha_b_fnclause |
|
73 term alpha_b_fnclauses |
|
74 term alpha_b_lrb |
|
75 term alpha_b_lrbs |
|
76 term alpha_b_pat |
|
77 |
|
78 term alpha_b_fnclause_raw |
|
79 term alpha_b_fnclauses_raw |
|
80 term alpha_b_lrb_raw |
|
81 term alpha_b_lrbs_raw |
|
82 term alpha_b_pat_raw |
|
83 |
|
84 lemma uu1: |
|
85 fixes as0::exp and as1::fnclause |
|
86 shows "(\<lambda>x::exp. True) (as0::exp)" |
|
87 and "alpha_b_fnclause as1 (permute_b_fnclause p as1)" |
|
88 and "alpha_b_fnclauses as2 (permute_b_fnclauses p as2)" |
|
89 and "alpha_b_lrb as3 (permute_b_lrb p as3)" |
|
90 and "alpha_b_lrbs as4 (permute_b_lrbs p as4)" |
|
91 and "alpha_b_pat as5 (permute_b_pat p as5)" |
|
92 apply(induct as0 and as1 and as2 and as3 and as4 and as5 rule: fun_recs.inducts) |
|
93 apply(simp_all) |
|
94 apply(simp only: fun_recs.perm_bn_simps) |
|
95 apply(simp only: fun_recs.eq_iff) |
|
96 apply(simp) |
|
97 oops |
|
98 |
|
99 |
52 thm fun_recs.distinct |
100 thm fun_recs.distinct |
53 thm fun_recs.induct |
101 thm fun_recs.induct |
54 thm fun_recs.inducts |
102 thm fun_recs.inducts |
55 thm fun_recs.exhaust |
103 thm fun_recs.exhaust |
56 thm fun_recs.fv_defs |
104 thm fun_recs.fv_defs |