src/HOL/Tools/specification_package.ML
changeset 14166 1ed8f955727d
parent 14164 8c3fab596219
child 14167 3c29bba24aa4
--- a/src/HOL/Tools/specification_package.ML	Tue Aug 26 19:33:04 2003 +0200
+++ b/src/HOL/Tools/specification_package.ML	Tue Aug 26 19:33:35 2003 +0200
@@ -99,7 +99,21 @@
 	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 prop  = myfoldr HOLogic.mk_conj props'
+
+	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)
+			       "Only free variables of sort 'type' allowed in specifications"
+		val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop)
+	    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 (prop_thawed,vmap) = Type.varify (prop,[])
@@ -109,6 +123,7 @@
 	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,[]))
@@ -121,19 +136,18 @@
 		  | [cf] => unvarify cf vmap
 		  | _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification")
 	    end
-	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)
-		"Only free variables of sort 'type' allowed in specifications"
-	val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop)
 	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("x",T,Term.abstract_over (c,prop))
+		HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop))
 	    end
-	val ex_prop = foldr mk_exist (proc_consts,prop_closed)
+	val ex_prop = foldr mk_exist (proc_consts,prop)
 	val cnames = map (fst o dest_Const) proc_consts
 	fun zip3 [] [] [] = []
 	  | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
@@ -149,7 +163,7 @@
 			thm RS spec'
 		    end
 		fun remove_alls frees thm = foldl (inst_all (sign_of_thm thm)) (thm,frees)
-		fun process_single (name,atts) rew_imp args =
+		fun process_single (name,atts) rew_imp frees args =
 		    let
 			fun undo_imps thm =
 			    equal_elim (symmetric rew_imp) thm
@@ -161,31 +175,31 @@
 			    else (writeln ("  " ^ name ^ ": " ^ (string_of_thm thm));
 				  PureThy.store_thm((name,thm),[]) thy)
 		    in
-			args |> apsnd (undo_imps)
+			args |> apsnd (remove_alls frees)
+			     |> apsnd (undo_imps)
 			     |> apsnd standard
 			     |> apply_atts
 			     |> add_final
 		    end
 
-		fun process_all [alt_name] [rew_imp] args =
-		    process_single alt_name rew_imp args
-		  | process_all (alt_name::rest_alt) (rew_imp::rest_imp) (thy,thm) = 
+		fun process_all [alt_name] [rew_imp] [frees] args =
+		    process_single alt_name rew_imp frees args
+		  | process_all (alt_name::rest_alt) (rew_imp::rest_imp) (frees::rest_frees) (thy,thm) = 
 		    let
 			val single_th = thm RS conjunct1
 			val rest_th   = thm RS conjunct2
-			val (thy',_)  = process_single alt_name rew_imp (thy,single_th)
+			val (thy',_)  = process_single alt_name rew_imp frees (thy,single_th)
 		    in
-			process_all rest_alt rest_imp (thy',rest_th)
+			process_all rest_alt rest_imp rest_frees (thy',rest_th)
 		    end
-		  | process_all _ _ _ = error "SpecificationPackage.process_spec internal error"
+		  | 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
-		    |> apsnd (remove_alls frees)
-		    |> process_all alt_names rew_imps
+		    |> process_all alt_names rew_imps frees
 	    end
     in
 	IsarThy.theorem_i Drule.internalK