instantiation replacing primitive instance plus overloaded defs
authorhaftmann
Mon Apr 07 15:37:33 2008 +0200 (2008-04-07)
changeset 2656636a93808642c
parent 26565 522f45a8604e
child 26567 7bcebb8c2d33
instantiation replacing primitive instance plus overloaded defs
src/HOL/Bali/Decl.thy
src/HOL/Hyperreal/HyperDef.thy
     1.1 --- a/src/HOL/Bali/Decl.thy	Mon Apr 07 15:37:32 2008 +0200
     1.2 +++ b/src/HOL/Bali/Decl.thy	Mon Apr 07 15:37:33 2008 +0200
     1.3 @@ -6,7 +6,9 @@
     1.4  *}
     1.5  
     1.6  (** order is significant, because of clash for "var" **)
     1.7 -theory Decl imports Term Table begin
     1.8 +theory Decl
     1.9 +imports Term Table
    1.10 +begin
    1.11  
    1.12  text {*
    1.13  improvements:
    1.14 @@ -50,21 +52,21 @@
    1.15    Private < Package < Protected < Public
    1.16  *}
    1.17   
    1.18 -instance acc_modi:: ord ..
    1.19 +instantiation acc_modi :: linorder
    1.20 +begin
    1.21  
    1.22 -defs (overloaded)
    1.23 -less_acc_def: 
    1.24 - "a < (b::acc_modi) 
    1.25 -      \<equiv> (case a of
    1.26 +definition
    1.27 +  less_acc_def: "a < b
    1.28 +      \<longleftrightarrow> (case a of
    1.29               Private    \<Rightarrow> (b=Package \<or> b=Protected \<or> b=Public)
    1.30             | Package    \<Rightarrow> (b=Protected \<or> b=Public)
    1.31             | Protected  \<Rightarrow> (b=Public)
    1.32             | Public     \<Rightarrow> False)"
    1.33 -le_acc_def:
    1.34 - "a \<le> (b::acc_modi) \<equiv> (a = b) \<or> (a < b)"
    1.35  
    1.36 -instance acc_modi:: order
    1.37 -proof
    1.38 +definition
    1.39 +  le_acc_def: "a \<le> (b::acc_modi) \<longleftrightarrow> (a = b) \<or> (a < b)"
    1.40 +
    1.41 +instance proof
    1.42    fix x y z::acc_modi
    1.43    {
    1.44    show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
    1.45 @@ -86,14 +88,12 @@
    1.46    show "(x < y) = (x \<le> y \<and> x \<noteq> y)"
    1.47      by (auto simp add: le_acc_def less_acc_def split add: acc_modi.split) 
    1.48    }
    1.49 -qed
    1.50 -  
    1.51 -instance acc_modi:: linorder
    1.52 -proof
    1.53    fix x y:: acc_modi
    1.54    show  "x \<le> y \<or> y \<le> x"   
    1.55    by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
    1.56  qed
    1.57 +  
    1.58 +end
    1.59  
    1.60  lemma acc_modi_top [simp]: "Public \<le> a \<Longrightarrow> a = Public"
    1.61  by (auto simp add: le_acc_def less_acc_def split: acc_modi.splits)
     2.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Mon Apr 07 15:37:32 2008 +0200
     2.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Apr 07 15:37:33 2008 +0200
     2.3 @@ -43,11 +43,16 @@
     2.4  
     2.5  subsection {* Real vector class instances *}
     2.6  
     2.7 -instance star :: (scaleR) scaleR ..
     2.8 +instantiation star :: (scaleR) scaleR
     2.9 +begin
    2.10  
    2.11 -defs (overloaded)
    2.12 +definition
    2.13    star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
    2.14  
    2.15 +instance ..
    2.16 +
    2.17 +end
    2.18 +
    2.19  lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> scaleR r x \<in> Standard"
    2.20  by (simp add: star_scaleR_def)
    2.21