1.1 --- a/src/HOL/Bali/Term.thy	Mon Feb 22 17:02:39 2010 +0100
     1.2 +++ b/src/HOL/Bali/Term.thy	Tue Feb 23 10:11:12 2010 +0100
     1.3 @@ -295,8 +295,8 @@
     1.4  following.
     1.5  *}
     1.6  
     1.7 -axclass inj_term < "type"
     1.8 -consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
     1.9 +class inj_term =
    1.10 +  fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
    1.11  
    1.12  text {* How this overloaded injections work can be seen in the theory 
    1.13  @{text DefiniteAssignment}. Other big inductive relations on
    1.14 @@ -308,10 +308,15 @@
    1.15  as bridge between the different conventions.  
    1.16  *}
    1.17  
    1.18 -instance stmt::inj_term ..
    1.19 +instantiation stmt :: inj_term
    1.20 +begin
    1.21  
    1.22 -defs (overloaded)
    1.23 -stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    1.24 +definition
    1.25 +  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
    1.26 +
    1.27 +instance ..
    1.28 +
    1.29 +end
    1.30  
    1.31  lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
    1.32  by (simp add: stmt_inj_term_def)
    1.33 @@ -319,10 +324,15 @@
    1.34  lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    1.35    by (simp add: stmt_inj_term_simp)
    1.36  
    1.37 -instance expr::inj_term ..
    1.38 +instantiation expr :: inj_term
    1.39 +begin
    1.40  
    1.41 -defs (overloaded)
    1.42 -expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    1.43 +definition
    1.44 +  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
    1.45 +
    1.46 +instance ..
    1.47 +
    1.48 +end
    1.49  
    1.50  lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
    1.51  by (simp add: expr_inj_term_def)
    1.52 @@ -330,10 +340,15 @@
    1.53  lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    1.54    by (simp add: expr_inj_term_simp)
    1.55  
    1.56 -instance var::inj_term ..
    1.57 +instantiation var :: inj_term
    1.58 +begin
    1.59  
    1.60 -defs (overloaded)
    1.61 -var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    1.62 +definition
    1.63 +  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
    1.64 +
    1.65 +instance ..
    1.66 +
    1.67 +end
    1.68  
    1.69  lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
    1.70  by (simp add: var_inj_term_def)
    1.71 @@ -341,10 +356,32 @@
    1.72  lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
    1.73    by (simp add: var_inj_term_simp)
    1.74  
    1.75 -instance "list":: (type) inj_term ..
    1.76 +class expr_of =
    1.77 +  fixes expr_of :: "'a \<Rightarrow> expr"
    1.78 +
    1.79 +instantiation expr :: expr_of
    1.80 +begin
    1.81 +
    1.82 +definition
    1.83 +  "expr_of = (\<lambda>(e::expr). e)"
    1.84 +
    1.85 +instance ..
    1.86 +
    1.87 +end 
    1.88  
    1.89 -defs (overloaded)
    1.90 -expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
    1.91 +instantiation list :: (expr_of) inj_term
    1.92 +begin
    1.93 +
    1.94 +definition
    1.95 +  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
    1.96 +
    1.97 +instance ..
    1.98 +
    1.99 +end
   1.100 +
   1.101 +lemma expr_list_inj_term_def:
   1.102 +  "\<langle>es::expr list\<rangle> \<equiv> In3 es"
   1.103 +  by (simp add: inj_term_list_def expr_of_expr_def)
   1.104  
   1.105  lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
   1.106  by (simp add: expr_list_inj_term_def)