# HG changeset patch
# User skalberg
# Date 1065621774 -7200
# Node ID 1e61f23fd359eec1c0a3d67f3678f98d175f54a0
# Parent  9276f30eaed61c83924dc45c300903a1b7751382
Added axiomatic specifications (ax_specification).

diff -r 9276f30eaed6 -r 1e61f23fd359 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Wed Oct 08 15:58:15 2003 +0200
+++ b/src/HOL/Tools/specification_package.ML	Wed Oct 08 16:02:54 2003 +0200
@@ -9,7 +9,7 @@
 signature SPECIFICATION_PACKAGE =
 sig
     val quiet_mode: bool ref
-    val add_specification_i: (bstring * xstring * bool) list
+    val add_specification_i: string option -> (bstring * xstring * bool) list
 			     -> theory * thm -> theory * thm
 end
 
@@ -35,27 +35,67 @@
 
 (* Actual code *)
 
-fun proc_exprop [] arg = arg
-  | proc_exprop ((thname,cname,covld)::cos) (thy,thm) =
-    case concl_of thm of
-	Const("Trueprop",_) $ (Const("Ex",_) $ P) =>
+local
+    fun mk_definitional [] arg = arg
+      | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
+	case HOLogic.dest_Trueprop (concl_of thm) of
+	    Const("Ex",_) $ P =>
+	    let
+		val ctype = domain_type (type_of P)
+		val cname_full = Sign.intern_const (sign_of thy) cname
+		val cdefname = if thname = ""
+			       then Thm.def_name (Sign.base_name cname)
+			       else thname
+		val def_eq = Logic.mk_equals (Const(cname_full,ctype),choice_const ctype $  P)
+		val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
+		val thm' = [thm,hd thms] MRS helper
+	    in
+		mk_definitional cos (thy',thm')
+	    end
+	  | _ => raise THM ("Internal error: Bad specification theorem",0,[thm])
+
+    fun mk_axiomatic axname cos arg =
 	let
-	    val ctype = domain_type (type_of P)
-	    val cname_full = Sign.intern_const (sign_of thy) cname
-	    val cdefname = if thname = ""
-			   then Thm.def_name (Sign.base_name cname)
-			   else thname
-	    val def_eq = Logic.mk_equals (Const(cname_full,ctype),choice_const ctype $  P)
-	    val (thy',thms) = PureThy.add_defs_i covld [((cdefname,def_eq),[])] thy
-	    val thm' = [thm,hd thms] MRS helper
+	    fun process [] (thy,tm) =
+		let
+		    val (thy',thms) = PureThy.add_axioms_i [((axname,HOLogic.mk_Trueprop tm),[])] thy
+		in
+		    (thy',hd thms)
+		end
+	      | process ((thname,cname,covld)::cos) (thy,tm) =
+		case tm of
+		    Const("Ex",_) $ P =>
+		    let
+			val ctype = domain_type (type_of P)
+			val cname_full = Sign.intern_const (sign_of thy) cname
+			val cdefname = if thname = ""
+				       then Thm.def_name (Sign.base_name cname)
+				       else thname
+			val co = Const(cname_full,ctype)
+			val def = Logic.mk_implies(HOLogic.mk_Trueprop HOLogic.false_const,
+						   Logic.mk_equals (co,choice_const ctype $ P))
+			val (thy',_) = PureThy.add_defs_i covld [((cdefname,def),[])] thy
+			val tm' = case P of
+				      Abs(_, _, bodt) => subst_bound (co, bodt)
+				    | _ => P $ co
+		    in
+			process cos (thy',tm')
+		    end
+		  | _ => raise TERM ("Internal error: Bad specification theorem",[tm])
 	in
-	    proc_exprop cos (thy',thm')
+	    process cos arg
 	end
-      | _ => raise THM ("Internal error: Bad specification theorem",0,[thm])
 
-fun add_specification_i cos arg =
+in
+fun proc_exprop axiomatic cos arg =
+    case axiomatic of
+	Some axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg)
+      | None => mk_definitional cos arg
+end
+
+fun add_specification_i axiomatic cos arg =
     arg |> apsnd freezeT
-	|> proc_exprop cos
+	|> proc_exprop axiomatic cos
 	|> apsnd standard
 
 (* Collect all intances of constants in term *)
@@ -80,7 +120,7 @@
 
 (* The syntactic meddling needed to setup add_specification for work *)
 
-fun process_spec cos alt_props int thy =
+fun process_spec axiomatic cos alt_props int thy =
     let
 	fun zip3 [] [] [] = []
 	  | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
@@ -204,7 +244,7 @@
 	    end
     in
 	IsarThy.theorem_i Drule.internalK
-	    (("",[add_specification_i (zip3 (names:string list) (cnames:string list) (overloaded:bool list)),post_process]),
+	    (("",[add_specification_i axiomatic (zip3 names cnames overloaded),post_process]),
 	     (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy
     end
 
@@ -225,9 +265,21 @@
 val specificationP =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
     (specification_decl >> (fn (cos,alt_props) =>
-			       Toplevel.print o (Toplevel.theory_to_proof (process_spec cos alt_props))))
+			       Toplevel.print o (Toplevel.theory_to_proof
+						     (process_spec None cos alt_props))))
+
+val ax_specification_decl =
+    P.name --
+    (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
+	   Scan.repeat1 (P.opt_thm_name ":" -- P.prop))
 
-val _ = OuterSyntax.add_parsers [specificationP]
+val ax_specificationP =
+  OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
+    (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
+			       Toplevel.print o (Toplevel.theory_to_proof
+						     (process_spec (Some axname) cos alt_props))))
+
+val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP]
 
 end