simplified proofs
authorhaftmann
Tue Aug 07 09:38:46 2007 +0200 (2007-08-07)
changeset 241639e6a2a7da86a
parent 24162 8dfd5dd65d82
child 24164 911b46812018
simplified proofs
src/HOL/Finite_Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Aug 07 09:38:44 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Aug 07 09:38:46 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Finite sets *}
     1.5  
     1.6  theory Finite_Set
     1.7 -imports IntDef Divides
     1.8 +imports IntDef Divides Option
     1.9  begin
    1.10  
    1.11  subsection {* Definition and basic properties *}
    1.12 @@ -2687,18 +2687,14 @@
    1.13  interpretation
    1.14    Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
    1.15  where
    1.16 -  "Linorder.Min (op \<le>) = Min" and "Linorder.Max (op \<le>) = Max"
    1.17 +  "Linorder.Min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = Min"
    1.18 +  and "Linorder.Max (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = Max"
    1.19  proof -
    1.20    show "Linorder (op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool) op <"
    1.21    by (rule Linorder.intro, rule linorder_axioms)
    1.22 -  have "Linorder (op \<le> \<Colon> 'b \<Rightarrow> 'b \<Rightarrow> bool) op <"
    1.23 -  by (rule Linorder.intro, rule linorder_axioms)
    1.24 -  then interpret Linorder1: Linorder ["op \<le> \<Colon> 'b \<Rightarrow> 'b \<Rightarrow> bool" "op <"] .
    1.25 -  show "Linorder1.Min = Min" by (simp add: Min_def Linorder1.Min_def ord_class.min)
    1.26 -  have "Linorder (op \<le> \<Colon> 'c \<Rightarrow> 'c \<Rightarrow> bool) op <"
    1.27 -  by (rule Linorder.intro, rule linorder_axioms)
    1.28 -  then interpret Linorder2: Linorder ["op \<le> \<Colon> 'c \<Rightarrow> 'c \<Rightarrow> bool" "op <"] .
    1.29 -  show "Linorder2.Max = Max" by (simp add: Max_def Linorder2.Max_def ord_class.max)
    1.30 +  then interpret Linorder: Linorder ["op \<le> \<Colon> 'a \<Rightarrow> 'a \<Rightarrow> bool" "op <"] .
    1.31 +  show "Linorder.Min = Min" by (simp add: Min_def Linorder.Min_def ord_class.min)
    1.32 +  show "Linorder.Max = Max" by (simp add: Max_def Linorder.Max_def ord_class.max)
    1.33  qed
    1.34  
    1.35  interpretation