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";