# HG changeset patch # User wenzelm # Date 853422817 -3600 # Node ID 0a7169d89b7a60f0709cfd8795692d3ce86de8ae # Parent ce48daa388a78b12a99e509b597ec6099176f38a added termless parameter; added simplification procedures; diff -r ce48daa388a7 -r 0a7169d89b7a src/Provers/simplifier.ML --- a/src/Provers/simplifier.ML Thu Jan 16 13:44:47 1997 +0100 +++ b/src/Provers/simplifier.ML Thu Jan 16 14:53:37 1997 +0100 @@ -8,29 +8,40 @@ TODO: - stamps to identify funs / tacs - merge: fail if incompatible funs + - improve merge *) -infix 4 addsimps addeqcongs addsolver delsimps - setsolver setloop setmksimps setsubgoaler; +infix 4 addsimps addeqcongs addsimprocs delsimprocs addsolver delsimps + setsolver setloop setmksimps settermless setsubgoaler; signature SIMPLIFIER = sig + type simproc + val mk_simproc: string -> cterm list -> (Sign.sg -> term -> thm option) -> simproc + val name_of_simproc: simproc -> string + val conv_prover: (term * term -> term) -> thm -> (thm -> thm) + -> tactic -> (int -> tactic) -> Sign.sg -> term -> term -> thm (* FIXME move?, rename? *) type simpset val empty_ss: simpset - val rep_ss: simpset -> {simps: thm list, congs: thm list} + val rep_ss: simpset -> {simps: thm list, procs: string list, congs: thm list} val prems_of_ss: simpset -> thm list val setloop: simpset * (int -> tactic) -> simpset val setsolver: simpset * (thm list -> int -> tactic) -> simpset val addsolver: simpset * (thm list -> int -> tactic) -> simpset val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset val setmksimps: simpset * (thm -> thm list) -> simpset + val settermless: simpset * (term * term -> bool) -> simpset val addsimps: simpset * thm list -> simpset val delsimps: simpset * thm list -> simpset + val addsimprocs: simpset * simproc list -> simpset + val delsimprocs: simpset * simproc list -> simpset val addeqcongs: simpset * thm list -> simpset val merge_ss: simpset * simpset -> simpset val simpset: simpset ref val Addsimps: thm list -> unit val Delsimps: thm list -> unit + val Addsimprocs: simproc list -> unit + val Delsimprocs: simproc list -> unit val simp_tac: simpset -> int -> tactic val asm_simp_tac: simpset -> int -> tactic val full_simp_tac: simpset -> int -> tactic @@ -45,6 +56,51 @@ structure Simplifier: SIMPLIFIER = struct + +(** simplification procedures **) + +(* datatype simproc *) + +datatype simproc = + Simproc of { + name: string, + procs: (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list} + +(* FIXME stamps!? *) +fun eq_simproc (Simproc {name = name1, ...}, Simproc {name = name2, ...}) = + (name1 = name2); + +fun mk_simproc name lhss proc = + let + fun mk_proc lhs = + (#sign (Thm.rep_cterm lhs), Logic.varify (term_of lhs), proc, stamp ()); + in + Simproc {name = name, procs = map mk_proc lhss} + end; + +fun name_of_simproc (Simproc {name, ...}) = name; + + +(* generic conversion prover *) (* FIXME move?, rename? *) + +fun conv_prover mk_eqv eqv_refl mk_meta_eq expand_tac norm_tac sg t u = + let + val X = Free (gensym "X.", fastype_of t); + val goal = Logic.mk_implies (mk_eqv (X, t), mk_eqv (X, u)); + val pre_result = + prove_goalw_cterm [] (cterm_of sg goal) (*goal: X=t ==> X=u*) + (fn prems => [ + expand_tac, (*expand u*) + ALLGOALS (cut_facts_tac prems), + ALLGOALS norm_tac]); (*normalize both t and u*) + in + mk_meta_eq (eqv_refl RS pre_result) (*final result: t==u*) + end + handle ERROR => error ("The error(s) above occurred while trying to prove " ^ + (string_of_cterm (cterm_of sg (mk_eqv (t, u))))); + + + (** simplification sets **) (* type simpset *) @@ -53,82 +109,106 @@ Simpset of { mss: meta_simpset, simps: thm list, + procs: simproc list, congs: thm list, subgoal_tac: simpset -> int -> tactic, finish_tac: thm list -> int -> tactic, loop_tac: int -> tactic}; -fun make_ss (mss, simps, congs, subgoal_tac, finish_tac, loop_tac) = - Simpset {mss = mss, simps = simps, congs = congs, +fun make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac) = + Simpset {mss = mss, simps = simps, procs = procs, congs = congs, subgoal_tac = subgoal_tac, finish_tac = finish_tac, loop_tac = loop_tac}; val empty_ss = - make_ss (Thm.empty_mss, [], [], K (K no_tac), K (K no_tac), K no_tac); + make_ss (Thm.empty_mss, [], [], [], K (K no_tac), K (K no_tac), K no_tac); -fun rep_ss (Simpset {simps, congs, ...}) = {simps = simps, congs = congs}; +fun rep_ss (Simpset {simps, procs, congs, ...}) = + {simps = simps, procs = map name_of_simproc procs, congs = congs}; fun prems_of_ss (Simpset {mss, ...}) = Thm.prems_of_mss mss; (* extend simpsets *) -fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac = _}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac = _}) setloop loop_tac = - make_ss (mss, simps, congs, subgoal_tac, finish_tac, DETERM o loop_tac); + make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, DETERM o loop_tac); -fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac = _, loop_tac}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac = _, loop_tac}) setsolver finish_tac = - make_ss (mss, simps, congs, subgoal_tac, finish_tac, loop_tac); + make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); -fun (Simpset {mss, simps, congs, subgoal_tac, loop_tac, finish_tac}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac, loop_tac, finish_tac}) addsolver tac = - make_ss (mss, simps, congs, subgoal_tac, + make_ss (mss, simps, procs, congs, subgoal_tac, fn hyps => finish_tac hyps ORELSE' tac hyps, loop_tac); -fun (Simpset {mss, simps, congs, subgoal_tac = _, finish_tac, loop_tac}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac = _, finish_tac, loop_tac}) setsubgoaler subgoal_tac = - make_ss (mss, simps, congs, subgoal_tac, finish_tac, loop_tac); + make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); -fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) setmksimps mk_simps = - make_ss (Thm.set_mk_rews (mss, mk_simps), simps, congs, + make_ss (Thm.set_mk_rews (mss, mk_simps), simps, procs, congs, subgoal_tac, finish_tac, loop_tac); -fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) + settermless termless = + make_ss (Thm.set_termless (mss, termless), simps, procs, congs, + subgoal_tac, finish_tac, loop_tac); + +fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) addsimps rews = let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in make_ss (Thm.add_simps (mss, rews'), rews' @ simps, - congs, subgoal_tac, finish_tac, loop_tac) + procs, congs, subgoal_tac, finish_tac, loop_tac) end; -fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) delsimps rews = let val rews' = flat (map (Thm.mk_rews_of_mss mss) rews) in make_ss (Thm.del_simps (mss, rews'), foldl (gen_rem eq_thm) (simps, rews'), - congs, subgoal_tac, finish_tac, loop_tac) + procs, congs, subgoal_tac, finish_tac, loop_tac) end; -fun (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}) +fun (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) addeqcongs newcongs = make_ss (Thm.add_congs (mss, newcongs), - simps, newcongs @ congs, subgoal_tac, finish_tac, loop_tac); + simps, procs, newcongs @ congs, subgoal_tac, finish_tac, loop_tac); + +fun addsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}), + simproc as Simproc {name = _, procs = procs'}) = + make_ss (Thm.add_simprocs (mss, procs'), + simps, gen_ins eq_simproc (simproc, procs), + congs, subgoal_tac, finish_tac, loop_tac); + +val op addsimprocs = foldl addsimproc; + +fun delsimproc ((Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}), + simproc as Simproc {name = _, procs = procs'}) = + make_ss (Thm.del_simprocs (mss, procs'), + simps, gen_rem eq_simproc (procs, simproc), + congs, subgoal_tac, finish_tac, loop_tac); + +val op delsimprocs = foldl delsimproc; (* merge simpsets *) -(*prefers first simpset*) -fun merge_ss (Simpset {mss, simps, congs, subgoal_tac, finish_tac, loop_tac}, - Simpset {simps = simps2, congs = congs2, ...}) = +(*prefers first simpset (FIXME improve?)*) +fun merge_ss (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}, + Simpset {simps = simps2, procs = procs2, congs = congs2, ...}) = let val simps' = gen_union eq_thm (simps, simps2); + val procs' = gen_union eq_simproc (procs, procs2); val congs' = gen_union eq_thm (congs, congs2); val mss' = Thm.set_mk_rews (empty_mss, Thm.mk_rews_of_mss mss); val mss' = Thm.add_simps (mss', simps'); val mss' = Thm.add_congs (mss', congs'); in - make_ss (mss', simps', congs', subgoal_tac, finish_tac, loop_tac) + make_ss (mss', simps', procs', congs', subgoal_tac, finish_tac, loop_tac) end; @@ -139,6 +219,9 @@ fun Addsimps rews = (simpset := ! simpset addsimps rews); fun Delsimps rews = (simpset := ! simpset delsimps rews); +fun Addsimprocs procs = (simpset := ! simpset addsimprocs procs); +fun Delsimprocs procs = (simpset := ! simpset delsimprocs procs); + (** simplification tactics **) @@ -148,11 +231,10 @@ tac THEN STATE (fn state1 => tacf (nprems_of state1 - nprems_of state0))); fun gen_simp_tac mode = - fn (Simpset{mss,simps,congs,subgoal_tac,finish_tac,loop_tac}) => + fn (Simpset {mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac}) => let fun solve_all_tac mss = - let val ss = Simpset{mss=mss,simps=simps,congs=congs, - subgoal_tac=subgoal_tac, - finish_tac=finish_tac, loop_tac=loop_tac} + let val ss = + make_ss (mss, simps, procs, congs, subgoal_tac, finish_tac, loop_tac); val solve1_tac = NEWSUBGOALS (subgoal_tac ss 1) (fn n => if n<0 then all_tac else no_tac) diff -r ce48daa388a7 -r 0a7169d89b7a src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Jan 16 13:44:47 1997 +0100 +++ b/src/Pure/thm.ML Thu Jan 16 14:53:37 1997 +0100 @@ -144,10 +144,15 @@ val del_simps : meta_simpset * thm list -> meta_simpset val mss_of : thm list -> meta_simpset val add_congs : meta_simpset * thm list -> meta_simpset + val add_simprocs : meta_simpset * + (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset + val del_simprocs : meta_simpset * + (Sign.sg * term * (Sign.sg -> term -> thm option) * stamp) list -> meta_simpset val add_prems : meta_simpset * thm list -> meta_simpset val prems_of_mss : meta_simpset -> thm list val set_mk_rews : meta_simpset * (thm -> thm list) -> meta_simpset val mk_rews_of_mss : meta_simpset -> thm -> thm list + val set_termless : meta_simpset * (term * term -> bool) -> meta_simpset val trace_simp : bool ref val rewrite_cterm : bool * bool -> meta_simpset -> (meta_simpset -> thm -> thm option) -> cterm -> thm @@ -236,6 +241,8 @@ T = ty --> T2, maxidx=Int.max(maxidx1, maxidx2)} | cabs _ _ = raise CTERM "cabs: first arg is not a free variable"; + + (** read cterms **) (*exception ERROR*) (*read term, infer types, certify term*) @@ -311,7 +318,7 @@ | Bicompose of bool * bool * int * int * Envir.env | Flexflex_rule of Envir.env (*identifies unifier chosen*) (*other derived rules*) - | Class_triv of theory * class (*derived rule????*) + | Class_triv of theory * class | VarifyT | FreezeT (*for the simplifier*) @@ -359,6 +366,7 @@ else make_min_infer (squash_derivs ders); + (*** Meta theorems ***) datatype thm = Thm of @@ -572,6 +580,7 @@ prop = Term.compress_term prop}; + (*** Meta rules ***) (*Check that term does not contain same var with different typing/sorting. @@ -1372,194 +1381,230 @@ -(*** Meta simp sets ***) - -type rrule = {thm:thm, lhs:term, perm:bool}; -type cong = {thm:thm, lhs:term}; -datatype meta_simpset = - Mss of {net:rrule Net.net, congs:(string * cong)list, bounds:string list, - prems: thm list, mk_rews: thm -> thm list}; +(*** Meta Simplification ***) -(*A "mss" contains data needed during conversion: - net: discrimination net of rewrite rules - congs: association list of congruence rules - bounds: names of bound variables already used; - for generating new names when rewriting under lambda abstractions - mk_rews: used when local assumptions are added -*) - -val empty_mss = Mss{net = Net.empty, congs = [], bounds=[], prems = [], - mk_rews = K[]}; +(** diagnostics **) exception SIMPLIFIER of string * thm; -fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); - +fun prtm a sign t = (writeln a; writeln (Sign.string_of_term sign t)); fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t)); val trace_simp = ref false; -fun trace_term a sign t = if !trace_simp then prtm a sign t else (); +fun trace_warning a = if ! trace_simp then warning a else (); +fun trace_term a sign t = if ! trace_simp then prtm a sign t else (); +fun trace_term_warning a sign t = if ! trace_simp then prtm_warning a sign t else (); +fun trace_thm a (Thm {sign, prop, ...}) = trace_term a sign prop; +fun trace_thm_warning a (Thm {sign, prop, ...}) = trace_term_warning a sign prop; -fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop; -fun trace_term_warning a sign t = if !trace_simp then prtm_warning a sign t else (); -fun trace_thm_warning a (Thm{sign,prop,...}) = trace_term_warning a sign prop; +(** meta simp sets **) + +(* basic components *) -fun vperm(Var _, Var _) = true - | vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t) - | vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2) - | vperm(t,u) = (t=u); +type rrule = {thm: thm, lhs: term, perm: bool}; +type cong = {thm: thm, lhs: term}; +type simproc = (Sign.sg -> term -> thm option) * stamp; -fun var_perm(t,u) = vperm(t,u) andalso - eq_set_term (term_vars t, term_vars u) +fun eq_rrule ({thm = Thm{prop = p1, ...}, ...}: rrule, + {thm = Thm {prop = p2, ...}, ...}: rrule) = p1 aconv p2; + +val eq_simproc = eq_snd; + + +(* datatype mss *) -(*simple test for looping rewrite*) -fun loops sign prems (lhs,rhs) = - is_Var(lhs) - orelse - (exists (apl(lhs, Logic.occs)) (rhs::prems)) - orelse - (null(prems) andalso - Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); -(* the condition "null(prems)" in the last case is necessary because - conditional rewrites with extra variables in the conditions may terminate - although the rhs is an instance of the lhs. Example: - ?m < ?n ==> f(?n) == f(?m) +(* + A "mss" contains data needed during conversion: + rules: discrimination net of rewrite rules; + congs: association list of congruence rules; + procs: discrimination net of simplification procedures + (functions that prove rewrite rules on the fly); + bounds: names of bound variables already used + (for generating new names when rewriting under lambda abstractions); + prems: current premises; + mk_rews: turns simplification thms into rewrite rules; + termless: relation for ordered rewriting; *) -fun mk_rrule raw_thm = +datatype meta_simpset = + Mss of { + rules: rrule Net.net, + congs: (string * cong) list, + procs: simproc Net.net, + bounds: string list, + prems: thm list, + mk_rews: thm -> thm list, + termless: term * term -> bool}; + +fun mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless) = + Mss {rules = rules, congs = congs, procs = procs, bounds = bounds, + prems = prems, mk_rews = mk_rews, termless = termless}; + +val empty_mss = + mk_mss (Net.empty, [], Net.empty, [], [], K [], Logic.termless); + + + +(** simpset operations **) + +(* mk_rrule *) + +fun vperm (Var _, Var _) = true + | vperm (Abs (_, _, s), Abs (_, _, t)) = vperm (s, t) + | vperm (t1 $ t2, u1 $ u2) = vperm (t1, u1) andalso vperm (t2, u2) + | vperm (t, u) = (t = u); + +fun var_perm (t, u) = + vperm (t, u) andalso eq_set_term (term_vars t, term_vars u); + +(*simple test for looping rewrite*) +fun loops sign prems (lhs, rhs) = + is_Var lhs + orelse + (exists (apl (lhs, Logic.occs)) (rhs :: prems)) + orelse + (null prems andalso + Pattern.matches (#tsig (Sign.rep_sg sign)) (lhs, rhs)); +(*the condition "null prems" in the last case is necessary because + conditional rewrites with extra variables in the conditions may terminate + although the rhs is an instance of the lhs. Example: + ?m < ?n ==> f(?n) == f(?m)*) + +fun mk_rrule (thm as Thm {sign, prop, ...}) = let - val thm = strip_shyps raw_thm; - val Thm{sign,prop,maxidx,...} = thm; - val prems = Logic.strip_imp_prems prop - val concl = Logic.strip_imp_concl prop - val (lhs,_) = Logic.dest_equals concl handle TERM _ => - raise SIMPLIFIER("Rewrite rule not a meta-equality",thm) - val econcl = Pattern.eta_contract concl - val (elhs,erhs) = Logic.dest_equals econcl - val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs) - andalso not(is_Var(elhs)) - in if not((term_vars erhs) subset - (union_term (term_vars elhs, flat(map term_vars prems)))) - then (prtm_warning "extra Var(s) on rhs" sign prop; None) else - if not perm andalso loops sign prems (elhs,erhs) - then (prtm_warning "ignoring looping rewrite rule" sign prop; None) - else Some{thm=thm,lhs=lhs,perm=perm} + val prems = Logic.strip_imp_prems prop; + val concl = Logic.strip_imp_concl prop; + val (lhs, _) = Logic.dest_equals concl handle TERM _ => + raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); + val econcl = Pattern.eta_contract concl; + val (elhs, erhs) = Logic.dest_equals econcl; + val perm = var_perm (elhs, erhs) andalso not (elhs aconv erhs) + andalso not (is_Var elhs); + in + if not ((term_vars erhs) subset + (union_term (term_vars elhs, flat(map term_vars prems)))) then + (prtm_warning "extra Var(s) on rhs" sign prop; None) + else if not perm andalso loops sign prems (elhs, erhs) then + (prtm_warning "ignoring looping rewrite rule" sign prop; None) + else Some {thm = thm, lhs = lhs, perm = perm} end; -local - fun eq({thm=Thm{prop=p1,...},...}:rrule, - {thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2 -in + +(* add_simps *) -fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, - thm as Thm{sign,prop,...}) = - case mk_rrule thm of +fun add_simp + (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, + thm as Thm {sign, prop, ...}) = + (case mk_rrule thm of None => mss - | Some(rrule as {lhs,...}) => + | Some (rrule as {lhs, ...}) => (trace_thm "Adding rewrite rule:" thm; - Mss{net = (Net.insert_term((lhs,rrule),net,eq) - handle Net.INSERT => - (prtm_warning "ignoring duplicate rewrite rule" sign prop; - net)), - congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); - -fun del_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, - thm as Thm{sign,prop,...}) = - case mk_rrule thm of - None => mss - | Some(rrule as {lhs,...}) => - Mss{net = (Net.delete_term((lhs,rrule),net,eq) - handle Net.DELETE => - (prtm_warning "rewrite rule not in simpset" sign prop; - net)), - congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} - -end; + mk_mss (Net.insert_term ((lhs, rrule), rules, eq_rrule) handle Net.INSERT => + (prtm_warning "ignoring duplicate rewrite rule" sign prop; rules), + congs, procs, bounds, prems, mk_rews, termless))); val add_simps = foldl add_simp; + +fun mss_of thms = add_simps (empty_mss, thms); + + +(* del_simps *) + +fun del_simp + (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, + thm as Thm {sign, prop, ...}) = + (case mk_rrule thm of + None => mss + | Some (rrule as {lhs, ...}) => + mk_mss (Net.delete_term ((lhs, rrule), rules, eq_rrule) handle Net.DELETE => + (prtm_warning "rewrite rule not in simpset" sign prop; rules), + congs, procs, bounds, prems, mk_rews, termless)); + val del_simps = foldl del_simp; -fun mss_of thms = add_simps(empty_mss,thms); + +(* congs *) -fun add_cong(Mss{net,congs,bounds,prems,mk_rews},thm) = - let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ => - raise SIMPLIFIER("Congruence not a meta-equality",thm) -(* val lhs = Pattern.eta_contract lhs*) - val (a,_) = dest_Const (head_of lhs) handle TERM _ => - raise SIMPLIFIER("Congruence must start with a constant",thm) - in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, - prems=prems, mk_rews=mk_rews} +fun add_cong (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thm) = + let + val (lhs, _) = Logic.dest_equals (concl_of thm) handle TERM _ => + raise SIMPLIFIER ("Congruence not a meta-equality", thm); +(* val lhs = Pattern.eta_contract lhs; *) + val (a, _) = dest_Const (head_of lhs) handle TERM _ => + raise SIMPLIFIER ("Congruence must start with a constant", thm); + in + mk_mss (rules, (a, {lhs = lhs, thm = thm}) :: congs, procs, bounds, + prems, mk_rews, termless) end; val (op add_congs) = foldl add_cong; -fun add_prems(Mss{net,congs,bounds,prems,mk_rews},thms) = - Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; + +(* add_simprocs *) + +fun add_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, + (sign, lhs, proc, id)) = + (trace_term "Adding simplification procedure for:" sign lhs; + mk_mss (rules, congs, + Net.insert_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.INSERT => + (trace_warning "ignored duplicate"; procs), + bounds, prems, mk_rews, termless)); -fun prems_of_mss(Mss{prems,...}) = prems; +val add_simprocs = foldl add_simproc; + + +(* del_simprocs *) -fun set_mk_rews(Mss{net,congs,bounds,prems,...},mk_rews) = - Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; -fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; +fun del_simproc (mss as Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, + (sign, lhs, proc, id)) = + mk_mss (rules, congs, + Net.delete_term ((lhs, (proc, id)), procs, eq_simproc) handle Net.DELETE => + (trace_warning "simplification procedure not in simpset"; procs), + bounds, prems, mk_rews, termless); + +val del_simprocs = foldl del_simproc; -(*** Meta-level rewriting - uses conversions, omitting proofs for efficiency. See - L C Paulson, A higher-order implementation of rewriting, - Science of Computer Programming 3 (1983), pages 119-149. ***) +(* prems *) + +fun add_prems (Mss {rules, congs, procs, bounds, prems, mk_rews, termless}, thms) = + mk_mss (rules, congs, procs, bounds, thms @ prems, mk_rews, termless); + +fun prems_of_mss (Mss {prems, ...}) = prems; + + +(* mk_rews *) + +fun set_mk_rews + (Mss {rules, congs, procs, bounds, prems, mk_rews = _, termless}, mk_rews) = + mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless); + +fun mk_rews_of_mss (Mss {mk_rews, ...}) = mk_rews; + + +(* termless *) + +fun set_termless + (Mss {rules, congs, procs, bounds, prems, mk_rews, termless = _}, termless) = + mk_mss (rules, congs, procs, bounds, prems, mk_rews, termless); + + + +(** rewriting **) + +(* + Uses conversions, omitting proofs for efficiency. See: + L C Paulson, A higher-order implementation of rewriting, + Science of Computer Programming 3 (1983), pages 119-149. +*) type prover = meta_simpset -> thm -> thm option; type termrec = (Sign.sg * term list) * term; type conv = meta_simpset -> termrec -> termrec; -datatype order = LESS | EQUAL | GREATER; - -fun stringord(a,b:string) = if a 1. size(s) < size(t) or - 2. size(s) = size(t) and s=f(...) and t = g(...) and f let val (f,ts) = strip_comb t and (g,us) = strip_comb u - in case stringord(string_of_hd f, string_of_hd g) of - EQUAL => lextermord(ts,us) - | ord => ord - end - | ord => ord) -and lextermord(t::ts,u::us) = - (case termord(t,u) of - EQUAL => lextermord(ts,us) - | ord => ord) - | lextermord([],[]) = EQUAL - | lextermord _ = error("lextermord"); - -fun termless tu = (termord tu = LESS); - fun check_conv (thm as Thm{shyps,hyps,prop,sign,der,maxidx,...}, prop0, ders) = let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; trace_term "Should have proved" sign prop0; @@ -1587,8 +1632,35 @@ add_typs_sorts (map snd iTs, add_terms_sorts (map snd is, Ss)); -(*Conversion to apply the meta simpset to a term*) -fun rewritec (prover,signt) (mss as Mss{net,...}) +(* mk_procrule *) + +fun mk_procrule (thm as Thm {sign, prop, ...}) = + let + val prems = Logic.strip_imp_prems prop; + val concl = Logic.strip_imp_concl prop; + val (lhs, _) = Logic.dest_equals concl handle TERM _ => + raise SIMPLIFIER ("Rewrite rule not a meta-equality", thm); + val econcl = Pattern.eta_contract concl; + val (elhs, erhs) = Logic.dest_equals econcl; + in + if not ((term_vars erhs) subset + (union_term (term_vars elhs, flat(map term_vars prems)))) then + (prtm_warning "extra Var(s) on rhs" sign prop; []) + else [{thm = thm, lhs = lhs, perm = false}] + end; + + +(* conversion to apply the meta simpset to a term *) + +(* + we try in order: + (1) beta reduction + (2) unconditional rewrite rules + (3) conditional rewrite rules + (4) simplification procedures (* FIXME (un-)conditional !! *) +*) + +fun rewritec (prover,signt) (mss as Mss{rules, procs, mk_rews, termless, ...}) (shypst,hypst,maxt,t,ders) = let val etat = Pattern.eta_contract t; fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} = @@ -1609,7 +1681,7 @@ t = prop', T = propT, maxidx = maxidx'} - val der' = infer_derivs (RewriteC ct', [der]) + val der' = infer_derivs (RewriteC ct', [der]) (* FIXME fix!? *) val thm' = Thm{sign = signt, der = der', shyps = shyps', @@ -1628,7 +1700,7 @@ end fun rews [] = None - | rews (rrule::rrules) = + | rews (rrule :: rrules) = let val opt = rew rrule handle Pattern.MATCH => None in case opt of None => rews rrules | some => some end; fun sort_rrules rrs = let @@ -1641,14 +1713,29 @@ else sort rrs (re1,rr::re2) in sort rrs ([],[]) end - in case etat of - Abs(_,_,body) $ u => Some(shypst, hypst, maxt, - subst_bound (u, body), - ders) - | _ => rews (sort_rrules (Net.match_term net etat)) + + fun proc_rews [] = None + | proc_rews ((f, _) :: fs) = + (case f signt etat of + None => proc_rews fs + | Some raw_thm => + (trace_thm "Proved rewrite rule: " raw_thm; + (case rews (mk_procrule raw_thm) of + None => proc_rews fs + | some => some))); + in + (case etat of + Abs (_, _, body) $ u => (* FIXME bug!? (because of beta/eta overlap) *) + Some (shypst, hypst, maxt, subst_bound (u, body), ders) + | _ => + (case rews (sort_rrules (Net.match_term rules etat)) of + None => proc_rews (Net.match_term procs etat) + | some => some)) end; -(*Conversion to apply a congruence rule to a term*) + +(* conversion to apply a congruence rule to a term *) + fun congc (prover,signt) {thm=cong,lhs=lhs} (shypst,hypst,maxt,t,ders) = let val Thm{sign,der,shyps,hyps,maxidx,prop,...} = cong val unit = if Sign.subsig(sign,signt) then () @@ -1669,7 +1756,7 @@ T = propT, maxidx = maxidx'} val thm' = Thm{sign = signt, - der = infer_derivs (CongC ct', [der]), + der = infer_derivs (CongC ct', [der]), (* FIXME fix!? *) shyps = shyps', hyps = union_term(hyps,hypst), prop = prop', @@ -1701,14 +1788,13 @@ Some(trec1) => trec1 | None => trec) - and subc (mss as Mss{net,congs,bounds,prems,mk_rews}) + and subc (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) (trec as (shyps,hyps,maxidx,t0,ders)) = (case t0 of Abs(a,T,t) => let val b = variant bounds a val v = Free("." ^ b,T) - val mss' = Mss{net=net, congs=congs, bounds=b::bounds, - prems=prems,mk_rews=mk_rews} + val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless) in case botc true mss' (shyps,hyps,maxidx,subst_bound (v,t),ders) of Some(shyps',hyps',maxidx',t',ders') => @@ -1775,12 +1861,16 @@ (*** Meta-rewriting: rewrites t to u and returns the theorem t==u ***) -(* Parameters: - mode = (simplify A, use A in simplifying B) when simplifying A ==> B - mss: contains equality theorems of the form [|p1,...|] ==> t==u - prover: how to solve premises in conditional rewrites and congruences + +(* + Parameters: + mode = (simplify A, use A in simplifying B) when simplifying A ==> B + mss: contains equality theorems of the form [|p1,...|] ==> t==u + prover: how to solve premises in conditional rewrites and congruences *) -(*** FIXME: check that #bounds(mss) does not "occur" in ct alread ***) + +(* FIXME: check that #bounds(mss) does not "occur" in ct alread *) + fun rewrite_cterm mode mss prover ct = let val {sign, t, T, maxidx} = rep_cterm ct; val (shyps,hyps,maxu,u,ders) = @@ -1797,6 +1887,9 @@ end + +(*** Oracles ***) + fun invoke_oracle (thy, sign, exn) = case #oraopt(rep_theory thy) of None => raise THM ("No oracle in supplied theory", 0, [])