generalize lemmas from nat to 'a::wellorder
authorhuffman
Fri Feb 20 22:25:36 2009 -0800 (2009-02-20)
changeset 300376ff7793d0f0d
parent 30036 3a074e3a9a18
child 30038 4a1fa865c57a
generalize lemmas from nat to 'a::wellorder
src/HOL/Library/Permutations.thy
     1.1 --- a/src/HOL/Library/Permutations.thy	Fri Feb 20 22:10:37 2009 -0800
     1.2 +++ b/src/HOL/Library/Permutations.thy	Fri Feb 20 22:25:36 2009 -0800
     1.3 @@ -683,13 +683,13 @@
     1.4  (* ------------------------------------------------------------------------- *)
     1.5  
     1.6  lemma permutes_natset_le:
     1.7 -  assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S.  p i <= i" shows "p = id"
     1.8 +  assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i <= i" shows "p = id"
     1.9  proof-
    1.10    {fix n
    1.11      have "p n = n" 
    1.12        using p le
    1.13 -    proof(induct n arbitrary: S rule: nat_less_induct)
    1.14 -      fix n S assume H: "\<forall> m< n. \<forall>S. p permutes S \<longrightarrow> (\<forall>i\<in>S. p i \<le> i) \<longrightarrow> p m = m" 
    1.15 +    proof(induct n arbitrary: S rule: less_induct)
    1.16 +      fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m" 
    1.17  	"p permutes S" "\<forall>i \<in>S. p i \<le> i"
    1.18        {assume "n \<notin> S"
    1.19  	with H(2) have "p n = n" unfolding permutes_def by metis}
    1.20 @@ -699,7 +699,7 @@
    1.21  	moreover{assume h: "p n < n"
    1.22  	  from H h have "p (p n) = p n" by metis
    1.23  	  with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
    1.24 -	  with h have False by arith}
    1.25 +	  with h have False by simp}
    1.26  	ultimately have "p n = n" by blast }
    1.27        ultimately show "p n = n"  by blast
    1.28      qed}
    1.29 @@ -707,7 +707,7 @@
    1.30  qed
    1.31  
    1.32  lemma permutes_natset_ge:
    1.33 -  assumes p: "p permutes (S:: nat set)" and le: "\<forall>i \<in> S.  p i \<ge> i" shows "p = id"
    1.34 +  assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S.  p i \<ge> i" shows "p = id"
    1.35  proof-
    1.36    {fix i assume i: "i \<in> S"
    1.37      from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp