# HG changeset patch # User wenzelm # Date 1395684380 -3600 # Node ID ce9c7a527c4b7415903c09319bd7f3afb972d6a2 # Parent 2ba733f6e54849fc23502e3a2d744236f24d9a44 removed unused 'ax_specification', to give 'specification' a chance to become localized; tuned whitespace; diff -r 2ba733f6e548 -r ce9c7a527c4b etc/isar-keywords.el --- a/etc/isar-keywords.el Mon Mar 24 18:05:21 2014 +0100 +++ b/etc/isar-keywords.el Mon Mar 24 19:06:20 2014 +0100 @@ -28,7 +28,6 @@ "assume" "atom_decl" "attribute_setup" - "ax_specification" "axiomatization" "back" "bnf" @@ -243,8 +242,8 @@ "simps_of_case" "sledgehammer" "sledgehammer_params" + "smt2_status" "smt_status" - "smt2_status" "solve_direct" "sorry" "spark_end" @@ -447,8 +446,8 @@ "quickcheck" "refute" "sledgehammer" + "smt2_status" "smt_status" - "smt2_status" "solve_direct" "spark_status" "term" @@ -597,8 +596,7 @@ '()) (defconst isar-keywords-theory-goal - '("ax_specification" - "bnf" + '("bnf" "code_pred" "corollary" "cpodef" diff -r 2ba733f6e548 -r ce9c7a527c4b src/Doc/IsarRef/HOL_Specific.thy --- a/src/Doc/IsarRef/HOL_Specific.thy Mon Mar 24 18:05:21 2014 +0100 +++ b/src/Doc/IsarRef/HOL_Specific.thy Mon Mar 24 19:06:20 2014 +0100 @@ -1386,20 +1386,18 @@ *} - section {* Definition by specification \label{sec:hol-specification} *} text {* \begin{matharray}{rcl} @{command_def (HOL) "specification"} & : & @{text "theory \ proof(prove)"} \\ - @{command_def (HOL) "ax_specification"} & : & @{text "theory \ proof(prove)"} \\ \end{matharray} @{rail \ - (@@{command (HOL) specification} | @@{command (HOL) ax_specification}) - '(' (decl +) ')' \ (@{syntax thmdecl}? @{syntax prop} +) + @@{command (HOL) specification} '(' (decl +) ')' \ + (@{syntax thmdecl}? @{syntax prop} +) ; - decl: ((@{syntax name} ':')? @{syntax term} '(' @'overloaded' ')'?) + decl: (@{syntax name} ':')? @{syntax term} ('(' @'overloaded' ')')? \} \begin{description} @@ -1411,31 +1409,15 @@ constants, as well as with theorems stating the properties for these constants. - \item @{command (HOL) "ax_specification"}~@{text "decls \"} sets up - a goal stating the existence of terms with the properties specified - to hold for the constants given in @{text decls}. After finishing - the proof, the theory will be augmented with axioms expressing the - properties given in the first place. - - \item @{text decl} declares a constant to be defined by the + @{text decl} declares a constant to be defined by the specification given. The definition for the constant @{text c} is bound to the name @{text c_def} unless a theorem name is given in the declaration. Overloaded constants should be declared as such. \end{description} - - Whether to use @{command (HOL) "specification"} or @{command (HOL) - "ax_specification"} is to some extent a matter of style. @{command - (HOL) "specification"} introduces no new axioms, and so by - construction cannot introduce inconsistencies, whereas @{command - (HOL) "ax_specification"} does introduce axioms, but only after the - user has explicitly proven it to be safe. A practical issue must be - considered, though: After introducing two constants with the same - properties using @{command (HOL) "specification"}, one can prove - that the two constants are, in fact, equal. If this might be a - problem, one should use @{command (HOL) "ax_specification"}. *} + section {* Adhoc overloading of constants *} text {* diff -r 2ba733f6e548 -r ce9c7a527c4b src/HOL/Hilbert_Choice.thy --- a/src/HOL/Hilbert_Choice.thy Mon Mar 24 18:05:21 2014 +0100 +++ b/src/HOL/Hilbert_Choice.thy Mon Mar 24 19:06:20 2014 +0100 @@ -7,7 +7,7 @@ theory Hilbert_Choice imports Nat Wellfounded -keywords "specification" "ax_specification" :: thy_goal +keywords "specification" :: thy_goal begin subsection {* Hilbert's epsilon *} diff -r 2ba733f6e548 -r ce9c7a527c4b src/HOL/Tools/choice_specification.ML --- a/src/HOL/Tools/choice_specification.ML Mon Mar 24 18:05:21 2014 +0100 +++ b/src/HOL/Tools/choice_specification.ML Mon Mar 24 19:06:20 2014 +0100 @@ -7,237 +7,189 @@ signature CHOICE_SPECIFICATION = sig val close_form : term -> term - val add_specification: string option -> (bstring * xstring * bool) list -> - theory * thm -> theory * thm + val add_specification: (bstring * xstring * bool) list -> theory * thm -> theory * thm end structure Choice_Specification: CHOICE_SPECIFICATION = struct -(* actual code *) - -fun close_form t = - fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t)) - (map dest_Free (Misc_Legacy.term_frees t)) t - -fun add_final overloaded (c, T) thy = - let - val ctxt = Syntax.init_pretty_global thy; - val _ = Theory.check_overloading ctxt overloaded (c, T); - in Theory.add_deps ctxt "" (c, T) [] thy end; +local -local - fun mk_definitional [] arg = arg - | mk_definitional ((thname,cname,covld)::cos) (thy,thm) = - case HOLogic.dest_Trueprop (concl_of thm) of - Const(@{const_name Ex},_) $ P => - let - val ctype = domain_type (type_of P) - val cname_full = Sign.intern_const thy cname - val cdefname = if thname = "" - then Thm.def_name (Long_Name.base_name cname) - else thname - val def_eq = Logic.mk_equals (Const(cname_full,ctype), - HOLogic.choice_const ctype $ P) - val (thms, thy') = Global_Theory.add_defs covld [((Binding.name cdefname, def_eq),[])] thy - val thm' = [thm,hd thms] MRS @{thm exE_some} - 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 (thm, thy') = - Specification.axiom ((Binding.name axname, []), HOLogic.mk_Trueprop tm) thy - in - (thy', Drule.export_without_context thm) - end - | process ((thname,cname,covld)::cos) (thy,tm) = - case tm of - Const(@{const_name Ex},_) $ P => - let - val ctype = domain_type (type_of P) - val cname_full = Sign.intern_const thy cname - val cdefname = if thname = "" - then Thm.def_name (Long_Name.base_name cname) - else thname - val thy' = add_final covld (cname_full,ctype) thy - val co = Const (cname_full,ctype) - 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 +fun mk_definitional [] arg = arg + | mk_definitional ((thname, cname, covld) :: cos) (thy, thm) = + (case HOLogic.dest_Trueprop (concl_of thm) of + Const (@{const_name Ex},_) $ P => + let + val ctype = domain_type (type_of P) + val cname_full = Sign.intern_const thy cname + val cdefname = + if thname = "" + then Thm.def_name (Long_Name.base_name cname) + else thname + val def_eq = + Logic.mk_equals (Const (cname_full, ctype), HOLogic.choice_const ctype $ P) + val (thms, thy') = + Global_Theory.add_defs covld [((Binding.name cdefname, def_eq), [])] thy + val thm' = [thm,hd thms] MRS @{thm exE_some} + in + mk_definitional cos (thy',thm') + end + | _ => raise THM ("Bad specification theorem", 0, [thm])) in -fun proc_exprop axiomatic cos arg = - case axiomatic of - SOME axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg) - | NONE => mk_definitional cos arg + +fun add_specification cos = + mk_definitional cos #> apsnd Drule.export_without_context + end -fun add_specification axiomatic cos = - proc_exprop axiomatic cos - #> apsnd Drule.export_without_context - (* 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) = insert (op aconv) tm tms - | collect_consts ( _,tms) = tms +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) = insert (op aconv) tm tms + | collect_consts (_, tms) = tms + (* Complementing Type.varify_global... *) fun unvarify_global t fmap = - let - val fmap' = map Library.swap fmap - fun unthaw (f as (a, S)) = - (case AList.lookup (op =) fmap' a of - NONE => TVar f - | SOME (b, _) => TFree (b, S)) - in - map_types (map_type_tvar unthaw) t - end + let + val fmap' = map Library.swap fmap + fun unthaw (f as (a, S)) = + (case AList.lookup (op =) fmap' a of + NONE => TVar f + | SOME (b, _) => TFree (b, S)) + in map_types (map_type_tvar unthaw) t end + (* The syntactic meddling needed to setup add_specification for work *) -fun process_spec axiomatic cos alt_props thy = - let - val ctxt = Proof_Context.init_global thy +fun close_form t = + fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t)) + (map dest_Free (Misc_Legacy.term_frees t)) t - fun zip3 [] [] [] = [] - | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs - | zip3 _ _ _ = error "Choice_Specification.process_spec internal error" +fun zip3 [] [] [] = [] + | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs + | zip3 _ _ _ = raise Fail "Choice_Specification.process_spec internal error" - fun myfoldr f [x] = x - | myfoldr f (x::xs) = f (x,myfoldr f xs) - | myfoldr f [] = error "Choice_Specification.process_spec internal error" +fun myfoldr f [x] = x + | myfoldr f (x::xs) = f (x,myfoldr f xs) + | myfoldr f [] = raise Fail "Choice_Specification.process_spec internal error" - val rew_imps = alt_props |> - map (Object_Logic.atomize ctxt o Thm.cterm_of thy o Syntax.read_prop_global thy o snd) - val props' = rew_imps |> - map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) +fun process_spec cos alt_props thy = + let + val ctxt = Proof_Context.init_global thy - fun proc_single prop = - let - val frees = Misc_Legacy.term_frees prop - val _ = forall (fn v => Sign.of_sort thy (type_of v,@{sort type})) frees - orelse error "Specificaton: Only free variables of sort 'type' allowed" - val prop_closed = close_form prop - in - (prop_closed,frees) - end + val rew_imps = alt_props |> + map (Object_Logic.atomize ctxt o Thm.cterm_of thy o Syntax.read_prop_global thy o snd) + val props' = rew_imps |> + map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of) - val props'' = map proc_single props' - val frees = map snd props'' - val prop = myfoldr HOLogic.mk_conj (map fst props'') - val cprop = cterm_of thy (HOLogic.mk_Trueprop prop) + fun proc_single prop = + let + val frees = Misc_Legacy.term_frees prop + val _ = forall (fn v => Sign.of_sort thy (type_of v, @{sort type})) frees + orelse error "Specificaton: Only free variables of sort 'type' allowed" + val prop_closed = close_form prop + in (prop_closed, frees) end - val (vmap, prop_thawed) = Type.varify_global [] 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 (Syntax.read_term_global thy) sconsts - val _ = not (Library.exists (not o Term.is_Const) consts) - orelse error "Specification: Non-constant found as parameter" + val props'' = map proc_single props' + val frees = map snd props'' + val prop = myfoldr HOLogic.mk_conj (map fst props'') + + val (vmap, prop_thawed) = Type.varify_global [] prop + val thawed_prop_consts = collect_consts (prop_thawed, []) + val (altcos, overloaded) = split_list cos + val (names, sconsts) = split_list altcos + val consts = map (Syntax.read_term_global thy) sconsts + val _ = not (Library.exists (not o Term.is_Const) consts) + orelse error "Specification: Non-constant found as parameter" - fun proc_const c = - let - val (_, c') = Type.varify_global [] c - val (cname,ctyp) = dest_Const c' - in - case filter (fn t => let val (name,typ) = dest_Const t - in name = cname andalso Sign.typ_equiv thy (typ, ctyp) - end) thawed_prop_consts of - [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found") - | [cf] => unvarify_global cf vmap - | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy 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 = Long_Name.base_name (fst (dest_Const c)) - val vname = if Symbol_Pos.is_identifier cname - then cname - else "x" - in - HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c,prop)) - end - val ex_prop = fold_rev mk_exist proc_consts prop - val cnames = map (fst o dest_Const) proc_consts - fun post_process (arg as (thy,thm)) = - let - fun inst_all thy v thm = - let - val cv = cterm_of thy 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 = - fold (inst_all (Thm.theory_of_thm thm)) frees thm - fun process_single ((name,atts),rew_imp,frees) args = - let - fun undo_imps thm = - Thm.equal_elim (Thm.symmetric rew_imp) thm + fun proc_const c = + let + val (_, c') = Type.varify_global [] c + val (cname,ctyp) = dest_Const c' + in + (case filter (fn t => + let val (name, typ) = dest_Const t + in name = cname andalso Sign.typ_equiv thy (typ, ctyp) + end) thawed_prop_consts of + [] => + error ("Specification: No suitable instances of constant \"" ^ + Syntax.string_of_term_global thy c ^ "\" found") + | [cf] => unvarify_global cf vmap + | _ => error ("Specification: Several variations of \"" ^ + Syntax.string_of_term_global thy 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 = Long_Name.base_name (fst (dest_Const c)) + val vname = if Symbol_Pos.is_identifier cname then cname else "x" + in HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c, prop)) end + val ex_prop = fold_rev mk_exist proc_consts prop + val cnames = map (fst o dest_Const) proc_consts + fun post_process (arg as (thy,thm)) = + let + fun inst_all thy v thm = + let + val cv = cterm_of thy 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 = fold (inst_all (Thm.theory_of_thm thm)) frees thm + fun process_single ((name, atts), rew_imp, frees) args = + let + fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm - fun add_final (thm, thy) = - if name = "" - then (thm, thy) - else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); - Global_Theory.store_thm (Binding.name name, thm) thy) - in - swap args - |> apfst (remove_alls frees) - |> apfst undo_imps - |> apfst Drule.export_without_context - |-> Thm.theory_attributes - (map (Attrib.attribute_cmd_global thy) - (@{attributes [nitpick_choice_spec]} @ atts)) - |> add_final - |> swap - end + fun add_final (thm, thy) = + if name = "" + then (thm, thy) + else (writeln (" " ^ name ^ ": " ^ Display.string_of_thm_global thy thm); + Global_Theory.store_thm (Binding.name name, thm) thy) + in + swap args + |> apfst (remove_alls frees) + |> apfst undo_imps + |> apfst Drule.export_without_context + |-> Thm.theory_attributes + (map (Attrib.attribute_cmd_global thy) + (@{attributes [nitpick_choice_spec]} @ atts)) + |> add_final + |> swap + 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 "Choice_Specification.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 Thm.unvarify_global - |> 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 [] _ = raise Fail "Choice_Specification.process_spec internal error" + val alt_names = map fst alt_props + val _ = + if exists (fn (name, _) => name <> "") alt_names + then writeln "specification" + else () + in + arg + |> apsnd Thm.unvarify_global + |> process_all (zip3 alt_names rew_imps frees) + end - fun after_qed [[thm]] = Proof_Context.background_theory (fn thy => - #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))); - in - thy - |> Proof_Context.init_global - |> Variable.declare_term ex_prop - |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]] - end; + fun after_qed [[thm]] = Proof_Context.background_theory (fn thy => + #1 (post_process (add_specification (zip3 names cnames overloaded) (thy, thm)))); + in + thy + |> Proof_Context.init_global + |> Variable.declare_term ex_prop + |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]] + end (* outer syntax *) @@ -250,14 +202,6 @@ (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} -- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop) >> (fn (cos, alt_props) => Toplevel.print o - (Toplevel.theory_to_proof (process_spec NONE cos alt_props)))) - -val _ = - Outer_Syntax.command @{command_spec "ax_specification"} "define constants by specification" - (Parse.name -- - (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} -- - Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)) - >> (fn (axname, (cos, alt_props)) => - Toplevel.print o (Toplevel.theory_to_proof (process_spec (SOME axname) cos alt_props)))) + (Toplevel.theory_to_proof (process_spec cos alt_props)))) end