--- a/src/HOL/Bali/AxCompl.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/AxCompl.thy Mon Jan 28 23:35:20 2002 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/AxCompl.thy
ID: $Id$
Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {*
--- a/src/HOL/Bali/AxExample.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/AxExample.thy Mon Jan 28 23:35:20 2002 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/AxExample.thy
ID: $Id$
Author: David von Oheimb
- Copyright 2000 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Example of a proof based on the Bali axiomatic semantics *}
--- a/src/HOL/Bali/AxSem.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/AxSem.thy Mon Jan 28 23:35:20 2002 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/AxSem.thy
ID: $Id$
Author: David von Oheimb
- Copyright 1998 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Axiomatic semantics of Java expressions and statements
--- a/src/HOL/Bali/AxSound.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/AxSound.thy Mon Jan 28 23:35:20 2002 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/AxSound.thy
ID: $Id$
Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Soundness proof for Axiomatic semantics of Java expressions and
statements
--- a/src/HOL/Bali/Basis.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/Basis.thy Mon Jan 28 23:35:20 2002 +0100
@@ -11,11 +11,6 @@
ML_setup {*
Unify.search_bound := 40;
Unify.trace_bound := 40;
-
-quick_and_dirty:=true;
-
-Pretty.setmargin 77;
-goals_limit:=2;
*}
(*print_depth 100;*)
(*Syntax.ambiguity_level := 1;*)
--- a/src/HOL/Bali/Decl.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/Decl.thy Mon Jan 28 23:35:20 2002 +0100
@@ -51,8 +51,7 @@
Private < Package < Protected < Public
*}
-instance acc_modi:: ord
-by intro_classes
+instance acc_modi:: ord ..
defs (overloaded)
less_acc_def:
@@ -66,7 +65,7 @@
"a \<le> (b::acc_modi) \<equiv> (a = b) \<or> (a < b)"
instance acc_modi:: order
-proof (intro_classes)
+proof
fix x y z::acc_modi
{
show "x \<le> x" \<spacespace>\<spacespace> -- reflexivity
@@ -91,7 +90,7 @@
qed
instance acc_modi:: linorder
-proof intro_classes
+proof
fix x y:: acc_modi
show "x \<le> y \<or> y \<le> x"
by (auto simp add: less_acc_def le_acc_def split add: acc_modi.split)
@@ -238,8 +237,7 @@
consts
memberid :: "'a::has_memberid \<Rightarrow> memberid"
-instance memberdecl::has_memberid
-by (intro_classes)
+instance memberdecl::has_memberid ..
defs (overloaded)
memberdecl_memberid_def:
@@ -259,8 +257,7 @@
lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
by (cases m) (simp add: memberdecl_memberid_def)
-instance * :: ("type","has_memberid") has_memberid
-by (intro_classes)
+instance * :: (type, has_memberid) has_memberid ..
defs (overloaded)
pair_memberid_def:
--- a/src/HOL/Bali/DeclConcepts.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Mon Jan 28 23:35:20 2002 +0100
@@ -79,8 +79,7 @@
axclass has_accmodi < "type"
consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
-instance acc_modi::has_accmodi
-by (intro_classes)
+instance acc_modi::has_accmodi ..
defs (overloaded)
acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
@@ -88,8 +87,7 @@
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
by (simp add: acc_modi_accmodi_def)
-instance access_field_type:: ("type","type") has_accmodi
-by (intro_classes)
+instance access_field_type:: ("type","type") has_accmodi ..
defs (overloaded)
decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
@@ -98,8 +96,7 @@
lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
by (simp add: decl_acc_modi_def)
-instance * :: ("type",has_accmodi) has_accmodi
-by (intro_classes)
+instance * :: ("type",has_accmodi) has_accmodi ..
defs (overloaded)
pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
@@ -107,8 +104,7 @@
lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
by (simp add: pair_acc_modi_def)
-instance memberdecl :: has_accmodi
-by (intro_classes)
+instance memberdecl :: has_accmodi ..
defs (overloaded)
memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
@@ -129,8 +125,7 @@
axclass has_declclass < "type"
consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
-instance pid_field_type::("type","type") has_declclass
-by (intro_classes)
+instance pid_field_type::("type","type") has_declclass ..
defs (overloaded)
qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
@@ -138,8 +133,7 @@
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
by (simp add: qtname_declclass_def)
-instance * :: ("has_declclass","type") has_declclass
-by (intro_classes)
+instance * :: ("has_declclass","type") has_declclass ..
defs (overloaded)
pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
@@ -158,15 +152,13 @@
consts is_static :: "'a \<Rightarrow> bool"
*)
-instance access_field_type :: ("type","has_static") has_static
-by (intro_classes)
+instance access_field_type :: ("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 static_field_type :: ("type","type") has_static
-by (intro_classes)
+instance static_field_type :: ("type","type") has_static ..
defs (overloaded)
static_field_type_is_static_def:
@@ -178,8 +170,7 @@
decl_is_static_def Decl.member.dest_convs)
done
-instance * :: ("type","has_static") has_static
-by (intro_classes)
+instance * :: ("type","has_static") has_static ..
defs (overloaded)
pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
@@ -190,8 +181,7 @@
lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
by (simp add: pair_is_static_def)
-instance memberdecl:: has_static
-by (intro_classes)
+instance memberdecl:: has_static ..
defs (overloaded)
memberdecl_is_static_def:
@@ -432,31 +422,27 @@
axclass has_resTy < "type"
consts resTy:: "'a::has_resTy \<Rightarrow> ty"
-instance access_field_type :: ("type","has_resTy") has_resTy
-by (intro_classes)
+instance access_field_type :: ("type","has_resTy") has_resTy ..
defs (overloaded)
decl_resTy_def:
"resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)"
-instance static_field_type :: ("type","has_resTy") has_resTy
-by (intro_classes)
+instance static_field_type :: ("type","has_resTy") has_resTy ..
defs (overloaded)
static_field_type_resTy_def:
"resTy (m::(bool,'b::has_resTy) static_field_type)
\<equiv> resTy (static_more m)"
-instance pars_field_type :: ("type","has_resTy") has_resTy
-by (intro_classes)
+instance pars_field_type :: ("type","has_resTy") has_resTy ..
defs (overloaded)
pars_field_type_resTy_def:
"resTy (m::(vname list,'b::has_resTy) pars_field_type)
\<equiv> resTy (pars_more m)"
-instance resT_field_type :: ("type","type") has_resTy
-by (intro_classes)
+instance resT_field_type :: ("type","type") has_resTy ..
defs (overloaded)
resT_field_type_resTy_def:
@@ -473,8 +459,7 @@
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
by (simp add: mhead_def mhead_resTy_simp)
-instance * :: ("type","has_resTy") has_resTy
-by (intro_classes)
+instance * :: ("type","has_resTy") has_resTy ..
defs (overloaded)
pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
--- a/src/HOL/Bali/Evaln.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/Evaln.thy Mon Jan 28 23:35:20 2002 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/Bali/Evaln.thy
ID: $Id$
Author: David von Oheimb
- Copyright 1999 Technische Universitaet Muenchen
+ License: GPL (GNU GENERAL PUBLIC LICENSE)
*)
header {* Operational evaluation (big-step) semantics of Java expressions and
statements
--- a/src/HOL/Bali/Name.thy Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/Name.thy Mon Jan 28 23:35:20 2002 +0100
@@ -71,8 +71,7 @@
axclass has_pname < "type"
consts pname::"'a::has_pname \<Rightarrow> pname"
-instance pname::has_pname
-by (intro_classes)
+instance pname::has_pname ..
defs (overloaded)
pname_pname_def: "pname (p::pname) \<equiv> p"
@@ -80,8 +79,7 @@
axclass has_tname < "type"
consts tname::"'a::has_tname \<Rightarrow> tname"
-instance tname::has_tname
-by (intro_classes)
+instance tname::has_tname ..
defs (overloaded)
tname_tname_def: "tname (t::tname) \<equiv> t"
@@ -90,8 +88,7 @@
consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
(* Declare qtname as instance of has_qtname *)
-instance pid_field_type::(has_pname,"type") has_qtname
-by intro_classes
+instance pid_field_type::(has_pname,"type") has_qtname ..
defs (overloaded)
qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
--- a/src/HOL/Bali/ROOT.ML Mon Jan 28 18:51:48 2002 +0100
+++ b/src/HOL/Bali/ROOT.ML Mon Jan 28 23:35:20 2002 +0100
@@ -1,13 +1,4 @@
-use_thy "WellForm";
-
-(*The dynamic part of Bali, including type-safety*)
-use_thy "Evaln";
-use_thy "Example";
-use_thy "TypeSafe";
-(*###use_thy "Trans";*)
-
-(*The Hoare logic for Bali*)
use_thy "AxExample";
use_thy "AxSound";
use_thy "AxCompl";