src/Pure/Isar/specification.ML
changeset 18810 6dc5416368e9
parent 18786 591a37d48794
child 18828 26b80ed2259b
     1.1 --- a/src/Pure/Isar/specification.ML	Fri Jan 27 19:03:15 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Fri Jan 27 19:03:16 2006 +0100
     1.3 @@ -2,8 +2,8 @@
     1.4      ID:         $Id$
     1.5      Author:     Makarius
     1.6  
     1.7 -Common theory/locale specifications --- with type-inference, but
     1.8 -without internal polymorphism.
     1.9 +Common theory/locale specifications --- with type-inference and
    1.10 +toplevel polymorphism.
    1.11  *)
    1.12  
    1.13  signature SPECIFICATION =
    1.14 @@ -18,16 +18,16 @@
    1.15      Proof.context
    1.16    val axiomatization: xstring option -> (string * string option * mixfix) list ->
    1.17      ((bstring * Attrib.src list) * string list) list -> theory ->
    1.18 -    (term list * (bstring * thm list) list) * (theory * Proof.context)
    1.19 +    (term list * (bstring * thm list) list) * (Proof.context * theory)
    1.20    val axiomatization_i: string option -> (string * typ option * mixfix) list ->
    1.21      ((bstring * Attrib.src list) * term list) list -> theory ->
    1.22 -    (term list * (bstring * thm list) list) * (theory * Proof.context)
    1.23 +    (term list * (bstring * thm list) list) * (Proof.context * theory)
    1.24    val definition: xstring option ->
    1.25      ((string * string option * mixfix) option * ((string * Attrib.src list) * string)) list ->
    1.26 -    theory -> (term * (bstring * thm)) list * (theory * Proof.context)
    1.27 +    theory -> (term * (bstring * thm)) list * (Proof.context * theory)
    1.28    val definition_i: string option ->
    1.29      ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
    1.30 -    theory -> (term * (bstring * thm)) list * (theory * Proof.context)
    1.31 +    theory -> (term * (bstring * thm)) list * (Proof.context * theory)
    1.32  end;
    1.33  
    1.34  structure Specification: SPECIFICATION =
    1.35 @@ -73,8 +73,10 @@
    1.36        |> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props)))
    1.37        ||> LocalTheory.theory (Theory.add_finals_i false (map Term.head_of consts));
    1.38  
    1.39 -    val _ = Pretty.writeln (LocalTheory.pretty_consts ctxt (map fst vars));
    1.40 -  in ((consts, axioms), `LocalTheory.exit axioms_ctxt) end;
    1.41 +    val _ =
    1.42 +      if null vars then ()
    1.43 +      else Pretty.writeln (LocalTheory.pretty_consts ctxt (map fst vars));
    1.44 +  in ((consts, axioms), LocalTheory.exit axioms_ctxt) end;
    1.45  
    1.46  val axiomatization = gen_axiomatization read_specification LocalTheory.init;
    1.47  val axiomatization_i = gen_axiomatization cert_specification LocalTheory.init_i;
    1.48 @@ -88,8 +90,9 @@
    1.49        let
    1.50          val (vars, [(a, [prop])]) = fst (prep (the_list raw_var) [(raw_a, [raw_prop])] ctxt);
    1.51          val ((x, T), rhs) = prop
    1.52 +          |> ObjectLogic.rulify_term thy
    1.53 +          |> ObjectLogic.unatomize_term thy   (*produce meta-level equality*)
    1.54            |> Logic.strip_imp_concl
    1.55 -          |> ObjectLogic.reverse_atomize_term thy
    1.56            |> (snd o ProofContext.cert_def ctxt)
    1.57            |> ProofContext.abs_def;
    1.58          val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
    1.59 @@ -98,22 +101,30 @@
    1.60  
    1.61          fun prove ctxt' const def =
    1.62            let
    1.63 +            val thy' = ProofContext.theory_of ctxt';
    1.64              val prop' = Term.subst_atomic [(Free (x, T), const)] prop;
    1.65 -            val (As, B) = Logic.strip_horn prop';
    1.66 +            val frees = Term.fold_aterms (fn Free (x, _) =>
    1.67 +              if ProofContext.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    1.68            in
    1.69 -            (Goal.prove (ProofContext.theory_of ctxt') [] As B (K (ALLGOALS
    1.70 -              (ObjectLogic.reverse_atomize_tac THEN'
    1.71 +            Goal.prove thy' frees [] prop' (K (ALLGOALS
    1.72 +              (ObjectLogic.rulify_tac THEN'
    1.73 +                ObjectLogic.unatomize_tac THEN'
    1.74                  Tactic.rewrite_goal_tac [def] THEN'
    1.75                  Tactic.resolve_tac [Drule.reflexive_thm])))
    1.76 -              handle ERROR msg => cat_error msg "Failed to prove definitional specification.")
    1.77 -            |> LocalTheory.standard (ProofContext.fix_frees prop' ctxt')
    1.78 +            handle ERROR msg => cat_error msg "Failed to prove definitional specification."
    1.79            end;
    1.80 -      in ctxt |> LocalTheory.def' prove ((x, mx), (a, rhs)) |>> pair (x, T) end;
    1.81 +      in
    1.82 +        ctxt
    1.83 +        |> LocalTheory.def_finish prove ((x, mx), (a, rhs))
    1.84 +        |>> pair (x, T)
    1.85 +      end;
    1.86  
    1.87      val ctxt = init locale thy;
    1.88      val ((decls, defs), defs_ctxt) = ctxt |> fold_map define args |>> split_list;
    1.89 -    val _ = Pretty.writeln (LocalTheory.pretty_consts ctxt decls);
    1.90 -  in (defs, `LocalTheory.exit defs_ctxt) end;
    1.91 +    val _ =
    1.92 +      if null decls then ()
    1.93 +      else Pretty.writeln (LocalTheory.pretty_consts ctxt decls);
    1.94 +  in (defs, LocalTheory.exit defs_ctxt) end;
    1.95  
    1.96  val definition = gen_definition read_specification LocalTheory.init;
    1.97  val definition_i = gen_definition cert_specification LocalTheory.init_i;