added dest_mss, merge_mss;
authorwenzelm
Tue Jul 22 18:45:43 1997 +0200 (1997-07-22)
changeset 35502c833cb21f8d
parent 3549 e8c8d76810a6
child 3551 7c013a617813
added dest_mss, merge_mss;
fixed matching of simproc lhss;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Tue Jul 22 17:52:47 1997 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Jul 22 18:45:43 1997 +0200
     1.3 @@ -140,18 +140,21 @@
     1.4      int -> thm -> thm Sequence.seq
     1.5  
     1.6    (*meta simplification*)
     1.7 +  exception SIMPLIFIER of string * thm
     1.8    type meta_simpset
     1.9 -  exception SIMPLIFIER of string * thm
    1.10 +  val dest_mss		: meta_simpset ->
    1.11 +    {simps: thm list, congs: thm list, procs: (string * cterm list) list}
    1.12    val empty_mss         : meta_simpset
    1.13 +  val merge_mss		: meta_simpset * meta_simpset -> meta_simpset
    1.14    val add_simps         : meta_simpset * thm list -> meta_simpset
    1.15    val del_simps         : meta_simpset * thm list -> meta_simpset
    1.16    val mss_of            : thm list -> meta_simpset
    1.17    val add_congs         : meta_simpset * thm list -> meta_simpset
    1.18    val del_congs         : meta_simpset * thm list -> meta_simpset
    1.19    val add_simprocs	: meta_simpset *
    1.20 -    (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
    1.21 +    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
    1.22    val del_simprocs	: meta_simpset *
    1.23 -    (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
    1.24 +    (string * cterm list * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset
    1.25    val add_prems         : meta_simpset * thm list -> meta_simpset
    1.26    val prems_of_mss      : meta_simpset -> thm list
    1.27    val set_mk_rews       : meta_simpset * (thm -> thm list) -> meta_simpset
    1.28 @@ -164,7 +167,7 @@
    1.29    val invoke_oracle     : theory * Sign.sg * exn -> thm
    1.30  end;
    1.31  
    1.32 -structure Thm : THM =
    1.33 +structure Thm: THM =
    1.34  struct
    1.35  
    1.36  (*** Certified terms and types ***)
    1.37 @@ -1443,12 +1446,20 @@
    1.38  
    1.39  type rrule = {thm: thm, lhs: term, perm: bool};
    1.40  type cong = {thm: thm, lhs: term};
    1.41 -type simproc = (Sign.sg -> term -> thm option) * stamp;
    1.42 +type simproc = {name: string, proc: Sign.sg -> term -> thm option, lhs: cterm, id: stamp};
    1.43  
    1.44 -fun eq_rrule ({thm = Thm{prop = p1, ...}, ...}: rrule,
    1.45 +fun eq_rrule ({thm = Thm {prop = p1, ...}, ...}: rrule,
    1.46    {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2;
    1.47  
    1.48 -val eq_simproc = eq_snd;
    1.49 +fun eq_cong ({thm = Thm {prop = p1, ...}, ...}: cong,
    1.50 +  {thm = Thm {prop = p2, ...}, ...}: cong) = p1 aconv p2;
    1.51 +
    1.52 +fun eq_prem (Thm {prop = p1, ...}, Thm {prop = p2, ...}) = p1 aconv p2;
    1.53 +
    1.54 +fun eq_simproc ({id = s1, ...}:simproc, {id = s2, ...}:simproc) = (s1 = s2);
    1.55 +
    1.56 +fun mk_simproc (name, proc, lhs, id) =
    1.57 +  {name = name, proc = proc, lhs = lhs, id = id};
    1.58  
    1.59  
    1.60  (* datatype mss *)
    1.61 @@ -1487,6 +1498,33 @@
    1.62  
    1.63  (** simpset operations **)
    1.64  
    1.65 +(* dest_mss *)
    1.66 +
    1.67 +fun dest_mss (Mss {rules, congs, procs, ...}) =
    1.68 +  {simps = map (fn (_, {thm, ...}) => thm) (Net.dest rules),
    1.69 +   congs = map (fn (_, {thm, ...}) => thm) congs,
    1.70 +   procs =
    1.71 +     map (fn (_, {name, lhs, id, ...}) => ((name, lhs), id)) (Net.dest procs)
    1.72 +     |> partition_eq eq_snd
    1.73 +     |> map (fn ps => (#1 (#1 (hd ps)), map (#2 o #1) ps))};
    1.74 +
    1.75 +
    1.76 +(* merge_mss *)		(*NOTE: ignores mk_rews and termless of 2nd mss*)
    1.77 +
    1.78 +fun merge_mss
    1.79 + (Mss {rules = rules1, congs = congs1, procs = procs1, bounds = bounds1,
    1.80 +    prems = prems1, mk_rews, termless},
    1.81 +  Mss {rules = rules2, congs = congs2, procs = procs2, bounds = bounds2,
    1.82 +    prems = prems2, ...}) =
    1.83 +      mk_mss
    1.84 +       (Net.merge (rules1, rules2, eq_rrule),
    1.85 +        generic_merge (eq_cong o pairself snd) I I congs1 congs2,
    1.86 +        Net.merge (procs1, procs2, eq_simproc),
    1.87 +        merge_lists bounds1 bounds2,
    1.88 +        generic_merge eq_prem I I prems1 prems2,
    1.89 +        mk_rews, termless);
    1.90 +
    1.91 +
    1.92  (* mk_rrule *)
    1.93  
    1.94  fun vperm (Var _, Var _) = true
    1.95 @@ -1599,25 +1637,31 @@
    1.96  
    1.97  (* add_simprocs *)
    1.98  
    1.99 -fun add_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   1.100 -    (sign, lhs, proc, id)) =
   1.101 -  (trace_term "Adding simplification procedure for:" sign lhs;
   1.102 +fun add_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   1.103 +    (name, lhs as Cterm {sign, t, ...}, proc, id)) =
   1.104 +  (trace_term ("Adding simplification procedure " ^ name ^ " for:") sign t;
   1.105      mk_mss (rules, congs,
   1.106 -      Net.insert_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.INSERT =>
   1.107 -        (trace_warning "ignored duplicate"; procs),
   1.108 +      Net.insert_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.109 +        handle Net.INSERT => (trace_warning "ignored duplicate"; procs),
   1.110          bounds, prems, mk_rews, termless));
   1.111  
   1.112 +fun add_simproc (mss, (name, lhss, proc, id)) =
   1.113 +  foldl add_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   1.114 +
   1.115  val add_simprocs = foldl add_simproc;
   1.116  
   1.117  
   1.118  (* del_simprocs *)
   1.119  
   1.120 -fun del_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   1.121 -    (sign:Sign.sg, lhs, proc, id)) =
   1.122 +fun del_proc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless},
   1.123 +    (name, lhs as Cterm {t, ...}, proc, id)) =
   1.124    mk_mss (rules, congs,
   1.125 -    Net.delete_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.DELETE =>
   1.126 -      (trace_warning "simplification procedure not in simpset"; procs),
   1.127 -          bounds, prems, mk_rews, termless);
   1.128 +    Net.delete_term ((t, mk_simproc (name, proc, lhs, id)), procs, eq_simproc)
   1.129 +      handle Net.DELETE => (trace_warning "simplification procedure not in simpset"; procs),
   1.130 +      bounds, prems, mk_rews, termless);
   1.131 +
   1.132 +fun del_simproc (mss, (name, lhss, proc, id)) =
   1.133 +  foldl del_proc (mss, map (fn lhs => (name, lhs, proc, id)) lhss);
   1.134  
   1.135  val del_simprocs = foldl del_simproc;
   1.136  
   1.137 @@ -1711,12 +1755,14 @@
   1.138      (1) beta reduction
   1.139      (2) unconditional rewrite rules
   1.140      (3) conditional rewrite rules
   1.141 -    (4) simplification procedures		(* FIXME (un-)conditional !! *)
   1.142 +    (4) simplification procedures
   1.143  *)
   1.144  
   1.145  fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) 
   1.146               (shypst,hypst,maxt,t,ders) =
   1.147 -  let fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
   1.148 +  let
   1.149 +      val tsigt = #tsig(Sign.rep_sg signt);
   1.150 +      fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
   1.151          let val unit = if Sign.subsig(sign,signt) then ()
   1.152                    else (trace_thm_warning "rewrite rule from different theory"
   1.153                            thm;
   1.154 @@ -1725,7 +1771,7 @@
   1.155                          else Logic.incr_indexes([],maxt+1) prop;
   1.156              val rlhs = if maxt = ~1 then lhs
   1.157                         else fst(Logic.dest_equals(Logic.strip_imp_concl rprop))
   1.158 -            val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,t)
   1.159 +            val insts = Pattern.match tsigt (rlhs,t);
   1.160              val prop' = ren_inst(insts,rprop,rlhs,t);
   1.161              val hyps' = union_term(hyps,hypst);
   1.162              val shyps' = add_insts_sorts (insts, union_sort(shyps,shypst));
   1.163 @@ -1734,7 +1780,7 @@
   1.164                              t = prop',
   1.165                              T = propT,
   1.166                              maxidx = maxidx'}
   1.167 -            val der' = infer_derivs (RewriteC ct', [der])	(* FIXME fix!? *)
   1.168 +            val der' = infer_derivs (RewriteC ct', [der]);
   1.169              val thm' = Thm{sign = signt, 
   1.170                             der = der',
   1.171                             shyps = shyps',
   1.172 @@ -1756,6 +1802,7 @@
   1.173          | rews (rrule :: rrules) =
   1.174              let val opt = rew rrule handle Pattern.MATCH => None
   1.175              in case opt of None => rews rrules | some => some end;
   1.176 +
   1.177        fun sort_rrules rrs = let
   1.178          fun is_simple {thm as Thm{prop,...}, lhs, perm} = case prop of 
   1.179                                          Const("==",_) $ _ $ _ => true
   1.180 @@ -1767,18 +1814,20 @@
   1.181        in sort rrs ([],[]) 
   1.182        end
   1.183  
   1.184 -      fun proc_rews _ [] = None
   1.185 -        | proc_rews eta_t ((f, _) :: fs) =
   1.186 -            (case f signt eta_t of
   1.187 -              None => proc_rews eta_t fs
   1.188 -            | Some raw_thm =>
   1.189 -                (trace_thm "Proved rewrite rule: " raw_thm;
   1.190 -                 (case rews (mk_procrule raw_thm) of
   1.191 -                   None => proc_rews eta_t fs
   1.192 -                 | some => some)));
   1.193 +      fun proc_rews _ ([]:simproc list) = None
   1.194 +        | proc_rews eta_t ({name, proc, lhs = Cterm {t = plhs, ...}, ...} :: ps) =
   1.195 +            if Pattern.matches tsigt (plhs, t) then
   1.196 +              (case proc signt eta_t of
   1.197 +                None => proc_rews eta_t ps
   1.198 +              | Some raw_thm =>
   1.199 +                 (trace_thm ("Procedure" ^ name ^ " proved rewrite rule:") raw_thm;
   1.200 +                   (case rews (mk_procrule raw_thm) of
   1.201 +                     None => proc_rews eta_t ps
   1.202 +                   | some => some)))
   1.203 +            else proc_rews eta_t ps;
   1.204    in
   1.205      (case t of
   1.206 -      Abs (_, _, body) $ u =>		(* FIXME bug!? (because of beta/eta overlap) *)
   1.207 +      Abs (_, _, body) $ u =>
   1.208          Some (shypst, hypst, maxt, subst_bound (u, body), ders)
   1.209       | _ =>
   1.210        (case rews (sort_rrules (Net.match_term rules t)) of
   1.211 @@ -1809,7 +1858,7 @@
   1.212                        T = propT,
   1.213                        maxidx = maxidx'}
   1.214        val thm' = Thm{sign = signt, 
   1.215 -                     der = infer_derivs (CongC ct', [der]),	(* FIXME fix!? *)
   1.216 +                     der = infer_derivs (CongC ct', [der]),
   1.217                       shyps = shyps',
   1.218                       hyps = union_term(hyps,hypst),
   1.219                       prop = prop',