# HG changeset patch # User wenzelm # Date 1129651168 -7200 # Node ID 6274b426594bf60612dc9f9327989ede2fca1a45 # Parent f2fdd22accaa71f196edbaeb1fcc3722fc5916eb moved helper lemma to HilbertChoice.thy; use actual ObjectLogic.atomize_cterm; eliminated obsolete sign_of; diff -r f2fdd22accaa -r 6274b426594b src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Tue Oct 18 17:59:27 2005 +0200 +++ b/src/HOL/Tools/specification_package.ML Tue Oct 18 17:59:28 2005 +0200 @@ -12,7 +12,7 @@ theory attribute end -structure SpecificationPackage : SPECIFICATION_PACKAGE = +structure SpecificationPackage: SPECIFICATION_PACKAGE = struct (* messages *) @@ -20,18 +20,12 @@ 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 (* Actual code *) local + val exE_some = thm "exE_some"; + fun mk_definitional [] arg = arg | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = case HOLogic.dest_Trueprop (concl_of thm) of @@ -45,7 +39,7 @@ 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 + val thm' = [thm,hd thms] MRS exE_some in mk_definitional cos (thy',thm') end @@ -125,13 +119,12 @@ | 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); + fun typ_equiv t u = Sign.typ_instance thy (t,u) andalso Sign.typ_instance thy (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 rew_imps = alt_props |> + map (ObjectLogic.atomize_cterm thy o Thm.read_cterm thy o rpair Term.propT o snd) + val props' = rew_imps |> + map (HOLogic.dest_Trueprop o term_of o snd o dest_equals o cprop_of) fun proc_single prop = let @@ -147,13 +140,13 @@ 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 cprop = cterm_of thy (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 consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts val _ = assert (not (Library.exists (not o Term.is_Const) consts)) "Specification: Non-constant found as parameter" @@ -165,9 +158,9 @@ 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") + [] => error ("Specification: No suitable instances of constant \"" ^ (Sign.string_of_term thy c) ^ "\" found") | [cf] => unvarify cf vmap - | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found (try applying explicit type constraints)") + | _ => error ("Specification: Several variations of \"" ^ (Sign.string_of_term thy c) ^ "\" found (try applying explicit type constraints)") end val proc_consts = map proc_const consts fun mk_exist (c,prop) = @@ -184,9 +177,9 @@ val cnames = map (fst o dest_Const) proc_consts fun post_process (arg as (thy,thm)) = let - fun inst_all sg (thm,v) = + fun inst_all thy (thm,v) = let - val cv = cterm_of sg v + val cv = cterm_of thy v val cT = ctyp_of_term cv val spec' = instantiate' [SOME cT] [NONE,SOME cv] spec in