src/Pure/Isar/specification.ML
changeset 21705 0f3ad56548bc
parent 21691 826ab43d43f5
child 21729 7b3ccdae9212
     1.1 --- a/src/Pure/Isar/specification.ML	Thu Dec 07 21:08:48 2006 +0100
     1.2 +++ b/src/Pure/Isar/specification.ML	Thu Dec 07 21:08:50 2006 +0100
     1.3 @@ -25,14 +25,14 @@
     1.4      ((bstring * Attrib.src list) * term list) list -> local_theory ->
     1.5      (term list * (bstring * thm list) list) * local_theory
     1.6    val definition:
     1.7 -    ((string * string option * mixfix) option * ((string * Attrib.src list) * string)) list ->
     1.8 -    local_theory -> (term * (bstring * thm)) list * local_theory
     1.9 +    (string * string option * mixfix) option * ((string * Attrib.src list) * string) ->
    1.10 +    local_theory -> (term * (bstring * thm)) * local_theory
    1.11    val definition_i:
    1.12 -    ((string * typ option * mixfix) option * ((string * Attrib.src list) * term)) list ->
    1.13 -    local_theory -> (term * (bstring * thm)) list * local_theory
    1.14 -  val abbreviation: Syntax.mode -> ((string * string option * mixfix) option * string) list ->
    1.15 +    (string * typ option * mixfix) option * ((string * Attrib.src list) * term) ->
    1.16 +    local_theory -> (term * (bstring * thm)) * local_theory
    1.17 +  val abbreviation: Syntax.mode -> (string * string option * mixfix) option * string ->
    1.18      local_theory -> local_theory
    1.19 -  val abbreviation_i: Syntax.mode -> ((string * typ option * mixfix) option * term) list ->
    1.20 +  val abbreviation_i: Syntax.mode -> (string * typ option * mixfix) option * term ->
    1.21      local_theory -> local_theory
    1.22    val notation: Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
    1.23    val notation_i: Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.24 @@ -117,58 +117,49 @@
    1.25  
    1.26  (* definition *)
    1.27  
    1.28 -fun gen_defs prep args lthy =
    1.29 +fun gen_def prep (raw_var, (raw_a, raw_prop)) lthy =
    1.30    let
    1.31 -    fun define (raw_var, (raw_a, raw_prop)) lthy1 =
    1.32 -      let
    1.33 -        val (vars, [((raw_name, atts), [prop])]) =
    1.34 -          fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy1);
    1.35 -        val (((x, T), rhs), prove) = LocalDefs.derived_def lthy1 true prop;
    1.36 -        val name = Thm.def_name_optional x raw_name;
    1.37 -        val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
    1.38 -          if x = x' then mx
    1.39 -          else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
    1.40 -        val ((lhs, (_, th)), lthy2) = lthy1
    1.41 -(*          |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
    1.42 -          |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
    1.43 -        val ((b, [th']), lthy3) = lthy2
    1.44 -          |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]);
    1.45 -      in (((x, T), (lhs, (b, th'))), LocalTheory.restore lthy3) end;
    1.46 +    val (vars, [((raw_name, atts), [prop])]) =
    1.47 +      fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
    1.48 +    val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
    1.49 +    val name = Thm.def_name_optional x raw_name;
    1.50 +    val mx = (case vars of [] => NoSyn | [((x', _), mx)] =>
    1.51 +      if x = x' then mx
    1.52 +      else error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote x'));
    1.53 +    val ((lhs, (_, th)), lthy2) = lthy
    1.54 +(*    |> LocalTheory.def ((x, mx), ((name ^ "_raw", []), rhs));  FIXME *)
    1.55 +      |> LocalTheory.def Thm.definitionK ((x, mx), ((name, []), rhs));
    1.56 +    val ((b, [th']), lthy3) = lthy2
    1.57 +      |> LocalTheory.note Thm.definitionK ((name, atts), [prove lthy2 th]);
    1.58  
    1.59 -    val ((cs, defs), lthy') = lthy |> fold_map define args |>> split_list;
    1.60 -    val def_frees = member (op =) (fold (Term.add_frees o fst) defs []);
    1.61 -    val _ = print_consts lthy' def_frees cs;
    1.62 -  in (defs, lthy') end;
    1.63 +    val lhs' = Morphism.term (LocalTheory.target_morphism lthy3) lhs;
    1.64 +    val _ = print_consts lthy3 (member (op =) (Term.add_frees lhs' [])) [(x, T)];
    1.65 +  in ((lhs, (b, th')), lthy3) end;
    1.66  
    1.67 -val definition = gen_defs read_specification;
    1.68 -val definition_i = gen_defs cert_specification;
    1.69 +val definition = gen_def read_specification;
    1.70 +val definition_i = gen_def cert_specification;
    1.71  
    1.72  
    1.73  (* abbreviation *)
    1.74  
    1.75 -fun gen_abbrevs prep mode args lthy =
    1.76 +fun gen_abbrev prep mode (raw_var, raw_prop) lthy =
    1.77    let
    1.78 -    fun abbrev (raw_var, raw_prop) lthy1 =
    1.79 -      let
    1.80 -        val ((vars, [(_, [prop])]), _) =
    1.81 -          prep (the_list raw_var) [(("", []), [raw_prop])]
    1.82 -            (lthy1 |> ProofContext.expand_abbrevs false);
    1.83 -        val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy1 prop));
    1.84 -        val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
    1.85 -          if x = y then mx
    1.86 -          else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
    1.87 -        val lthy2 = lthy1 |> TermSyntax.abbrevs mode [((x, mx), rhs)];
    1.88 -      in ((x, T), LocalTheory.restore lthy2) end;
    1.89 -
    1.90 -    val (cs, lthy') = lthy
    1.91 -      |> ProofContext.set_syntax_mode mode
    1.92 -      |> fold_map abbrev args
    1.93 -      ||> ProofContext.restore_syntax_mode lthy;
    1.94 -    val _ = print_consts lthy' (K false) cs;
    1.95 +    val ((vars, [(_, [prop])]), _) =
    1.96 +      prep (the_list raw_var) [(("", []), [raw_prop])]
    1.97 +        (lthy |> ProofContext.expand_abbrevs false);
    1.98 +    val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
    1.99 +    val mx = (case vars of [] => NoSyn | [((y, _), mx)] =>
   1.100 +      if x = y then mx
   1.101 +      else error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y));
   1.102 +    val lthy' = lthy
   1.103 +      |> ProofContext.set_syntax_mode mode    (* FIXME !? *)
   1.104 +      |> TermSyntax.abbrevs mode [((x, mx), rhs)]
   1.105 +      |> ProofContext.restore_syntax_mode lthy;
   1.106 +    val _ = print_consts lthy' (K false) [(x, T)]
   1.107    in lthy' end;
   1.108  
   1.109 -val abbreviation = gen_abbrevs read_specification;
   1.110 -val abbreviation_i = gen_abbrevs cert_specification;
   1.111 +val abbreviation = gen_abbrev read_specification;
   1.112 +val abbreviation_i = gen_abbrev cert_specification;
   1.113  
   1.114  
   1.115  (* notation *)