equal
deleted
inserted
replaced
56 thm fun_pats.size_eqvt |
56 thm fun_pats.size_eqvt |
57 thm fun_pats.supports |
57 thm fun_pats.supports |
58 thm fun_pats.fsupp |
58 thm fun_pats.fsupp |
59 thm fun_pats.supp |
59 thm fun_pats.supp |
60 |
60 |
61 |
|
62 ML {* |
|
63 fun add_ss thms = |
|
64 HOL_basic_ss addsimps thms |
|
65 |
|
66 fun symmetric thms = |
|
67 map (fn thm => thm RS @{thm sym}) thms |
|
68 *} |
|
69 |
|
70 lemma |
61 lemma |
71 "(fv_exp x = supp x) \<and> |
62 "(fv_exp x = supp x) \<and> |
72 (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and> |
63 (fv_fnclause xa = supp xa \<and> fv_b_lrb xa = supp_rel alpha_b_lrb xa) \<and> |
73 (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and> |
64 (fv_fnclauses xb = supp xb \<and> fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb) \<and> |
74 (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and> |
65 (fv_lrb xc = supp xc \<and> fv_b_fnclause xc = supp_rel alpha_b_fnclause xc) \<and> |
90 "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and |
81 "fv_b_lrbs xd = supp_rel alpha_b_lrbs xd" and |
91 "fv_b_pat xe = supp_rel alpha_b_pat xe" and |
82 "fv_b_pat xe = supp_rel alpha_b_pat xe" and |
92 "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and |
83 "fv_b_fnclauses xb = supp_rel alpha_b_fnclauses xb" and |
93 "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and |
84 "fv_b_fnclause xc = supp_rel alpha_b_fnclause xc" and |
94 "fv_b_lrb y = supp_rel alpha_b_lrb y" |
85 "fv_b_lrb y = supp_rel alpha_b_lrb y" |
95 apply(induct "x::exp" and "y::fnclause" and xb and xc and xd and xe rule: fun_pats.inducts) |
86 thm fun_pats.inducts |
|
87 apply(induct rule: fun_pats.inducts(1)[where ?exp="x::exp"] |
|
88 fun_pats.inducts(2)[where ?fnclause="y"] |
|
89 fun_pats.inducts(3)[where ?fnclauses="xb"] |
|
90 fun_pats.inducts(4)[where ?lrb="xc"] |
|
91 fun_pats.inducts(5)[where ?lrbs="xd"] |
|
92 fun_pats.inducts(6)[where ?pat="xe"]) |
96 thm fun_pats.inducts |
93 thm fun_pats.inducts |
97 oops |
94 oops |
98 |
95 |
99 end |
96 end |
100 |
97 |