tuned;
authorwenzelm
Mon Jan 28 23:35:20 2002 +0100 (2002-01-28)
changeset 12859f63315dfffd4
parent 12858 6214f03d6d27
child 12860 7fc3fbfed8ef
tuned;
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxExample.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Basis.thy
src/HOL/Bali/Decl.thy
src/HOL/Bali/DeclConcepts.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Name.thy
src/HOL/Bali/ROOT.ML
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Mon Jan 28 18:51:48 2002 +0100
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Mon Jan 28 23:35:20 2002 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Bali/AxCompl.thy
     1.5      ID:         $Id$
     1.6      Author:     David von Oheimb
     1.7 -    Copyright   1999 Technische Universitaet Muenchen
     1.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9  *)
    1.10  
    1.11  header {*
     2.1 --- a/src/HOL/Bali/AxExample.thy	Mon Jan 28 18:51:48 2002 +0100
     2.2 +++ b/src/HOL/Bali/AxExample.thy	Mon Jan 28 23:35:20 2002 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  (*  Title:      HOL/Bali/AxExample.thy
     2.5      ID:         $Id$
     2.6      Author:     David von Oheimb
     2.7 -    Copyright   2000 Technische Universitaet Muenchen
     2.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     2.9  *)
    2.10  header {* Example of a proof based on the Bali axiomatic semantics *}
    2.11  
     3.1 --- a/src/HOL/Bali/AxSem.thy	Mon Jan 28 18:51:48 2002 +0100
     3.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Jan 28 23:35:20 2002 +0100
     3.3 @@ -1,7 +1,7 @@
     3.4  (*  Title:      HOL/Bali/AxSem.thy
     3.5      ID:         $Id$
     3.6      Author:     David von Oheimb
     3.7 -    Copyright   1998 Technische Universitaet Muenchen
     3.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     3.9  *)
    3.10  
    3.11  header {* Axiomatic semantics of Java expressions and statements 
     4.1 --- a/src/HOL/Bali/AxSound.thy	Mon Jan 28 18:51:48 2002 +0100
     4.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Jan 28 23:35:20 2002 +0100
     4.3 @@ -1,7 +1,7 @@
     4.4  (*  Title:      HOL/Bali/AxSound.thy
     4.5      ID:         $Id$
     4.6      Author:     David von Oheimb
     4.7 -    Copyright   1999 Technische Universitaet Muenchen
     4.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     4.9  *)
    4.10  header {* Soundness proof for Axiomatic semantics of Java expressions and 
    4.11            statements
     5.1 --- a/src/HOL/Bali/Basis.thy	Mon Jan 28 18:51:48 2002 +0100
     5.2 +++ b/src/HOL/Bali/Basis.thy	Mon Jan 28 23:35:20 2002 +0100
     5.3 @@ -11,11 +11,6 @@
     5.4  ML_setup {*
     5.5  Unify.search_bound := 40;
     5.6  Unify.trace_bound  := 40;
     5.7 -
     5.8 -quick_and_dirty:=true;
     5.9 -
    5.10 -Pretty.setmargin 77;
    5.11 -goals_limit:=2;
    5.12  *}
    5.13  (*print_depth 100;*)
    5.14  (*Syntax.ambiguity_level := 1;*)
     6.1 --- a/src/HOL/Bali/Decl.thy	Mon Jan 28 18:51:48 2002 +0100
     6.2 +++ b/src/HOL/Bali/Decl.thy	Mon Jan 28 23:35:20 2002 +0100
     6.3 @@ -51,8 +51,7 @@
     6.4    Private < Package < Protected < Public
     6.5  *}
     6.6   
     6.7 -instance acc_modi:: ord
     6.8 -by intro_classes
     6.9 +instance acc_modi:: ord ..
    6.10  
    6.11  defs (overloaded)
    6.12  less_acc_def: 
    6.13 @@ -66,7 +65,7 @@
    6.14   "a \<le> (b::acc_modi) \<equiv> (a = b) \<or> (a < b)"
    6.15  
    6.16  instance acc_modi:: order
    6.17 -proof (intro_classes)
    6.18 +proof
    6.19    fix x y z::acc_modi
    6.20    {
    6.21    show "x \<le> x"               \<spacespace>\<spacespace>    -- reflexivity
    6.22 @@ -91,7 +90,7 @@
    6.23  qed
    6.24    
    6.25  instance acc_modi:: linorder
    6.26 -proof intro_classes
    6.27 +proof
    6.28    fix x y:: acc_modi
    6.29    show  "x \<le> y \<or> y \<le> x"   
    6.30    by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
    6.31 @@ -238,8 +237,7 @@
    6.32  consts
    6.33   memberid :: "'a::has_memberid \<Rightarrow> memberid"
    6.34  
    6.35 -instance memberdecl::has_memberid
    6.36 -by (intro_classes)
    6.37 +instance memberdecl::has_memberid ..
    6.38  
    6.39  defs (overloaded)
    6.40  memberdecl_memberid_def:
    6.41 @@ -259,8 +257,7 @@
    6.42  lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
    6.43  by (cases m) (simp add: memberdecl_memberid_def)
    6.44  
    6.45 -instance * :: ("type","has_memberid") has_memberid
    6.46 -by (intro_classes)
    6.47 +instance * :: (type, has_memberid) has_memberid ..
    6.48  
    6.49  defs (overloaded)
    6.50  pair_memberid_def:
     7.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Jan 28 18:51:48 2002 +0100
     7.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Jan 28 23:35:20 2002 +0100
     7.3 @@ -79,8 +79,7 @@
     7.4  axclass has_accmodi < "type"
     7.5  consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
     7.6  
     7.7 -instance acc_modi::has_accmodi
     7.8 -by (intro_classes)
     7.9 +instance acc_modi::has_accmodi ..
    7.10  
    7.11  defs (overloaded)
    7.12  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
    7.13 @@ -88,8 +87,7 @@
    7.14  lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
    7.15  by (simp add: acc_modi_accmodi_def)
    7.16  
    7.17 -instance access_field_type:: ("type","type") has_accmodi
    7.18 -by (intro_classes)
    7.19 +instance access_field_type:: ("type","type") has_accmodi ..
    7.20  
    7.21  defs (overloaded)
    7.22  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
    7.23 @@ -98,8 +96,7 @@
    7.24  lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
    7.25  by (simp add: decl_acc_modi_def)
    7.26  
    7.27 -instance * :: ("type",has_accmodi) has_accmodi
    7.28 -by (intro_classes)
    7.29 +instance * :: ("type",has_accmodi) has_accmodi ..
    7.30  
    7.31  defs (overloaded)
    7.32  pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
    7.33 @@ -107,8 +104,7 @@
    7.34  lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
    7.35  by (simp add: pair_acc_modi_def)
    7.36  
    7.37 -instance memberdecl :: has_accmodi
    7.38 -by (intro_classes)
    7.39 +instance memberdecl :: has_accmodi ..
    7.40  
    7.41  defs (overloaded)
    7.42  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
    7.43 @@ -129,8 +125,7 @@
    7.44  axclass has_declclass < "type"
    7.45  consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
    7.46  
    7.47 -instance pid_field_type::("type","type") has_declclass
    7.48 -by (intro_classes)
    7.49 +instance pid_field_type::("type","type") has_declclass ..
    7.50  
    7.51  defs (overloaded)
    7.52  qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
    7.53 @@ -138,8 +133,7 @@
    7.54  lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
    7.55  by (simp add: qtname_declclass_def)
    7.56  
    7.57 -instance * :: ("has_declclass","type") has_declclass
    7.58 -by (intro_classes)
    7.59 +instance * :: ("has_declclass","type") has_declclass ..
    7.60  
    7.61  defs (overloaded)
    7.62  pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
    7.63 @@ -158,15 +152,13 @@
    7.64  consts is_static :: "'a \<Rightarrow> bool"
    7.65  *)
    7.66  
    7.67 -instance access_field_type :: ("type","has_static") has_static
    7.68 -by (intro_classes) 
    7.69 +instance access_field_type :: ("type","has_static") has_static ..
    7.70  
    7.71  defs (overloaded)
    7.72  decl_is_static_def: 
    7.73   "is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 
    7.74  
    7.75 -instance static_field_type :: ("type","type") has_static
    7.76 -by (intro_classes)
    7.77 +instance static_field_type :: ("type","type") has_static ..
    7.78  
    7.79  defs (overloaded)
    7.80  static_field_type_is_static_def: 
    7.81 @@ -178,8 +170,7 @@
    7.82                   decl_is_static_def Decl.member.dest_convs)
    7.83  done
    7.84  
    7.85 -instance * :: ("type","has_static") has_static
    7.86 -by (intro_classes)
    7.87 +instance * :: ("type","has_static") has_static ..
    7.88  
    7.89  defs (overloaded)
    7.90  pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
    7.91 @@ -190,8 +181,7 @@
    7.92  lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
    7.93  by (simp add: pair_is_static_def)
    7.94  
    7.95 -instance memberdecl:: has_static
    7.96 -by (intro_classes)
    7.97 +instance memberdecl:: has_static ..
    7.98  
    7.99  defs (overloaded)
   7.100  memberdecl_is_static_def: 
   7.101 @@ -432,31 +422,27 @@
   7.102  axclass has_resTy < "type"
   7.103  consts resTy:: "'a::has_resTy \<Rightarrow> ty"
   7.104  
   7.105 -instance access_field_type :: ("type","has_resTy") has_resTy
   7.106 -by (intro_classes)
   7.107 +instance access_field_type :: ("type","has_resTy") has_resTy ..
   7.108  
   7.109  defs (overloaded)
   7.110  decl_resTy_def: 
   7.111   "resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 
   7.112  
   7.113 -instance static_field_type :: ("type","has_resTy") has_resTy
   7.114 -by (intro_classes)
   7.115 +instance static_field_type :: ("type","has_resTy") has_resTy ..
   7.116  
   7.117  defs (overloaded)
   7.118  static_field_type_resTy_def: 
   7.119   "resTy (m::(bool,'b::has_resTy) static_field_type) 
   7.120    \<equiv> resTy (static_more m)" 
   7.121  
   7.122 -instance pars_field_type :: ("type","has_resTy") has_resTy
   7.123 -by (intro_classes)
   7.124 +instance pars_field_type :: ("type","has_resTy") has_resTy ..
   7.125  
   7.126  defs (overloaded)
   7.127  pars_field_type_resTy_def: 
   7.128   "resTy (m::(vname list,'b::has_resTy) pars_field_type) 
   7.129    \<equiv> resTy (pars_more m)" 
   7.130  
   7.131 -instance resT_field_type :: ("type","type") has_resTy
   7.132 -by (intro_classes)
   7.133 +instance resT_field_type :: ("type","type") has_resTy ..
   7.134  
   7.135  defs (overloaded)
   7.136  resT_field_type_resTy_def: 
   7.137 @@ -473,8 +459,7 @@
   7.138  lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
   7.139  by (simp add: mhead_def mhead_resTy_simp)
   7.140  
   7.141 -instance * :: ("type","has_resTy") has_resTy
   7.142 -by (intro_classes)
   7.143 +instance * :: ("type","has_resTy") has_resTy ..
   7.144  
   7.145  defs (overloaded)
   7.146  pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
     8.1 --- a/src/HOL/Bali/Evaln.thy	Mon Jan 28 18:51:48 2002 +0100
     8.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Jan 28 23:35:20 2002 +0100
     8.3 @@ -1,7 +1,7 @@
     8.4  (*  Title:      HOL/Bali/Evaln.thy
     8.5      ID:         $Id$
     8.6      Author:     David von Oheimb
     8.7 -    Copyright   1999 Technische Universitaet Muenchen
     8.8 +    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     8.9  *)
    8.10  header {* Operational evaluation (big-step) semantics of Java expressions and 
    8.11            statements
     9.1 --- a/src/HOL/Bali/Name.thy	Mon Jan 28 18:51:48 2002 +0100
     9.2 +++ b/src/HOL/Bali/Name.thy	Mon Jan 28 23:35:20 2002 +0100
     9.3 @@ -71,8 +71,7 @@
     9.4  axclass has_pname < "type"
     9.5  consts pname::"'a::has_pname \<Rightarrow> pname"
     9.6  
     9.7 -instance pname::has_pname
     9.8 -by (intro_classes)
     9.9 +instance pname::has_pname ..
    9.10  
    9.11  defs (overloaded)
    9.12  pname_pname_def: "pname (p::pname) \<equiv> p"
    9.13 @@ -80,8 +79,7 @@
    9.14  axclass has_tname < "type"
    9.15  consts tname::"'a::has_tname \<Rightarrow> tname"
    9.16  
    9.17 -instance tname::has_tname
    9.18 -by (intro_classes)
    9.19 +instance tname::has_tname ..
    9.20  
    9.21  defs (overloaded)
    9.22  tname_tname_def: "tname (t::tname) \<equiv> t"
    9.23 @@ -90,8 +88,7 @@
    9.24  consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
    9.25  
    9.26  (* Declare qtname as instance of has_qtname *)
    9.27 -instance pid_field_type::(has_pname,"type") has_qtname
    9.28 -by intro_classes 
    9.29 +instance pid_field_type::(has_pname,"type") has_qtname ..
    9.30  
    9.31  defs (overloaded)
    9.32  qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
    10.1 --- a/src/HOL/Bali/ROOT.ML	Mon Jan 28 18:51:48 2002 +0100
    10.2 +++ b/src/HOL/Bali/ROOT.ML	Mon Jan 28 23:35:20 2002 +0100
    10.3 @@ -1,13 +1,4 @@
    10.4  
    10.5 -use_thy "WellForm";
    10.6 -
    10.7 -(*The dynamic part of Bali, including type-safety*)
    10.8 -use_thy "Evaln";
    10.9 -use_thy "Example"; 
   10.10 -use_thy "TypeSafe";
   10.11 -(*###use_thy "Trans";*)
   10.12 -
   10.13 -(*The Hoare logic for Bali*)
   10.14  use_thy "AxExample";
   10.15  use_thy "AxSound";
   10.16  use_thy "AxCompl";