equal
deleted
inserted
replaced
138 "(supp (atom x)) supports (BVr x)" |
138 "(supp (atom x)) supports (BVr x)" |
139 "(supp a \<union> supp b) supports (BPr a b)" |
139 "(supp a \<union> supp b) supports (BPr a b)" |
140 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
140 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
141 done |
141 done |
142 |
142 |
143 lemma rtrm1_bp_fs: |
143 prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *} |
144 "finite (supp (x :: trm1))" |
144 apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *}) |
145 "finite (supp (b :: bp))" |
145 done |
146 apply (induct x and b rule: trm1_bp_inducts) |
|
147 apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *}) |
|
148 apply(simp_all add: supp_atom) |
|
149 done |
|
150 |
146 |
151 instance trm1 and bp :: fs |
147 instance trm1 and bp :: fs |
152 apply default |
148 apply default |
153 apply (rule rtrm1_bp_fs)+ |
149 apply (rule rtrm1_bp_fs)+ |
154 done |
150 done |