merged
authorhaftmann
Fri Jul 10 07:59:44 2009 +0200 (2009-07-10)
changeset 31989a290c36e94d6
parent 31983 7b7dfbf38034
parent 31988 801aabf9f376
child 31990 1d4d0b305f16
merged
src/Pure/Isar/expression.ML
     1.1 --- a/src/HOL/Library/comm_ring.ML	Fri Jul 10 00:49:32 2009 +0200
     1.2 +++ b/src/HOL/Library/comm_ring.ML	Fri Jul 10 07:59:44 2009 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  fun reif_pol T vs (t as Free _) =
     1.5        let
     1.6          val one = @{term "1::nat"};
     1.7 -        val i = find_index_eq t vs
     1.8 +        val i = find_index (fn t' => t' = t) vs
     1.9        in if i = 0
    1.10          then pol_PX T $ (pol_Pc T $ cring_one T)
    1.11            $ one $ (pol_Pc T $ cring_zero T)
     2.1 --- a/src/HOL/Library/reflection.ML	Fri Jul 10 00:49:32 2009 +0200
     2.2 +++ b/src/HOL/Library/reflection.ML	Fri Jul 10 07:59:44 2009 +0200
     2.3 @@ -103,8 +103,8 @@
     2.4            NONE => error "index_of : type not found in environements!"
     2.5          | SOME (tbs,tats) =>
     2.6            let
     2.7 -            val i = find_index_eq t tats
     2.8 -            val j = find_index_eq t tbs
     2.9 +            val i = find_index (fn t' => t' = t) tats
    2.10 +            val j = find_index (fn t' => t' = t) tbs
    2.11            in (if j = ~1 then
    2.12                if i = ~1
    2.13                then (length tbs + length tats,
     3.1 --- a/src/HOL/Quickcheck.thy	Fri Jul 10 00:49:32 2009 +0200
     3.2 +++ b/src/HOL/Quickcheck.thy	Fri Jul 10 07:59:44 2009 +0200
     3.3 @@ -23,8 +23,8 @@
     3.4  begin
     3.5  
     3.6  definition
     3.7 -  "random i = Random.range i o\<rightarrow>
     3.8 -    (\<lambda>k. Pair (if (k div 2 = 0) then Code_Eval.valtermify True else Code_Eval.valtermify False))"
     3.9 +  "random i = Random.range 2 o\<rightarrow>
    3.10 +    (\<lambda>k. Pair (if k = 0 then Code_Eval.valtermify False else Code_Eval.valtermify True))"
    3.11  
    3.12  instance ..
    3.13  
    3.14 @@ -97,7 +97,7 @@
    3.15    \<Rightarrow> Random.seed \<Rightarrow> (('a\<Colon>term_of \<Rightarrow> 'b\<Colon>typerep) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
    3.16    "random_fun_lift f = random_fun_aux TYPEREP('a) TYPEREP('b) (op =) Code_Eval.term_of f Random.split_seed"
    3.17  
    3.18 -instantiation "fun" :: ("{eq, term_of}", "{type, random}") random
    3.19 +instantiation "fun" :: ("{eq, term_of}", random) random
    3.20  begin
    3.21  
    3.22  definition random_fun :: "code_numeral \<Rightarrow> Random.seed \<Rightarrow> (('a \<Rightarrow> 'b) \<times> (unit \<Rightarrow> term)) \<times> Random.seed" where
     4.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Jul 10 00:49:32 2009 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Jul 10 07:59:44 2009 +0200
     4.3 @@ -111,7 +111,7 @@
     4.4              else
     4.5                Const ("Sum_Type.Inr", T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
     4.6            end
     4.7 -      in mk_inj' sumT (length leafTs) (1 + find_index_eq T' leafTs)
     4.8 +      in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
     4.9        end;
    4.10  
    4.11      (* make injections for constructors *)
    4.12 @@ -137,7 +137,7 @@
    4.13              if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
    4.14              else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
    4.15            end
    4.16 -      in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
    4.17 +      in mk_inj branchT (length branchTs) (1 + find_index (fn T'' => T'' = T') branchTs)
    4.18        end;
    4.19  
    4.20      val mk_lim = List.foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
     5.1 --- a/src/HOL/Tools/inductive.ML	Fri Jul 10 00:49:32 2009 +0200
     5.2 +++ b/src/HOL/Tools/inductive.ML	Fri Jul 10 07:59:44 2009 +0200
     5.3 @@ -222,7 +222,7 @@
     5.4      val k = length params;
     5.5      val (c, ts) = strip_comb t;
     5.6      val (xs, ys) = chop k ts;
     5.7 -    val i = find_index_eq c cs;
     5.8 +    val i = find_index (fn c' => c' = c) cs;
     5.9    in
    5.10      if xs = params andalso i >= 0 then
    5.11        SOME (c, i, ys, chop (length ys)
     6.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jul 10 00:49:32 2009 +0200
     6.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 10 07:59:44 2009 +0200
     6.3 @@ -204,9 +204,9 @@
     6.4  fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
     6.5    let
     6.6      val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
     6.7 -    val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
     6.8 -      SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
     6.9 -        find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
    6.10 +    val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
    6.11 +      SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
    6.12 +        (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
    6.13      val fs = maps (fn ((intrs, prems), dummy) =>
    6.14        let
    6.15          val fs = map (fn (rule, (ivs, intr)) =>
     7.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Fri Jul 10 00:49:32 2009 +0200
     7.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Fri Jul 10 07:59:44 2009 +0200
     7.3 @@ -27,7 +27,7 @@
     7.4  
     7.5  fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => term"})
     7.6  val size = @{term "i::code_numeral"};
     7.7 -val size1 = @{term "(i::code_numeral) - 1"};
     7.8 +val size_pred = @{term "(i::code_numeral) - 1"};
     7.9  val size' = @{term "j::code_numeral"};
    7.10  val seed = @{term "s::Random.seed"};
    7.11  
    7.12 @@ -243,7 +243,7 @@
    7.13            | mk_random_fun_lift (fT :: fTs) t =
    7.14                mk_const @{const_name random_fun_lift} [fTs ---> T, fT] $
    7.15                  mk_random_fun_lift fTs t;
    7.16 -        val t = mk_random_fun_lift fTs (nth random_auxs k $ size1 $ size');
    7.17 +        val t = mk_random_fun_lift fTs (nth random_auxs k $ size_pred $ size');
    7.18          val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k)
    7.19            |> the_default 0;
    7.20        in (SOME size, (t, fTs ---> T)) end;
     8.1 --- a/src/HOL/Tools/refute.ML	Fri Jul 10 00:49:32 2009 +0200
     8.2 +++ b/src/HOL/Tools/refute.ML	Fri Jul 10 07:59:44 2009 +0200
     8.3 @@ -2401,7 +2401,7 @@
     8.4                    (* by our assumption on the order of recursion operators *)
     8.5                    (* and datatypes, this is the index of the datatype      *)
     8.6                    (* corresponding to the given recursion operator         *)
     8.7 -                  val idt_index = find_index_eq s (#rec_names info)
     8.8 +                  val idt_index = find_index (fn s' => s' = s) (#rec_names info)
     8.9                    (* mutually recursive types must have the same type   *)
    8.10                    (* parameters, unless the mutual recursion comes from *)
    8.11                    (* indirect recursion                                 *)
    8.12 @@ -2535,7 +2535,7 @@
    8.13                    (* returned                                              *)
    8.14                    (* interpretation -> int -> int list option *)
    8.15                    fun get_args (Leaf xs) elem =
    8.16 -                    if find_index_eq True xs = elem then
    8.17 +                    if find_index (fn x => x = True) xs = elem then
    8.18                        SOME []
    8.19                      else
    8.20                        NONE
    8.21 @@ -2606,7 +2606,7 @@
    8.22                          (* corresponding recursive argument                 *)
    8.23                          fun rec_intr (DatatypeAux.DtRec i) (Leaf xs) =
    8.24                            (* recursive argument is "rec_i params elem" *)
    8.25 -                          compute_array_entry i (find_index_eq True xs)
    8.26 +                          compute_array_entry i (find_index (fn x => x = True) xs)
    8.27                            | rec_intr (DatatypeAux.DtRec _) (Node _) =
    8.28                            raise REFUTE ("IDT_recursion_interpreter",
    8.29                              "interpretation for IDT is a node")
    8.30 @@ -3237,7 +3237,7 @@
    8.31                    def_eq=false, next_idx=1, bounds=[], wellformed=True} cTerm
    8.32                  (* interpretation -> int list option *)
    8.33                  fun get_args (Leaf xs) =
    8.34 -                  if find_index_eq True xs = element then
    8.35 +                  if find_index (fn x => x = True) xs = element then
    8.36                      SOME []
    8.37                    else
    8.38                      NONE
     9.1 --- a/src/HOL/ex/predicate_compile.ML	Fri Jul 10 00:49:32 2009 +0200
     9.2 +++ b/src/HOL/ex/predicate_compile.ML	Fri Jul 10 07:59:44 2009 +0200
     9.3 @@ -419,8 +419,8 @@
     9.4                error ("Too few arguments for inductive predicate " ^ name)
     9.5              else chop (length iss) args;
     9.6            val k = length args2;
     9.7 -          val perm = map (fn i => (find_index_eq (Bound (b - i)) args2) + 1)
     9.8 -            (1 upto b)  
     9.9 +          val perm = map (fn i => (find_index (fn t => t = Bound (b - i)) args2) + 1)
    9.10 +            (1 upto b)
    9.11            val partial_mode = (1 upto k) \\ perm
    9.12          in
    9.13            if not (partial_mode subset is) then [] else
    9.14 @@ -627,7 +627,7 @@
    9.15          val (params, args') = chop (length ms) args
    9.16          val (inargs, outargs) = get_args is' args'
    9.17          val b = length vs
    9.18 -        val perm = map (fn i => (find_index_eq (Bound (b - i)) args') + 1) (1 upto b)
    9.19 +        val perm = map (fn i => find_index (fn t => t = Bound (b - i)) args' + 1) (1 upto b)
    9.20          val outp_perm =
    9.21            snd (get_args is perm)
    9.22            |> map (fn i => i - length (filter (fn x => x < i) is'))
    10.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Fri Jul 10 00:49:32 2009 +0200
    10.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Fri Jul 10 07:59:44 2009 +0200
    10.3 @@ -121,7 +121,7 @@
    10.4        val thy' = thy'' |> Domain_Syntax.add_syntax comp_dnam eqs';
    10.5        val dts  = map (Type o fst) eqs';
    10.6        val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
    10.7 -      fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
    10.8 +      fun strip ss = Library.drop (find_index (fn s => s = "'") ss + 1, ss);
    10.9        fun typid (Type  (id,_)) =
   10.10            let val c = hd (Symbol.explode (Long_Name.base_name id))
   10.11            in if Symbol.is_letter c then c else "t" end
    11.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Fri Jul 10 00:49:32 2009 +0200
    11.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Fri Jul 10 07:59:44 2009 +0200
    11.3 @@ -365,7 +365,7 @@
    11.4  fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
    11.5  val mk_ctuple_pat = foldr1 cpair_pat;
    11.6  fun lift_defined f = lift (fn x => defined (f x));
    11.7 -fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
    11.8 +fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
    11.9  
   11.10  fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = 
   11.11      (case cont_eta_contract body  of
    12.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Jul 10 00:49:32 2009 +0200
    12.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Jul 10 07:59:44 2009 +0200
    12.3 @@ -391,7 +391,7 @@
    12.4             |> hd
    12.5           val (eq as Lineq(_,_,ceq,_),othereqs) =
    12.6                 extract_first (fn Lineq(_,_,l,_) => c mem l) eqs
    12.7 -         val v = find_index_eq c ceq
    12.8 +         val v = find_index (fn v => v = c) ceq
    12.9           val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0)
   12.10                                       (othereqs @ noneqs)
   12.11           val others = map (elim_var v eq) roth @ ioth
    13.1 --- a/src/Pure/Isar/class.ML	Fri Jul 10 00:49:32 2009 +0200
    13.2 +++ b/src/Pure/Isar/class.ML	Fri Jul 10 07:59:44 2009 +0200
    13.3 @@ -311,7 +311,7 @@
    13.4      val proto_sub = case TheoryTarget.peek lthy
    13.5       of {is_class = false, ...} => error "Not in a class context"
    13.6        | {target, ...} => target;
    13.7 -    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup)
    13.8 +    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
    13.9  
   13.10      val expr = ([(sup, (("", false), Expression.Positional []))], []);
   13.11      val (([props], deps, export), goal_ctxt) =
    14.1 --- a/src/Pure/Isar/class_target.ML	Fri Jul 10 00:49:32 2009 +0200
    14.2 +++ b/src/Pure/Isar/class_target.ML	Fri Jul 10 07:59:44 2009 +0200
    14.3 @@ -242,16 +242,15 @@
    14.4      val diff_sort = Sign.complete_sort thy [sup]
    14.5        |> subtract (op =) (Sign.complete_sort thy [sub])
    14.6        |> filter (is_class thy);
    14.7 +    val deps_witss = case some_dep_morph
    14.8 +     of SOME dep_morph => [((sup, dep_morph), the_list some_wit)]
    14.9 +      | NONE => []
   14.10    in
   14.11      thy
   14.12      |> AxClass.add_classrel classrel
   14.13      |> ClassData.map (Graph.add_edge (sub, sup))
   14.14      |> activate_defs sub (these_defs thy diff_sort)
   14.15 -    |> fold (fn dep_morph => Locale.add_dependency sub (sup,
   14.16 -        dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
   14.17 -          (the_list some_dep_morph)
   14.18 -    |> (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
   14.19 -        (Locale.get_registrations thy) thy)
   14.20 +    |> Locale.add_dependencies sub deps_witss export
   14.21    end;
   14.22  
   14.23  
    15.1 --- a/src/Pure/Isar/expression.ML	Fri Jul 10 00:49:32 2009 +0200
    15.2 +++ b/src/Pure/Isar/expression.ML	Fri Jul 10 07:59:44 2009 +0200
    15.3 @@ -796,14 +796,9 @@
    15.4    let
    15.5      val target = intern thy raw_target;
    15.6      val target_ctxt = Locale.init target thy;
    15.7 -
    15.8      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    15.9 -
   15.10      fun after_qed witss = ProofContext.theory
   15.11 -      (fold2 (fn (name, morph) => fn wits => Locale.add_dependency target
   15.12 -        (name, morph $> Element.satisfy_morphism wits $> export)) deps witss #>
   15.13 -      (fn thy => fold_rev (Context.theory_map o Locale.activate_facts)
   15.14 -        (Locale.get_registrations thy) thy));
   15.15 +      (Locale.add_dependencies target (deps ~~ witss) export);
   15.16    in Element.witness_proof after_qed propss goal_ctxt end;
   15.17  
   15.18  in
   15.19 @@ -860,7 +855,7 @@
   15.20            end;
   15.21  
   15.22      fun after_qed wits eqs = ProofContext.theory (fold_map store_reg (regs ~~ wits)
   15.23 -        #-> (fn regs => store_eqns_activate regs eqs));
   15.24 +      #-> (fn regs => store_eqns_activate regs eqs));
   15.25  
   15.26    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
   15.27  
    16.1 --- a/src/Pure/Isar/locale.ML	Fri Jul 10 00:49:32 2009 +0200
    16.2 +++ b/src/Pure/Isar/locale.ML	Fri Jul 10 07:59:44 2009 +0200
    16.3 @@ -45,7 +45,6 @@
    16.4    val instance_of: theory -> string -> morphism -> term list
    16.5    val specification_of: theory -> string -> term option * term list
    16.6    val declarations_of: theory -> string -> declaration list * declaration list
    16.7 -  val dependencies_of: theory -> string -> (string * morphism) list
    16.8  
    16.9    (* Storing results *)
   16.10    val add_thmss: string -> string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   16.11 @@ -53,7 +52,6 @@
   16.12    val add_type_syntax: string -> declaration -> Proof.context -> Proof.context
   16.13    val add_term_syntax: string -> declaration -> Proof.context -> Proof.context
   16.14    val add_declaration: string -> declaration -> Proof.context -> Proof.context
   16.15 -  val add_dependency: string -> string * morphism -> theory -> theory
   16.16  
   16.17    (* Activation *)
   16.18    val activate_declarations: string * morphism -> Proof.context -> Proof.context
   16.19 @@ -69,10 +67,11 @@
   16.20    val unfold_add: attribute
   16.21    val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
   16.22  
   16.23 -  (* Registrations *)
   16.24 +  (* Registrations and dependencies *)
   16.25    val add_registration: string * (morphism * morphism) -> theory -> theory
   16.26    val amend_registration: morphism -> string * morphism -> theory -> theory
   16.27 -  val get_registrations: theory -> (string * morphism) list
   16.28 +  val add_dependencies: string -> ((string * morphism) * Element.witness list) list ->
   16.29 +    morphism  -> theory -> theory
   16.30  
   16.31    (* Diagnostic *)
   16.32    val print_locales: theory -> unit
   16.33 @@ -338,13 +337,19 @@
   16.34      (* FIXME consolidate with dependencies, consider one data slot only *)
   16.35  );
   16.36  
   16.37 -val get_registrations =
   16.38 -  Registrations.get #> map (#1 #> apsnd op $>);
   16.39 +fun reg_morph ((name, (base, export)), _) = (name, base $> export);
   16.40 +
   16.41 +fun these_registrations thy name = Registrations.get thy
   16.42 +  |> filter (curry (op =) name o fst o fst)
   16.43 +  |> map reg_morph;
   16.44 +
   16.45 +fun all_registrations thy = Registrations.get thy
   16.46 +  |> map reg_morph;
   16.47  
   16.48  fun add_registration (name, (base_morph, export)) thy =
   16.49    roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
   16.50 -    (name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
   16.51 -    (* FIXME |-> put_global_idents ?*)
   16.52 +    (name, base_morph) (get_idents (Context.Theory thy), thy)
   16.53 +  (* FIXME |-> (Context.theory_map o put_idents_diag)*) |> snd;
   16.54  
   16.55  fun amend_registration morph (name, base_morph) thy =
   16.56    let
   16.57 @@ -364,6 +369,17 @@
   16.58    end;
   16.59  
   16.60  
   16.61 +(*** Dependencies ***)
   16.62 +
   16.63 +fun add_dependencies loc deps_witss export thy =
   16.64 +  thy
   16.65 +  |> fold (fn ((dep, morph), wits) => (change_locale loc o apsnd)
   16.66 +      (cons ((dep, morph $> Element.satisfy_morphism wits $> export), stamp ())))
   16.67 +        deps_witss
   16.68 +  |> (fn thy => fold_rev (Context.theory_map o activate_facts)
   16.69 +      (all_registrations thy) thy);
   16.70 +
   16.71 +
   16.72  (*** Storing results ***)
   16.73  
   16.74  (* Theorems *)
   16.75 @@ -375,12 +391,12 @@
   16.76        (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
   16.77          #>
   16.78        (* Registrations *)
   16.79 -      (fn thy => fold_rev (fn (name, morph) =>
   16.80 +      (fn thy => fold_rev (fn (_, morph) =>
   16.81              let
   16.82                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   16.83                  Attrib.map_facts (Attrib.attribute_i thy)
   16.84              in PureThy.note_thmss kind args'' #> snd end)
   16.85 -        (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   16.86 +        (these_registrations thy loc) thy))
   16.87    in ctxt'' end;
   16.88  
   16.89  
   16.90 @@ -404,11 +420,6 @@
   16.91  end;
   16.92  
   16.93  
   16.94 -(* Dependencies *)
   16.95 -
   16.96 -fun add_dependency loc dep = (change_locale loc o apsnd) (cons (dep, stamp ()));
   16.97 -
   16.98 -
   16.99  (*** Reasoning about locales ***)
  16.100  
  16.101  (* Storage for witnesses, intro and unfold rules *)
    17.1 --- a/src/Pure/library.ML	Fri Jul 10 00:49:32 2009 +0200
    17.2 +++ b/src/Pure/library.ML	Fri Jul 10 07:59:44 2009 +0200
    17.3 @@ -97,7 +97,6 @@
    17.4    val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
    17.5    val split_last: 'a list -> 'a list * 'a
    17.6    val find_index: ('a -> bool) -> 'a list -> int
    17.7 -  val find_index_eq: ''a -> ''a list -> int
    17.8    val find_first: ('a -> bool) -> 'a list -> 'a option
    17.9    val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   17.10    val get_first: ('a -> 'b option) -> 'a list -> 'b option
   17.11 @@ -503,8 +502,6 @@
   17.12          | find n (x :: xs) = if pred x then n else find (n + 1) xs;
   17.13    in find 0 end;
   17.14  
   17.15 -fun find_index_eq x = find_index (equal x);
   17.16 -
   17.17  (*find first element satisfying predicate*)
   17.18  val find_first = List.find;
   17.19