# HG changeset patch # User wenzelm # Date 1012257320 -3600 # Node ID f63315dfffd42a2da87af02d6c9c036a7d708691 # Parent 6214f03d6d27118d53d5b162bf682030247d606c tuned; diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/AxCompl.thy --- 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 {* diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/AxExample.thy --- 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 *} diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/AxSem.thy --- 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 diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/AxSound.thy --- 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 diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/Basis.thy --- 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;*) diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/Decl.thy --- 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 \ (b::acc_modi) \ (a = b) \ (a < b)" instance acc_modi:: order -proof (intro_classes) +proof fix x y z::acc_modi { show "x \ x" \\ -- reflexivity @@ -91,7 +90,7 @@ qed instance acc_modi:: linorder -proof intro_classes +proof fix x y:: acc_modi show "x \ y \ y \ 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 \ 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: diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/DeclConcepts.thy --- 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 \ 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) \ 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) \ 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 \ (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 \ (case m of @@ -129,8 +125,7 @@ axclass has_declclass < "type" consts declclass:: "'a::has_declclass \ 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) \ 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 \ declclass (fst p)" @@ -158,15 +152,13 @@ consts is_static :: "'a \ 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) \ 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 \ 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 \ 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) \ 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) \ 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) \ 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 \ resTy (snd p)" diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/Evaln.thy --- 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 diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/Name.thy --- 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 \ pname" -instance pname::has_pname -by (intro_classes) +instance pname::has_pname .. defs (overloaded) pname_pname_def: "pname (p::pname) \ p" @@ -80,8 +79,7 @@ axclass has_tname < "type" consts tname::"'a::has_tname \ tname" -instance tname::has_tname -by (intro_classes) +instance tname::has_tname .. defs (overloaded) tname_tname_def: "tname (t::tname) \ t" @@ -90,8 +88,7 @@ consts qtname:: "'a::has_qtname \ 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) \ q" diff -r 6214f03d6d27 -r f63315dfffd4 src/HOL/Bali/ROOT.ML --- 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";