src/HOL/Tools/choice_specification.ML
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 56895 f058120aaad4
child 59582 0fbed69ff081
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Tools/choice_specification.ML
     2     Author:     Sebastian Skalberg, TU Muenchen
     3 
     4 Package for defining constants by specification.
     5 *)
     6 
     7 signature CHOICE_SPECIFICATION =
     8 sig
     9   val close_form : term -> term
    10   val add_specification: (bstring * xstring * bool) list -> theory * thm -> theory * thm
    11 end
    12 
    13 structure Choice_Specification: CHOICE_SPECIFICATION =
    14 struct
    15 
    16 local
    17 
    18 fun mk_definitional [] arg = arg
    19   | mk_definitional ((thname, cname, covld) :: cos) (thy, thm) =
    20       (case HOLogic.dest_Trueprop (concl_of thm) of
    21         Const (@{const_name Ex},_) $ P =>
    22           let
    23             val ctype = domain_type (type_of P)
    24             val cname_full = Sign.intern_const thy cname
    25             val cdefname =
    26               if thname = ""
    27               then Thm.def_name (Long_Name.base_name cname)
    28               else thname
    29             val def_eq =
    30               Logic.mk_equals (Const (cname_full, ctype), HOLogic.choice_const ctype $ P)
    31             val (thms, thy') =
    32               Global_Theory.add_defs covld [((Binding.name cdefname, def_eq), [])] thy
    33             val thm' = [thm,hd thms] MRS @{thm exE_some}
    34           in
    35             mk_definitional cos (thy',thm')
    36           end
    37       | _ => raise THM ("Bad specification theorem", 0, [thm]))
    38 
    39 in
    40 
    41 fun add_specification cos =
    42   mk_definitional cos #> apsnd Drule.export_without_context
    43 
    44 end
    45 
    46 
    47 (* Collect all intances of constants in term *)
    48 
    49 fun collect_consts (t $ u, tms) = collect_consts (u, collect_consts (t, tms))
    50   | collect_consts (Abs (_, _, t), tms) = collect_consts (t, tms)
    51   | collect_consts (tm as Const _, tms) = insert (op aconv) tm tms
    52   | collect_consts (_, tms) = tms
    53 
    54 
    55 (* Complementing Type.varify_global... *)
    56 
    57 fun unvarify_global t fmap =
    58   let
    59     val fmap' = map Library.swap fmap
    60     fun unthaw (f as (a, S)) =
    61       (case AList.lookup (op =) fmap' a of
    62         NONE => TVar f
    63       | SOME (b, _) => TFree (b, S))
    64   in map_types (map_type_tvar unthaw) t end
    65 
    66 
    67 (* The syntactic meddling needed to setup add_specification for work *)
    68 
    69 fun close_form t =
    70   fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
    71     (map dest_Free (Misc_Legacy.term_frees t)) t
    72 
    73 fun zip3 [] [] [] = []
    74   | zip3 (x::xs) (y::ys) (z::zs) = (x,y,z)::zip3 xs ys zs
    75   | zip3 _ _ _ = raise Fail "Choice_Specification.process_spec internal error"
    76 
    77 fun myfoldr f [x] = x
    78   | myfoldr f (x::xs) = f (x,myfoldr f xs)
    79   | myfoldr f [] = raise Fail "Choice_Specification.process_spec internal error"
    80 
    81 fun process_spec cos alt_props thy =
    82   let
    83     val ctxt = Proof_Context.init_global thy
    84 
    85     val rew_imps = alt_props |>
    86       map (Object_Logic.atomize ctxt o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
    87     val props' = rew_imps |>
    88       map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
    89 
    90     fun proc_single prop =
    91       let
    92         val frees = Misc_Legacy.term_frees prop
    93         val _ = forall (fn v => Sign.of_sort thy (type_of v, @{sort type})) frees
    94           orelse error "Specificaton: Only free variables of sort 'type' allowed"
    95         val prop_closed = close_form prop
    96       in (prop_closed, frees) end
    97 
    98     val props'' = map proc_single props'
    99     val frees = map snd props''
   100     val prop = myfoldr HOLogic.mk_conj (map fst props'')
   101 
   102     val (vmap, prop_thawed) = Type.varify_global [] prop
   103     val thawed_prop_consts = collect_consts (prop_thawed, [])
   104     val (altcos, overloaded) = split_list cos
   105     val (names, sconsts) = split_list altcos
   106     val consts = map (Syntax.read_term_global thy) sconsts
   107     val _ = not (Library.exists (not o Term.is_Const) consts)
   108       orelse error "Specification: Non-constant found as parameter"
   109 
   110     fun proc_const c =
   111       let
   112         val (_, c') = Type.varify_global [] c
   113         val (cname,ctyp) = dest_Const c'
   114       in
   115         (case filter (fn t =>
   116             let val (name, typ) = dest_Const t
   117             in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
   118             end) thawed_prop_consts of
   119           [] =>
   120             error ("Specification: No suitable instances of constant \"" ^
   121               Syntax.string_of_term_global thy c ^ "\" found")
   122         | [cf] => unvarify_global cf vmap
   123         | _ => error ("Specification: Several variations of \"" ^
   124             Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)"))
   125       end
   126     val proc_consts = map proc_const consts
   127     fun mk_exist c prop =
   128       let
   129         val T = type_of c
   130         val cname = Long_Name.base_name (fst (dest_Const c))
   131         val vname = if Symbol_Pos.is_identifier cname then cname else "x"
   132       in HOLogic.exists_const T $ Abs(vname,T,Term.abstract_over (c, prop)) end
   133     val ex_prop = fold_rev mk_exist proc_consts prop
   134     val cnames = map (fst o dest_Const) proc_consts
   135     fun post_process (arg as (thy,thm)) =
   136       let
   137         fun inst_all thy v thm =
   138           let
   139             val cv = cterm_of thy v
   140             val cT = ctyp_of_term cv
   141             val spec' = instantiate' [SOME cT] [NONE, SOME cv] spec
   142           in thm RS spec' end
   143         fun remove_alls frees thm = fold (inst_all (Thm.theory_of_thm thm)) frees thm
   144         fun process_single ((name, atts), rew_imp, frees) args =
   145           let
   146             fun undo_imps thm = Thm.equal_elim (Thm.symmetric rew_imp) thm
   147 
   148             fun add_final (thm, thy) =
   149               if name = ""
   150               then (thm, thy)
   151               else (writeln ("  " ^ name ^ ": " ^ Display.string_of_thm_global thy thm);
   152                 Global_Theory.store_thm (Binding.name name, thm) thy)
   153           in
   154             swap args
   155             |> apfst (remove_alls frees)
   156             |> apfst undo_imps
   157             |> apfst Drule.export_without_context
   158             |-> Thm.theory_attributes
   159               (map (Attrib.attribute_cmd_global thy)
   160                 (@{attributes [nitpick_choice_spec]} @ atts))
   161             |> add_final
   162             |> swap
   163           end
   164 
   165         fun process_all [proc_arg] args =
   166             process_single proc_arg args
   167           | process_all (proc_arg::rest) (thy,thm) =
   168               let
   169                 val single_th = thm RS conjunct1
   170                 val rest_th = thm RS conjunct2
   171                 val (thy', _) = process_single proc_arg (thy, single_th)
   172               in process_all rest (thy', rest_th) end
   173           | process_all [] _ = raise Fail "Choice_Specification.process_spec internal error"
   174         val alt_names = map fst alt_props
   175         val _ =
   176           if exists (fn (name, _) => name <> "") alt_names
   177           then writeln "specification"
   178           else ()
   179       in
   180         arg
   181         |> apsnd Thm.unvarify_global
   182         |> process_all (zip3 alt_names rew_imps frees)
   183       end
   184 
   185     fun after_qed [[thm]] = Proof_Context.background_theory (fn thy =>
   186       #1 (post_process (add_specification (zip3 names cnames overloaded) (thy, thm))));
   187   in
   188     thy
   189     |> Proof_Context.init_global
   190     |> Variable.declare_term ex_prop
   191     |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
   192   end
   193 
   194 
   195 (* outer syntax *)
   196 
   197 val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
   198 val opt_overloaded = Parse.opt_keyword "overloaded"
   199 
   200 val _ =
   201   Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
   202     (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
   203       Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
   204       >> (fn (cos, alt_props) => Toplevel.theory_to_proof (process_spec cos alt_props)))
   205 
   206 end