src/Pure/Isar/specification.ML
changeset 18786 591a37d48794
parent 18771 63efe00371af
child 18810 6dc5416368e9
     1.1 --- a/src/Pure/Isar/specification.ML	Wed Jan 25 00:21:43 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Jan 25 00:21:44 2006 +0100
     1.3 @@ -22,6 +22,12 @@
     1.4    val axiomatization_i: string option -> (string * typ option * mixfix) list ->
     1.5      ((bstring * Attrib.src list) * term list) list -> theory ->
     1.6      (term list * (bstring * thm list) list) * (theory * Proof.context)
     1.7 +  val definition: xstring option ->
     1.8 +    ((string * string option * mixfix) option * ((string * Attrib.src list) * string)) list ->
     1.9 +    theory -> (term * (bstring * thm)) list * (theory * Proof.context)
    1.10 +  val definition_i: string option ->
    1.11 +    ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
    1.12 +    theory -> (term * (bstring * thm)) list * (theory * Proof.context)
    1.13  end;
    1.14  
    1.15  structure Specification: SPECIFICATION =
    1.16 @@ -56,17 +62,60 @@
    1.17  
    1.18  fun gen_axiomatization prep init locale raw_vars raw_specs thy =
    1.19    let
    1.20 -    val ((vars, specs), ctxt) = init locale thy |> prep raw_vars raw_specs;
    1.21 +    val ctxt = init locale thy;
    1.22 +    val (vars, specs) = fst (prep raw_vars raw_specs ctxt);
    1.23 +
    1.24      val (consts, consts_ctxt) = ctxt |> LocalTheory.consts vars;
    1.25      val subst = Term.subst_atomic (map (Free o fst) vars ~~ consts);
    1.26 +
    1.27      val (axioms, axioms_ctxt) =
    1.28        consts_ctxt
    1.29        |> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props)))
    1.30 -      ||> LocalTheory.map_theory (Theory.add_finals_i false (map Term.head_of consts));
    1.31 +      ||> LocalTheory.theory (Theory.add_finals_i false (map Term.head_of consts));
    1.32 +
    1.33      val _ = Pretty.writeln (LocalTheory.pretty_consts ctxt (map fst vars));
    1.34    in ((consts, axioms), `LocalTheory.exit axioms_ctxt) end;
    1.35  
    1.36  val axiomatization = gen_axiomatization read_specification LocalTheory.init;
    1.37  val axiomatization_i = gen_axiomatization cert_specification LocalTheory.init_i;
    1.38  
    1.39 +
    1.40 +(* definition *)
    1.41 +
    1.42 +fun gen_definition prep init locale args thy =
    1.43 +  let
    1.44 +    fun define (raw_var, (raw_a, raw_prop)) ctxt =
    1.45 +      let
    1.46 +        val (vars, [(a, [prop])]) = fst (prep (the_list raw_var) [(raw_a, [raw_prop])] ctxt);
    1.47 +        val ((x, T), rhs) = prop
    1.48 +          |> Logic.strip_imp_concl
    1.49 +          |> ObjectLogic.reverse_atomize_term thy
    1.50 +          |> (snd o ProofContext.cert_def ctxt)
    1.51 +          |> ProofContext.abs_def;
    1.52 +        val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
    1.53 +          if x = x' then mx
    1.54 +          else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
    1.55 +
    1.56 +        fun prove ctxt' const def =
    1.57 +          let
    1.58 +            val prop' = Term.subst_atomic [(Free (x, T), const)] prop;
    1.59 +            val (As, B) = Logic.strip_horn prop';
    1.60 +          in
    1.61 +            (Goal.prove (ProofContext.theory_of ctxt') [] As B (K (ALLGOALS
    1.62 +              (ObjectLogic.reverse_atomize_tac THEN'
    1.63 +                Tactic.rewrite_goal_tac [def] THEN'
    1.64 +                Tactic.resolve_tac [Drule.reflexive_thm])))
    1.65 +              handle ERROR msg => cat_error msg "Failed to prove definitional specification.")
    1.66 +            |> LocalTheory.standard (ProofContext.fix_frees prop' ctxt')
    1.67 +          end;
    1.68 +      in ctxt |> LocalTheory.def' prove ((x, mx), (a, rhs)) |>> pair (x, T) end;
    1.69 +
    1.70 +    val ctxt = init locale thy;
    1.71 +    val ((decls, defs), defs_ctxt) = ctxt |> fold_map define args |>> split_list;
    1.72 +    val _ = Pretty.writeln (LocalTheory.pretty_consts ctxt decls);
    1.73 +  in (defs, `LocalTheory.exit defs_ctxt) end;
    1.74 +
    1.75 +val definition = gen_definition read_specification LocalTheory.init;
    1.76 +val definition_i = gen_definition cert_specification LocalTheory.init_i;
    1.77 +
    1.78  end;