canonical merge operations
authorhaftmann
Fri Apr 13 16:40:16 2007 +0200 (2007-04-13)
changeset 226623e492ba59355
parent 22661 f3ba63a2663e
child 22663 73517244fc46
canonical merge operations
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_rewrite_rules.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Fri Apr 13 15:43:25 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Apr 13 16:40:16 2007 +0200
     1.3 @@ -206,8 +206,8 @@
     1.4       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
     1.5       types = merge_alists types1 types2,
     1.6       realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
     1.7 -     defs = gen_merge_lists Thm.eq_thm defs1 defs2,
     1.8 -     expand = merge_lists expand1 expand2,
     1.9 +     defs = Library.merge Thm.eq_thm (defs1, defs2),
    1.10 +     expand = Library.merge (op =) (expand1, expand2),
    1.11       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    1.12  
    1.13    fun print _ _ = ();
     2.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML	Fri Apr 13 15:43:25 2007 +0200
     2.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML	Fri Apr 13 16:40:16 2007 +0200
     2.3 @@ -187,7 +187,7 @@
     2.4    in rew' end;
     2.5  
     2.6  fun rprocs b = [("Pure/meta_equality", rew b)];
     2.7 -val _ = Context.add_setup (Proofterm.add_prf_rprocs (rprocs false));
     2.8 +val _ = Context.add_setup (fold Proofterm.add_prf_rproc (rprocs false));
     2.9  
    2.10  
    2.11  (**** apply rewriting function to all terms in proof ****)
     3.1 --- a/src/Pure/proofterm.ML	Fri Apr 13 15:43:25 2007 +0200
     3.2 +++ b/src/Pure/proofterm.ML	Fri Apr 13 16:40:16 2007 +0200
     3.3 @@ -103,8 +103,8 @@
     3.4    val get_name : term list -> term -> proof -> string
     3.5  
     3.6    (** rewriting on proof terms **)
     3.7 -  val add_prf_rrules : (proof * proof) list -> theory -> theory
     3.8 -  val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list ->
     3.9 +  val add_prf_rrule : proof * proof -> theory -> theory
    3.10 +  val add_prf_rproc : string * (Term.typ list -> proof -> proof option) ->
    3.11      theory -> theory
    3.12    val rewrite_proof : theory -> (proof * proof) list *
    3.13      (string * (typ list -> proof -> proof option)) list -> proof -> proof
    3.14 @@ -286,14 +286,14 @@
    3.15  
    3.16    in mapph end;
    3.17  
    3.18 -fun same f x =
    3.19 +fun same eq f x =
    3.20    let val x' = f x
    3.21 -  in if x = x' then raise SAME else x' end;
    3.22 +  in if eq (x, x') then raise SAME else x' end;
    3.23  
    3.24  fun map_proof_terms f g =
    3.25    map_proof_terms_option
    3.26 -   (fn t => SOME (same f t) handle SAME => NONE)
    3.27 -   (fn T => SOME (same g T) handle SAME => NONE);
    3.28 +   (fn t => SOME (same (op =) f t) handle SAME => NONE)
    3.29 +   (fn T => SOME (same (op =) g T) handle SAME => NONE);
    3.30  
    3.31  fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
    3.32    | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
    3.33 @@ -366,7 +366,7 @@
    3.34  fun prf_incr_bv' incP inct Plev tlev (PBound i) =
    3.35        if i >= Plev then PBound (i+incP) else raise SAME
    3.36    | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
    3.37 -      (AbsP (a, apsome' (same (incr_bv' inct tlev)) t,
    3.38 +      (AbsP (a, apsome' (same (op =) (incr_bv' inct tlev)) t,
    3.39           prf_incr_bv incP inct (Plev+1) tlev body) handle SAME =>
    3.40             AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
    3.41    | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
    3.42 @@ -376,7 +376,7 @@
    3.43         handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
    3.44    | prf_incr_bv' incP inct Plev tlev (prf % t) =
    3.45        (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t
    3.46 -       handle SAME => prf % apsome' (same (incr_bv' inct tlev)) t)
    3.47 +       handle SAME => prf % apsome' (same (op =) (incr_bv' inct tlev)) t)
    3.48    | prf_incr_bv' _ _ _ _ _ = raise SAME
    3.49  and prf_incr_bv incP inct Plev tlev prf =
    3.50        (prf_incr_bv' incP inct Plev tlev prf handle SAME => prf);
    3.51 @@ -683,19 +683,19 @@
    3.52      fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
    3.53  
    3.54      fun lift' Us Ts (Abst (s, T, prf)) =
    3.55 -          (Abst (s, apsome' (same (Logic.incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
    3.56 +          (Abst (s, apsome' (same (op =) (Logic.incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
    3.57             handle SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
    3.58        | lift' Us Ts (AbsP (s, t, prf)) =
    3.59 -          (AbsP (s, apsome' (same (lift'' Us Ts)) t, lifth' Us Ts prf)
    3.60 +          (AbsP (s, apsome' (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf)
    3.61             handle SAME => AbsP (s, t, lift' Us Ts prf))
    3.62        | lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t
    3.63 -          handle SAME => prf % apsome' (same (lift'' Us Ts)) t)
    3.64 +          handle SAME => prf % apsome' (same (op =) (lift'' Us Ts)) t)
    3.65        | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
    3.66            handle SAME => prf1 %% lift' Us Ts prf2)
    3.67        | lift' _ _ (PThm (s, prf, prop, Ts)) =
    3.68 -          PThm (s, prf, prop, apsome' (same (map (Logic.incr_tvar inc))) Ts)
    3.69 +          PThm (s, prf, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    3.70        | lift' _ _ (PAxm (s, prop, Ts)) =
    3.71 -          PAxm (s, prop, apsome' (same (map (Logic.incr_tvar inc))) Ts)
    3.72 +          PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    3.73        | lift' _ _ _ = raise SAME
    3.74      and lifth' Us Ts prf = (lift' Us Ts prf handle SAME => prf);
    3.75  
    3.76 @@ -1186,20 +1186,17 @@
    3.77    val empty = ([], []);
    3.78    val copy = I;
    3.79    val extend = I;
    3.80 -  fun merge _ ((rules1, procs1), (rules2, procs2)) =
    3.81 -    (merge_lists rules1 rules2, merge_alists procs1 procs2);
    3.82 +  fun merge _ ((rules1, procs1) : T, (rules2, procs2)) =
    3.83 +    (Library.merge (op =) (rules1, rules2),
    3.84 +      AList.merge (op =) (K true) (procs1, procs2));
    3.85    fun print _ _ = ();
    3.86  end);
    3.87  
    3.88  val init_data = ProofData.init;
    3.89  
    3.90 -fun add_prf_rrules rs thy =
    3.91 -  let val r = ProofData.get thy
    3.92 -  in ProofData.put (rs @ fst r, snd r) thy end;
    3.93 +fun add_prf_rrule r = (ProofData.map o apfst) (insert (op =) r);
    3.94  
    3.95 -fun add_prf_rprocs ps thy =
    3.96 -  let val r = ProofData.get thy
    3.97 -  in ProofData.put (fst r, ps @ snd r) thy end;
    3.98 +fun add_prf_rproc p = (ProofData.map o apsnd) (AList.update (op =) p);
    3.99  
   3.100  fun thm_proof thy name hyps prop prf =
   3.101    let