more instantiation
authorhaftmann
Sat Jan 05 09:16:27 2008 +0100 (2008-01-05)
changeset 25836f7771e4f7064
parent 25835 5dac4855a080
child 25837 2a7efcfe9b54
more instantiation
src/HOL/Datatype.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Datatype.thy	Sat Jan 05 09:16:11 2008 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Sat Jan 05 09:16:27 2008 +0100
     1.3 @@ -610,8 +610,13 @@
     1.4  lemma insert_None_conv_UNIV: "insert None (range Some) = UNIV"
     1.5    by (rule set_ext, case_tac x) auto
     1.6  
     1.7 -instance option :: (finite) finite
     1.8 -proof
     1.9 +instantiation option :: (finite) finite
    1.10 +begin
    1.11 +
    1.12 +definition
    1.13 +  "Finite_Set.itself = TYPE('a option)"
    1.14 +
    1.15 +instance proof
    1.16    have "finite (UNIV :: 'a set)" by (rule finite)
    1.17    hence "finite (insert None (Some ` (UNIV :: 'a set)))" by simp
    1.18    also have "insert None (Some ` (UNIV :: 'a set)) = UNIV"
    1.19 @@ -619,6 +624,8 @@
    1.20    finally show "finite (UNIV :: 'a option set)" .
    1.21  qed
    1.22  
    1.23 +end
    1.24 +
    1.25  lemma univ_option [noatp, code func]:
    1.26    "UNIV = insert (None \<Colon> 'a\<Colon>finite option) (image Some UNIV)"
    1.27    unfolding insert_None_conv_UNIV ..
     2.1 --- a/src/HOL/Power.thy	Sat Jan 05 09:16:11 2008 +0100
     2.2 +++ b/src/HOL/Power.thy	Sat Jan 05 09:16:27 2008 +0100
     2.3 @@ -323,19 +323,21 @@
     2.4  
     2.5  subsection{*Exponentiation for the Natural Numbers*}
     2.6  
     2.7 -instance nat :: power ..
     2.8 +instantiation nat :: recpower
     2.9 +begin
    2.10  
    2.11 -primrec (power)
    2.12 -  "p ^ 0 = 1"
    2.13 -  "p ^ (Suc n) = (p::nat) * (p ^ n)"
    2.14 +primrec power_nat where
    2.15 +  "p ^ 0 = (1\<Colon>nat)"
    2.16 +  | "p ^ (Suc n) = (p\<Colon>nat) * (p ^ n)"
    2.17  
    2.18 -instance nat :: recpower
    2.19 -proof
    2.20 +instance proof
    2.21    fix z n :: nat
    2.22    show "z^0 = 1" by simp
    2.23    show "z^(Suc n) = z * (z^n)" by simp
    2.24  qed
    2.25  
    2.26 +end
    2.27 +
    2.28  lemma of_nat_power:
    2.29    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
    2.30  by (induct n, simp_all add: power_Suc of_nat_mult)