src/Pure/Isar/expression.ML
changeset 55639 e4e8cbd9d780
parent 54883 dd04a8b654fc
child 55997 9dc5ce83202c
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Feb 20 21:55:37 2014 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Feb 20 23:16:33 2014 +0100
     1.3 @@ -19,10 +19,12 @@
     1.4      Proof.context -> (term * term list) list list * Proof.context
     1.5  
     1.6    (* Declaring locales *)
     1.7 -  val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
     1.8 +  val cert_declaration: expression_i -> (Proof.context -> Proof.context) ->
     1.9 +    Element.context_i list ->
    1.10      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    1.11        * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
    1.12 -  val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
    1.13 +  val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) ->
    1.14 +    Element.context list ->
    1.15      Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    1.16        * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
    1.17        (*FIXME*)
    1.18 @@ -39,13 +41,16 @@
    1.19      (term list list * (string * morphism) list * morphism) * Proof.context
    1.20    val read_goal_expression: expression -> Proof.context ->
    1.21      (term list list * (string * morphism) list * morphism) * Proof.context
    1.22 -  val permanent_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.23 -  val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.24 +  val permanent_interpretation: expression_i -> (Attrib.binding * term) list ->
    1.25 +    local_theory -> Proof.state
    1.26 +  val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list ->
    1.27 +    local_theory -> Proof.state
    1.28    val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state
    1.29    val interpret_cmd: expression -> (Attrib.binding * string) list ->
    1.30      bool -> Proof.state -> Proof.state
    1.31    val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.32 -  val interpretation_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    1.33 +  val interpretation_cmd: expression -> (Attrib.binding * string) list ->
    1.34 +    local_theory -> Proof.state
    1.35    val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state
    1.36    val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state
    1.37    val sublocale_global: (local_theory -> local_theory) -> string -> expression_i ->
    1.38 @@ -138,8 +143,11 @@
    1.39      val implicit'' =
    1.40        if strict then []
    1.41        else
    1.42 -        let val _ = reject_dups
    1.43 -          "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
    1.44 +        let
    1.45 +          val _ =
    1.46 +            reject_dups
    1.47 +              "Parameter(s) declared simultaneously in expression and for clause: "
    1.48 +              (implicit' @ fixed');
    1.49          in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
    1.50  
    1.51    in (expr', implicit'' @ fixed) end;
    1.52 @@ -492,7 +500,8 @@
    1.53    let
    1.54      val (asm, defs) = Locale.specification_of thy name;
    1.55    in
    1.56 -    (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph)
    1.57 +    (case asm of NONE => defs | SOME asm => asm :: defs)
    1.58 +    |> map (Morphism.term morph)
    1.59    end;
    1.60  
    1.61  fun prep_goal_expression prep expression context =
    1.62 @@ -581,12 +590,13 @@
    1.63      val (asm, defs) = Locale.specification_of thy loc;
    1.64      val asm' = Option.map (Morphism.term morph) asm;
    1.65      val defs' = map (Morphism.term morph) defs;
    1.66 -    val text' = text |>
    1.67 -      (if is_some asm
    1.68 -        then eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
    1.69 +    val text' =
    1.70 +      text |>
    1.71 +       (if is_some asm then
    1.72 +          eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])])
    1.73          else I) |>
    1.74 -      (if not (null defs)
    1.75 -        then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
    1.76 +       (if not (null defs) then
    1.77 +          eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs'))
    1.78          else I)
    1.79  (* FIXME clone from locale.ML *)
    1.80    in text' end;
    1.81 @@ -618,7 +628,8 @@
    1.82      val body = Object_Logic.atomize_term thy t;
    1.83      val bodyT = Term.fastype_of body;
    1.84    in
    1.85 -    if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
    1.86 +    if bodyT = propT
    1.87 +    then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
    1.88      else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t))
    1.89    end;
    1.90  
    1.91 @@ -700,7 +711,8 @@
    1.92        if null exts then (NONE, NONE, [], thy)
    1.93        else
    1.94          let
    1.95 -          val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
    1.96 +          val abinding =
    1.97 +            if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding;
    1.98            val ((statement, intro, axioms), thy') =
    1.99              thy
   1.100              |> def_pred abinding parms defs' exts exts';
   1.101 @@ -761,7 +773,9 @@
   1.102      val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
   1.103  
   1.104      val extraTs =
   1.105 -      subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
   1.106 +      subtract (op =)
   1.107 +        (fold Term.add_tfreesT (map snd parms) [])
   1.108 +        (fold Term.add_tfrees exts' []);
   1.109      val _ =
   1.110        if null extraTs then ()
   1.111        else warning ("Additional type variable(s) in locale specification " ^
   1.112 @@ -790,14 +804,15 @@
   1.113              [(Attrib.internal o K) Locale.witness_add])])])]
   1.114        else [];
   1.115  
   1.116 -    val notes' = body_elems |>
   1.117 -      map (defines_to_notes pred_ctxt) |>
   1.118 -      map (Element.transform_ctxt a_satisfy) |>
   1.119 -      (fn elems =>
   1.120 -        fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |>
   1.121 -      fst |>
   1.122 -      map (Element.transform_ctxt b_satisfy) |>
   1.123 -      map_filter (fn Notes notes => SOME notes | _ => NONE);
   1.124 +    val notes' =
   1.125 +      body_elems
   1.126 +      |> map (defines_to_notes pred_ctxt)
   1.127 +      |> map (Element.transform_ctxt a_satisfy)
   1.128 +      |> (fn elems =>
   1.129 +        fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms))
   1.130 +      |> fst
   1.131 +      |> map (Element.transform_ctxt b_satisfy)
   1.132 +      |> map_filter (fn Notes notes => SOME notes | _ => NONE);
   1.133  
   1.134      val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
   1.135      val axioms = map (Element.conclude_witness pred_ctxt) b_axioms;
   1.136 @@ -836,7 +851,8 @@
   1.137    let
   1.138      val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt;
   1.139      val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns;
   1.140 -    val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
   1.141 +    val attrss =
   1.142 +      map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns;
   1.143      val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
   1.144      val export' = Variable.export_morphism goal_ctxt expr_ctxt;
   1.145    in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end;
   1.146 @@ -918,8 +934,10 @@
   1.147  
   1.148  fun subscribe_locale_only lthy =
   1.149    let
   1.150 -    val _ = if Named_Target.is_theory lthy
   1.151 -      then error "Not possible on level of global theory" else ();
   1.152 +    val _ =
   1.153 +      if Named_Target.is_theory lthy
   1.154 +      then error "Not possible on level of global theory"
   1.155 +      else ();
   1.156    in subscribe lthy end;
   1.157  
   1.158  
   1.159 @@ -929,7 +947,7 @@
   1.160      before_exit raw_locale expression raw_eqns thy =
   1.161    thy
   1.162    |> Named_Target.init before_exit (prep_loc thy raw_locale)
   1.163 -  |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns
   1.164 +  |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns;
   1.165  
   1.166  in
   1.167