equal
deleted
inserted
replaced
135 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
135 "(supp (atom x) \<union> supp t) supports (Lm1 x t)" |
136 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
136 "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)" |
137 "{} supports BUnit" |
137 "{} supports BUnit" |
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(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1) |
140 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *}) |
141 apply(rule_tac [!] allI)+ |
|
142 apply(rule_tac [!] impI) |
|
143 apply(tactic {* ALLGOALS (REPEAT o etac conjE) *}) |
|
144 apply(simp_all add: fresh_atom) |
|
145 done |
141 done |
146 |
142 |
147 lemma rtrm1_bp_fs: |
143 lemma rtrm1_bp_fs: |
148 "finite (supp (x :: trm1))" |
144 "finite (supp (x :: trm1))" |
149 "finite (supp (b :: bp))" |
145 "finite (supp (b :: bp))" |