# HG changeset patch
# User Thomas Sewell <tsewell@nicta.com.au>
# Date 1253869458 -36000
# Node ID 4e0256f7d219c2e73287c59ef3c32a81041e238d
# Parent  5fae12e4679ca662fdcbcc01c4b62ee37816f880
Avoid record-inner constants in polymorphic definitions in Bali

The Bali package needs to insert a record extension into a type
class and define an associated polymorphic constant. There is no
elegant way to do this.

The existing approach was to insert every record extension into
the type class, defining the polymorphic constant at each layer
using inner operations created by the record package. Some of
those operations have been removed. They can be replaced by use
of record_name.extend if necessary, but we can also sidestep
this altogether.

The simpler approach here is to use defs(overloaded) once to
provide a single definition for the composition of all the type
constructors, which seems to be permitted. This gets us exactly
the fact we need, with the cost that some types that were
admitted to the type class have no definition for the constant
at all.

diff -r 5fae12e4679c -r 4e0256f7d219 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Thu Sep 24 11:33:05 2009 +1000
+++ b/src/HOL/Bali/DeclConcepts.thy	Fri Sep 25 19:04:18 2009 +1000
@@ -154,21 +154,14 @@
 
 instance decl_ext_type :: ("has_static") has_static ..
 
-defs (overloaded)
-decl_is_static_def: 
- "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 
-
 instance member_ext_type :: ("type") has_static ..
 
 defs (overloaded)
 static_field_type_is_static_def: 
- "is_static (m::('b::type) member_ext_type) \<equiv> static_sel m"
+ "is_static (m::('b member_scheme)) \<equiv> static m"
 
 lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
-apply (cases m)
-apply (simp add: static_field_type_is_static_def 
-                 decl_is_static_def Decl.member.dest_convs)
-done
+by (simp add: static_field_type_is_static_def)
 
 instance * :: ("type","has_static") has_static ..
 
@@ -402,30 +395,16 @@
 
 instance decl_ext_type :: ("has_resTy") has_resTy ..
 
-defs (overloaded)
-decl_resTy_def: 
- "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 
-
 instance member_ext_type :: ("has_resTy") has_resTy ..
 
-defs (overloaded)
-member_ext_type_resTy_def: 
- "resTy (m::('b::has_resTy) member_ext_type) 
-  \<equiv> resTy (member.more_sel m)" 
-
 instance mhead_ext_type :: ("type") has_resTy ..
 
 defs (overloaded)
 mhead_ext_type_resTy_def: 
- "resTy (m::('b mhead_ext_type)) 
-  \<equiv> resT_sel m" 
+ "resTy (m::('b mhead_scheme)) \<equiv> resT m"
 
 lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
-apply (cases m)
-apply (simp add: decl_resTy_def member_ext_type_resTy_def 
-                 mhead_ext_type_resTy_def 
-                 member.dest_convs mhead.dest_convs)
-done
+by (simp add: mhead_ext_type_resTy_def)
 
 lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
 by (simp add: mhead_def mhead_resTy_simp)