Hid swap
authornipkow
Thu Jun 12 14:10:41 2008 +0200 (2008-06-12)
changeset 27165e1c49eb8cee6
parent 27164 81632fd4ff61
child 27166 968a1450ae35
Hid swap
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Jun 12 11:51:47 2008 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Jun 12 14:10:41 2008 +0200
     1.3 @@ -535,7 +535,7 @@
     1.4    have nSuc: "n = Suc m" by fact
     1.5    have mlessn: "m<n" by (simp add: nSuc)
     1.6    from aA obtain k where hkeq: "h k = a" and klessn: "k<n" by (blast elim!: equalityE)
     1.7 -  let ?hm = "swap k m h"
     1.8 +  let ?hm = "Fun.swap k m h"
     1.9    have inj_hm: "inj_on ?hm {i. i < n}" using klessn mlessn 
    1.10      by (simp add: inj_on_swap_iff inj_on)
    1.11    show ?thesis
    1.12 @@ -545,7 +545,7 @@
    1.13      show "m<n" by (rule mlessn)
    1.14      show "A = ?hm ` {i. i < m}" 
    1.15      proof (rule insert_image_inj_on_eq)
    1.16 -      show "inj_on (swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
    1.17 +      show "inj_on (Fun.swap k m h) {i. i < Suc m}" using inj_hm nSuc by simp
    1.18        show "?hm m \<notin> A" by (simp add: swap_def hkeq anot) 
    1.19        show "insert (?hm m) A = ?hm ` {i. i < Suc m}"
    1.20  	using aA hkeq nSuc klessn
     2.1 --- a/src/HOL/Fun.thy	Thu Jun 12 11:51:47 2008 +0200
     2.2 +++ b/src/HOL/Fun.thy	Thu Jun 12 14:10:41 2008 +0200
     2.3 @@ -460,7 +460,7 @@
     2.4    thus "inj_on f A" by simp 
     2.5  next
     2.6    assume "inj_on f A"
     2.7 -  with A show "inj_on (swap a b f) A" by (iprover intro: inj_on_imp_inj_on_swap)
     2.8 +  with A show "inj_on (swap a b f) A" by(iprover intro: inj_on_imp_inj_on_swap)
     2.9  qed
    2.10  
    2.11  lemma surj_imp_surj_swap: "surj f ==> surj (swap a b f)"
    2.12 @@ -482,6 +482,7 @@
    2.13  lemma bij_swap_iff: "bij (swap a b f) = bij f"
    2.14  by (simp add: bij_def)
    2.15  
    2.16 +hide const swap
    2.17  
    2.18  subsection {* Proof tool setup *} 
    2.19