src/Pure/Isar/specification.ML
changeset 18828 26b80ed2259b
parent 18810 6dc5416368e9
child 18880 b8a1c3cdf739
     1.1 --- a/src/Pure/Isar/specification.ML	Sat Jan 28 17:29:02 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Sat Jan 28 17:29:03 2006 +0100
     1.3 @@ -22,12 +22,18 @@
     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) * (Proof.context * theory)
     1.7 +  val axiomatization_loc: (string * typ option * mixfix) list ->
     1.8 +    ((bstring * Attrib.src list) * term list) list -> Proof.context ->
     1.9 +    (term list * (bstring * thm list) list) * Proof.context
    1.10    val definition: xstring option ->
    1.11      ((string * string option * mixfix) option * ((string * Attrib.src list) * string)) list ->
    1.12      theory -> (term * (bstring * thm)) list * (Proof.context * theory)
    1.13    val definition_i: string option ->
    1.14      ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
    1.15      theory -> (term * (bstring * thm)) list * (Proof.context * theory)
    1.16 +  val definition_loc:
    1.17 +    ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
    1.18 +    Proof.context -> (term * (bstring * thm)) list * Proof.context
    1.19  end;
    1.20  
    1.21  structure Specification: SPECIFICATION =
    1.22 @@ -35,8 +41,7 @@
    1.23  
    1.24  (* prepare specification *)
    1.25  
    1.26 -fun prep_specification prep_vars prep_propp prep_att
    1.27 -    raw_vars raw_specs ctxt =
    1.28 +fun prep_specification prep_vars prep_propp prep_att raw_vars raw_specs ctxt =
    1.29    let
    1.30      val thy = ProofContext.theory_of ctxt;
    1.31  
    1.32 @@ -60,73 +65,55 @@
    1.33  
    1.34  (* axiomatization *)
    1.35  
    1.36 -fun gen_axiomatization prep init locale raw_vars raw_specs thy =
    1.37 +fun gen_axioms prep init exit print raw_vars raw_specs context =
    1.38    let
    1.39 -    val ctxt = init locale thy;
    1.40 +    val ctxt = init context;
    1.41      val (vars, specs) = fst (prep raw_vars raw_specs ctxt);
    1.42 +    val cs = map fst vars;
    1.43  
    1.44      val (consts, consts_ctxt) = ctxt |> LocalTheory.consts vars;
    1.45 -    val subst = Term.subst_atomic (map (Free o fst) vars ~~ consts);
    1.46 +    val subst = Term.subst_atomic (map Free cs ~~ consts);
    1.47  
    1.48      val (axioms, axioms_ctxt) =
    1.49        consts_ctxt
    1.50        |> LocalTheory.axioms (specs |> map (fn (a, props) => (a, map subst props)))
    1.51        ||> LocalTheory.theory (Theory.add_finals_i false (map Term.head_of consts));
    1.52 +    val _ = print ctxt cs;
    1.53 +  in ((consts, axioms), exit axioms_ctxt) end;
    1.54  
    1.55 -    val _ =
    1.56 -      if null vars then ()
    1.57 -      else Pretty.writeln (LocalTheory.pretty_consts ctxt (map fst vars));
    1.58 -  in ((consts, axioms), LocalTheory.exit axioms_ctxt) end;
    1.59 -
    1.60 -val axiomatization = gen_axiomatization read_specification LocalTheory.init;
    1.61 -val axiomatization_i = gen_axiomatization cert_specification LocalTheory.init_i;
    1.62 +fun axiomatization loc =
    1.63 +  gen_axioms read_specification (LocalTheory.init loc) LocalTheory.exit LocalTheory.print_consts;
    1.64 +fun axiomatization_i loc =
    1.65 +  gen_axioms cert_specification (LocalTheory.init_i loc) LocalTheory.exit LocalTheory.print_consts;
    1.66 +val axiomatization_loc = gen_axioms cert_specification I I (K (K ()));
    1.67  
    1.68  
    1.69  (* definition *)
    1.70  
    1.71 -fun gen_definition prep init locale args thy =
    1.72 +fun gen_defs prep init exit print args context =
    1.73    let
    1.74      fun define (raw_var, (raw_a, raw_prop)) ctxt =
    1.75        let
    1.76          val (vars, [(a, [prop])]) = fst (prep (the_list raw_var) [(raw_a, [raw_prop])] ctxt);
    1.77 -        val ((x, T), rhs) = prop
    1.78 -          |> ObjectLogic.rulify_term thy
    1.79 -          |> ObjectLogic.unatomize_term thy   (*produce meta-level equality*)
    1.80 -          |> Logic.strip_imp_concl
    1.81 -          |> (snd o ProofContext.cert_def ctxt)
    1.82 -          |> ProofContext.abs_def;
    1.83 +        val (((x, T), rhs), prove) = LocalDefs.derived_def ctxt prop;
    1.84          val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
    1.85            if x = x' then mx
    1.86            else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
    1.87 -
    1.88 -        fun prove ctxt' const def =
    1.89 -          let
    1.90 -            val thy' = ProofContext.theory_of ctxt';
    1.91 -            val prop' = Term.subst_atomic [(Free (x, T), const)] prop;
    1.92 -            val frees = Term.fold_aterms (fn Free (x, _) =>
    1.93 -              if ProofContext.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop' [];
    1.94 -          in
    1.95 -            Goal.prove thy' frees [] prop' (K (ALLGOALS
    1.96 -              (ObjectLogic.rulify_tac THEN'
    1.97 -                ObjectLogic.unatomize_tac THEN'
    1.98 -                Tactic.rewrite_goal_tac [def] THEN'
    1.99 -                Tactic.resolve_tac [Drule.reflexive_thm])))
   1.100 -            handle ERROR msg => cat_error msg "Failed to prove definitional specification."
   1.101 -          end;
   1.102        in
   1.103          ctxt
   1.104          |> LocalTheory.def_finish prove ((x, mx), (a, rhs))
   1.105          |>> pair (x, T)
   1.106        end;
   1.107  
   1.108 -    val ctxt = init locale thy;
   1.109 -    val ((decls, defs), defs_ctxt) = ctxt |> fold_map define args |>> split_list;
   1.110 -    val _ =
   1.111 -      if null decls then ()
   1.112 -      else Pretty.writeln (LocalTheory.pretty_consts ctxt decls);
   1.113 -  in (defs, LocalTheory.exit defs_ctxt) end;
   1.114 +    val ctxt = init context;
   1.115 +    val ((cs, defs), defs_ctxt) = ctxt |> fold_map define args |>> split_list;
   1.116 +    val _ = print ctxt cs;
   1.117 +  in (defs, exit defs_ctxt) end;
   1.118  
   1.119 -val definition = gen_definition read_specification LocalTheory.init;
   1.120 -val definition_i = gen_definition cert_specification LocalTheory.init_i;
   1.121 +fun definition loc =
   1.122 +  gen_defs read_specification (LocalTheory.init loc) LocalTheory.exit LocalTheory.print_consts;
   1.123 +fun definition_i loc =
   1.124 +  gen_defs cert_specification (LocalTheory.init_i loc) LocalTheory.exit LocalTheory.print_consts;
   1.125 +val definition_loc = gen_defs cert_specification I I (K (K ()));
   1.126  
   1.127  end;