1.1 --- a/src/HOL/Tools/specification_package.ML Fri Aug 22 11:51:42 2003 +0200
1.2 +++ b/src/HOL/Tools/specification_package.ML Tue Aug 26 18:49:17 2003 +0200
1.3 @@ -80,8 +80,12 @@
1.4
1.5 (* The syntactic meddling needed to setup add_specification for work *)
1.6
1.7 -fun process_spec cos alt_name sprop int thy =
1.8 +fun process_spec cos alt_props int thy =
1.9 let
1.10 + fun myfoldr f [] = error "SpecificationPackage.process_spec internal error"
1.11 + | myfoldr f [x] = x
1.12 + | myfoldr f (x::xs) = f (x,myfoldr f xs)
1.13 +
1.14 val sg = sign_of thy
1.15 fun typ_equiv t u =
1.16 let
1.17 @@ -90,8 +94,14 @@
1.18 Type.typ_instance(tsig,t,u) andalso
1.19 Type.typ_instance(tsig,u,t)
1.20 end
1.21 - val cprop = Thm.read_cterm sg (sprop,Term.propT)
1.22 - val prop = term_of cprop
1.23 +
1.24 + val cprops = map (Thm.read_cterm sg o rpair Term.propT o snd) alt_props
1.25 + val ss = empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"]
1.26 + val rew_imps = map (Simplifier.full_rewrite ss) cprops
1.27 + val props' = map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) rew_imps
1.28 + val prop = myfoldr HOLogic.mk_conj props'
1.29 + val cprop = cterm_of sg (HOLogic.mk_Trueprop prop)
1.30 +
1.31 val (prop_thawed,vmap) = Type.varify (prop,[])
1.32 val thawed_prop_consts = collect_consts (prop_thawed,[])
1.33 val (altcos,overloaded) = Library.split_list cos
1.34 @@ -111,14 +121,11 @@
1.35 | [cf] => unvarify cf vmap
1.36 | _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification")
1.37 end
1.38 - val rew_imp = Simplifier.full_rewrite (empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"]) cprop
1.39 - val cprop' = snd (dest_equals (cprop_of rew_imp))
1.40 - val prop' = HOLogic.dest_Trueprop (term_of cprop')
1.41 - val frees = Term.term_frees prop'
1.42 + val frees = Term.term_frees prop
1.43 val tsig = Sign.tsig_of (sign_of thy)
1.44 val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
1.45 "Only free variables of sort 'type' allowed in specifications"
1.46 - val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop')
1.47 + val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop)
1.48 val proc_consts = map proc_const consts
1.49 fun mk_exist (c,prop) =
1.50 let
1.51 @@ -131,12 +138,6 @@
1.52 fun zip3 [] [] [] = []
1.53 | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
1.54 | zip3 _ _ _ = error "Internal error: Bad specification syntax"
1.55 - val (name,atts) = alt_name
1.56 - fun add_final (arg as (thy,thm)) =
1.57 - if name = ""
1.58 - then arg
1.59 - else (writeln ("specification " ^ name ^ ": " ^ (string_of_thm thm));
1.60 - PureThy.store_thm((name,thm),[]) thy)
1.61 fun post_process (arg as (thy,thm)) =
1.62 let
1.63 fun inst_all sg (thm,v) =
1.64 @@ -148,16 +149,43 @@
1.65 thm RS spec'
1.66 end
1.67 fun remove_alls frees thm = foldl (inst_all (sign_of_thm thm)) (thm,frees)
1.68 - fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts)
1.69 - fun undo_imps thm =
1.70 - equal_elim (symmetric rew_imp) thm
1.71 + fun process_single (name,atts) rew_imp args =
1.72 + let
1.73 + fun undo_imps thm =
1.74 + equal_elim (symmetric rew_imp) thm
1.75 +
1.76 + fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts)
1.77 + fun add_final (arg as (thy,thm)) =
1.78 + if name = ""
1.79 + then arg
1.80 + else (writeln (" " ^ name ^ ": " ^ (string_of_thm thm));
1.81 + PureThy.store_thm((name,thm),[]) thy)
1.82 + in
1.83 + args |> apsnd (undo_imps)
1.84 + |> apsnd standard
1.85 + |> apply_atts
1.86 + |> add_final
1.87 + end
1.88 +
1.89 + fun process_all [alt_name] [rew_imp] args =
1.90 + process_single alt_name rew_imp args
1.91 + | process_all (alt_name::rest_alt) (rew_imp::rest_imp) (thy,thm) =
1.92 + let
1.93 + val single_th = thm RS conjunct1
1.94 + val rest_th = thm RS conjunct2
1.95 + val (thy',_) = process_single alt_name rew_imp (thy,single_th)
1.96 + in
1.97 + process_all rest_alt rest_imp (thy',rest_th)
1.98 + end
1.99 + | process_all _ _ _ = error "SpecificationPackage.process_spec internal error"
1.100 + val alt_names = map fst alt_props
1.101 + val _ = if exists (fn(name,_) => not (name = "")) alt_names
1.102 + then writeln "specification"
1.103 + else ()
1.104 in
1.105 arg |> apsnd freezeT
1.106 |> apsnd (remove_alls frees)
1.107 - |> apsnd (undo_imps)
1.108 - |> apsnd standard
1.109 - |> apply_atts
1.110 - |> add_final
1.111 + |> process_all alt_names rew_imps
1.112 end
1.113 in
1.114 IsarThy.theorem_i Drule.internalK
1.115 @@ -177,12 +205,12 @@
1.116
1.117 val specification_decl =
1.118 P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
1.119 - P.opt_thm_name ":" -- P.prop
1.120 + Scan.repeat1 (P.opt_thm_name ":" -- P.prop)
1.121
1.122 val specificationP =
1.123 OuterSyntax.command "specification" "define constants by specification" K.thy_goal
1.124 - (specification_decl >> (fn ((cos,alt_name), prop) =>
1.125 - Toplevel.print o (Toplevel.theory_to_proof (process_spec cos alt_name prop))))
1.126 + (specification_decl >> (fn (cos,alt_props) =>
1.127 + Toplevel.print o (Toplevel.theory_to_proof (process_spec cos alt_props))))
1.128
1.129 val _ = OuterSyntax.add_parsers [specificationP]
1.130