tuned signature -- refined terminology;
authorwenzelm
Fri Oct 28 17:15:52 2011 +0200 (2011-10-28 ago)
changeset 45290f599ac41e7f5
parent 45289 25e9e7f527b4
child 45291 57cd50f98fdc
tuned signature -- refined terminology;
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/inductive.ML
src/Pure/Isar/args.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/named_target.ML
src/Pure/raw_simplifier.ML
src/Pure/simplifier.ML
src/Tools/interpretation_with_defs.ML
     1.1 --- a/src/HOL/Tools/Function/function.ML	Fri Oct 28 15:38:41 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Oct 28 17:15:52 2011 +0200
     1.3 @@ -128,7 +128,7 @@
     1.4          val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
     1.5        in
     1.6          (info,
     1.7 -         lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))
     1.8 +         lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info))
     1.9        end
    1.10    in
    1.11      ((goal_state, afterqed), lthy')
    1.12 @@ -203,7 +203,7 @@
    1.13              in
    1.14                (info',
    1.15                 lthy 
    1.16 -               |> Local_Theory.declaration false (add_function_data o morph_function_data info')
    1.17 +               |> Local_Theory.declaration false (add_function_data o transform_function_data info')
    1.18                 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
    1.19              end)
    1.20          end
     2.1 --- a/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 15:38:41 2011 +0200
     2.2 +++ b/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 17:15:52 2011 +0200
     2.3 @@ -93,10 +93,12 @@
     2.4    termination : thm,
     2.5    domintros : thm list option}
     2.6  
     2.7 -fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
     2.8 +fun transform_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
     2.9    simps, inducts, termination, defname, is_partial} : info) phi =
    2.10      let
    2.11 -      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
    2.12 +      val term = Morphism.term phi
    2.13 +      val thm = Morphism.thm phi
    2.14 +      val fact = Morphism.fact phi
    2.15        val name = Binding.name_of o Morphism.binding phi o Binding.name
    2.16      in
    2.17        { add_simps = add_simps, case_names = case_names,
    2.18 @@ -132,7 +134,7 @@
    2.19      val inst_morph = lift_morphism thy o Thm.instantiate
    2.20  
    2.21      fun match (trm, data) =
    2.22 -      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
    2.23 +      SOME (transform_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
    2.24        handle Pattern.MATCH => NONE
    2.25    in
    2.26      get_first match (Item_Net.retrieve (get_function ctxt) t)
     3.1 --- a/src/HOL/Tools/inductive.ML	Fri Oct 28 15:38:41 2011 +0200
     3.2 +++ b/src/HOL/Tools/inductive.ML	Fri Oct 28 17:15:52 2011 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4    type inductive_result =
     3.5      {preds: term list, elims: thm list, raw_induct: thm,
     3.6       induct: thm, inducts: thm list, intrs: thm list, eqs: thm list}
     3.7 -  val morph_result: morphism -> inductive_result -> inductive_result
     3.8 +  val transform_result: morphism -> inductive_result -> inductive_result
     3.9    type inductive_info = {names: string list, coind: bool} * inductive_result
    3.10    val the_inductive: Proof.context -> string -> inductive_info
    3.11    val print_inductives: Proof.context -> unit
    3.12 @@ -120,7 +120,7 @@
    3.13    {preds: term list, elims: thm list, raw_induct: thm,
    3.14     induct: thm, inducts: thm list, intrs: thm list, eqs: thm list};
    3.15  
    3.16 -fun morph_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
    3.17 +fun transform_result phi {preds, elims, raw_induct: thm, induct, inducts, intrs, eqs} =
    3.18    let
    3.19      val term = Morphism.term phi;
    3.20      val thm = Morphism.thm phi;
    3.21 @@ -932,7 +932,7 @@
    3.22  
    3.23      val lthy4 = lthy3
    3.24        |> Local_Theory.declaration false (fn phi =>
    3.25 -        let val result' = morph_result phi result;
    3.26 +        let val result' = transform_result phi result;
    3.27          in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
    3.28    in (result, lthy4) end;
    3.29  
     4.1 --- a/src/Pure/Isar/args.ML	Fri Oct 28 15:38:41 2011 +0200
     4.2 +++ b/src/Pure/Isar/args.ML	Fri Oct 28 17:15:52 2011 +0200
     4.3 @@ -12,7 +12,7 @@
     4.4    val dest_src: src -> (string * Token.T list) * Position.T
     4.5    val pretty_src: Proof.context -> src -> Pretty.T
     4.6    val map_name: (string -> string) -> src -> src
     4.7 -  val morph_values: morphism -> src -> src
     4.8 +  val transform_values: morphism -> src -> src
     4.9    val assignable: src -> src
    4.10    val closure: src -> src
    4.11    val context: Proof.context context_parser
    4.12 @@ -96,7 +96,7 @@
    4.13  
    4.14  (* values *)
    4.15  
    4.16 -fun morph_values phi = map_args (Token.map_value
    4.17 +fun transform_values phi = map_args (Token.map_value
    4.18    (fn Token.Text s => Token.Text s
    4.19      | Token.Typ T => Token.Typ (Morphism.typ phi T)
    4.20      | Token.Term t => Token.Term (Morphism.term phi t)
     5.1 --- a/src/Pure/Isar/element.ML	Fri Oct 28 15:38:41 2011 +0200
     5.2 +++ b/src/Pure/Isar/element.ML	Fri Oct 28 17:15:52 2011 +0200
     5.3 @@ -28,7 +28,7 @@
     5.4      ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
     5.5    val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
     5.6      ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
     5.7 -  val morph_ctxt: morphism -> context_i -> context_i
     5.8 +  val transform_ctxt: morphism -> context_i -> context_i
     5.9    val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
    5.10    val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
    5.11    val pretty_statement: Proof.context -> string -> thm -> Pretty.T
    5.12 @@ -43,7 +43,7 @@
    5.13    val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
    5.14      string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
    5.15      Proof.state
    5.16 -  val morph_witness: morphism -> witness -> witness
    5.17 +  val transform_witness: morphism -> witness -> witness
    5.18    val conclude_witness: witness -> thm
    5.19    val pretty_witness: Proof.context -> witness -> Pretty.T
    5.20    val instT_type: typ Symtab.table -> typ -> typ
    5.21 @@ -110,13 +110,13 @@
    5.22  fun map_ctxt_attrib attrib =
    5.23    map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
    5.24  
    5.25 -fun morph_ctxt phi = map_ctxt
    5.26 +fun transform_ctxt phi = map_ctxt
    5.27   {binding = Morphism.binding phi,
    5.28    typ = Morphism.typ phi,
    5.29    term = Morphism.term phi,
    5.30    pattern = Morphism.term phi,
    5.31    fact = Morphism.fact phi,
    5.32 -  attrib = Args.morph_values phi};
    5.33 +  attrib = Args.transform_values phi};
    5.34  
    5.35  
    5.36  
    5.37 @@ -269,7 +269,7 @@
    5.38  fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
    5.39  fun map_witness f (Witness witn) = Witness (f witn);
    5.40  
    5.41 -fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
    5.42 +fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
    5.43  
    5.44  fun prove_witness ctxt t tac =
    5.45    Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
    5.46 @@ -461,7 +461,7 @@
    5.47      | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
    5.48  
    5.49  val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
    5.50 -val satisfy_facts = facts_map o morph_ctxt o satisfy_morphism;
    5.51 +val satisfy_facts = facts_map o transform_ctxt o satisfy_morphism;
    5.52  
    5.53  
    5.54  (* rewriting with equalities *)
     6.1 --- a/src/Pure/Isar/expression.ML	Fri Oct 28 15:38:41 2011 +0200
     6.2 +++ b/src/Pure/Isar/expression.ML	Fri Oct 28 17:15:52 2011 +0200
     6.3 @@ -771,10 +771,10 @@
     6.4  
     6.5      val notes' = body_elems |>
     6.6        map (defines_to_notes thy') |>
     6.7 -      map (Element.morph_ctxt a_satisfy) |>
     6.8 +      map (Element.transform_ctxt a_satisfy) |>
     6.9        (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
    6.10        fst |>
    6.11 -      map (Element.morph_ctxt b_satisfy) |>
    6.12 +      map (Element.transform_ctxt b_satisfy) |>
    6.13        map_filter (fn Notes notes => SOME notes | _ => NONE);
    6.14  
    6.15      val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
    6.16 @@ -823,7 +823,7 @@
    6.17      |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    6.18        fn context =>
    6.19          Locale.add_registration (dep, morph $> Element.satisfy_morphism
    6.20 -            (map (Element.morph_witness export') wits))
    6.21 +            (map (Element.transform_witness export') wits))
    6.22            (Element.eq_morphism (Context.theory_of context) eqns |>
    6.23              Option.map (rpair true))
    6.24            export context) (deps ~~ witss))
    6.25 @@ -902,7 +902,7 @@
    6.26        fn theory =>
    6.27          Locale.add_dependency target
    6.28            (dep, morph $> Element.satisfy_morphism
    6.29 -            (map (Element.morph_witness export') wits))
    6.30 +            (map (Element.transform_witness export') wits))
    6.31            (Element.eq_morphism theory eqns' |> Option.map (rpair true))
    6.32            export theory) (deps ~~ witss))
    6.33    end;
     7.1 --- a/src/Pure/Isar/locale.ML	Fri Oct 28 15:38:41 2011 +0200
     7.2 +++ b/src/Pure/Isar/locale.ML	Fri Oct 28 17:15:52 2011 +0200
     7.3 @@ -425,7 +425,7 @@
     7.4              NONE => Morphism.identity
     7.5            | SOME export => collect_mixins context (name, morph $> export) $> export);
     7.6          val facts' = facts
     7.7 -          |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
     7.8 +          |> Element.facts_map (Element.transform_ctxt (transfer input $> morph $> mixin));
     7.9        in activ_elem (Notes (kind, facts')) input end;
    7.10    in
    7.11      fold_rev activate notes input
    7.12 @@ -562,7 +562,7 @@
    7.13        (* Registrations *)
    7.14        (fn thy => fold_rev (fn (_, morph) =>
    7.15              let
    7.16 -              val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
    7.17 +              val args'' = snd args' |> Element.facts_map (Element.transform_ctxt morph) |>
    7.18                  Attrib.map_facts (Attrib.attribute_i thy)
    7.19              in Global_Theory.note_thmss kind args'' #> snd end)
    7.20          (registrations_of (Context.Theory thy) loc) thy))
     8.1 --- a/src/Pure/Isar/named_target.ML	Fri Oct 28 15:38:41 2011 +0200
     8.2 +++ b/src/Pure/Isar/named_target.ML	Fri Oct 28 17:15:52 2011 +0200
     8.3 @@ -118,7 +118,7 @@
     8.4    let
     8.5      val global_facts' = Attrib.map_facts (K I) global_facts;
     8.6      val local_facts' = Element.facts_map
     8.7 -      (Element.morph_ctxt (Local_Theory.target_morphism lthy)) local_facts;
     8.8 +      (Element.transform_ctxt (Local_Theory.target_morphism lthy)) local_facts;
     8.9    in
    8.10      lthy
    8.11      |> Local_Theory.background_theory (Global_Theory.note_thmss kind global_facts' #> snd)
     9.1 --- a/src/Pure/raw_simplifier.ML	Fri Oct 28 15:38:41 2011 +0200
     9.2 +++ b/src/Pure/raw_simplifier.ML	Fri Oct 28 17:15:52 2011 +0200
     9.3 @@ -33,7 +33,7 @@
     9.4      safe_solvers: string list}
     9.5    type simproc
     9.6    val eq_simproc: simproc * simproc -> bool
     9.7 -  val morph_simproc: morphism -> simproc -> simproc
     9.8 +  val transform_simproc: morphism -> simproc -> simproc
     9.9    val make_simproc: {name: string, lhss: cterm list,
    9.10      proc: morphism -> simpset -> cterm -> thm option, identifier: thm list} -> simproc
    9.11    val mk_simproc: string -> cterm list -> (theory -> simpset -> term -> thm option) -> simproc
    9.12 @@ -625,7 +625,7 @@
    9.13  
    9.14  fun eq_simproc (Simproc {id = id1, ...}, Simproc {id = id2, ...}) = eq_procid (id1, id2);
    9.15  
    9.16 -fun morph_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
    9.17 +fun transform_simproc phi (Simproc {name, lhss, proc, id = (s, ths)}) =
    9.18    Simproc
    9.19     {name = name,
    9.20      lhss = map (Morphism.cterm phi) lhss,
    10.1 --- a/src/Pure/simplifier.ML	Fri Oct 28 15:38:41 2011 +0200
    10.2 +++ b/src/Pure/simplifier.ML	Fri Oct 28 17:15:52 2011 +0200
    10.3 @@ -195,7 +195,7 @@
    10.4      lthy |> Local_Theory.declaration false (fn phi => fn context =>
    10.5        let
    10.6          val b' = Morphism.binding phi b;
    10.7 -        val simproc' = morph_simproc phi simproc;
    10.8 +        val simproc' = transform_simproc phi simproc;
    10.9        in
   10.10          context
   10.11          |> Data.map (fn (ss, tab) =>
   10.12 @@ -298,7 +298,7 @@
   10.13    (Args.del -- Args.colon >> K (op delsimprocs) ||
   10.14      Scan.option (Args.add -- Args.colon) >> K (op addsimprocs))
   10.15    >> (fn f => fn simproc => fn phi => Thm.declaration_attribute
   10.16 -      (K (map_ss (fn ss => f (ss, [morph_simproc phi simproc])))));
   10.17 +      (K (map_ss (fn ss => f (ss, [transform_simproc phi simproc])))));
   10.18  
   10.19  in
   10.20  
    11.1 --- a/src/Tools/interpretation_with_defs.ML	Fri Oct 28 15:38:41 2011 +0200
    11.2 +++ b/src/Tools/interpretation_with_defs.ML	Fri Oct 28 17:15:52 2011 +0200
    11.3 @@ -30,7 +30,7 @@
    11.4      |-> (fn eqns => fold (fn ((dep, morph), wits) =>
    11.5        fn context =>
    11.6          Locale.add_registration (dep, morph $> Element.satisfy_morphism
    11.7 -            (map (Element.morph_witness export') wits))
    11.8 +            (map (Element.transform_witness export') wits))
    11.9            (Element.eq_morphism (Context.theory_of context) (def_eqns @ eqns) |>
   11.10              Option.map (rpair true))
   11.11            export context) (deps ~~ witss))