equal
deleted
inserted
replaced
299 apply(rule perm_supp_eq) |
299 apply(rule perm_supp_eq) |
300 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
300 using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) |
301 finally show ?thesis by simp |
301 finally show ?thesis by simp |
302 qed |
302 qed |
303 |
303 |
304 typedef ('a::fs, 'b::fs) ffun = "{f::'a => 'b. finite (supp f)}" |
|
305 apply(subgoal_tac "\<exists>x::'b::fs. x \<in> (UNIV::('b::fs) set)") |
|
306 apply(erule exE) |
|
307 apply(rule_tac x="\<lambda>_. x" in exI) |
|
308 apply(auto) |
|
309 apply(rule_tac S="supp x" in supports_finite) |
|
310 apply(simp add: supports_def) |
|
311 apply(perm_simp) |
|
312 apply(simp add: fresh_def[symmetric]) |
|
313 apply(simp add: swap_fresh_fresh) |
|
314 apply(simp add: finite_supp) |
|
315 done |
|
316 |
|
317 lemma Abs_lst_fcb2: |
304 lemma Abs_lst_fcb2: |
318 fixes as bs :: "atom list" |
305 fixes as bs :: "atom list" |
319 and x y :: "'b :: fs" |
306 and x y :: "'b :: fs" |
320 and c::"'c::fs" |
307 and c::"'c::fs" |
321 assumes eq: "[as]lst. x = [bs]lst. y" |
308 assumes eq: "[as]lst. x = [bs]lst. y" |