src/Pure/proofterm.ML
changeset 22662 3e492ba59355
parent 21646 c07b5b0e8492
child 22846 fb79144af9a3
     1.1 --- a/src/Pure/proofterm.ML	Fri Apr 13 15:43:25 2007 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Fri Apr 13 16:40:16 2007 +0200
     1.3 @@ -103,8 +103,8 @@
     1.4    val get_name : term list -> term -> proof -> string
     1.5  
     1.6    (** rewriting on proof terms **)
     1.7 -  val add_prf_rrules : (proof * proof) list -> theory -> theory
     1.8 -  val add_prf_rprocs : (string * (Term.typ list -> proof -> proof option)) list ->
     1.9 +  val add_prf_rrule : proof * proof -> theory -> theory
    1.10 +  val add_prf_rproc : string * (Term.typ list -> proof -> proof option) ->
    1.11      theory -> theory
    1.12    val rewrite_proof : theory -> (proof * proof) list *
    1.13      (string * (typ list -> proof -> proof option)) list -> proof -> proof
    1.14 @@ -286,14 +286,14 @@
    1.15  
    1.16    in mapph end;
    1.17  
    1.18 -fun same f x =
    1.19 +fun same eq f x =
    1.20    let val x' = f x
    1.21 -  in if x = x' then raise SAME else x' end;
    1.22 +  in if eq (x, x') then raise SAME else x' end;
    1.23  
    1.24  fun map_proof_terms f g =
    1.25    map_proof_terms_option
    1.26 -   (fn t => SOME (same f t) handle SAME => NONE)
    1.27 -   (fn T => SOME (same g T) handle SAME => NONE);
    1.28 +   (fn t => SOME (same (op =) f t) handle SAME => NONE)
    1.29 +   (fn T => SOME (same (op =) g T) handle SAME => NONE);
    1.30  
    1.31  fun fold_proof_terms f g (Abst (_, SOME T, prf)) = g T #> fold_proof_terms f g prf
    1.32    | fold_proof_terms f g (Abst (_, NONE, prf)) = fold_proof_terms f g prf
    1.33 @@ -366,7 +366,7 @@
    1.34  fun prf_incr_bv' incP inct Plev tlev (PBound i) =
    1.35        if i >= Plev then PBound (i+incP) else raise SAME
    1.36    | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
    1.37 -      (AbsP (a, apsome' (same (incr_bv' inct tlev)) t,
    1.38 +      (AbsP (a, apsome' (same (op =) (incr_bv' inct tlev)) t,
    1.39           prf_incr_bv incP inct (Plev+1) tlev body) handle SAME =>
    1.40             AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
    1.41    | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
    1.42 @@ -376,7 +376,7 @@
    1.43         handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
    1.44    | prf_incr_bv' incP inct Plev tlev (prf % t) =
    1.45        (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t
    1.46 -       handle SAME => prf % apsome' (same (incr_bv' inct tlev)) t)
    1.47 +       handle SAME => prf % apsome' (same (op =) (incr_bv' inct tlev)) t)
    1.48    | prf_incr_bv' _ _ _ _ _ = raise SAME
    1.49  and prf_incr_bv incP inct Plev tlev prf =
    1.50        (prf_incr_bv' incP inct Plev tlev prf handle SAME => prf);
    1.51 @@ -683,19 +683,19 @@
    1.52      fun lift'' Us Ts t = strip_abs Ts (Logic.incr_indexes (Us, inc) (mk_abs Ts t));
    1.53  
    1.54      fun lift' Us Ts (Abst (s, T, prf)) =
    1.55 -          (Abst (s, apsome' (same (Logic.incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
    1.56 +          (Abst (s, apsome' (same (op =) (Logic.incr_tvar inc)) T, lifth' Us (dummyT::Ts) prf)
    1.57             handle SAME => Abst (s, T, lift' Us (dummyT::Ts) prf))
    1.58        | lift' Us Ts (AbsP (s, t, prf)) =
    1.59 -          (AbsP (s, apsome' (same (lift'' Us Ts)) t, lifth' Us Ts prf)
    1.60 +          (AbsP (s, apsome' (same (op =) (lift'' Us Ts)) t, lifth' Us Ts prf)
    1.61             handle SAME => AbsP (s, t, lift' Us Ts prf))
    1.62        | lift' Us Ts (prf % t) = (lift' Us Ts prf % Option.map (lift'' Us Ts) t
    1.63 -          handle SAME => prf % apsome' (same (lift'' Us Ts)) t)
    1.64 +          handle SAME => prf % apsome' (same (op =) (lift'' Us Ts)) t)
    1.65        | lift' Us Ts (prf1 %% prf2) = (lift' Us Ts prf1 %% lifth' Us Ts prf2
    1.66            handle SAME => prf1 %% lift' Us Ts prf2)
    1.67        | lift' _ _ (PThm (s, prf, prop, Ts)) =
    1.68 -          PThm (s, prf, prop, apsome' (same (map (Logic.incr_tvar inc))) Ts)
    1.69 +          PThm (s, prf, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    1.70        | lift' _ _ (PAxm (s, prop, Ts)) =
    1.71 -          PAxm (s, prop, apsome' (same (map (Logic.incr_tvar inc))) Ts)
    1.72 +          PAxm (s, prop, apsome' (same (op =) (map (Logic.incr_tvar inc))) Ts)
    1.73        | lift' _ _ _ = raise SAME
    1.74      and lifth' Us Ts prf = (lift' Us Ts prf handle SAME => prf);
    1.75  
    1.76 @@ -1186,20 +1186,17 @@
    1.77    val empty = ([], []);
    1.78    val copy = I;
    1.79    val extend = I;
    1.80 -  fun merge _ ((rules1, procs1), (rules2, procs2)) =
    1.81 -    (merge_lists rules1 rules2, merge_alists procs1 procs2);
    1.82 +  fun merge _ ((rules1, procs1) : T, (rules2, procs2)) =
    1.83 +    (Library.merge (op =) (rules1, rules2),
    1.84 +      AList.merge (op =) (K true) (procs1, procs2));
    1.85    fun print _ _ = ();
    1.86  end);
    1.87  
    1.88  val init_data = ProofData.init;
    1.89  
    1.90 -fun add_prf_rrules rs thy =
    1.91 -  let val r = ProofData.get thy
    1.92 -  in ProofData.put (rs @ fst r, snd r) thy end;
    1.93 +fun add_prf_rrule r = (ProofData.map o apfst) (insert (op =) r);
    1.94  
    1.95 -fun add_prf_rprocs ps thy =
    1.96 -  let val r = ProofData.get thy
    1.97 -  in ProofData.put (fst r, ps @ snd r) thy end;
    1.98 +fun add_prf_rproc p = (ProofData.map o apsnd) (AList.update (op =) p);
    1.99  
   1.100  fun thm_proof thy name hyps prop prf =
   1.101    let