# 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 \<Rightarrow> _) \<Longrightarrow> 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 \<Rightarrow> memberid"
+class has_memberid =
+  fixes memberid :: "'a \<Rightarrow> memberid"
 
-instance memberdecl::has_memberid ..
+instantiation memberdecl :: has_memberid
+begin
 
-defs (overloaded)
+definition
 memberdecl_memberid_def:
   "memberid m \<equiv> (case m of
                     fdecl (vn,f)  \<Rightarrow> fid vn
                   | mdecl (sig,m) \<Rightarrow> 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 \<equiv> 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 \<Rightarrow> acc_modi"
+class has_accmodi =
+  fixes accmodi:: "'a \<Rightarrow> acc_modi"
+
+instantiation acc_modi :: has_accmodi
+begin
 
-instance acc_modi::has_accmodi ..
+definition
+  acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
 
-defs (overloaded)
-acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> 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) \<equiv> access d"
+definition
+  decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> 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 \<equiv> (accmodi (snd p))"
+definition
+  pair_acc_modi_def: "accmodi p \<equiv> (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 \<equiv> (case m of
+definition
+  memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
                                           fdecl f \<Rightarrow> accmodi f
                                         | mdecl m \<Rightarrow> 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 \<Rightarrow> qtname"
+class has_declclass =
+  fixes declclass:: "'a \<Rightarrow> qtname"
+
+instantiation qtname_ext_type :: (type) has_declclass
+begin
 
-instance qtname_ext_type::("type") has_declclass ..
+definition
+  "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
+
+instance ..
 
-defs (overloaded)
-qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
+end
+
+lemma qtname_declclass_def:
+  "declclass q \<equiv> (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 \<equiv> declclass (fst p)"
+definition
+  pair_declclass_def: "declclass p \<equiv> 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 \<Rightarrow> bool"
 
-axclass has_static < "type"
-consts is_static :: "'a::has_static \<Rightarrow> 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)) \<equiv> static m"
+end
+
+axiomatization where
+  static_field_type_is_static_def: "is_static (m::('a member_scheme)) \<equiv> 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 \<equiv> is_static (snd p)"
+definition
+  pair_is_static_def: "is_static p \<equiv> 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 \<equiv> (case m of
                     fdecl f \<Rightarrow> is_static f
                   | mdecl m \<Rightarrow> 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 \<Rightarrow> ty"
+class has_resTy =
+  fixes resTy:: "'a \<Rightarrow> 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)) \<equiv> resT m"
+instance ..
+
+end
+
+axiomatization where
+  mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \<equiv> 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 \<equiv> resTy (snd p)"
+definition
+  pair_resTy_def: "resTy p \<equiv> 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 \<Rightarrow> pname"
+class has_pname =
+  fixes pname :: "'a \<Rightarrow> pname"
 
-instance pname::has_pname ..
+instantiation pname :: has_pname
+begin
 
-defs (overloaded)
-pname_pname_def: "pname (p::pname) \<equiv> p"
+definition
+  pname_pname_def: "pname (p::pname) \<equiv> p"
 
-axclass has_tname < "type"
-consts tname::"'a::has_tname \<Rightarrow> tname"
+instance ..
+
+end
 
-instance tname::has_tname ..
+class has_tname =
+  fixes tname :: "'a \<Rightarrow> tname"
 
-defs (overloaded)
-tname_tname_def: "tname (t::tname) \<equiv> t"
+instantiation tname :: has_tname
+begin
 
-axclass has_qtname < type
-consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
+definition
+  tname_tname_def: "tname (t::tname) \<equiv> t"
+
+instance ..
 
-instance qtname_ext_type :: (type) has_qtname ..
+end
 
-defs (overloaded)
-qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
+definition
+  qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> 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 \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
+class inj_term =
+  fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 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: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+definition
+  stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+
+instance ..
+
+end
 
 lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
 by (simp add: stmt_inj_term_def)
@@ -319,10 +324,15 @@
 lemma  stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   by (simp add: stmt_inj_term_simp)
 
-instance expr::inj_term ..
+instantiation expr :: inj_term
+begin
 
-defs (overloaded)
-expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+definition
+  expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+
+instance ..
+
+end
 
 lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
 by (simp add: expr_inj_term_def)
@@ -330,10 +340,15 @@
 lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   by (simp add: expr_inj_term_simp)
 
-instance var::inj_term ..
+instantiation var :: inj_term
+begin
 
-defs (overloaded)
-var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+definition
+  var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+
+instance ..
+
+end
 
 lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
 by (simp add: var_inj_term_def)
@@ -341,10 +356,32 @@
 lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
   by (simp add: var_inj_term_simp)
 
-instance "list":: (type) inj_term ..
+class expr_of =
+  fixes expr_of :: "'a \<Rightarrow> expr"
+
+instantiation expr :: expr_of
+begin
+
+definition
+  "expr_of = (\<lambda>(e::expr). e)"
+
+instance ..
+
+end 
 
-defs (overloaded)
-expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+instantiation list :: (expr_of) inj_term
+begin
+
+definition
+  "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
+
+instance ..
+
+end
+
+lemma expr_list_inj_term_def:
+  "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+  by (simp add: inj_term_list_def expr_of_expr_def)
 
 lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = 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 \<noteq> 0} z \<noteq> 0 \<rightarrow> 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 \<Rightarrow> '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 \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> 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 \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
-by (auto simp:Valid_def)
-
-lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
-by (auto simp:Valid_def)
-
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
-by (auto simp:Valid_def)
-
-lemma CondRule:
- "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
-  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> 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 ==>
-       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
-
-lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> 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 \<Rightarrow> '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 = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
-"iter (Suc n) b S =
-  (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
-
-consts Sem :: "'a com => 'a sem"
-primrec
-"Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
-"Sem Abort s s' = (s' = None)"
-"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
-"Sem(IF b THEN c1 ELSE c2 FI) s s' =
- (case s of None \<Rightarrow> s' = None
-  | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
-"Sem(While b x c) s s' =
- (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
-
-constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
-  "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> 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 \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
-by (auto simp:Valid_def)
-
-lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
-by (auto simp:Valid_def)
-
-lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
-by (auto simp:Valid_def)
-
-lemma CondRule:
- "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
-  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
-by (fastsimp simp:Valid_def image_def)
-
-lemma iter_aux:
- "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
-  (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
-apply(unfold image_def)
-apply(induct n)
- apply clarsimp
-apply(simp (no_asm_use))
-apply blast
-done
-
-lemma WhileRule:
- "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> 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 \<subseteq> {s. False} \<Longrightarrow> 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 \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
-  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
-translations
-  "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
-  "a[i] := v" => "(i < CONST length a) \<rightarrow> (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 \<rightarrow> 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 \<Rightarrow> '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 \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> 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 \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
+by (auto simp:Valid_def)
+
+lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
+by (auto simp:Valid_def)
+
+lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
+by (auto simp:Valid_def)
+
+lemma CondRule:
+ "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
+  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> 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 ==>
+       (\<And>s s'. s : I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' : I & s' ~: b)";
+apply(induct n)
+ apply clarsimp
+apply(simp (no_asm_use))
+apply blast
+done
+
+lemma WhileRule:
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> 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 \<Rightarrow> '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 = (\<lambda>s s'. s \<notin> Some ` b \<and> s=s')"
+"iter (Suc n) b S =
+  (\<lambda>s s'. s \<in> Some ` b \<and> (\<exists>s''. S s s'' \<and> iter n b S s'' s'))"
+
+consts Sem :: "'a com => 'a sem"
+primrec
+"Sem(Basic f) s s' = (case s of None \<Rightarrow> s' = None | Some t \<Rightarrow> s' = Some(f t))"
+"Sem Abort s s' = (s' = None)"
+"Sem(c1;c2) s s' = (\<exists>s''. Sem c1 s s'' \<and> Sem c2 s'' s')"
+"Sem(IF b THEN c1 ELSE c2 FI) s s' =
+ (case s of None \<Rightarrow> s' = None
+  | Some t \<Rightarrow> ((t \<in> b \<longrightarrow> Sem c1 s s') \<and> (t \<notin> b \<longrightarrow> Sem c2 s s')))"
+"Sem(While b x c) s s' =
+ (if s = None then s' = None else \<exists>n. iter n b (Sem c) s s')"
+
+constdefs Valid :: "'a bexp \<Rightarrow> 'a com \<Rightarrow> 'a bexp \<Rightarrow> bool"
+  "Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> 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 \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
+by (auto simp:Valid_def)
+
+lemma BasicRule: "p \<subseteq> {s. f s \<in> q} \<Longrightarrow> Valid p (Basic f) q"
+by (auto simp:Valid_def)
+
+lemma SeqRule: "Valid P c1 Q \<Longrightarrow> Valid Q c2 R \<Longrightarrow> Valid P (c1;c2) R"
+by (auto simp:Valid_def)
+
+lemma CondRule:
+ "p \<subseteq> {s. (s \<in> b \<longrightarrow> s \<in> w) \<and> (s \<notin> b \<longrightarrow> s \<in> w')}
+  \<Longrightarrow> Valid w c1 q \<Longrightarrow> Valid w' c2 q \<Longrightarrow> Valid p (Cond b c1 c2) q"
+by (fastsimp simp:Valid_def image_def)
+
+lemma iter_aux:
+ "! s s'. Sem c s s' \<longrightarrow> s \<in> Some ` (I \<inter> b) \<longrightarrow> s' \<in> Some ` I \<Longrightarrow>
+  (\<And>s s'. s \<in> Some ` I \<Longrightarrow> iter n b (Sem c) s s' \<Longrightarrow> s' \<in> Some ` (I \<inter> -b))";
+apply(unfold image_def)
+apply(induct n)
+ apply clarsimp
+apply(simp (no_asm_use))
+apply blast
+done
+
+lemma WhileRule:
+ "p \<subseteq> i \<Longrightarrow> Valid (i \<inter> b) c i \<Longrightarrow> i \<inter> (-b) \<subseteq> q \<Longrightarrow> 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 \<subseteq> {s. False} \<Longrightarrow> 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 \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
+  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
+translations
+  "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
+  "a[i] := v" => "(i < CONST length a) \<rightarrow> (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 \<rightarrow> 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 \<subseteq> partial_order
-  ex_Inf: "\<exists>inf. is_Inf A inf"
+class complete_lattice =
+  assumes ex_Inf: "\<exists>inf. is_Inf A inf"
 
 theorem ex_Sup: "\<exists>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 \<subseteq> partial_order
-  ex_inf: "\<exists>inf. is_inf x y inf"
-  ex_sup: "\<exists>sup. is_sup x y sup"
+class lattice =
+  assumes ex_inf: "\<exists>inf. is_inf x y inf"
+  assumes ex_sup: "\<exists>sup. is_sup x y sup"
 
 text {*
   The @{text \<sqinter>} (meet) and @{text \<squnion>} (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 \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
+class leq =
+  fixes leq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "[=" 50)
+
 notation (xsymbols)
   leq  (infixl "\<sqsubseteq>" 50)
 
-axclass quasi_order < leq
-  leq_refl [intro?]: "x \<sqsubseteq> x"
-  leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
+class quasi_order = leq +
+  assumes leq_refl [intro?]: "x \<sqsubseteq> x"
+  assumes leq_trans [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
 
-axclass partial_order < quasi_order
-  leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
+class partial_order = quasi_order +
+  assumes leq_antisym [trans]: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
 
-axclass linear_order < partial_order
-  leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
+class linear_order = partial_order +
+  assumes leq_linear: "x \<sqsubseteq> y \<or> y \<sqsubseteq> x"
 
 lemma linear_order_cases:
     "((x::'a::linear_order) \<sqsubseteq> y \<Longrightarrow> C) \<Longrightarrow> (y \<sqsubseteq> x \<Longrightarrow> C) \<Longrightarrow> 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' \<sqsubseteq> y' \<equiv> undual y' \<sqsubseteq> undual x'"
 
+instance ..
+
+end
+
 lemma undual_leq [iff?]: "(undual x' \<sqsubseteq> undual y') = (y' \<sqsubseteq> 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 \<sqsubseteq> q \<equiv> fst p \<sqsubseteq> fst q \<and> snd p \<sqsubseteq> snd q"
 
+instance ..
+
+end
+
 lemma leq_prodI [intro?]:
     "fst p \<sqsubseteq> fst q \<Longrightarrow> snd p \<sqsubseteq> snd q \<Longrightarrow> p \<sqsubseteq> 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 \<sqsubseteq> g \<equiv> \<forall>x. f x \<sqsubseteq> g x"
 
+instance ..
+
+end
+
 lemma leq_funI [intro?]: "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> f \<sqsubseteq> 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"                ("(_/ \<in> _)" [50, 51] 50)
   "_liftNotMem" :: "[lift, lift] => lift"                ("(_/ \<notin> _)" [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 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<!-- $Id$ -->
-
-<HTML>
-
-<HEAD>
-  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
-  <TITLE>HOL/W0/README</TITLE>
-</HEAD>
-
-<BODY>
-
-<H1>Type Inference for MiniML (without <tt>let</tt>)</H1>
-
-This theory defines the type inference rules and the type inference algorithm
-<em>W</em> for simply-typed lambda terms due to Milner. It proves the
-soundness and completeness of <em>W</em> w.r.t. to the rules. An optimized
-version <em>I</em> is shown to implement <em>W</em>.
-
-<P>
-
-A report describing the theory is found here:<br>
-<A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/tphol96.html">
-Formal Verification of Algorithm W: The Monomorphic Case</A>.
-
-<P>
-
-<B>NOTE:</B> This theory has been superseded by a more recent development
-which formalizes type inference for a language including <tt>let</tt>. For
-details click <A HREF="../MiniML/index.html">here</A>.
-</BODY>
-</HTML>
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 \<Rightarrow> ('a \<Rightarrow> 'b maybe) \<Rightarrow> 'b maybe"    (infixl "\<bind>" 60) where
-  "m \<bind> f = (case m of Ok r \<Rightarrow> f r | Fail \<Rightarrow> Fail)"
-
-syntax
-  "_bind" :: "patterns \<Rightarrow> 'a maybe \<Rightarrow> 'b \<Rightarrow> 'c"    ("(_ := _;//_)" 0)
-translations
-  "P := E; F" == "E \<bind> (\<lambda>P. F)"
-
-lemma bind_Ok [simp]: "(Ok s) \<bind> f = (f s)"
-  by (simp add: bind_def)
-
-lemma bind_Fail [simp]: "Fail \<bind> f = Fail"
-  by (simp add: bind_def)
-
-lemma split_bind:
-    "P (res \<bind> f) = ((res = Fail \<longrightarrow> P Fail) \<and> (\<forall>s. res = Ok s \<longrightarrow> P (f s)))"
-  by (induct res) simp_all
-
-lemma split_bind_asm:
-  "P (res \<bind> f) = (\<not> (res = Fail \<and> \<not> P Fail \<or> (\<exists>s. res = Ok s \<and> \<not> P (f s))))"
-  by (simp split: split_bind)
-
-lemmas bind_splits = split_bind split_bind_asm
-
-lemma bind_eq_Fail [simp]:
-  "((m \<bind> f) = Fail) = ((m = Fail) \<or> (\<exists>p. m = Ok p \<and> 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 \<subseteq> 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 \<Rightarrow> 'a::type_struct \<Rightarrow> '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 \<equiv> map ($s)"
-
-consts
-  free_tv :: "'a::type_struct \<Rightarrow> 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 \<union> free_tv t2"
-
-primrec (free_tv_list)
-  "free_tv [] = {}"
-  "free_tv (x # xs) = free_tv x \<union> free_tv xs"
-
-definition
-  dom :: "subst \<Rightarrow> nat set" where
-  "dom s = {n. s n \<noteq> TVar n}"
-  -- {* domain of a substitution *}
-
-definition
-  cod :: "subst \<Rightarrow> nat set" where
-  "cod s = (\<Union>m \<in> dom s. free_tv (s m))"
-  -- {* codomain of a substitutions: the introduced variables *}
-
-defs (overloaded)
-  free_tv_subst: "free_tv s \<equiv> dom s \<union> 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 \<Rightarrow> 'a::type_struct \<Rightarrow> bool" where
-  "new_tv n ts = (\<forall>m. m \<in> free_tv ts \<longrightarrow> m < n)"
-
-
-subsubsection {* Identity substitution *}
-
-definition
-  id_subst :: subst where
-  "id_subst = (\<lambda>n. TVar n)"
-
-lemma app_subst_id_te [simp]:
-  "$id_subst = (\<lambda>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 = (\<lambda>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 \<in> free_tv (s n)"
-    and neq: "v \<noteq> n"
-  shows "v \<in> cod s"
-proof -
-  have "s n \<noteq> 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) = $(\<lambda>x. $g (f x)) t"
-  -- {* composition of substitutions *}
-  by (induct t) simp_all
-
-lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\<lambda>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 \<and> 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 \<and> 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 =
-    ((\<forall>m. n \<le> m \<longrightarrow> s m = TVar m) \<and>
-     (\<forall>l. l < n \<longrightarrow> new_tv n (s l)))"
-  apply (unfold new_tv_def)
-  apply (tactic "safe_tac HOL_cs")
-  -- {* @{text \<Longrightarrow>} *}
-    apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset}
-      addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
-   apply (subgoal_tac "m \<in> cod s \<or> 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 = "\<lambda>x. m \<in> 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 = (\<forall>y \<in> set x. new_tv n y)"
-  by (induct x) simp_all
-
-lemma subst_te_new_tv [simp]:
-  "new_tv n (t::typ) \<Longrightarrow> $(\<lambda>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) \<Longrightarrow> $(\<lambda>x. if x = n then t else s x) ts = $s ts"
-  by (induct ts) simp_all
-
-lemma new_tv_le: "n \<le> m \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> 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 \<Longrightarrow> new_tv (Suc n) (t::typ)"
-  by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
-
-lemma new_tv_list_le:
-  assumes "n \<le> m"
-  shows "new_tv n (ts::typ list) \<Longrightarrow> new_tv m ts"
-proof (induct ts)
-  case Nil
-  then show ?case by simp
-next
-  case Cons
-  with `n \<le> m` show ?case by (auto intro: new_tv_le)
-qed
-
-lemma [simp]: "new_tv n ts \<Longrightarrow> 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 \<le> m \<Longrightarrow> new_tv n (s::subst) \<Longrightarrow> 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 \<Longrightarrow> 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 \<Longrightarrow> new_tv m (s::subst) \<Longrightarrow> 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 \<Longrightarrow> new_tv n (t::typ) \<Longrightarrow> new_tv n ($s t)"
-  by (induct t) (auto simp add: new_tv_subst)
-
-lemma new_tv_subst_tel [simp]:
-    "new_tv n s \<Longrightarrow> new_tv n (ts::typ list) \<Longrightarrow> 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) \<Longrightarrow> new_tv n r \<Longrightarrow> 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) \<Longrightarrow> new_tv n r \<Longrightarrow> new_tv n (\<lambda>v. $r (s v))"
-  by (simp add: new_tv_subst)
-
-lemma new_tv_not_free_tv [simp]: "new_tv n ts \<Longrightarrow> n \<notin> 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) \<in> set ts \<Longrightarrow> free_tv t \<subseteq> 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 \<Longrightarrow> n \<in> free_tv t \<Longrightarrow> s1 n = s2 n"
-  by (induct t) auto
-
-lemma eq_free_eq_subst_te:
-    "(\<forall>n. n \<in> free_tv t --> s1 n = s2 n) \<Longrightarrow> $s1 (t::typ) = $s2 t"
-  by (induct t) auto
-
-lemma eq_subst_tel_eq_free:
-    "$s1 (ts::typ list) = $s2 ts \<Longrightarrow> n \<in> free_tv ts \<Longrightarrow> s1 n = s2 n"
-  by (induct ts) (auto intro: eq_subst_te_eq_free)
-
-lemma eq_free_eq_subst_tel:
-    "(\<forall>n. n \<in> free_tv ts --> s1 n = s2 n) \<Longrightarrow> $s1 (ts::typ list) = $s2 ts"
-  by (induct ts) (auto intro: eq_free_eq_subst_te)
-
-text {*
-  \medskip Some useful lemmas.
-*}
-
-lemma codD: "v \<in> cod s \<Longrightarrow> v \<in> free_tv s"
-  by (simp add: free_tv_subst)
-
-lemma not_free_impl_id: "x \<notin> free_tv s \<Longrightarrow> s x = TVar x"
-  by (simp add: free_tv_subst dom_def)
-
-lemma free_tv_le_new_tv: "new_tv n t \<Longrightarrow> m \<in> free_tv t \<Longrightarrow> m < n"
-  by (unfold new_tv_def) fast
-
-lemma free_tv_subst_var: "free_tv (s (v::nat)) \<le> insert v (cod s)"
-  by (cases "v \<in> dom s") (auto simp add: cod_def dom_def)
-
-lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \<subseteq> cod s \<union> 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)) \<subseteq> cod s \<union> 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 (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> 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 \<Rightarrow> typ \<Rightarrow> subst maybe"
-axioms
-  mgu_eq [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $u t1 = $u t2"
-  mgu_mg [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> $s t1 = $s t2 \<Longrightarrow> \<exists>r. s = $r o u"
-  mgu_Ok: "$s t1 = $s t2 \<Longrightarrow> \<exists>u. mgu t1 t2 = Ok u"
-  mgu_free [simp]: "mgu t1 t2 = Ok u \<Longrightarrow> free_tv u \<subseteq> free_tv t1 \<union> free_tv t2"
-
-lemma mgu_new: "mgu t1 t2 = Ok u \<Longrightarrow> new_tv n t1 \<Longrightarrow> new_tv n t2 \<Longrightarrow> 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 \<Rightarrow> expr \<Rightarrow> typ \<Rightarrow> bool"  ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
-  where
-    Var: "n < length a \<Longrightarrow> a |- Var n :: a ! n"
-  | Abs: "t1#a |- e :: t2 \<Longrightarrow> a |- Abs e :: t1 -> t2"
-  | App: "a |- e1 :: t2 -> t1 \<Longrightarrow> a |- e2 :: t2
-      \<Longrightarrow> 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
-  "\<W>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> (subst \<times> typ \<times> nat) maybe"
-primrec
-  "\<W> (Var i) a n =
-    (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
-  "\<W> (Abs e) a n =
-    ((s, t, m) := \<W> e (TVar n # a) (Suc n);
-     Ok (s, (s n) -> t, m))"
-  "\<W> (App e1 e2) a n =
-    ((s1, t1, m1) := \<W> e1 a n;
-     (s2, t2, m2) := \<W> 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) = \<W> e a n ==> $s a |- e :: t"
-proof (induct e arbitrary: a s t m n)
-  case (Var i)
-  from `Ok (s, t, m) = \<W> (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) = \<W> (Abs e) a n`
-  obtain t' where "t = s n -> t'"
-      and "Ok (s, t', m) = \<W> 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) = \<W> (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) = \<W> e1 a n"
-      and W2_ok: "Ok (s2, t2, n2) = \<W> 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. \<W> e a n = Ok (s, t, m) \<Longrightarrow> n \<le> 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) = \<W> e a n \<Longrightarrow> n \<le> m"
-  by (simp add: eq_sym_conv)
-
-lemma new_tv_W: "!!n a s t m.
-  new_tv n a \<Longrightarrow> \<W> e a n = Ok (s, t, m) \<Longrightarrow> 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. \<W> e a n = Ok (s, t, m) \<Longrightarrow>
-    (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> 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 \<W>} wrt.\ @{text has_type}.
-*}
-
-lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \<Longrightarrow> new_tv n a \<Longrightarrow>
-    (\<exists>s t. (\<exists>m. \<W> e a n = Ok (s, t, m)) \<and> (\<exists>r. $s' a = $r ($s a) \<and> 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 = "\<lambda>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
-    "$(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
-      else ra x)) ($ sa t) =
-    $(\<lambda>x. if x = ma then t' else (if x \<in> free_tv t - free_tv sa then r x
-      else ra x)) (ta -> (TVar ma))")
-   apply (rule_tac [2] t = "$(\<lambda>x. if x = ma then t'
-     else (if x \<in> (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 \<noteq> 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 \<in> free_tv sa")
-     txt {* @{text "na \<notin> free_tv sa"} *}
-     prefer 2
-     apply (frule not_free_impl_id)
-     apply simp
-    txt {* @{text "na \<in> 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 \<in> dom sa")
-     prefer 2
-     txt {* @{text "na \<noteq> dom sa"} *}
-     apply (simp add: dom_def)
-    txt {* @{text "na \<in> dom sa"} *}
-    apply (rule eq_free_eq_subst_te)
-    apply (intro strip)
-    apply (subgoal_tac "nb \<noteq> 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 \<noteq> 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 \<in> free_tv t - free_tv sa")
-    prefer 2
-    txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
-    apply simp
-    defer
-    txt {* case @{text "na \<in> 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 \<noteq> 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 \<in> free_tv t - free_tv sa")
-   prefer 2
-   txt {* case @{text "na \<notin> free_tv t - free_tv sa"} *}
-   apply simp
-   defer
-   txt {* case @{text "na \<in> 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' ==>
-    \<exists>s t. (\<exists>m. \<W> e [] n = Ok (s, t, m)) \<and> (\<exists>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 \<I>} for
-  Mini-ML.
-*}
-
-consts
-  "\<I>" :: "expr \<Rightarrow> typ list \<Rightarrow> nat \<Rightarrow> subst \<Rightarrow> (subst \<times> typ \<times> nat) maybe"
-primrec
-  "\<I> (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
-  "\<I> (Abs e) a n s = ((s, t, m) := \<I> e (TVar n # a) (Suc n) s;
-    Ok (s, TVar n -> t, m))"
-  "\<I> (App e1 e2) a n s =
-    ((s1, t1, m1) := \<I> e1 a n s;
-    (s2, t2, m2) := \<I> 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 \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Ok (s', t, n) \<Longrightarrow>
-    \<exists>r. \<W> e ($s a) m = Ok (r, $s' t, n) \<and> 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 \<and> new_tv n2 r \<and> 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 \<and> new_tv m s \<Longrightarrow> \<I> e a m s = Fail \<Longrightarrow> \<W> 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 "\<sim>" 50)
-
-axclass partial_equiv < type
-  partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
-  partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
+class partial_equiv =
+  fixes eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
+  assumes partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
+  assumes partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> 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 \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> 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 \<sim> g"
   show "g \<sim> f"
@@ -110,6 +109,8 @@
   qed
 qed
 
+end
+
 
 subsection {* Total equivalence *}
 
@@ -120,8 +121,8 @@
   symmetric.
 *}
 
-axclass equiv < partial_equiv
-  eqv_refl [intro]: "x \<sim> x"
+class equiv =
+  assumes eqv_refl [intro]: "x \<sim> 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 \<sim> x}| a::'a. True}"
+typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
   by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> 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: "\<exists>x y. x \<noteq> y"
+class classC =
+  assumes classC_ax: "\<exists>x y. x \<noteq> 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 \<Rightarrow> 'a"
-
-axclass classD < type
-  classD_ax: "classD_const (classD_const x) = classD_const x"
+class classD =
+  fixes classD_const :: "'a \<Rightarrow> '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.$$$ "\\<subseteq>" || 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 *)