# HG changeset patch # User haftmann # Date 1266930794 -3600 # Node ID f8bae261e7a982f3e61b34166a872eb567f49aa3 # Parent cbdf785a1eb3e02c77e7b95009516be3a629c80e# Parent c298a4fc324be0150c35dccf40688c305c6f6b48 merged diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Algebra/abstract/Ideal2.thy --- a/src/HOL/Algebra/abstract/Ideal2.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Algebra/abstract/Ideal2.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,6 +1,5 @@ (* Ideals for commutative rings - $Id$ Author: Clemens Ballarin, started 24 September 1999 *) @@ -23,9 +22,8 @@ text {* Principle ideal domains *} -axclass pid < "domain" - pid_ax: "is_ideal I ==> is_pideal I" - +class pid = + assumes pid_ax: "is_ideal (I :: 'a::domain \ _) \ is_pideal I" (* is_ideal *) diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Bali/Decl.thy --- a/src/HOL/Bali/Decl.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Bali/Decl.thy Tue Feb 23 14:13:14 2010 +0100 @@ -230,18 +230,22 @@ datatype memberid = fid vname | mid sig -axclass has_memberid < "type" -consts - memberid :: "'a::has_memberid \ memberid" +class has_memberid = + fixes memberid :: "'a \ memberid" -instance memberdecl::has_memberid .. +instantiation memberdecl :: has_memberid +begin -defs (overloaded) +definition memberdecl_memberid_def: "memberid m \ (case m of fdecl (vn,f) \ fid vn | mdecl (sig,m) \ mid sig)" +instance .. + +end + lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn" by (simp add: memberdecl_memberid_def) @@ -254,12 +258,17 @@ lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)" by (cases m) (simp add: memberdecl_memberid_def) -instance * :: (type, has_memberid) has_memberid .. +instantiation * :: (type, has_memberid) has_memberid +begin -defs (overloaded) +definition pair_memberid_def: "memberid p \ memberid (snd p)" +instance .. + +end + lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m" by (simp add: pair_memberid_def) diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Bali/DeclConcepts.thy --- a/src/HOL/Bali/DeclConcepts.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Bali/DeclConcepts.thy Tue Feb 23 14:13:14 2010 +0100 @@ -79,41 +79,60 @@ text {* overloaded selector @{text accmodi} to select the access modifier out of various HOL types *} -axclass has_accmodi < "type" -consts accmodi:: "'a::has_accmodi \ acc_modi" +class has_accmodi = + fixes accmodi:: "'a \ acc_modi" + +instantiation acc_modi :: has_accmodi +begin -instance acc_modi::has_accmodi .. +definition + acc_modi_accmodi_def: "accmodi (a::acc_modi) \ a" -defs (overloaded) -acc_modi_accmodi_def: "accmodi (a::acc_modi) \ a" +instance .. + +end lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" by (simp add: acc_modi_accmodi_def) -instance decl_ext_type:: ("type") has_accmodi .. +instantiation decl_ext_type:: (type) has_accmodi +begin -defs (overloaded) -decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \ access d" +definition + decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \ access d" +instance .. + +end 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 .. +instantiation * :: (type, has_accmodi) has_accmodi +begin -defs (overloaded) -pair_acc_modi_def: "accmodi p \ (accmodi (snd p))" +definition + pair_acc_modi_def: "accmodi p \ (accmodi (snd p))" + +instance .. + +end lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)" by (simp add: pair_acc_modi_def) -instance memberdecl :: has_accmodi .. +instantiation memberdecl :: has_accmodi +begin -defs (overloaded) -memberdecl_acc_modi_def: "accmodi m \ (case m of +definition + memberdecl_acc_modi_def: "accmodi m \ (case m of fdecl f \ accmodi f | mdecl m \ accmodi m)" +instance .. + +end + lemma memberdecl_fdecl_acc_modi_simp[simp]: "accmodi (fdecl m) = accmodi m" by (simp add: memberdecl_acc_modi_def) @@ -125,21 +144,35 @@ text {* overloaded selector @{text declclass} to select the declaring class out of various HOL types *} -axclass has_declclass < "type" -consts declclass:: "'a::has_declclass \ qtname" +class has_declclass = + fixes declclass:: "'a \ qtname" + +instantiation qtname_ext_type :: (type) has_declclass +begin -instance qtname_ext_type::("type") has_declclass .. +definition + "declclass q \ \ pid = pid q, tid = tid q \" + +instance .. -defs (overloaded) -qtname_declclass_def: "declclass (q::qtname) \ q" +end + +lemma qtname_declclass_def: + "declclass q \ (q::qtname)" + by (induct q) (simp add: declclass_qtname_ext_type_def) lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" by (simp add: qtname_declclass_def) -instance * :: ("has_declclass","type") has_declclass .. +instantiation * :: (has_declclass, type) has_declclass +begin -defs (overloaded) -pair_declclass_def: "declclass p \ declclass (fst p)" +definition + pair_declclass_def: "declclass p \ declclass (fst p)" + +instance .. + +end lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" by (simp add: pair_declclass_def) @@ -147,25 +180,38 @@ text {* overloaded selector @{text is_static} to select the static modifier out of various HOL types *} +class has_static = + fixes is_static :: "'a \ bool" -axclass has_static < "type" -consts is_static :: "'a::has_static \ bool" +instantiation decl_ext_type :: (has_static) has_static +begin -instance decl_ext_type :: ("has_static") has_static .. +instance .. + +end -instance member_ext_type :: ("type") has_static .. +instantiation member_ext_type :: (type) has_static +begin + +instance .. -defs (overloaded) -static_field_type_is_static_def: - "is_static (m::('b member_scheme)) \ static m" +end + +axiomatization where + static_field_type_is_static_def: "is_static (m::('a member_scheme)) \ static m" lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" by (simp add: static_field_type_is_static_def) -instance * :: ("type","has_static") has_static .. +instantiation * :: (type, has_static) has_static +begin -defs (overloaded) -pair_is_static_def: "is_static p \ is_static (snd p)" +definition + pair_is_static_def: "is_static p \ is_static (snd p)" + +instance .. + +end lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s" by (simp add: pair_is_static_def) @@ -173,14 +219,19 @@ lemma pair_is_static_simp1: "is_static p = is_static (snd p)" by (simp add: pair_is_static_def) -instance memberdecl:: has_static .. +instantiation memberdecl :: has_static +begin -defs (overloaded) +definition memberdecl_is_static_def: "is_static m \ (case m of fdecl f \ is_static f | mdecl m \ is_static m)" +instance .. + +end + lemma memberdecl_is_static_fdecl_simp[simp]: "is_static (fdecl f) = is_static f" by (simp add: memberdecl_is_static_def) @@ -389,18 +440,32 @@ text {* overloaded selector @{text resTy} to select the result type out of various HOL types *} -axclass has_resTy < "type" -consts resTy:: "'a::has_resTy \ ty" +class has_resTy = + fixes resTy:: "'a \ ty" + +instantiation decl_ext_type :: (has_resTy) has_resTy +begin -instance decl_ext_type :: ("has_resTy") has_resTy .. +instance .. + +end + +instantiation member_ext_type :: (has_resTy) has_resTy +begin -instance member_ext_type :: ("has_resTy") has_resTy .. +instance .. -instance mhead_ext_type :: ("type") has_resTy .. +end + +instantiation mhead_ext_type :: (type) has_resTy +begin -defs (overloaded) -mhead_ext_type_resTy_def: - "resTy (m::('b mhead_scheme)) \ resT m" +instance .. + +end + +axiomatization where + mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \ resT m" lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" by (simp add: mhead_ext_type_resTy_def) @@ -408,10 +473,15 @@ lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" by (simp add: mhead_def mhead_resTy_simp) -instance * :: ("type","has_resTy") has_resTy .. +instantiation * :: ("type","has_resTy") has_resTy +begin -defs (overloaded) -pair_resTy_def: "resTy p \ resTy (snd p)" +definition + pair_resTy_def: "resTy p \ resTy (snd p)" + +instance .. + +end lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m" by (simp add: pair_resTy_def) diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Bali/Name.thy --- a/src/HOL/Bali/Name.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Bali/Name.thy Tue Feb 23 14:13:14 2010 +0100 @@ -48,29 +48,34 @@ pid :: pname tid :: tname -axclass has_pname < "type" -consts pname::"'a::has_pname \ pname" +class has_pname = + fixes pname :: "'a \ pname" -instance pname::has_pname .. +instantiation pname :: has_pname +begin -defs (overloaded) -pname_pname_def: "pname (p::pname) \ p" +definition + pname_pname_def: "pname (p::pname) \ p" -axclass has_tname < "type" -consts tname::"'a::has_tname \ tname" +instance .. + +end -instance tname::has_tname .. +class has_tname = + fixes tname :: "'a \ tname" -defs (overloaded) -tname_tname_def: "tname (t::tname) \ t" +instantiation tname :: has_tname +begin -axclass has_qtname < type -consts qtname:: "'a::has_qtname \ qtname" +definition + tname_tname_def: "tname (t::tname) \ t" + +instance .. -instance qtname_ext_type :: (type) has_qtname .. +end -defs (overloaded) -qtname_qtname_def: "qtname (q::qtname) \ q" +definition + qtname_qtname_def: "qtname (q::'a qtname_ext_type) \ q" translations "mname" <= "Name.mname" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Bali/Term.thy --- a/src/HOL/Bali/Term.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Bali/Term.thy Tue Feb 23 14:13:14 2010 +0100 @@ -295,8 +295,8 @@ following. *} -axclass inj_term < "type" -consts inj_term:: "'a::inj_term \ term" ("\_\" 1000) +class inj_term = + fixes inj_term:: "'a \ term" ("\_\" 1000) text {* How this overloaded injections work can be seen in the theory @{text DefiniteAssignment}. Other big inductive relations on @@ -308,10 +308,15 @@ as bridge between the different conventions. *} -instance stmt::inj_term .. +instantiation stmt :: inj_term +begin -defs (overloaded) -stmt_inj_term_def: "\c::stmt\ \ In1r c" +definition + stmt_inj_term_def: "\c::stmt\ \ In1r c" + +instance .. + +end lemma stmt_inj_term_simp: "\c::stmt\ = In1r c" by (simp add: stmt_inj_term_def) @@ -319,10 +324,15 @@ lemma stmt_inj_term [iff]: "\x::stmt\ = \y\ \ x = y" by (simp add: stmt_inj_term_simp) -instance expr::inj_term .. +instantiation expr :: inj_term +begin -defs (overloaded) -expr_inj_term_def: "\e::expr\ \ In1l e" +definition + expr_inj_term_def: "\e::expr\ \ In1l e" + +instance .. + +end lemma expr_inj_term_simp: "\e::expr\ = In1l e" by (simp add: expr_inj_term_def) @@ -330,10 +340,15 @@ lemma expr_inj_term [iff]: "\x::expr\ = \y\ \ x = y" by (simp add: expr_inj_term_simp) -instance var::inj_term .. +instantiation var :: inj_term +begin -defs (overloaded) -var_inj_term_def: "\v::var\ \ In2 v" +definition + var_inj_term_def: "\v::var\ \ In2 v" + +instance .. + +end lemma var_inj_term_simp: "\v::var\ = In2 v" by (simp add: var_inj_term_def) @@ -341,10 +356,32 @@ lemma var_inj_term [iff]: "\x::var\ = \y\ \ x = y" by (simp add: var_inj_term_simp) -instance "list":: (type) inj_term .. +class expr_of = + fixes expr_of :: "'a \ expr" + +instantiation expr :: expr_of +begin + +definition + "expr_of = (\(e::expr). e)" + +instance .. + +end -defs (overloaded) -expr_list_inj_term_def: "\es::expr list\ \ In3 es" +instantiation list :: (expr_of) inj_term +begin + +definition + "\es::'a list\ \ In3 (map expr_of es)" + +instance .. + +end + +lemma expr_list_inj_term_def: + "\es::expr list\ \ In3 es" + by (simp add: inj_term_list_def expr_of_expr_def) lemma expr_list_inj_term_simp: "\es::expr list\ = In3 es" by (simp add: expr_list_inj_term_def) diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/Examples.thy --- a/src/HOL/Hoare/Examples.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/Examples.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Hoare/Examples.thy - ID: $Id$ Author: Norbert Galm Copyright 1998 TUM Various examples. *) -theory Examples imports Hoare Arith2 begin +theory Examples imports Hoare_Logic Arith2 begin (*** ARITHMETIC ***) diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/ExamplesAbort.thy --- a/src/HOL/Hoare/ExamplesAbort.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/ExamplesAbort.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,12 +1,11 @@ (* Title: HOL/Hoare/ExamplesAbort.thy - ID: $Id$ Author: Tobias Nipkow Copyright 1998 TUM Some small examples for programs that may abort. *) -theory ExamplesAbort imports HoareAbort begin +theory ExamplesAbort imports Hoare_Logic_Abort begin lemma "VARS x y z::nat {y = z & z \ 0} z \ 0 \ x := y div z {x = 1}" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/HeapSyntax.thy --- a/src/HOL/Hoare/HeapSyntax.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/HeapSyntax.thy Tue Feb 23 14:13:14 2010 +0100 @@ -3,7 +3,7 @@ Copyright 2002 TUM *) -theory HeapSyntax imports Hoare Heap begin +theory HeapSyntax imports Hoare_Logic Heap begin subsection "Field access and update" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/HeapSyntaxAbort.thy --- a/src/HOL/Hoare/HeapSyntaxAbort.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/HeapSyntaxAbort.thy Tue Feb 23 14:13:14 2010 +0100 @@ -3,7 +3,7 @@ Copyright 2002 TUM *) -theory HeapSyntaxAbort imports HoareAbort Heap begin +theory HeapSyntaxAbort imports Hoare_Logic_Abort Heap begin subsection "Field access and update" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/Hoare.thy --- a/src/HOL/Hoare/Hoare.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/Hoare.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,245 +1,9 @@ -(* Title: HOL/Hoare/Hoare.thy - Author: Leonor Prensa Nieto & Tobias Nipkow - Copyright 1998 TUM - -Sugared semantic embedding of Hoare logic. -Strictly speaking a shallow embedding (as implemented by Norbert Galm -following Mike Gordon) would suffice. Maybe the datatype com comes in useful -later. +(* Author: Tobias Nipkow + Copyright 1998-2003 TUM *) theory Hoare -imports Main -uses ("hoare_tac.ML") +imports Examples ExamplesAbort Pointers0 Pointer_Examples Pointer_ExamplesAbort SchorrWaite Separation begin -types - 'a bexp = "'a set" - 'a assn = "'a set" - -datatype - 'a com = Basic "'a \ 'a" - | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) - | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) - | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) - -abbreviation annskip ("SKIP") where "SKIP == Basic id" - -types 'a sem = "'a => 'a => bool" - -consts iter :: "nat => 'a bexp => 'a sem => 'a sem" -primrec -"iter 0 b S = (%s s'. s ~: b & (s=s'))" -"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))" - -consts Sem :: "'a com => 'a sem" -primrec -"Sem(Basic f) s s' = (s' = f s)" -"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')" -"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') & - (s ~: b --> Sem c2 s s'))" -"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')" - -constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" - "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q" - - - -(** parse translations **) - -syntax - "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) - -syntax - "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) -syntax ("" output) - "_hoare" :: "['a assn,'a com,'a assn] => bool" - ("{_} // _ // {_}" [0,55,0] 50) -ML {* - -local - -fun abs((a,T),body) = - let val a = absfree(a, dummyT, body) - in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end -in - -fun mk_abstuple [x] body = abs (x, body) - | mk_abstuple (x::xs) body = - Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); - -fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b - | mk_fbody a e ((b,_)::xs) = - Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs; - -fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) end -*} - -(* bexp_tr & assn_tr *) -(*all meta-variables for bexp except for TRUE are translated as if they - were boolean expressions*) -ML{* -fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) - | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; - -fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; -*} -(* com_tr *) -ML{* -fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = - Syntax.const @{const_syntax Basic} $ mk_fexp a e xs - | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f - | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = - Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = - Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = - Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs - | com_tr t _ = t (* if t is just a Free/Var *) -*} - -(* triple_tr *) (* FIXME does not handle "_idtdummy" *) -ML{* -local - -fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *) - | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T); - -fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars - | vars_tr t = [var_tr t] - -in -fun hoare_vars_tr [vars, pre, prg, post] = - let val xs = vars_tr vars - in Syntax.const @{const_syntax Valid} $ - assn_tr pre xs $ com_tr prg xs $ assn_tr post xs - end - | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); -end -*} - -parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *} - - -(*****************************************************************************) - -(*** print translations ***) -ML{* -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = - subst_bound (Syntax.free v, dest_abstuple body) - | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) - | dest_abstuple trm = trm; - -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t - | abs2list (Abs(x,T,t)) = [Free (x, T)] - | abs2list _ = []; - -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t - | mk_ts (Abs(x,_,t)) = mk_ts t - | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) - | mk_ts t = [t]; - -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = - ((Syntax.free x)::(abs2list t), mk_ts t) - | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) - | mk_vts t = raise Match; - -fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) - | find_ch ((v,t)::vts) i xs = - if t = Bound i then find_ch vts (i-1) xs - else (true, (v, subst_bounds (xs, t))); - -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true - | is_f (Abs(x,_,t)) = true - | is_f t = false; -*} - -(* assn_tr' & bexp_tr'*) -ML{* -fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | assn_tr' (Const (@{const_syntax inter}, _) $ - (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) = - Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 - | assn_tr' t = t; - -fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | bexp_tr' t = t; -*} - -(*com_tr' *) -ML{* -fun mk_assign f = - let val (vs, ts) = mk_vts f; - val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) - in - if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which - else Syntax.const @{const_syntax annskip} - end; - -fun com_tr' (Const (@{const_syntax Basic},_) $ f) = - if is_f f then mk_assign f - else Syntax.const @{const_syntax Basic} $ f - | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = - Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = - Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = - Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c - | com_tr' t = t; - -fun spec_tr' [p, c, q] = - Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q -*} - -print_translation {* [(@{const_syntax Valid}, spec_tr')] *} - -lemma SkipRule: "p \ q \ Valid p (Basic id) q" -by (auto simp:Valid_def) - -lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" -by (auto simp:Valid_def) - -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" -by (auto simp:Valid_def) - -lemma CondRule: - "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} - \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" -by (auto simp:Valid_def) - -lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==> - (\s s'. s : I \ iter n b (Sem c) s s' \ s' : I & s' ~: b)"; -apply(induct n) - apply clarsimp -apply(simp (no_asm_use)) -apply blast -done - -lemma WhileRule: - "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" -apply (clarsimp simp:Valid_def) -apply(drule iter_aux) - prefer 2 apply assumption - apply blast -apply blast -done - - -lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" - by blast - -lemmas AbortRule = SkipRule -- "dummy version" -use "hoare_tac.ML" - -method_setup vcg = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} - "verification condition generator" - -method_setup vcg_simp = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} - "verification condition generator plus simplification" - -end diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/HoareAbort.thy --- a/src/HOL/Hoare/HoareAbort.thy Tue Feb 23 14:11:46 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,269 +0,0 @@ -(* Title: HOL/Hoare/HoareAbort.thy - Author: Leonor Prensa Nieto & Tobias Nipkow - Copyright 2003 TUM - -Like Hoare.thy, but with an Abort statement for modelling run time errors. -*) - -theory HoareAbort -imports Main -uses ("hoare_tac.ML") -begin - -types - 'a bexp = "'a set" - 'a assn = "'a set" - -datatype - 'a com = Basic "'a \ 'a" - | Abort - | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) - | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) - | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) - -abbreviation annskip ("SKIP") where "SKIP == Basic id" - -types 'a sem = "'a option => 'a option => bool" - -consts iter :: "nat => 'a bexp => 'a sem => 'a sem" -primrec -"iter 0 b S = (\s s'. s \ Some ` b \ s=s')" -"iter (Suc n) b S = - (\s s'. s \ Some ` b \ (\s''. S s s'' \ iter n b S s'' s'))" - -consts Sem :: "'a com => 'a sem" -primrec -"Sem(Basic f) s s' = (case s of None \ s' = None | Some t \ s' = Some(f t))" -"Sem Abort s s' = (s' = None)" -"Sem(c1;c2) s s' = (\s''. Sem c1 s s'' \ Sem c2 s'' s')" -"Sem(IF b THEN c1 ELSE c2 FI) s s' = - (case s of None \ s' = None - | Some t \ ((t \ b \ Sem c1 s s') \ (t \ b \ Sem c2 s s')))" -"Sem(While b x c) s s' = - (if s = None then s' = None else \n. iter n b (Sem c) s s')" - -constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" - "Valid p c q == \s s'. Sem c s s' \ s : Some ` p \ s' : Some ` q" - - - -(** parse translations **) - -syntax - "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) - -syntax - "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" - ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) -syntax ("" output) - "_hoare" :: "['a assn,'a com,'a assn] => bool" - ("{_} // _ // {_}" [0,55,0] 50) -ML {* - -local -fun free a = Free(a,dummyT) -fun abs((a,T),body) = - let val a = absfree(a, dummyT, body) - in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end -in - -fun mk_abstuple [x] body = abs (x, body) - | mk_abstuple (x::xs) body = - Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); - -fun mk_fbody a e [x as (b,_)] = if a=b then e else free b - | mk_fbody a e ((b,_)::xs) = - Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs; - -fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) -end -*} - -(* bexp_tr & assn_tr *) -(*all meta-variables for bexp except for TRUE are translated as if they - were boolean expressions*) -ML{* -fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) - | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; - -fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; -*} -(* com_tr *) -ML{* -fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = - Syntax.const @{const_syntax Basic} $ mk_fexp a e xs - | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f - | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = - Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = - Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs - | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = - Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs - | com_tr t _ = t (* if t is just a Free/Var *) -*} - -(* triple_tr *) (* FIXME does not handle "_idtdummy" *) -ML{* -local - -fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *) - | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T); - -fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars - | vars_tr t = [var_tr t] - -in -fun hoare_vars_tr [vars, pre, prg, post] = - let val xs = vars_tr vars - in Syntax.const @{const_syntax Valid} $ - assn_tr pre xs $ com_tr prg xs $ assn_tr post xs - end - | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); -end -*} - -parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *} - - -(*****************************************************************************) - -(*** print translations ***) -ML{* -fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = - subst_bound (Syntax.free v, dest_abstuple body) - | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) - | dest_abstuple trm = trm; - -fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t - | abs2list (Abs(x,T,t)) = [Free (x, T)] - | abs2list _ = []; - -fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t - | mk_ts (Abs(x,_,t)) = mk_ts t - | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) - | mk_ts t = [t]; - -fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = - ((Syntax.free x)::(abs2list t), mk_ts t) - | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) - | mk_vts t = raise Match; - -fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) - | find_ch ((v,t)::vts) i xs = - if t = Bound i then find_ch vts (i-1) xs - else (true, (v, subst_bounds (xs,t))); - -fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true - | is_f (Abs(x,_,t)) = true - | is_f t = false; -*} - -(* assn_tr' & bexp_tr'*) -ML{* -fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $ - (Const (@{const_syntax Collect},_) $ T2)) = - Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 - | assn_tr' t = t; - -fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T - | bexp_tr' t = t; -*} - -(*com_tr' *) -ML{* -fun mk_assign f = - let val (vs, ts) = mk_vts f; - val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) - in - if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which - else Syntax.const @{const_syntax annskip} - end; - -fun com_tr' (Const (@{const_syntax Basic},_) $ f) = - if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f - | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = - Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = - Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 - | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = - Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c - | com_tr' t = t; - -fun spec_tr' [p, c, q] = - Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q -*} - -print_translation {* [(@{const_syntax Valid}, spec_tr')] *} - -(*** The proof rules ***) - -lemma SkipRule: "p \ q \ Valid p (Basic id) q" -by (auto simp:Valid_def) - -lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" -by (auto simp:Valid_def) - -lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" -by (auto simp:Valid_def) - -lemma CondRule: - "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} - \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" -by (fastsimp simp:Valid_def image_def) - -lemma iter_aux: - "! s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \ - (\s s'. s \ Some ` I \ iter n b (Sem c) s s' \ s' \ Some ` (I \ -b))"; -apply(unfold image_def) -apply(induct n) - apply clarsimp -apply(simp (no_asm_use)) -apply blast -done - -lemma WhileRule: - "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" -apply(simp add:Valid_def) -apply(simp (no_asm) add:image_def) -apply clarify -apply(drule iter_aux) - prefer 2 apply assumption - apply blast -apply blast -done - -lemma AbortRule: "p \ {s. False} \ Valid p Abort q" -by(auto simp:Valid_def) - - -subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *} - -lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" - by blast - -use "hoare_tac.ML" - -method_setup vcg = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} - "verification condition generator" - -method_setup vcg_simp = {* - Scan.succeed (fn ctxt => - SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} - "verification condition generator plus simplification" - -(* Special syntax for guarded statements and guarded array updates: *) - -syntax - guarded_com :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) - array_update :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) -translations - "P \ c" == "IF P THEN c ELSE CONST Abort FI" - "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" - (* reverse translation not possible because of duplicate "a" *) - -text{* Note: there is no special syntax for guarded array access. Thus -you must write @{text"j < length a \ a[i] := a!j"}. *} - -end diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/Hoare_Logic.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Hoare_Logic.thy Tue Feb 23 14:13:14 2010 +0100 @@ -0,0 +1,245 @@ +(* Title: HOL/Hoare/Hoare.thy + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 1998 TUM + +Sugared semantic embedding of Hoare logic. +Strictly speaking a shallow embedding (as implemented by Norbert Galm +following Mike Gordon) would suffice. Maybe the datatype com comes in useful +later. +*) + +theory Hoare_Logic +imports Main +uses ("hoare_tac.ML") +begin + +types + 'a bexp = "'a set" + 'a assn = "'a set" + +datatype + 'a com = Basic "'a \ 'a" + | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) + | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) + | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) + +abbreviation annskip ("SKIP") where "SKIP == Basic id" + +types 'a sem = "'a => 'a => bool" + +consts iter :: "nat => 'a bexp => 'a sem => 'a sem" +primrec +"iter 0 b S = (%s s'. s ~: b & (s=s'))" +"iter (Suc n) b S = (%s s'. s : b & (? s''. S s s'' & iter n b S s'' s'))" + +consts Sem :: "'a com => 'a sem" +primrec +"Sem(Basic f) s s' = (s' = f s)" +"Sem(c1;c2) s s' = (? s''. Sem c1 s s'' & Sem c2 s'' s')" +"Sem(IF b THEN c1 ELSE c2 FI) s s' = ((s : b --> Sem c1 s s') & + (s ~: b --> Sem c2 s s'))" +"Sem(While b x c) s s' = (? n. iter n b (Sem c) s s')" + +constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" + "Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q" + + + +(** parse translations **) + +syntax + "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) + +syntax + "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" + ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) +syntax ("" output) + "_hoare" :: "['a assn,'a com,'a assn] => bool" + ("{_} // _ // {_}" [0,55,0] 50) +ML {* + +local + +fun abs((a,T),body) = + let val a = absfree(a, dummyT, body) + in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end +in + +fun mk_abstuple [x] body = abs (x, body) + | mk_abstuple (x::xs) body = + Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); + +fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b + | mk_fbody a e ((b,_)::xs) = + Syntax.const @{const_syntax Pair} $ (if a=b then e else Syntax.free b) $ mk_fbody a e xs; + +fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) +end +*} + +(* bexp_tr & assn_tr *) +(*all meta-variables for bexp except for TRUE are translated as if they + were boolean expressions*) +ML{* +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) + | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; + +fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; +*} +(* com_tr *) +ML{* +fun com_tr (Const(@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = + Syntax.const @{const_syntax Basic} $ mk_fexp a e xs + | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f + | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = + Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = + Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = + Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs + | com_tr t _ = t (* if t is just a Free/Var *) +*} + +(* triple_tr *) (* FIXME does not handle "_idtdummy" *) +ML{* +local + +fun var_tr(Free(a,_)) = (a,Bound 0) (* Bound 0 = dummy term *) + | var_tr(Const (@{syntax_const "_constrain"}, _) $ (Free (a,_)) $ T) = (a,T); + +fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars + | vars_tr t = [var_tr t] + +in +fun hoare_vars_tr [vars, pre, prg, post] = + let val xs = vars_tr vars + in Syntax.const @{const_syntax Valid} $ + assn_tr pre xs $ com_tr prg xs $ assn_tr post xs + end + | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); +end +*} + +parse_translation {* [(@{syntax_const "_hoare_vars"}, hoare_vars_tr)] *} + + +(*****************************************************************************) + +(*** print translations ***) +ML{* +fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = + subst_bound (Syntax.free v, dest_abstuple body) + | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) + | dest_abstuple trm = trm; + +fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t + | abs2list (Abs(x,T,t)) = [Free (x, T)] + | abs2list _ = []; + +fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t + | mk_ts (Abs(x,_,t)) = mk_ts t + | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) + | mk_ts t = [t]; + +fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = + ((Syntax.free x)::(abs2list t), mk_ts t) + | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) + | mk_vts t = raise Match; + +fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) + | find_ch ((v,t)::vts) i xs = + if t = Bound i then find_ch vts (i-1) xs + else (true, (v, subst_bounds (xs, t))); + +fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true + | is_f (Abs(x,_,t)) = true + | is_f t = false; +*} + +(* assn_tr' & bexp_tr'*) +ML{* +fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | assn_tr' (Const (@{const_syntax inter}, _) $ + (Const (@{const_syntax Collect},_) $ T1) $ (Const (@{const_syntax Collect},_) $ T2)) = + Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 + | assn_tr' t = t; + +fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | bexp_tr' t = t; +*} + +(*com_tr' *) +ML{* +fun mk_assign f = + let val (vs, ts) = mk_vts f; + val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) + in + if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which + else Syntax.const @{const_syntax annskip} + end; + +fun com_tr' (Const (@{const_syntax Basic},_) $ f) = + if is_f f then mk_assign f + else Syntax.const @{const_syntax Basic} $ f + | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = + Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = + Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = + Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c + | com_tr' t = t; + +fun spec_tr' [p, c, q] = + Syntax.const @{syntax_const "_hoare"} $ assn_tr' p $ com_tr' c $ assn_tr' q +*} + +print_translation {* [(@{const_syntax Valid}, spec_tr')] *} + +lemma SkipRule: "p \ q \ Valid p (Basic id) q" +by (auto simp:Valid_def) + +lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" +by (auto simp:Valid_def) + +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +by (auto simp:Valid_def) + +lemma CondRule: + "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} + \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" +by (auto simp:Valid_def) + +lemma iter_aux: "! s s'. Sem c s s' --> s : I & s : b --> s' : I ==> + (\s s'. s : I \ iter n b (Sem c) s s' \ s' : I & s' ~: b)"; +apply(induct n) + apply clarsimp +apply(simp (no_asm_use)) +apply blast +done + +lemma WhileRule: + "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" +apply (clarsimp simp:Valid_def) +apply(drule iter_aux) + prefer 2 apply assumption + apply blast +apply blast +done + + +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" + by blast + +lemmas AbortRule = SkipRule -- "dummy version" +use "hoare_tac.ML" + +method_setup vcg = {* + Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} + "verification condition generator" + +method_setup vcg_simp = {* + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} + "verification condition generator plus simplification" + +end diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/Hoare_Logic_Abort.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy Tue Feb 23 14:13:14 2010 +0100 @@ -0,0 +1,269 @@ +(* Title: HOL/Hoare/HoareAbort.thy + Author: Leonor Prensa Nieto & Tobias Nipkow + Copyright 2003 TUM + +Like Hoare.thy, but with an Abort statement for modelling run time errors. +*) + +theory Hoare_Logic_Abort +imports Main +uses ("hoare_tac.ML") +begin + +types + 'a bexp = "'a set" + 'a assn = "'a set" + +datatype + 'a com = Basic "'a \ 'a" + | Abort + | Seq "'a com" "'a com" ("(_;/ _)" [61,60] 60) + | Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61) + | While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61) + +abbreviation annskip ("SKIP") where "SKIP == Basic id" + +types 'a sem = "'a option => 'a option => bool" + +consts iter :: "nat => 'a bexp => 'a sem => 'a sem" +primrec +"iter 0 b S = (\s s'. s \ Some ` b \ s=s')" +"iter (Suc n) b S = + (\s s'. s \ Some ` b \ (\s''. S s s'' \ iter n b S s'' s'))" + +consts Sem :: "'a com => 'a sem" +primrec +"Sem(Basic f) s s' = (case s of None \ s' = None | Some t \ s' = Some(f t))" +"Sem Abort s s' = (s' = None)" +"Sem(c1;c2) s s' = (\s''. Sem c1 s s'' \ Sem c2 s'' s')" +"Sem(IF b THEN c1 ELSE c2 FI) s s' = + (case s of None \ s' = None + | Some t \ ((t \ b \ Sem c1 s s') \ (t \ b \ Sem c2 s s')))" +"Sem(While b x c) s s' = + (if s = None then s' = None else \n. iter n b (Sem c) s s')" + +constdefs Valid :: "'a bexp \ 'a com \ 'a bexp \ bool" + "Valid p c q == \s s'. Sem c s s' \ s : Some ` p \ s' : Some ` q" + + + +(** parse translations **) + +syntax + "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61) + +syntax + "_hoare_abort_vars" :: "[idts, 'a assn,'a com,'a assn] => bool" + ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) +syntax ("" output) + "_hoare_abort" :: "['a assn,'a com,'a assn] => bool" + ("{_} // _ // {_}" [0,55,0] 50) +ML {* + +local +fun free a = Free(a,dummyT) +fun abs((a,T),body) = + let val a = absfree(a, dummyT, body) + in if T = Bound 0 then a else Const(Syntax.constrainAbsC,dummyT) $ a $ T end +in + +fun mk_abstuple [x] body = abs (x, body) + | mk_abstuple (x::xs) body = + Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body); + +fun mk_fbody a e [x as (b,_)] = if a=b then e else free b + | mk_fbody a e ((b,_)::xs) = + Syntax.const @{const_syntax Pair} $ (if a=b then e else free b) $ mk_fbody a e xs; + +fun mk_fexp a e xs = mk_abstuple xs (mk_fbody a e xs) +end +*} + +(* bexp_tr & assn_tr *) +(*all meta-variables for bexp except for TRUE are translated as if they + were boolean expressions*) +ML{* +fun bexp_tr (Const ("TRUE", _)) xs = Syntax.const "TRUE" (* FIXME !? *) + | bexp_tr b xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs b; + +fun assn_tr r xs = Syntax.const @{const_syntax Collect} $ mk_abstuple xs r; +*} +(* com_tr *) +ML{* +fun com_tr (Const (@{syntax_const "_assign"},_) $ Free (a,_) $ e) xs = + Syntax.const @{const_syntax Basic} $ mk_fexp a e xs + | com_tr (Const (@{const_syntax Basic},_) $ f) xs = Syntax.const @{const_syntax Basic} $ f + | com_tr (Const (@{const_syntax Seq},_) $ c1 $ c2) xs = + Syntax.const @{const_syntax Seq} $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) xs = + Syntax.const @{const_syntax Cond} $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs + | com_tr (Const (@{const_syntax While},_) $ b $ I $ c) xs = + Syntax.const @{const_syntax While} $ bexp_tr b xs $ assn_tr I xs $ com_tr c xs + | com_tr t _ = t (* if t is just a Free/Var *) +*} + +(* triple_tr *) (* FIXME does not handle "_idtdummy" *) +ML{* +local + +fun var_tr (Free (a, _)) = (a, Bound 0) (* Bound 0 = dummy term *) + | var_tr (Const (@{syntax_const "_constrain"}, _) $ Free (a, _) $ T) = (a, T); + +fun vars_tr (Const (@{syntax_const "_idts"}, _) $ idt $ vars) = var_tr idt :: vars_tr vars + | vars_tr t = [var_tr t] + +in +fun hoare_vars_tr [vars, pre, prg, post] = + let val xs = vars_tr vars + in Syntax.const @{const_syntax Valid} $ + assn_tr pre xs $ com_tr prg xs $ assn_tr post xs + end + | hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); +end +*} + +parse_translation {* [(@{syntax_const "_hoare_abort_vars"}, hoare_vars_tr)] *} + + +(*****************************************************************************) + +(*** print translations ***) +ML{* +fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) = + subst_bound (Syntax.free v, dest_abstuple body) + | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body) + | dest_abstuple trm = trm; + +fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t + | abs2list (Abs(x,T,t)) = [Free (x, T)] + | abs2list _ = []; + +fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t + | mk_ts (Abs(x,_,t)) = mk_ts t + | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b) + | mk_ts t = [t]; + +fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = + ((Syntax.free x)::(abs2list t), mk_ts t) + | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t]) + | mk_vts t = raise Match; + +fun find_ch [] i xs = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) + | find_ch ((v,t)::vts) i xs = + if t = Bound i then find_ch vts (i-1) xs + else (true, (v, subst_bounds (xs,t))); + +fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true + | is_f (Abs(x,_,t)) = true + | is_f t = false; +*} + +(* assn_tr' & bexp_tr'*) +ML{* +fun assn_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | assn_tr' (Const (@{const_syntax inter},_) $ (Const (@{const_syntax Collect},_) $ T1) $ + (Const (@{const_syntax Collect},_) $ T2)) = + Syntax.const @{const_syntax inter} $ dest_abstuple T1 $ dest_abstuple T2 + | assn_tr' t = t; + +fun bexp_tr' (Const (@{const_syntax Collect},_) $ T) = dest_abstuple T + | bexp_tr' t = t; +*} + +(*com_tr' *) +ML{* +fun mk_assign f = + let val (vs, ts) = mk_vts f; + val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs) + in + if ch then Syntax.const @{syntax_const "_assign"} $ fst which $ snd which + else Syntax.const @{const_syntax annskip} + end; + +fun com_tr' (Const (@{const_syntax Basic},_) $ f) = + if is_f f then mk_assign f else Syntax.const @{const_syntax Basic} $ f + | com_tr' (Const (@{const_syntax Seq},_) $ c1 $ c2) = + Syntax.const @{const_syntax Seq} $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax Cond},_) $ b $ c1 $ c2) = + Syntax.const @{const_syntax Cond} $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 + | com_tr' (Const (@{const_syntax While},_) $ b $ I $ c) = + Syntax.const @{const_syntax While} $ bexp_tr' b $ assn_tr' I $ com_tr' c + | com_tr' t = t; + +fun spec_tr' [p, c, q] = + Syntax.const @{syntax_const "_hoare_abort"} $ assn_tr' p $ com_tr' c $ assn_tr' q +*} + +print_translation {* [(@{const_syntax Valid}, spec_tr')] *} + +(*** The proof rules ***) + +lemma SkipRule: "p \ q \ Valid p (Basic id) q" +by (auto simp:Valid_def) + +lemma BasicRule: "p \ {s. f s \ q} \ Valid p (Basic f) q" +by (auto simp:Valid_def) + +lemma SeqRule: "Valid P c1 Q \ Valid Q c2 R \ Valid P (c1;c2) R" +by (auto simp:Valid_def) + +lemma CondRule: + "p \ {s. (s \ b \ s \ w) \ (s \ b \ s \ w')} + \ Valid w c1 q \ Valid w' c2 q \ Valid p (Cond b c1 c2) q" +by (fastsimp simp:Valid_def image_def) + +lemma iter_aux: + "! s s'. Sem c s s' \ s \ Some ` (I \ b) \ s' \ Some ` I \ + (\s s'. s \ Some ` I \ iter n b (Sem c) s s' \ s' \ Some ` (I \ -b))"; +apply(unfold image_def) +apply(induct n) + apply clarsimp +apply(simp (no_asm_use)) +apply blast +done + +lemma WhileRule: + "p \ i \ Valid (i \ b) c i \ i \ (-b) \ q \ Valid p (While b i c) q" +apply(simp add:Valid_def) +apply(simp (no_asm) add:image_def) +apply clarify +apply(drule iter_aux) + prefer 2 apply assumption + apply blast +apply blast +done + +lemma AbortRule: "p \ {s. False} \ Valid p Abort q" +by(auto simp:Valid_def) + + +subsection {* Derivation of the proof rules and, most importantly, the VCG tactic *} + +lemma Compl_Collect: "-(Collect b) = {x. ~(b x)}" + by blast + +use "hoare_tac.ML" + +method_setup vcg = {* + Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} + "verification condition generator" + +method_setup vcg_simp = {* + Scan.succeed (fn ctxt => + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} + "verification condition generator plus simplification" + +(* Special syntax for guarded statements and guarded array updates: *) + +syntax + guarded_com :: "bool \ 'a com \ 'a com" ("(2_ \/ _)" 71) + array_update :: "'a list \ nat \ 'a \ 'a com" ("(2_[_] :=/ _)" [70, 65] 61) +translations + "P \ c" == "IF P THEN c ELSE CONST Abort FI" + "a[i] := v" => "(i < CONST length a) \ (a := CONST list_update a i v)" + (* reverse translation not possible because of duplicate "a" *) + +text{* Note: there is no special syntax for guarded array access. Thus +you must write @{text"j < length a \ a[i] := a!j"}. *} + +end diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/Pointer_Examples.thy --- a/src/HOL/Hoare/Pointer_Examples.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/Pointer_Examples.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Hoare/Pointers.thy - ID: $Id$ Author: Tobias Nipkow Copyright 2002 TUM diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/Pointers0.thy --- a/src/HOL/Hoare/Pointers0.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/Pointers0.thy Tue Feb 23 14:13:14 2010 +0100 @@ -9,12 +9,12 @@ - in fact in some case they appear to get (a bit) more complicated. *) -theory Pointers0 imports Hoare begin +theory Pointers0 imports Hoare_Logic begin subsection "References" -axclass ref < type -consts Null :: "'a::ref" +class ref = + fixes Null :: 'a subsection "Field access and update" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/ROOT.ML --- a/src/HOL/Hoare/ROOT.ML Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/ROOT.ML Tue Feb 23 14:13:14 2010 +0100 @@ -1,8 +1,2 @@ -(* Title: HOL/Hoare/ROOT.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1998-2003 TUM -*) -use_thys ["Examples", "ExamplesAbort", "Pointers0", "Pointer_Examples", - "Pointer_ExamplesAbort", "SchorrWaite", "Separation"]; +use_thy "Hoare"; diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Hoare/Separation.thy --- a/src/HOL/Hoare/Separation.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Hoare/Separation.thy Tue Feb 23 14:13:14 2010 +0100 @@ -12,7 +12,7 @@ *) -theory Separation imports HoareAbort SepLogHeap begin +theory Separation imports Hoare_Logic_Abort SepLogHeap begin text{* The semantic definition of a few connectives: *} diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/IsaMakefile Tue Feb 23 14:13:14 2010 +0100 @@ -66,7 +66,6 @@ TLA-Memory \ HOL-UNITY \ HOL-Unix \ - HOL-W0 \ HOL-Word-Examples \ HOL-ZF # ^ this is the sort position @@ -590,9 +589,10 @@ $(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \ Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \ + Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \ Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \ Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \ - Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy \ + Hoare/SchorrWaite.thy Hoare/Separation.thy \ Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib @$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare @@ -846,14 +846,6 @@ @$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog -## HOL-W0 - -HOL-W0: HOL $(LOG)/HOL-W0.gz - -$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex - @$(ISABELLE_TOOL) usedir $(OUT)/HOL W0 - - ## HOL-MicroJava HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz @@ -1319,7 +1311,7 @@ $(LOG)/HOL-SMT-Examples.gz $(LOG)/HOL-SMT.gz \ $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \ $(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \ - $(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz \ + $(LOG)/HOL-Word-Examples.gz \ $(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \ $(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz \ $(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz \ diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Isar_Examples/Group.thy --- a/src/HOL/Isar_Examples/Group.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Isar_Examples/Group.thy Tue Feb 23 14:13:14 2010 +0100 @@ -17,15 +17,12 @@ $\idt{times}$ is provided by the basic HOL theory. *} -consts - one :: "'a" - inverse :: "'a => 'a" +notation Groups.one ("one") -axclass - group < times - group_assoc: "(x * y) * z = x * (y * z)" - group_left_one: "one * x = x" - group_left_inverse: "inverse x * x = one" +class group = times + one + inverse + + assumes group_assoc: "(x * y) * z = x * (y * z)" + assumes group_left_one: "one * x = x" + assumes group_left_inverse: "inverse x * x = one" text {* The group axioms only state the properties of left one and inverse, @@ -144,10 +141,10 @@ \idt{one} :: \alpha)$ are defined like this. *} -axclass monoid < times - monoid_assoc: "(x * y) * z = x * (y * z)" - monoid_left_one: "one * x = x" - monoid_right_one: "x * one = x" +class monoid = times + one + + assumes monoid_assoc: "(x * y) * z = x * (y * z)" + assumes monoid_left_one: "one * x = x" + assumes monoid_right_one: "x * one = x" text {* Groups are \emph{not} yet monoids directly from the definition. For diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Lattice/Bounds.thy --- a/src/HOL/Lattice/Bounds.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Lattice/Bounds.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/Bounds.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Lattice/CompleteLattice.thy --- a/src/HOL/Lattice/CompleteLattice.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Lattice/CompleteLattice.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/CompleteLattice.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) @@ -16,8 +15,8 @@ bounds (see \S\ref{sec:connect-bounds}). *} -axclass complete_lattice \ partial_order - ex_Inf: "\inf. is_Inf A inf" +class complete_lattice = + assumes ex_Inf: "\inf. is_Inf A inf" theorem ex_Sup: "\sup::'a::complete_lattice. is_Sup A sup" proof - diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Lattice/Lattice.thy --- a/src/HOL/Lattice/Lattice.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Lattice/Lattice.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/Lattice.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) @@ -15,9 +14,9 @@ as well). *} -axclass lattice \ partial_order - ex_inf: "\inf. is_inf x y inf" - ex_sup: "\sup. is_sup x y sup" +class lattice = + assumes ex_inf: "\inf. is_inf x y inf" + assumes ex_sup: "\sup. is_sup x y sup" text {* The @{text \} (meet) and @{text \} (join) operations select such diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/Lattice/Orders.thy --- a/src/HOL/Lattice/Orders.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/Lattice/Orders.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Lattice/Orders.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) @@ -18,21 +17,21 @@ required to be related (in either direction). *} -axclass leq < type -consts - leq :: "'a::leq \ 'a \ bool" (infixl "[=" 50) +class leq = + fixes leq :: "'a \ 'a \ bool" (infixl "[=" 50) + notation (xsymbols) leq (infixl "\" 50) -axclass quasi_order < leq - leq_refl [intro?]: "x \ x" - leq_trans [trans]: "x \ y \ y \ z \ x \ z" +class quasi_order = leq + + assumes leq_refl [intro?]: "x \ x" + assumes leq_trans [trans]: "x \ y \ y \ z \ x \ z" -axclass partial_order < quasi_order - leq_antisym [trans]: "x \ y \ y \ x \ x = y" +class partial_order = quasi_order + + assumes leq_antisym [trans]: "x \ y \ y \ x \ x = y" -axclass linear_order < partial_order - leq_linear: "x \ y \ y \ x" +class linear_order = partial_order + + assumes leq_linear: "x \ y \ y \ x" lemma linear_order_cases: "((x::'a::linear_order) \ y \ C) \ (y \ x \ C) \ C" @@ -54,11 +53,16 @@ primrec undual_dual: "undual (dual x) = x" -instance dual :: (leq) leq .. +instantiation dual :: (leq) leq +begin -defs (overloaded) +definition leq_dual_def: "x' \ y' \ undual y' \ undual x'" +instance .. + +end + lemma undual_leq [iff?]: "(undual x' \ undual y') = (y' \ x')" by (simp add: leq_dual_def) @@ -192,11 +196,16 @@ \emph{not} be linear in general. *} -instance * :: (leq, leq) leq .. +instantiation * :: (leq, leq) leq +begin -defs (overloaded) +definition leq_prod_def: "p \ q \ fst p \ fst q \ snd p \ snd q" +instance .. + +end + lemma leq_prodI [intro?]: "fst p \ fst q \ snd p \ snd q \ p \ q" by (unfold leq_prod_def) blast @@ -249,11 +258,16 @@ orders need \emph{not} be linear in general. *} -instance "fun" :: (type, leq) leq .. +instantiation "fun" :: (type, leq) leq +begin -defs (overloaded) +definition leq_fun_def: "f \ g \ \x. f x \ g x" +instance .. + +end + lemma leq_funI [intro?]: "(\x. f x \ g x) \ f \ g" by (unfold leq_fun_def) blast diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/TLA/Action.thy --- a/src/HOL/TLA/Action.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/TLA/Action.thy Tue Feb 23 14:13:14 2010 +0100 @@ -16,8 +16,8 @@ 'a trfun = "(state * state) => 'a" action = "bool trfun" -instance - "*" :: (world, world) world .. +arities + "*" :: (world, world) world consts (** abstract syntax **) diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/TLA/Init.thy --- a/src/HOL/TLA/Init.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/TLA/Init.thy Tue Feb 23 14:13:14 2010 +0100 @@ -12,7 +12,7 @@ begin typedecl behavior -instance behavior :: world .. +arities behavior :: world types temporal = "behavior form" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/TLA/Intensional.thy --- a/src/HOL/TLA/Intensional.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/TLA/Intensional.thy Tue Feb 23 14:13:14 2010 +0100 @@ -10,8 +10,8 @@ imports Main begin -axclass - world < type +classes world +classrel world < type (** abstract syntax **) @@ -171,7 +171,7 @@ "_liftMem" :: "[lift, lift] => lift" ("(_/ \ _)" [50, 51] 50) "_liftNotMem" :: "[lift, lift] => lift" ("(_/ \ _)" [50, 51] 50) -axioms +defs Valid_def: "|- A == ALL w. w |= A" unl_con: "LIFT #c w == c" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/TLA/Stfun.thy --- a/src/HOL/TLA/Stfun.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/TLA/Stfun.thy Tue Feb 23 14:13:14 2010 +0100 @@ -11,7 +11,7 @@ typedecl state -instance state :: world .. +arities state :: world types 'a stfun = "state => 'a" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/W0/README.html --- a/src/HOL/W0/README.html Tue Feb 23 14:11:46 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,33 +0,0 @@ - - - - - - - - - HOL/W0/README - - - - -

Type Inference for MiniML (without let)

- -This theory defines the type inference rules and the type inference algorithm -W for simply-typed lambda terms due to Milner. It proves the -soundness and completeness of W w.r.t. to the rules. An optimized -version I is shown to implement W. - -

- -A report describing the theory is found here:
- -Formal Verification of Algorithm W: The Monomorphic Case. - -

- -NOTE: This theory has been superseded by a more recent development -which formalizes type inference for a language including let. For -details click here. - - diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/W0/ROOT.ML --- a/src/HOL/W0/ROOT.ML Tue Feb 23 14:11:46 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -use_thys ["W0"]; diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/W0/W0.thy --- a/src/HOL/W0/W0.thy Tue Feb 23 14:11:46 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,925 +0,0 @@ -(* Title: HOL/W0/W0.thy - ID: $Id$ - Author: Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel -*) - -theory W0 -imports Main -begin - -section {* Universal error monad *} - -datatype 'a maybe = Ok 'a | Fail - -definition - bind :: "'a maybe \ ('a \ 'b maybe) \ 'b maybe" (infixl "\" 60) where - "m \ f = (case m of Ok r \ f r | Fail \ Fail)" - -syntax - "_bind" :: "patterns \ 'a maybe \ 'b \ 'c" ("(_ := _;//_)" 0) -translations - "P := E; F" == "E \ (\P. F)" - -lemma bind_Ok [simp]: "(Ok s) \ f = (f s)" - by (simp add: bind_def) - -lemma bind_Fail [simp]: "Fail \ f = Fail" - by (simp add: bind_def) - -lemma split_bind: - "P (res \ f) = ((res = Fail \ P Fail) \ (\s. res = Ok s \ P (f s)))" - by (induct res) simp_all - -lemma split_bind_asm: - "P (res \ f) = (\ (res = Fail \ \ P Fail \ (\s. res = Ok s \ \ P (f s))))" - by (simp split: split_bind) - -lemmas bind_splits = split_bind split_bind_asm - -lemma bind_eq_Fail [simp]: - "((m \ f) = Fail) = ((m = Fail) \ (\p. m = Ok p \ f p = Fail))" - by (simp split: split_bind) - -lemma rotate_Ok: "(y = Ok x) = (Ok x = y)" - by (rule eq_sym_conv) - - -section {* MiniML-types and type substitutions *} - -axclass type_struct \ type - -- {* new class for structures containing type variables *} - -datatype "typ" = TVar nat | TFun "typ" "typ" (infixr "->" 70) - -- {* type expressions *} - -types subst = "nat => typ" - -- {* type variable substitution *} - -instance "typ" :: type_struct .. -instance list :: (type_struct) type_struct .. -instance "fun" :: (type, type_struct) type_struct .. - - -subsection {* Substitutions *} - -consts - app_subst :: "subst \ 'a::type_struct \ 'a::type_struct" ("$") - -- {* extension of substitution to type structures *} -primrec (app_subst_typ) - app_subst_TVar: "$s (TVar n) = s n" - app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2" - -defs (overloaded) - app_subst_list: "$s \ map ($s)" - -consts - free_tv :: "'a::type_struct \ nat set" - -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *} - -primrec (free_tv_typ) - "free_tv (TVar m) = {m}" - "free_tv (t1 -> t2) = free_tv t1 \ free_tv t2" - -primrec (free_tv_list) - "free_tv [] = {}" - "free_tv (x # xs) = free_tv x \ free_tv xs" - -definition - dom :: "subst \ nat set" where - "dom s = {n. s n \ TVar n}" - -- {* domain of a substitution *} - -definition - cod :: "subst \ nat set" where - "cod s = (\m \ dom s. free_tv (s m))" - -- {* codomain of a substitutions: the introduced variables *} - -defs (overloaded) - free_tv_subst: "free_tv s \ dom s \ cod s" - -text {* - @{text "new_tv s n"} checks whether @{text n} is a new type variable - wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater - than any type variable occuring in the type structure. -*} - -definition - new_tv :: "nat \ 'a::type_struct \ bool" where - "new_tv n ts = (\m. m \ free_tv ts \ m < n)" - - -subsubsection {* Identity substitution *} - -definition - id_subst :: subst where - "id_subst = (\n. TVar n)" - -lemma app_subst_id_te [simp]: - "$id_subst = (\t::typ. t)" - -- {* application of @{text id_subst} does not change type expression *} -proof - fix t :: "typ" - show "$id_subst t = t" - by (induct t) (simp_all add: id_subst_def) -qed - -lemma app_subst_id_tel [simp]: "$id_subst = (\ts::typ list. ts)" - -- {* application of @{text id_subst} does not change list of type expressions *} -proof - fix ts :: "typ list" - show "$id_subst ts = ts" - by (induct ts) (simp_all add: app_subst_list) -qed - -lemma o_id_subst [simp]: "$s o id_subst = s" - by (rule ext) (simp add: id_subst_def) - -lemma dom_id_subst [simp]: "dom id_subst = {}" - by (simp add: dom_def id_subst_def) - -lemma cod_id_subst [simp]: "cod id_subst = {}" - by (simp add: cod_def) - -lemma free_tv_id_subst [simp]: "free_tv id_subst = {}" - by (simp add: free_tv_subst) - - -lemma cod_app_subst [simp]: - assumes free: "v \ free_tv (s n)" - and neq: "v \ n" - shows "v \ cod s" -proof - - have "s n \ TVar n" - proof - assume "s n = TVar n" - with free have "v = n" by simp - with neq show False .. - qed - with free show ?thesis - by (auto simp add: dom_def cod_def) -qed - -lemma subst_comp_te: "$g ($f t :: typ) = $(\x. $g (f x)) t" - -- {* composition of substitutions *} - by (induct t) simp_all - -lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\x. $g (f x)) ts" - by (induct ts) (simp_all add: app_subst_list subst_comp_te) - - -lemma app_subst_Nil [simp]: "$s [] = []" - by (simp add: app_subst_list) - -lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)" - by (simp add: app_subst_list) - -lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)" - by (simp add: new_tv_def) - -lemma new_tv_Fun [simp]: - "new_tv n (t1 -> t2) = (new_tv n t1 \ new_tv n t2)" - by (auto simp add: new_tv_def) - -lemma new_tv_Nil [simp]: "new_tv n []" - by (simp add: new_tv_def) - -lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \ new_tv n ts)" - by (auto simp add: new_tv_def) - -lemma new_tv_id_subst [simp]: "new_tv n id_subst" - by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def) - -lemma new_tv_subst: - "new_tv n s = - ((\m. n \ m \ s m = TVar m) \ - (\l. l < n \ new_tv n (s l)))" - apply (unfold new_tv_def) - apply (tactic "safe_tac HOL_cs") - -- {* @{text \} *} - apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset} - addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *}) - apply (subgoal_tac "m \ cod s \ s l = TVar l") - apply (tactic "safe_tac HOL_cs") - apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (@{simpset} - addsimps [thm "free_tv_subst"])) 1 *}) - apply (drule_tac P = "\x. m \ free_tv x" in subst, assumption) - apply simp - apply (unfold free_tv_subst cod_def dom_def) - apply clarsimp - apply safe - apply metis - apply (metis linorder_not_less)+ - done - -lemma new_tv_list: "new_tv n x = (\y \ set x. new_tv n y)" - by (induct x) simp_all - -lemma subst_te_new_tv [simp]: - "new_tv n (t::typ) \ $(\x. if x = n then t' else s x) t = $s t" - -- {* substitution affects only variables occurring freely *} - by (induct t) simp_all - -lemma subst_tel_new_tv [simp]: - "new_tv n (ts::typ list) \ $(\x. if x = n then t else s x) ts = $s ts" - by (induct ts) simp_all - -lemma new_tv_le: "n \ m \ new_tv n (t::typ) \ new_tv m t" - -- {* all greater variables are also new *} -proof (induct t) - case (TVar n) - then show ?case by (auto intro: less_le_trans) -next - case TFun - then show ?case by simp -qed - -lemma [simp]: "new_tv n t \ new_tv (Suc n) (t::typ)" - by (rule lessI [THEN less_imp_le [THEN new_tv_le]]) - -lemma new_tv_list_le: - assumes "n \ m" - shows "new_tv n (ts::typ list) \ new_tv m ts" -proof (induct ts) - case Nil - then show ?case by simp -next - case Cons - with `n \ m` show ?case by (auto intro: new_tv_le) -qed - -lemma [simp]: "new_tv n ts \ new_tv (Suc n) (ts::typ list)" - by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]]) - -lemma new_tv_subst_le: "n \ m \ new_tv n (s::subst) \ new_tv m s" - apply (simp add: new_tv_subst) - apply clarify - apply (rule_tac P = "l < n" and Q = "n <= l" in disjE) - apply clarify - apply (simp_all add: new_tv_le) - done - -lemma [simp]: "new_tv n s \ new_tv (Suc n) (s::subst)" - by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]]) - -lemma new_tv_subst_var: - "n < m \ new_tv m (s::subst) \ new_tv m (s n)" - -- {* @{text new_tv} property remains if a substitution is applied *} - by (simp add: new_tv_subst) - -lemma new_tv_subst_te [simp]: - "new_tv n s \ new_tv n (t::typ) \ new_tv n ($s t)" - by (induct t) (auto simp add: new_tv_subst) - -lemma new_tv_subst_tel [simp]: - "new_tv n s \ new_tv n (ts::typ list) \ new_tv n ($s ts)" - by (induct ts) (fastsimp simp add: new_tv_subst)+ - -lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)" - -- {* auxilliary lemma *} - by (simp add: new_tv_list) - -lemma new_tv_subst_comp_1 [simp]: - "new_tv n (s::subst) \ new_tv n r \ new_tv n ($r o s)" - -- {* composition of substitutions preserves @{text new_tv} proposition *} - by (simp add: new_tv_subst) - -lemma new_tv_subst_comp_2 [simp]: - "new_tv n (s::subst) \ new_tv n r \ new_tv n (\v. $r (s v))" - by (simp add: new_tv_subst) - -lemma new_tv_not_free_tv [simp]: "new_tv n ts \ n \ free_tv ts" - -- {* new type variables do not occur freely in a type structure *} - by (auto simp add: new_tv_def) - -lemma ftv_mem_sub_ftv_list [simp]: - "(t::typ) \ set ts \ free_tv t \ free_tv ts" - by (induct ts) auto - -text {* - If two substitutions yield the same result if applied to a type - structure the substitutions coincide on the free type variables - occurring in the type structure. -*} - -lemma eq_subst_te_eq_free: - "$s1 (t::typ) = $s2 t \ n \ free_tv t \ s1 n = s2 n" - by (induct t) auto - -lemma eq_free_eq_subst_te: - "(\n. n \ free_tv t --> s1 n = s2 n) \ $s1 (t::typ) = $s2 t" - by (induct t) auto - -lemma eq_subst_tel_eq_free: - "$s1 (ts::typ list) = $s2 ts \ n \ free_tv ts \ s1 n = s2 n" - by (induct ts) (auto intro: eq_subst_te_eq_free) - -lemma eq_free_eq_subst_tel: - "(\n. n \ free_tv ts --> s1 n = s2 n) \ $s1 (ts::typ list) = $s2 ts" - by (induct ts) (auto intro: eq_free_eq_subst_te) - -text {* - \medskip Some useful lemmas. -*} - -lemma codD: "v \ cod s \ v \ free_tv s" - by (simp add: free_tv_subst) - -lemma not_free_impl_id: "x \ free_tv s \ s x = TVar x" - by (simp add: free_tv_subst dom_def) - -lemma free_tv_le_new_tv: "new_tv n t \ m \ free_tv t \ m < n" - by (unfold new_tv_def) fast - -lemma free_tv_subst_var: "free_tv (s (v::nat)) \ insert v (cod s)" - by (cases "v \ dom s") (auto simp add: cod_def dom_def) - -lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \ cod s \ free_tv t" - by (induct t) (auto simp add: free_tv_subst_var) - -lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \ cod s \ free_tv ts" - apply (induct ts) - apply simp - apply (cut_tac free_tv_app_subst_te) - apply fastsimp - done - -lemma free_tv_comp_subst: - "free_tv (\u::nat. $s1 (s2 u) :: typ) \ free_tv s1 \ free_tv s2" - apply (unfold free_tv_subst dom_def) - apply (auto dest!: free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD] - simp add: cod_def dom_def simp del: bex_simps) - done - - -subsection {* Most general unifiers *} - -consts - mgu :: "typ \ typ \ subst maybe" -axioms - mgu_eq [simp]: "mgu t1 t2 = Ok u \ $u t1 = $u t2" - mgu_mg [simp]: "mgu t1 t2 = Ok u \ $s t1 = $s t2 \ \r. s = $r o u" - mgu_Ok: "$s t1 = $s t2 \ \u. mgu t1 t2 = Ok u" - mgu_free [simp]: "mgu t1 t2 = Ok u \ free_tv u \ free_tv t1 \ free_tv t2" - -lemma mgu_new: "mgu t1 t2 = Ok u \ new_tv n t1 \ new_tv n t2 \ new_tv n u" - -- {* @{text mgu} does not introduce new type variables *} - by (unfold new_tv_def) (blast dest: mgu_free) - - -section {* Mini-ML with type inference rules *} - -datatype - expr = Var nat | Abs expr | App expr expr - - -text {* Type inference rules. *} - -inductive - has_type :: "typ list \ expr \ typ \ bool" ("((_) |-/ (_) :: (_))" [60, 0, 60] 60) - where - Var: "n < length a \ a |- Var n :: a ! n" - | Abs: "t1#a |- e :: t2 \ a |- Abs e :: t1 -> t2" - | App: "a |- e1 :: t2 -> t1 \ a |- e2 :: t2 - \ a |- App e1 e2 :: t1" - - -text {* Type assigment is closed wrt.\ substitution. *} - -lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t" -proof (induct set: has_type) - case (Var n a) - then have "n < length (map ($ s) a)" by simp - then have "map ($ s) a |- Var n :: map ($ s) a ! n" - by (rule has_type.Var) - also have "map ($ s) a ! n = $ s (a ! n)" - by (rule nth_map) (rule Var) - also have "map ($ s) a = $ s a" - by (simp only: app_subst_list) - finally show ?case . -next - case (Abs t1 a e t2) - then have "$ s t1 # map ($ s) a |- e :: $ s t2" - by (simp add: app_subst_list) - then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2" - by (rule has_type.Abs) - then show ?case - by (simp add: app_subst_list) -next - case App - then show ?case by (simp add: has_type.App) -qed - - -section {* Correctness and completeness of the type inference algorithm W *} - -consts - "\" :: "expr \ typ list \ nat \ (subst \ typ \ nat) maybe" -primrec - "\ (Var i) a n = - (if i < length a then Ok (id_subst, a ! i, n) else Fail)" - "\ (Abs e) a n = - ((s, t, m) := \ e (TVar n # a) (Suc n); - Ok (s, (s n) -> t, m))" - "\ (App e1 e2) a n = - ((s1, t1, m1) := \ e1 a n; - (s2, t2, m2) := \ e2 ($s1 a) m1; - u := mgu ($ s2 t1) (t2 -> TVar m2); - Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))" - -theorem W_correct: "Ok (s, t, m) = \ e a n ==> $s a |- e :: t" -proof (induct e arbitrary: a s t m n) - case (Var i) - from `Ok (s, t, m) = \ (Var i) a n` - show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits) -next - case (Abs e) - from `Ok (s, t, m) = \ (Abs e) a n` - obtain t' where "t = s n -> t'" - and "Ok (s, t', m) = \ e (TVar n # a) (Suc n)" - by (auto split: bind_splits) - with Abs.hyps show "$s a |- Abs e :: t" - by (force intro: has_type.Abs) -next - case (App e1 e2) - from `Ok (s, t, m) = \ (App e1 e2) a n` - obtain s1 t1 n1 s2 t2 n2 u where - s: "s = $u o $s2 o s1" - and t: "t = u n2" - and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u" - and W1_ok: "Ok (s1, t1, n1) = \ e1 a n" - and W2_ok: "Ok (s2, t2, n2) = \ e2 ($s1 a) n1" - by (auto split: bind_splits simp: that) - show "$s a |- App e1 e2 :: t" - proof (rule has_type.App) - from s have s': "$u ($s2 ($s1 a)) = $s a" - by (simp add: subst_comp_tel o_def) - show "$s a |- e1 :: $u t2 -> t" - proof - - from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps(1)) - then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)" - by (intro has_type_subst_closed) - with s' t mgu_ok show ?thesis by simp - qed - show "$s a |- e2 :: $u t2" - proof - - from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps(2)) - then have "$u ($s2 ($s1 a)) |- e2 :: $u t2" - by (rule has_type_subst_closed) - with s' show ?thesis by simp - qed - qed -qed - - -inductive_cases has_type_casesE: - "s |- Var n :: t" - "s |- Abs e :: t" - "s |- App e1 e2 ::t" - - -lemmas [simp] = Suc_le_lessD - and [simp del] = less_imp_le ex_simps all_simps - -lemma W_var_ge [simp]: "!!a n s t m. \ e a n = Ok (s, t, m) \ n \ m" - -- {* the resulting type variable is always greater or equal than the given one *} - apply (atomize (full)) - apply (induct e) - txt {* case @{text "Var n"} *} - apply clarsimp - txt {* case @{text "Abs e"} *} - apply (simp split add: split_bind) - apply (fast dest: Suc_leD) - txt {* case @{text "App e1 e2"} *} - apply (simp (no_asm) split add: split_bind) - apply (intro strip) - apply (rename_tac s t na sa ta nb sb) - apply (erule_tac x = a in allE) - apply (erule_tac x = n in allE) - apply (erule_tac x = "$s a" in allE) - apply (erule_tac x = s in allE) - apply (erule_tac x = t in allE) - apply (erule_tac x = na in allE) - apply (erule_tac x = na in allE) - apply (simp add: eq_sym_conv) - done - -lemma W_var_geD: "Ok (s, t, m) = \ e a n \ n \ m" - by (simp add: eq_sym_conv) - -lemma new_tv_W: "!!n a s t m. - new_tv n a \ \ e a n = Ok (s, t, m) \ new_tv m s & new_tv m t" - -- {* resulting type variable is new *} - apply (atomize (full)) - apply (induct e) - txt {* case @{text "Var n"} *} - apply clarsimp - apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst) - txt {* case @{text "Abs e"} *} - apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind) - apply (intro strip) - apply (erule_tac x = "Suc n" in allE) - apply (erule_tac x = "TVar n # a" in allE) - apply (fastsimp simp add: new_tv_subst new_tv_Suc_list) - txt {* case @{text "App e1 e2"} *} - apply (simp (no_asm) split add: split_bind) - apply (intro strip) - apply (rename_tac s t na sa ta nb sb) - apply (erule_tac x = n in allE) - apply (erule_tac x = a in allE) - apply (erule_tac x = s in allE) - apply (erule_tac x = t in allE) - apply (erule_tac x = na in allE) - apply (erule_tac x = na in allE) - apply (simp add: eq_sym_conv) - apply (erule_tac x = "$s a" in allE) - apply (erule_tac x = sa in allE) - apply (erule_tac x = ta in allE) - apply (erule_tac x = nb in allE) - apply (simp add: o_def rotate_Ok) - apply (rule conjI) - apply (rule new_tv_subst_comp_2) - apply (rule new_tv_subst_comp_2) - apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le]) - apply (rule_tac n = na in new_tv_subst_le) - apply (simp add: rotate_Ok) - apply (simp (no_asm_simp)) - apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel - lessI [THEN less_imp_le, THEN new_tv_subst_le]) - apply (erule sym [THEN mgu_new]) - apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel - lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le] - new_tv_le) - apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"] - addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"] - addss @{simpset}) 1 *}) - apply (rule lessI [THEN new_tv_subst_var]) - apply (erule sym [THEN mgu_new]) - apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te - dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel - lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le) - apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"] - addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"] - addss @{simpset}) 1 *}) - done - -lemma free_tv_W: "!!n a s t m v. \ e a n = Ok (s, t, m) \ - (v \ free_tv s \ v \ free_tv t) \ v < n \ v \ free_tv a" - apply (atomize (full)) - apply (induct e) - txt {* case @{text "Var n"} *} - apply clarsimp - apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *}) - txt {* case @{text "Abs e"} *} - apply (simp add: free_tv_subst split add: split_bind) - apply (intro strip) - apply (rename_tac s t n1 v) - apply (erule_tac x = "Suc n" in allE) - apply (erule_tac x = "TVar n # a" in allE) - apply (erule_tac x = s in allE) - apply (erule_tac x = t in allE) - apply (erule_tac x = n1 in allE) - apply (erule_tac x = v in allE) - apply (force elim!: allE intro: cod_app_subst) - txt {* case @{text "App e1 e2"} *} - apply (simp (no_asm) split add: split_bind) - apply (intro strip) - apply (rename_tac s t n1 s1 t1 n2 s3 v) - apply (erule_tac x = n in allE) - apply (erule_tac x = a in allE) - apply (erule_tac x = s in allE) - apply (erule_tac x = t in allE) - apply (erule_tac x = n1 in allE) - apply (erule_tac x = n1 in allE) - apply (erule_tac x = v in allE) - txt {* second case *} - apply (erule_tac x = "$ s a" in allE) - apply (erule_tac x = s1 in allE) - apply (erule_tac x = t1 in allE) - apply (erule_tac x = n2 in allE) - apply (erule_tac x = v in allE) - apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])") - apply (simp add: rotate_Ok o_def) - apply (drule W_var_geD) - apply (drule W_var_geD) - apply (frule less_le_trans, assumption) - apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD - free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE) - apply simp - apply (drule sym [THEN W_var_geD]) - apply (drule sym [THEN W_var_geD]) - apply (frule less_le_trans, assumption) - apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD", - thm "free_tv_subst_var" RS subsetD, - thm "free_tv_app_subst_te" RS subsetD, - thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD] - addSEs [UnE] addss (@{simpset} setSolver unsafe_solver)) 1 *}) - -- {* builtin arithmetic in simpset messes things up *} - done - -text {* - \medskip Completeness of @{text \} wrt.\ @{text has_type}. -*} - -lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \ new_tv n a \ - (\s t. (\m. \ e a n = Ok (s, t, m)) \ (\r. $s' a = $r ($s a) \ t' = $r t))" - apply (atomize (full)) - apply (induct e) - txt {* case @{text "Var n"} *} - apply (intro strip) - apply (simp (no_asm) cong add: conj_cong) - apply (erule has_type_casesE) - apply (simp add: eq_sym_conv app_subst_list) - apply (rule_tac x = s' in exI) - apply simp - txt {* case @{text "Abs e"} *} - apply (intro strip) - apply (erule has_type_casesE) - apply (erule_tac x = "\x. if x = n then t1 else (s' x)" in allE) - apply (erule_tac x = "TVar n # a" in allE) - apply (erule_tac x = t2 in allE) - apply (erule_tac x = "Suc n" in allE) - apply (fastsimp cong add: conj_cong split add: split_bind) - txt {* case @{text "App e1 e2"} *} - apply (intro strip) - apply (erule has_type_casesE) - apply (erule_tac x = s' in allE) - apply (erule_tac x = a in allE) - apply (erule_tac x = "t2 -> t'" in allE) - apply (erule_tac x = n in allE) - apply (tactic "safe_tac HOL_cs") - apply (erule_tac x = r in allE) - apply (erule_tac x = "$s a" in allE) - apply (erule_tac x = t2 in allE) - apply (erule_tac x = m in allE) - apply simp - apply (tactic "safe_tac HOL_cs") - apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD", - thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *}) - apply (subgoal_tac - "$(\x. if x = ma then t' else (if x \ free_tv t - free_tv sa then r x - else ra x)) ($ sa t) = - $(\x. if x = ma then t' else (if x \ free_tv t - free_tv sa then r x - else ra x)) (ta -> (TVar ma))") - apply (rule_tac [2] t = "$(\x. if x = ma then t' - else (if x \ (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and - s = "($ ra ta) -> t'" in ssubst) - prefer 2 - apply (simp add: subst_comp_te) - apply (rule eq_free_eq_subst_te) - apply (intro strip) - apply (subgoal_tac "na \ ma") - prefer 2 - apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le) - apply (case_tac "na \ free_tv sa") - txt {* @{text "na \ free_tv sa"} *} - prefer 2 - apply (frule not_free_impl_id) - apply simp - txt {* @{text "na \ free_tv sa"} *} - apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans]) - apply (drule_tac eq_subst_tel_eq_free) - apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W) - apply simp - apply (case_tac "na \ dom sa") - prefer 2 - txt {* @{text "na \ dom sa"} *} - apply (simp add: dom_def) - txt {* @{text "na \ dom sa"} *} - apply (rule eq_free_eq_subst_te) - apply (intro strip) - apply (subgoal_tac "nb \ ma") - prefer 2 - apply (frule new_tv_W, assumption) - apply (erule conjE) - apply (drule new_tv_subst_tel) - apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD]) - apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst) - apply (fastsimp simp add: cod_def free_tv_subst) - prefer 2 - apply (simp (no_asm)) - apply (rule eq_free_eq_subst_te) - apply (intro strip) - apply (subgoal_tac "na \ ma") - prefer 2 - apply (frule new_tv_W, assumption) - apply (erule conjE) - apply (drule sym [THEN W_var_geD]) - apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv) - apply (case_tac "na \ free_tv t - free_tv sa") - prefer 2 - txt {* case @{text "na \ free_tv t - free_tv sa"} *} - apply simp - defer - txt {* case @{text "na \ free_tv t - free_tv sa"} *} - apply simp - apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans]) - apply (drule eq_subst_tel_eq_free) - apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W) - apply (simp add: free_tv_subst dom_def) - prefer 2 apply fast - apply (simp (no_asm_simp) split add: split_bind) - apply (tactic "safe_tac HOL_cs") - apply (drule mgu_Ok) - apply fastsimp - apply (drule mgu_mg, assumption) - apply (erule exE) - apply (rule_tac x = rb in exI) - apply (rule conjI) - prefer 2 - apply (drule_tac x = ma in fun_cong) - apply (simp add: eq_sym_conv) - apply (simp (no_asm) add: o_def subst_comp_tel [symmetric]) - apply (rule subst_comp_tel [symmetric, THEN [2] trans]) - apply (simp add: o_def eq_sym_conv) - apply (rule eq_free_eq_subst_tel) - apply (tactic "safe_tac HOL_cs") - apply (subgoal_tac "ma \ na") - prefer 2 - apply (frule new_tv_W, assumption) - apply (erule conjE) - apply (drule new_tv_subst_tel) - apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD]) - apply (frule_tac n = m in new_tv_W, assumption) - apply (erule conjE) - apply (drule free_tv_app_subst_tel [THEN subsetD]) - apply (auto dest: W_var_geD [OF sym] new_tv_list_le - codD new_tv_not_free_tv) - apply (case_tac "na \ free_tv t - free_tv sa") - prefer 2 - txt {* case @{text "na \ free_tv t - free_tv sa"} *} - apply simp - defer - txt {* case @{text "na \ free_tv t - free_tv sa"} *} - apply simp - apply (drule free_tv_app_subst_tel [THEN subsetD]) - apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans] - eq_subst_tel_eq_free simp add: free_tv_subst dom_def) - done - -lemma W_complete: "[] |- e :: t' ==> - \s t. (\m. \ e [] n = Ok (s, t, m)) \ (\r. t' = $r t)" - apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux) - apply simp_all - done - - -section {* Equivalence of W and I *} - -text {* - Recursive definition of type inference algorithm @{text \} for - Mini-ML. -*} - -consts - "\" :: "expr \ typ list \ nat \ subst \ (subst \ typ \ nat) maybe" -primrec - "\ (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)" - "\ (Abs e) a n s = ((s, t, m) := \ e (TVar n # a) (Suc n) s; - Ok (s, TVar n -> t, m))" - "\ (App e1 e2) a n s = - ((s1, t1, m1) := \ e1 a n s; - (s2, t2, m2) := \ e2 a m1 s1; - u := mgu ($s2 t1) ($s2 t2 -> TVar m2); - Ok($u o s2, TVar m2, Suc m2))" - -text {* \medskip Correctness. *} - -lemma I_correct_wrt_W: "!!a m s s' t n. - new_tv m a \ new_tv m s \ \ e a m s = Ok (s', t, n) \ - \r. \ e ($s a) m = Ok (r, $s' t, n) \ s' = ($r o s)" - apply (atomize (full)) - apply (induct e) - txt {* case @{text "Var n"} *} - apply (simp add: app_subst_list split: split_if) - txt {* case @{text "Abs e"} *} - apply (tactic {* asm_full_simp_tac - (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *}) - apply (intro strip) - apply (rule conjI) - apply (intro strip) - apply (erule allE)+ - apply (erule impE) - prefer 2 apply (fastsimp simp add: new_tv_subst) - apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp, - thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *}) - apply (intro strip) - apply (erule allE)+ - apply (erule impE) - prefer 2 apply (fastsimp simp add: new_tv_subst) - apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp, - thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *}) - txt {* case @{text "App e1 e2"} *} - apply (tactic {* simp_tac (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *}) - apply (intro strip) - apply (rename_tac s1' t1 n1 s2' t2 n2 sa) - apply (rule conjI) - apply fastsimp - apply (intro strip) - apply (rename_tac s1 t1' n1') - apply (erule_tac x = a in allE) - apply (erule_tac x = m in allE) - apply (erule_tac x = s in allE) - apply (erule_tac x = s1' in allE) - apply (erule_tac x = t1 in allE) - apply (erule_tac x = n1 in allE) - apply (erule_tac x = a in allE) - apply (erule_tac x = n1 in allE) - apply (erule_tac x = s1' in allE) - apply (erule_tac x = s2' in allE) - apply (erule_tac x = t2 in allE) - apply (erule_tac x = n2 in allE) - apply (rule conjI) - apply (intro strip) - apply (rule notI) - apply simp - apply (erule impE) - apply (frule new_tv_subst_tel, assumption) - apply (drule_tac a = "$s a" in new_tv_W, assumption) - apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) - apply (fastsimp simp add: subst_comp_tel) - apply (intro strip) - apply (rename_tac s2 t2' n2') - apply (rule conjI) - apply (intro strip) - apply (rule notI) - apply simp - apply (erule impE) - apply (frule new_tv_subst_tel, assumption) - apply (drule_tac a = "$s a" in new_tv_W, assumption) - apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) - apply (fastsimp simp add: subst_comp_tel subst_comp_te) - apply (intro strip) - apply (erule (1) notE impE) - apply (erule (1) notE impE) - apply (erule exE) - apply (erule conjE) - apply (erule impE) - apply (frule new_tv_subst_tel, assumption) - apply (drule_tac a = "$s a" in new_tv_W, assumption) - apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) - apply (erule (1) notE impE) - apply (erule exE conjE)+ - apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+ - apply (subgoal_tac "new_tv n2 s \ new_tv n2 r \ new_tv n2 ra") - apply (simp add: new_tv_subst) - apply (frule new_tv_subst_tel, assumption) - apply (drule_tac a = "$s a" in new_tv_W, assumption) - apply (tactic "safe_tac HOL_cs") - apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) - apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le) - apply (drule_tac e = e1 in sym [THEN W_var_geD]) - apply (drule new_tv_subst_tel, assumption) - apply (drule_tac ts = "$s a" in new_tv_list_le, assumption) - apply (drule new_tv_subst_tel, assumption) - apply (bestsimp dest: new_tv_W simp add: subst_comp_tel) - done - -lemma I_complete_wrt_W: "!!a m s. - new_tv m a \ new_tv m s \ \ e a m s = Fail \ \ e ($s a) m = Fail" - apply (atomize (full)) - apply (induct e) - apply (simp add: app_subst_list) - apply (simp (no_asm)) - apply (intro strip) - apply (subgoal_tac "TVar m # $s a = $s (TVar m # a)") - apply (tactic {* asm_simp_tac (HOL_ss addsimps - [thm "new_tv_Suc_list", @{thm lessI} RS @{thm less_imp_le} RS thm "new_tv_subst_le"]) 1 *}) - apply (erule conjE) - apply (drule new_tv_not_free_tv [THEN not_free_impl_id]) - apply (simp (no_asm_simp)) - apply (simp (no_asm_simp)) - apply (intro strip) - apply (erule exE)+ - apply (erule conjE)+ - apply (drule I_correct_wrt_W [COMP swap_prems_rl]) - apply fast - apply (erule exE) - apply (erule conjE) - apply hypsubst - apply (simp (no_asm_simp)) - apply (erule disjE) - apply (rule disjI1) - apply (simp (no_asm_use) add: o_def subst_comp_tel) - apply (erule allE, erule allE, erule allE, erule impE, erule_tac [2] impE, - erule_tac [2] asm_rl, erule_tac [2] asm_rl) - apply (rule conjI) - apply (fast intro: W_var_ge [THEN new_tv_list_le]) - apply (rule new_tv_subst_comp_2) - apply (fast intro: W_var_ge [THEN new_tv_subst_le]) - apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1]) - apply (rule disjI2) - apply (erule exE)+ - apply (erule conjE) - apply (drule I_correct_wrt_W [COMP swap_prems_rl]) - apply (rule conjI) - apply (fast intro: W_var_ge [THEN new_tv_list_le]) - apply (rule new_tv_subst_comp_1) - apply (fast intro: W_var_ge [THEN new_tv_subst_le]) - apply (fast intro!: new_tv_subst_tel intro: new_tv_W [THEN conjunct1]) - apply (erule exE) - apply (erule conjE) - apply hypsubst - apply (simp add: o_def subst_comp_te [symmetric] subst_comp_tel [symmetric]) - done - -end diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/W0/document/root.tex --- a/src/HOL/W0/document/root.tex Tue Feb 23 14:11:46 2010 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,25 +0,0 @@ - -\documentclass[11pt,a4paper]{article} -\usepackage{isabelle,isabellesym} -\usepackage{pdfsetup} - -\urlstyle{rm} -\isabellestyle{it} - -\newcommand{\isasymbind}{\textsf{bind}} - -\begin{document} - -\title{Type inference for let-free MiniML} -\author{Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel} -\maketitle - -\tableofcontents - -\parindent 0pt\parskip 0.5ex -\input{session} - -%\bibliographystyle{abbrv} -%\bibliography{root} - -\end{document} diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/ex/PER.thy --- a/src/HOL/ex/PER.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/ex/PER.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/ex/PER.thy - ID: $Id$ Author: Oscar Slotosch and Markus Wenzel, TU Muenchen *) @@ -30,12 +29,10 @@ but not necessarily reflexive. *} -consts - eqv :: "'a => 'a => bool" (infixl "\" 50) - -axclass partial_equiv < type - partial_equiv_sym [elim?]: "x \ y ==> y \ x" - partial_equiv_trans [trans]: "x \ y ==> y \ z ==> x \ z" +class partial_equiv = + fixes eqv :: "'a => 'a => bool" (infixl "\" 50) + assumes partial_equiv_sym [elim?]: "x \ y ==> y \ x" + assumes partial_equiv_trans [trans]: "x \ y ==> y \ z ==> x \ z" text {* \medskip The domain of a partial equivalence relation is the set of @@ -70,7 +67,10 @@ structural one corresponding to the congruence property. *} -defs (overloaded) +instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv +begin + +definition eqv_fun_def: "f \ g == \x \ domain. \y \ domain. x \ y --> f x \ g y" lemma partial_equiv_funI [intro?]: @@ -86,8 +86,7 @@ spaces (in \emph{both} argument positions). *} -instance "fun" :: (partial_equiv, partial_equiv) partial_equiv -proof +instance proof fix f g h :: "'a::partial_equiv => 'b::partial_equiv" assume fg: "f \ g" show "g \ f" @@ -110,6 +109,8 @@ qed qed +end + subsection {* Total equivalence *} @@ -120,8 +121,8 @@ symmetric. *} -axclass equiv < partial_equiv - eqv_refl [intro]: "x \ x" +class equiv = + assumes eqv_refl [intro]: "x \ x" text {* On total equivalences all elements are reflexive, and congruence @@ -150,7 +151,7 @@ \emph{equivalence classes} over elements of the base type @{typ 'a}. *} -typedef 'a quot = "{{x. a \ x}| a::'a. True}" +typedef 'a quot = "{{x. a \ x}| a::'a::partial_equiv. True}" by blast lemma quotI [intro]: "{x. a \ x} \ quot" diff -r cbdf785a1eb3 -r f8bae261e7a9 src/HOL/ex/Refute_Examples.thy --- a/src/HOL/ex/Refute_Examples.thy Tue Feb 23 14:11:46 2010 +0100 +++ b/src/HOL/ex/Refute_Examples.thy Tue Feb 23 14:13:14 2010 +0100 @@ -1417,29 +1417,20 @@ (*****************************************************************************) -subsubsection {* Axiomatic type classes and overloading *} +subsubsection {* Type classes and overloading *} text {* A type class without axioms: *} -axclass classA +class classA lemma "P (x::'a::classA)" refute oops -text {* The axiom of this type class does not contain any type variables: *} - -axclass classB - classB_ax: "P | ~ P" - -lemma "P (x::'a::classB)" - refute -oops - text {* An axiom with a type variable (denoting types which have at least two elements): *} -axclass classC < type - classC_ax: "\x y. x \ y" +class classC = + assumes classC_ax: "\x y. x \ y" lemma "P (x::'a::classC)" refute @@ -1451,11 +1442,9 @@ text {* A type class for which a constant is defined: *} -consts - classD_const :: "'a \ 'a" - -axclass classD < type - classD_ax: "classD_const (classD_const x) = classD_const x" +class classD = + fixes classD_const :: "'a \ 'a" + assumes classD_ax: "classD_const (classD_const x) = classD_const x" lemma "P (x::'a::classD)" refute @@ -1463,16 +1452,12 @@ text {* A type class with multiple superclasses: *} -axclass classE < classC, classD +class classE = classC + classD lemma "P (x::'a::classE)" refute oops -lemma "P (x::'a::{classB, classE})" - refute -oops - text {* OFCLASS: *} lemma "OFCLASS('a::type, type_class)" @@ -1485,12 +1470,6 @@ apply intro_classes done -lemma "OFCLASS('a, classB_class)" - refute -- {* no countermodel exists *} - apply intro_classes - apply simp -done - lemma "OFCLASS('a::type, classC_class)" refute oops diff -r cbdf785a1eb3 -r f8bae261e7a9 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Tue Feb 23 14:11:46 2010 +0100 +++ b/src/Pure/Isar/class_target.ML Tue Feb 23 14:13:14 2010 +0100 @@ -56,11 +56,6 @@ (*tactics*) val intro_classes_tac: thm list -> tactic val default_intro_tac: Proof.context -> thm list -> tactic - - (*old axclass layer*) - val axclass_cmd: binding * xstring list - -> (Attrib.binding * string list) list - -> theory -> class * theory end; structure Class_Target : CLASS_TARGET = @@ -629,24 +624,5 @@ Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac)) "apply some intro/elim rule")); - -(** old axclass command **) - -fun axclass_cmd (class, raw_superclasses) raw_specs thy = - let - val _ = Output.legacy_feature "command \"axclass\" deprecated; use \"class\" instead."; - val ctxt = ProofContext.init thy; - val superclasses = map (Sign.read_class thy) raw_superclasses; - val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) - raw_specs; - val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) - raw_specs) - |> snd - |> (map o map) fst; - in - AxClass.define_class (class, superclasses) [] - (name_atts ~~ axiomss) thy - end; - end; diff -r cbdf785a1eb3 -r f8bae261e7a9 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Feb 23 14:11:46 2010 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Feb 23 14:13:14 2010 +0100 @@ -99,13 +99,6 @@ OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl (P.sort >> (Toplevel.theory o Sign.add_defsort)); -val _ = - OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl - (P.binding -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- - P.!!! (P.list1 P.xname)) [] - -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single)) - >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); - (* types *)