author huffman Fri Feb 20 22:25:36 2009 -0800 (2009-02-20) changeset 30037 6ff7793d0f0d parent 30036 3a074e3a9a18 child 30038 4a1fa865c57a
generalize lemmas from nat to 'a::wellorder
```     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
```