# HG changeset patch
# User skalberg
# Date 1058448200 -7200
# Node ID 65ec3f73d00ba579237609c3234c6928c3f6a9b6
# Parent  e97ca1034caa65e0577abfff7fd706ac9d712185
Added package for definition by specification.

diff -r e97ca1034caa -r 65ec3f73d00b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Wed Jul 16 12:09:41 2003 +0200
+++ b/etc/isar-keywords.el	Thu Jul 17 15:23:20 2003 +0200
@@ -136,6 +136,7 @@
     "setup"
     "show"
     "sorry"
+    "specification"
     "subsect"
     "subsection"
     "subsubsect"
@@ -373,6 +374,7 @@
     "instance"
     "lemma"
     "recdef_tc"
+    "specification"
     "theorem"
     "typedef"))
 
diff -r e97ca1034caa -r 65ec3f73d00b src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Jul 16 12:09:41 2003 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Jul 17 15:23:20 2003 +0200
@@ -7,7 +7,7 @@
 header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
 
 theory Hilbert_Choice = NatArith
-files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
+files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML") ("Tools/specification_package.ML"):
 
 
 subsection {* Hilbert's epsilon *}
@@ -268,4 +268,6 @@
 use "Tools/meson.ML"
 setup meson_setup
 
+use "Tools/specification_package.ML"
+
 end
diff -r e97ca1034caa -r 65ec3f73d00b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 16 12:09:41 2003 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 17 15:23:20 2003 +0200
@@ -104,6 +104,7 @@
   Tools/meson.ML Tools/numeral_syntax.ML \
   Tools/primrec_package.ML Tools/recdef_package.ML Tools/recfun_codegen.ML \
   Tools/record_package.ML Tools/rewrite_hol_proof.ML \
+  Tools/specification_package.ML \
   Tools/split_rule.ML Tools/typedef_package.ML \
   Transitive_Closure.thy Transitive_Closure.ML Typedef.thy \
   Wellfounded_Recursion.ML Wellfounded_Recursion.thy Wellfounded_Relations.ML \
diff -r e97ca1034caa -r 65ec3f73d00b src/HOL/Tools/specification_package.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/specification_package.ML	Thu Jul 17 15:23:20 2003 +0200
@@ -0,0 +1,162 @@
+(*  Title:      HOL/Tools/specification_package.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Package for defining constants by specification.
+*)
+
+signature SPECIFICATION_PACKAGE =
+sig
+    val quiet_mode: bool ref
+    val add_specification: (bstring * bool) list -> bstring * Args.src list
+			   -> theory * thm -> theory * thm
+    val add_specification_i: (bstring * bool) list -> bstring * theory attribute list
+			     -> theory * thm -> theory * thm
+end
+
+structure SpecificationPackage : SPECIFICATION_PACKAGE =
+struct
+
+(* messages *)
+
+val quiet_mode = ref false
+fun message s = if ! quiet_mode then () else writeln s
+
+local
+    val _ = Goal "[| Ex P ; c == Eps P |] ==> P c"
+    val _ = by (Asm_simp_tac 1)
+    val _ = by (rtac (thm "someI_ex") 1)
+    val _ = ba 1
+in
+val helper = Goals.result()
+end
+
+(* Akin to HOLogic.exists_const *)
+fun choice_const T = Const("Hilbert_Choice.Eps",(T-->HOLogic.boolT)-->T)
+
+(* Actual code *)
+
+fun proc_exprop [] arg = arg
+  | proc_exprop ((cname,covld)::cos) (thy,thm) =
+    case concl_of thm of
+	Const("Trueprop",_) $ (Const("Ex",_) $ P) =>
+	let
+	    val ctype = domain_type (type_of P)
+	    val cdefname = Thm.def_name (Sign.base_name cname)
+	    val def_eq = Logic.mk_equals (Const(cname,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
+	    proc_exprop cos (thy',thm')
+	end
+      | _ => raise THM ("Internal error: Bad specification theorem",0,[thm])
+
+fun add_specification_i cos (name,atts) arg =
+    let
+	fun apply_attributes arg = Thm.apply_attributes(arg,atts)
+	fun add_final (arg as (thy,thm)) =
+	    if name = ""
+	    then arg
+	    else (writeln ("specification " ^ name ^ ": " ^ (string_of_thm thm));
+		  PureThy.store_thm((name,thm),[]) thy)
+    in
+	arg |> apsnd freezeT
+	    |> proc_exprop cos
+	    |> apsnd standard
+	    |> apply_attributes
+	    |> add_final
+    end
+
+fun add_specification cos (name,atts) arg =
+    add_specification_i cos (name,map (Attrib.global_attribute thy) atts) arg
+
+(* Collect all intances of constants in term *)
+
+fun collect_consts (        t $ u,tms) = collect_consts (u,collect_consts (t,tms))
+  | collect_consts (   Abs(_,_,t),tms) = collect_consts (t,tms)
+  | collect_consts (tm as Const _,tms) = gen_ins (op aconv) (tm,tms)
+  | collect_consts (            _,tms) = tms
+
+(* Complementing Type.varify... *)
+
+fun unvarify t fmap =
+    let
+	val fmap' = map Library.swap fmap
+	fun unthaw (f as (a,S)) =
+	    (case assoc (fmap',a) of
+		 None => TVar f
+	       | Some b => TFree (b,S))
+    in
+	map_term_types (map_type_tvar unthaw) t
+    end
+
+(* The syntactic meddling needed to setup add_specification for work *)
+
+fun process_spec cos alt_name sprop int thy =
+    let
+	val sg = sign_of thy
+	fun typ_equiv t u =
+	    let
+		val tsig = Sign.tsig_of sg
+	    in
+		Type.typ_instance(tsig,t,u) andalso
+		Type.typ_instance(tsig,u,t)
+	    end
+	val prop = term_of (Thm.read_cterm sg (sprop,HOLogic.boolT))
+	val (prop_thawed,vmap) = Type.varify (prop,[])
+	val thawed_prop_consts = collect_consts (prop_thawed,[])
+	val (sconsts,overloaded) = Library.split_list cos
+	val consts = map (term_of o Thm.read_cterm sg o rpair TypeInfer.logicT) sconsts
+	val _ = assert (not (Library.exists (not o Term.is_Const) consts))
+		       "Non-constant found as parameter"
+	fun proc_const c =
+	    let
+		val c' = fst (Type.varify (c,[]))
+		val (cname,ctyp) = dest_Const c'
+	    in
+		case filter (fn t => let val (name,typ) = dest_Const t
+				     in name = cname andalso typ_equiv typ ctyp
+				     end) thawed_prop_consts of
+		    [] => error ("Constant \"" ^ (Sign.string_of_term sg c) ^ "\" not found in specification")
+		  | [cf] => unvarify cf vmap
+		  | _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification")
+	    end
+	val proc_consts = map proc_const consts
+	fun mk_exist (c,prop) =
+	    let
+		val T = type_of c
+	    in
+		HOLogic.exists_const T $ Abs("x",T,Term.abstract_over (c,prop))
+	    end
+	val ex_prop = foldr mk_exist (proc_consts,prop)
+	val cnames = map (fst o dest_Const) proc_consts
+    in
+	IsarThy.theorem_i Drule.internalK
+	    (("",[add_specification (cnames ~~ overloaded) alt_name]),
+	     (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy
+    end
+
+(* outer syntax *)
+
+local structure P = OuterParse and K = OuterSyntax.Keyword in
+
+(* taken from ~~/Pure/Isar/isar_syn.ML *)
+val opt_overloaded =
+  Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false
+
+val specification_decl =
+    P.$$$ "(" |-- Scan.repeat1 (P.term -- opt_overloaded) --| P.$$$ ")" --
+	  P.opt_thm_name ":" -- P.prop
+
+val specificationP =
+  OuterSyntax.command "specification" "define constants by specification" K.thy_goal
+    (specification_decl >> (fn ((cos,alt_name), prop) =>
+			       Toplevel.print o (Toplevel.theory_to_proof (process_spec cos alt_name prop))))
+
+val _ = OuterSyntax.add_parsers [specificationP]
+
+end
+
+
+end