src/HOL/Tools/specification_package.ML
changeset 17336 c05f72cff368
parent 17057 0934ac31985f
child 17377 afaa031ed4da
--- a/src/HOL/Tools/specification_package.ML	Tue Sep 13 17:05:59 2005 +0200
+++ b/src/HOL/Tools/specification_package.ML	Tue Sep 13 22:19:19 2005 +0200
@@ -7,9 +7,9 @@
 
 signature SPECIFICATION_PACKAGE =
 sig
-    val quiet_mode: bool ref
-    val add_specification_i: string option -> (bstring * xstring * bool) list
-			     -> theory * thm -> theory * thm
+  val quiet_mode: bool ref
+  val add_specification_i: string option -> (bstring * xstring * bool) list ->
+    theory attribute
 end
 
 structure SpecificationPackage : SPECIFICATION_PACKAGE =
@@ -34,64 +34,64 @@
 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),
-		                              HOLogic.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])
+        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),
+                                              HOLogic.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
-	    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 thy' = Theory.add_finals_i covld [co] 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
-	    process cos arg
-	end
+        let
+            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 thy' = Theory.add_finals_i covld [co] 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
+            process cos arg
+        end
 
 in
 fun proc_exprop axiomatic cos arg =
     case axiomatic of
-	SOME axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg)
+        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 axiomatic cos
-	|> apsnd standard
+        |> proc_exprop axiomatic cos
+        |> apsnd standard
 
 (* Collect all intances of constants in term *)
 
@@ -104,169 +104,167 @@
 
 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))
+        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
+        map_term_types (map_type_tvar unthaw) t
     end
 
 (* The syntactic meddling needed to setup add_specification for work *)
 
-fun process_spec axiomatic cos alt_props int thy =
+fun process_spec axiomatic cos alt_props thy =
     let
-	fun zip3 [] [] [] = []
-	  | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
-	  | zip3 _ _ _ = error "SpecificationPackage.process_spec internal error"
+        fun zip3 [] [] [] = []
+          | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
+          | zip3 _ _ _ = error "SpecificationPackage.process_spec internal error"
 
-	fun myfoldr f [x] = x
-	  | myfoldr f (x::xs) = f (x,myfoldr f xs)
-	  | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
+        fun myfoldr f [x] = x
+          | myfoldr f (x::xs) = f (x,myfoldr f xs)
+          | myfoldr f [] = error "SpecificationPackage.process_spec internal error"
 
-	val sg = sign_of thy
-	fun typ_equiv t u = Sign.typ_instance sg (t,u) andalso Sign.typ_instance sg (u,t);
+        val sg = sign_of thy
+        fun typ_equiv t u = Sign.typ_instance sg (t,u) andalso Sign.typ_instance sg (u,t);
 
-	val cprops = map (Thm.read_cterm sg o rpair Term.propT o snd) alt_props
-	val ss = empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"]
-	val rew_imps = map (Simplifier.full_rewrite ss) cprops
-	val props' = map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) rew_imps
+        val cprops = map (Thm.read_cterm sg o rpair Term.propT o snd) alt_props
+        val ss = empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"]
+        val rew_imps = map (Simplifier.full_rewrite ss) cprops
+        val props' = map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) rew_imps
 
-	fun proc_single prop =
-	    let
-		val frees = Term.term_frees prop
-		val tsig = Sign.tsig_of (sign_of thy)
-		val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
-			       "Specificaton: Only free variables of sort 'type' allowed"
-		val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
-	    in
-		(prop_closed,frees)
-	    end
+        fun proc_single prop =
+            let
+                val frees = Term.term_frees prop
+                val tsig = Sign.tsig_of (sign_of thy)
+                val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
+                               "Specificaton: Only free variables of sort 'type' allowed"
+                val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
+            in
+                (prop_closed,frees)
+            end
 
-	val props'' = map proc_single props'
-	val frees = map snd props''
-	val prop  = myfoldr HOLogic.mk_conj (map fst props'')
-	val cprop = cterm_of sg (HOLogic.mk_Trueprop prop)
+        val props'' = map proc_single props'
+        val frees = map snd props''
+        val prop  = myfoldr HOLogic.mk_conj (map fst props'')
+        val cprop = cterm_of sg (HOLogic.mk_Trueprop prop)
 
-	val (prop_thawed,vmap) = Type.varify (prop,[])
-	val thawed_prop_consts = collect_consts (prop_thawed,[])
-	val (altcos,overloaded) = Library.split_list cos
-	val (names,sconsts) = Library.split_list altcos
-	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))
-		       "Specification: Non-constant found as parameter"
+        val (prop_thawed,vmap) = Type.varify (prop,[])
+        val thawed_prop_consts = collect_consts (prop_thawed,[])
+        val (altcos,overloaded) = Library.split_list cos
+        val (names,sconsts) = Library.split_list altcos
+        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))
+                       "Specification: Non-constant found as parameter"
 
-	fun proc_const c =
-	    let
-		val c' = fst (Type.varify (c,[]))
-		val (cname,ctyp) = dest_Const c'
-	    in
-		case List.filter (fn t => let val (name,typ) = dest_Const t
-				     in name = cname andalso typ_equiv typ ctyp
-				     end) thawed_prop_consts of
-		    [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term sg c) ^ "\" found")
-		  | [cf] => unvarify cf vmap
-		  | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found (try applying explicit type constraints)")
-	    end
-	val proc_consts = map proc_const consts
-	fun mk_exist (c,prop) =
-	    let
-		val T = type_of c
-		val cname = Sign.base_name (fst (dest_Const c))
-		val vname = if Syntax.is_identifier cname
-			    then cname
-			    else "x"
-	    in
-		HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
-	    end
-	val ex_prop = foldr mk_exist prop proc_consts
-	val cnames = map (fst o dest_Const) proc_consts
-	fun post_process (arg as (thy,thm)) =
-	    let
-		fun inst_all sg (thm,v) =
-		    let
-			val cv = cterm_of sg v
-			val cT = ctyp_of_term cv
-			val spec' = instantiate' [SOME cT] [NONE,SOME cv] spec
-		    in
-			thm RS spec'
-		    end
-		fun remove_alls frees thm = Library.foldl (inst_all (sign_of_thm thm)) (thm,frees)
-		fun process_single ((name,atts),rew_imp,frees) args =
-		    let
-			fun undo_imps thm =
-			    equal_elim (symmetric rew_imp) thm
+        fun proc_const c =
+            let
+                val c' = fst (Type.varify (c,[]))
+                val (cname,ctyp) = dest_Const c'
+            in
+                case List.filter (fn t => let val (name,typ) = dest_Const t
+                                     in name = cname andalso typ_equiv typ ctyp
+                                     end) thawed_prop_consts of
+                    [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term sg c) ^ "\" found")
+                  | [cf] => unvarify cf vmap
+                  | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found (try applying explicit type constraints)")
+            end
+        val proc_consts = map proc_const consts
+        fun mk_exist (c,prop) =
+            let
+                val T = type_of c
+                val cname = Sign.base_name (fst (dest_Const c))
+                val vname = if Syntax.is_identifier cname
+                            then cname
+                            else "x"
+            in
+                HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
+            end
+        val ex_prop = foldr mk_exist prop proc_consts
+        val cnames = map (fst o dest_Const) proc_consts
+        fun post_process (arg as (thy,thm)) =
+            let
+                fun inst_all sg (thm,v) =
+                    let
+                        val cv = cterm_of sg v
+                        val cT = ctyp_of_term cv
+                        val spec' = instantiate' [SOME cT] [NONE,SOME cv] spec
+                    in
+                        thm RS spec'
+                    end
+                fun remove_alls frees thm = Library.foldl (inst_all (sign_of_thm thm)) (thm,frees)
+                fun process_single ((name,atts),rew_imp,frees) args =
+                    let
+                        fun undo_imps thm =
+                            equal_elim (symmetric rew_imp) thm
 
-			fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts)
-			fun add_final (arg as (thy,thm)) =
-			    if name = ""
-			    then arg
-			    else (writeln ("  " ^ name ^ ": " ^ (string_of_thm thm));
-				  PureThy.store_thm((name,thm),[]) thy)
-		    in
-			args |> apsnd (remove_alls frees)
-			     |> apsnd undo_imps
-			     |> apsnd standard
-			     |> apply_atts
-			     |> add_final
-		    end
+                        fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts)
+                        fun add_final (arg as (thy,thm)) =
+                            if name = ""
+                            then arg
+                            else (writeln ("  " ^ name ^ ": " ^ (string_of_thm thm));
+                                  PureThy.store_thm((name,thm),[]) thy)
+                    in
+                        args |> apsnd (remove_alls frees)
+                             |> apsnd undo_imps
+                             |> apsnd standard
+                             |> apply_atts
+                             |> add_final
+                    end
 
-		fun process_all [proc_arg] args =
-		    process_single proc_arg args
-		  | process_all (proc_arg::rest) (thy,thm) = 
-		    let
-			val single_th = thm RS conjunct1
-			val rest_th   = thm RS conjunct2
-			val (thy',_)  = process_single proc_arg (thy,single_th)
-		    in
-			process_all rest (thy',rest_th)
-		    end
-		  | process_all [] _ = error "SpecificationPackage.process_spec internal error"
-		val alt_names = map fst alt_props
-		val _ = if exists (fn(name,_) => not (name = "")) alt_names
-			then writeln "specification"
-			else ()
-	    in
-		arg |> apsnd freezeT
-		    |> process_all (zip3 alt_names rew_imps frees)
-	    end
+                fun process_all [proc_arg] args =
+                    process_single proc_arg args
+                  | process_all (proc_arg::rest) (thy,thm) =
+                    let
+                        val single_th = thm RS conjunct1
+                        val rest_th   = thm RS conjunct2
+                        val (thy',_)  = process_single proc_arg (thy,single_th)
+                    in
+                        process_all rest (thy',rest_th)
+                    end
+                  | process_all [] _ = error "SpecificationPackage.process_spec internal error"
+                val alt_names = map fst alt_props
+                val _ = if exists (fn(name,_) => not (name = "")) alt_names
+                        then writeln "specification"
+                        else ()
+            in
+                arg |> apsnd freezeT
+                    |> process_all (zip3 alt_names rew_imps frees)
+            end
     in
-	IsarThy.theorem_i Drule.internalK
-	    (("",[add_specification_i axiomatic (zip3 names cnames overloaded),post_process]),
-	     (HOLogic.mk_Trueprop ex_prop,([],[]))) int thy
+      IsarThy.theorem_i Drule.internalK
+        ("", [add_specification_i axiomatic (zip3 names cnames overloaded), post_process])
+        (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
     end
 
+
 (* outer syntax *)
 
 local structure P = OuterParse and K = OuterKeyword in
 
-(* taken from ~~/Pure/Isar/isar_syn.ML *)
-val opt_overloaded =
-  Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false
-
 val opt_name = Scan.optional (P.name --| P.$$$ ":") ""
+val opt_overloaded = P.opt_keyword "overloaded";
 
 val specification_decl =
-    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-	  Scan.repeat1 (P.opt_thm_name ":" -- P.prop)
+  P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
+          Scan.repeat1 (P.opt_thm_name ":" -- P.prop)
 
 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 NONE 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))
+           Scan.repeat1 (P.opt_thm_name ":" -- P.prop))
 
 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))))
+                               Toplevel.print o (Toplevel.theory_to_proof
+                                                     (process_spec (SOME axname) cos alt_props))))
 
 val _ = OuterSyntax.add_parsers [specificationP,ax_specificationP]