# HG changeset patch # User wenzelm # Date 1235826132 -3600 # Node ID 5f7b17941730dc97da50ff385b3d7d8352d0b37d # Parent 7b55b6b5c0c2561eb509a1ee91c8cbdd37318d83 moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete; diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sat Feb 28 13:54:47 2009 +0100 +++ b/src/FOL/IFOL.thy Sat Feb 28 14:02:12 2009 +0100 @@ -1,5 +1,4 @@ (* Title: FOL/IFOL.thy - ID: $Id$ Author: Lawrence C Paulson and Markus Wenzel *) @@ -14,9 +13,9 @@ "~~/src/Tools/IsaPlanner/isand.ML" "~~/src/Tools/IsaPlanner/rw_tools.ML" "~~/src/Tools/IsaPlanner/rw_inst.ML" - "~~/src/Provers/eqsubst.ML" + "~~/src/Tools/eqsubst.ML" "~~/src/Provers/quantifier1.ML" - "~~/src/Provers/project_rule.ML" + "~~/src/Tools/project_rule.ML" "~~/src/Tools/atomize_elim.ML" ("fologic.ML") ("hypsubstdata.ML") diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Sat Feb 28 13:54:47 2009 +0100 +++ b/src/FOL/IsaMakefile Sat Feb 28 14:02:12 2009 +0100 @@ -32,9 +32,9 @@ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML \ $(SRC)/Tools/IsaPlanner/rw_tools.ML \ - $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Provers/eqsubst.ML \ + $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML \ $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML \ - $(SRC)/Tools/atomize_elim.ML $(SRC)/Provers/project_rule.ML \ + $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/project_rule.ML \ $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.thy \ IFOL.thy ROOT.ML blastdata.ML cladata.ML document/root.tex \ fologic.ML hypsubstdata.ML intprover.ML simpdata.ML diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sat Feb 28 13:54:47 2009 +0100 +++ b/src/HOL/HOL.thy Sat Feb 28 14:02:12 2009 +0100 @@ -12,14 +12,14 @@ "~~/src/Tools/IsaPlanner/isand.ML" "~~/src/Tools/IsaPlanner/rw_tools.ML" "~~/src/Tools/IsaPlanner/rw_inst.ML" - "~~/src/Provers/project_rule.ML" + "~~/src/Tools/project_rule.ML" "~~/src/Provers/hypsubst.ML" "~~/src/Provers/splitter.ML" "~~/src/Provers/classical.ML" "~~/src/Provers/blast.ML" "~~/src/Provers/clasimp.ML" - "~~/src/Provers/coherent.ML" - "~~/src/Provers/eqsubst.ML" + "~~/src/Tools/coherent.ML" + "~~/src/Tools/eqsubst.ML" "~~/src/Provers/quantifier1.ML" ("Tools/simpdata.ML") "~~/src/Tools/random_word.ML" diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Feb 28 13:54:47 2009 +0100 +++ b/src/HOL/IsaMakefile Sat Feb 28 14:02:12 2009 +0100 @@ -78,38 +78,38 @@ $(OUT)/Pure: Pure BASE_DEPENDENCIES = $(OUT)/Pure \ + $(SRC)/Provers/blast.ML \ + $(SRC)/Provers/clasimp.ML \ + $(SRC)/Provers/classical.ML \ + $(SRC)/Provers/hypsubst.ML \ + $(SRC)/Provers/quantifier1.ML \ + $(SRC)/Provers/splitter.ML \ + $(SRC)/Tools/IsaPlanner/isand.ML \ + $(SRC)/Tools/IsaPlanner/rw_inst.ML \ + $(SRC)/Tools/IsaPlanner/rw_tools.ML \ + $(SRC)/Tools/IsaPlanner/zipper.ML \ + $(SRC)/Tools/atomize_elim.ML \ + $(SRC)/Tools/code/code_funcgr.ML \ + $(SRC)/Tools/code/code_haskell.ML \ + $(SRC)/Tools/code/code_ml.ML \ + $(SRC)/Tools/code/code_name.ML \ + $(SRC)/Tools/code/code_printer.ML \ + $(SRC)/Tools/code/code_target.ML \ + $(SRC)/Tools/code/code_thingol.ML \ + $(SRC)/Tools/code/code_wellsorted.ML \ + $(SRC)/Tools/coherent.ML \ + $(SRC)/Tools/eqsubst.ML \ + $(SRC)/Tools/induct.ML \ + $(SRC)/Tools/induct_tacs.ML \ + $(SRC)/Tools/nbe.ML \ + $(SRC)/Tools/project_rule.ML \ + $(SRC)/Tools/random_word.ML \ + $(SRC)/Tools/value.ML \ Code_Setup.thy \ HOL.thy \ Tools/hologic.ML \ Tools/recfun_codegen.ML \ Tools/simpdata.ML \ - $(SRC)/Tools/atomize_elim.ML \ - $(SRC)/Tools/code/code_funcgr.ML \ - $(SRC)/Tools/code/code_wellsorted.ML \ - $(SRC)/Tools/code/code_name.ML \ - $(SRC)/Tools/code/code_printer.ML \ - $(SRC)/Tools/code/code_target.ML \ - $(SRC)/Tools/code/code_ml.ML \ - $(SRC)/Tools/code/code_haskell.ML \ - $(SRC)/Tools/code/code_thingol.ML \ - $(SRC)/Tools/induct.ML \ - $(SRC)/Tools/induct_tacs.ML \ - $(SRC)/Tools/IsaPlanner/isand.ML \ - $(SRC)/Tools/IsaPlanner/rw_inst.ML \ - $(SRC)/Tools/IsaPlanner/rw_tools.ML \ - $(SRC)/Tools/IsaPlanner/zipper.ML \ - $(SRC)/Tools/nbe.ML \ - $(SRC)/Tools/random_word.ML \ - $(SRC)/Tools/value.ML \ - $(SRC)/Provers/blast.ML \ - $(SRC)/Provers/clasimp.ML \ - $(SRC)/Provers/classical.ML \ - $(SRC)/Provers/coherent.ML \ - $(SRC)/Provers/eqsubst.ML \ - $(SRC)/Provers/hypsubst.ML \ - $(SRC)/Provers/project_rule.ML \ - $(SRC)/Provers/quantifier1.ML \ - $(SRC)/Provers/splitter.ML \ $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES) @$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/Provers/coherent.ML --- a/src/Provers/coherent.ML Sat Feb 28 13:54:47 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,233 +0,0 @@ -(* Title: Provers/coherent.ML - Author: Stefan Berghofer, TU Muenchen - Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen - -Prover for coherent logic, see e.g. - - Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005 - -for a description of the algorithm. -*) - -signature COHERENT_DATA = -sig - val atomize_elimL: thm - val atomize_exL: thm - val atomize_conjL: thm - val atomize_disjL: thm - val operator_names: string list -end; - -signature COHERENT = -sig - val verbose: bool ref - val show_facts: bool ref - val coherent_tac: thm list -> Proof.context -> int -> tactic - val coherent_meth: thm list -> Proof.context -> Proof.method - val setup: theory -> theory -end; - -functor CoherentFun(Data: COHERENT_DATA) : COHERENT = -struct - -val verbose = ref false; - -fun message f = if !verbose then tracing (f ()) else (); - -datatype cl_prf = - ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list * - int list * (term list * cl_prf) list; - -val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1); - -local open Conv in - -fun rulify_elim_conv ct = - if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct - else concl_conv (length (Logic.strip_imp_prems (term_of ct))) - (rewr_conv (symmetric Data.atomize_elimL) then_conv - MetaSimplifier.rewrite true (map symmetric - [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct - -end; - -fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); - -(* Decompose elimination rule of the form - A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P -*) -fun dest_elim prop = - let - val prems = Logic.strip_imp_prems prop; - val concl = Logic.strip_imp_concl prop; - val (prems1, prems2) = - take_suffix (fn t => Logic.strip_assums_concl t = concl) prems; - in - (prems1, - if null prems2 then [([], [concl])] - else map (fn t => - (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2) - end; - -fun mk_rule th = - let - val th' = rulify_elim th; - val (prems, cases) = dest_elim (prop_of th') - in (th', prems, cases) end; - -fun mk_dom ts = fold (fn t => - Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty; - -val empty_env = (Vartab.empty, Vartab.empty); - -(* Find matcher that makes conjunction valid in given state *) -fun valid_conj ctxt facts env [] = Seq.single (env, []) - | valid_conj ctxt facts env (t :: ts) = - Seq.maps (fn (u, x) => Seq.map (apsnd (cons x)) - (valid_conj ctxt facts - (Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts - handle Pattern.MATCH => Seq.empty)) - (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t))); - -(* Instantiate variables that only occur free in conlusion *) -fun inst_extra_vars ctxt dom cs = - let - val vs = fold Term.add_vars (maps snd cs) []; - fun insts [] inst = Seq.single inst - | insts ((ixn, T) :: vs') inst = Seq.maps - (fn t => insts vs' (((ixn, T), t) :: inst)) - (Seq.of_list (case Typtab.lookup dom T of - NONE => error ("Unknown domain: " ^ - Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^ - commas (maps (map (Syntax.string_of_term ctxt) o snd) cs)) - | SOME ts => ts)) - in Seq.map (fn inst => - (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs)) - (insts vs []) - end; - -(* Check whether disjunction is valid in given state *) -fun is_valid_disj ctxt facts [] = false - | is_valid_disj ctxt facts ((Ts, ts) :: ds) = - let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts) - in case Seq.pull (valid_conj ctxt facts empty_env - (map (fn t => subst_bounds (vs, t)) ts)) of - SOME _ => true - | NONE => is_valid_disj ctxt facts ds - end; - -val show_facts = ref false; - -fun string_of_facts ctxt s facts = space_implode "\n" - (s :: map (Syntax.string_of_term ctxt) - (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n"; - -fun print_facts ctxt facts = - if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts) - else (); - -fun valid ctxt rules goal dom facts nfacts nparams = - let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) => - valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) => - let val cs' = map (fn (Ts, ts) => - (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs - in - inst_extra_vars ctxt dom cs' |> - Seq.map_filter (fn (inst, cs'') => - if is_valid_disj ctxt facts cs'' then NONE - else SOME (th, env, inst, is, cs'')) - end)) - in - case Seq.pull seq of - NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE) - | SOME ((th, env, inst, is, cs), _) => - if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, [])) - else - (case valid_cases ctxt rules goal dom facts nfacts nparams cs of - NONE => NONE - | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))) - end - -and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME [] - | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) = - let - val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts)); - val params = rev (map_index (fn (i, T) => - Free ("par" ^ string_of_int (nparams + i), T)) Ts); - val ts' = map_index (fn (i, t) => - (subst_bounds (params, t), nfacts + i)) ts; - val dom' = fold (fn (T, p) => - Typtab.map_default (T, []) (fn ps => ps @ [p])) - (Ts ~~ params) dom; - val facts' = fold (fn (t, i) => Net.insert_term op = - (t, (t, i))) ts' facts - in - case valid ctxt rules goal dom' facts' - (nfacts + length ts) (nparams + length Ts) of - NONE => NONE - | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of - NONE => NONE - | SOME prfs => SOME ((params, prf) :: prfs)) - end; - -(** proof replaying **) - -fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) = - let - val _ = message (fn () => space_implode "\n" - ("asms:" :: map Display.string_of_thm asms) ^ "\n\n"); - val th' = Drule.implies_elim_list - (Thm.instantiate - (map (fn (ixn, (S, T)) => - (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T)) - (Vartab.dest tye), - map (fn (ixn, (T, t)) => - (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)), - Thm.cterm_of thy t)) (Vartab.dest env) @ - map (fn (ixnT, t) => - (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th) - (map (nth asms) is); - val (_, cases) = dest_elim (prop_of th') - in - case (cases, prfs) of - ([([], [_])], []) => th' - | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf - | _ => Drule.implies_elim_list - (Thm.instantiate (Thm.match - (Drule.strip_imp_concl (cprop_of th'), goal)) th') - (map (thm_of_case_prf thy goal asms) (prfs ~~ cases)) - end - -and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) = - let - val cparams = map (cterm_of thy) params; - val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms' - in - Drule.forall_intr_list cparams (Drule.implies_intr_list asms'' - (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf)) - end; - - -(** external interface **) - -fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} => - rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN - SUBPROOF (fn {prems = prems', concl, context, ...} => - let val xs = map term_of params @ - map (fn (_, s) => Free (s, the (Variable.default_type context s))) - (Variable.fixes_of context) - in - case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl) - (mk_dom xs) Net.empty 0 0 of - NONE => no_tac - | SOME prf => - rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1 - end) context 1) ctxt; - -fun coherent_meth rules ctxt = - Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1); - -val setup = Method.add_method - ("coherent", Method.thms_ctxt_args coherent_meth, "Prove coherent formula"); - -end; diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Sat Feb 28 13:54:47 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,575 +0,0 @@ -(* Title: Provers/eqsubst.ML - Author: Lucas Dixon, University of Edinburgh - -A proof method to perform a substiution using an equation. -*) - -signature EQSUBST = -sig - (* a type abbreviation for match information *) - type match = - ((indexname * (sort * typ)) list (* type instantiations *) - * (indexname * (typ * term)) list) (* term instantiations *) - * (string * typ) list (* fake named type abs env *) - * (string * typ) list (* type abs env *) - * term (* outer term *) - - type searchinfo = - theory - * int (* maxidx *) - * Zipper.T (* focusterm to search under *) - - exception eqsubst_occL_exp of - string * int list * Thm.thm list * int * Thm.thm - - (* low level substitution functions *) - val apply_subst_in_asm : - int -> - Thm.thm -> - Thm.thm -> - (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq - val apply_subst_in_concl : - int -> - Thm.thm -> - Thm.cterm list * Thm.thm -> - Thm.thm -> match -> Thm.thm Seq.seq - - (* matching/unification within zippers *) - val clean_match_z : - Context.theory -> Term.term -> Zipper.T -> match option - val clean_unify_z : - Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq - - (* skipping things in seq seq's *) - - (* skipping non-empty sub-sequences but when we reach the end - of the seq, remembering how much we have left to skip. *) - datatype 'a skipseq = SkipMore of int - | SkipSeq of 'a Seq.seq Seq.seq; - - val skip_first_asm_occs_search : - ('a -> 'b -> 'c Seq.seq Seq.seq) -> - 'a -> int -> 'b -> 'c skipseq - val skip_first_occs_search : - int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq - val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq - - (* tactics *) - val eqsubst_asm_tac : - Proof.context -> - int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq - val eqsubst_asm_tac' : - Proof.context -> - (searchinfo -> int -> Term.term -> match skipseq) -> - int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq - val eqsubst_tac : - Proof.context -> - int list -> (* list of occurences to rewrite, use [0] for any *) - Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq - val eqsubst_tac' : - Proof.context -> (* proof context *) - (searchinfo -> Term.term -> match Seq.seq) (* search function *) - -> Thm.thm (* equation theorem to rewrite with *) - -> int (* subgoal number in goal theorem *) - -> Thm.thm (* goal theorem *) - -> Thm.thm Seq.seq (* rewritten goal theorem *) - - - val fakefree_badbounds : - (string * Term.typ) list -> - Term.term -> - (string * Term.typ) list * (string * Term.typ) list * Term.term - - val mk_foo_match : - (Term.term -> Term.term) -> - ('a * Term.typ) list -> Term.term -> Term.term - - (* preparing substitution *) - val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list - val prep_concl_subst : - int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo - val prep_subst_in_asm : - int -> Thm.thm -> int -> - (Thm.cterm list * int * int * Thm.thm) * searchinfo - val prep_subst_in_asms : - int -> Thm.thm -> - ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list - val prep_zipper_match : - Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term) - - (* search for substitutions *) - val valid_match_start : Zipper.T -> bool - val search_lr_all : Zipper.T -> Zipper.T Seq.seq - val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq - val searchf_lr_unify_all : - searchinfo -> Term.term -> match Seq.seq Seq.seq - val searchf_lr_unify_valid : - searchinfo -> Term.term -> match Seq.seq Seq.seq - val searchf_bt_unify_valid : - searchinfo -> Term.term -> match Seq.seq Seq.seq - - (* syntax tools *) - val ith_syntax : Args.T list -> int list * Args.T list - val options_syntax : Args.T list -> bool * Args.T list - - (* Isar level hooks *) - val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method - val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method - val subst_meth : Method.src -> Proof.context -> Proof.method - val setup : theory -> theory - -end; - -structure EqSubst -: EQSUBST -= struct - -structure Z = Zipper; - -(* changes object "=" to meta "==" which prepares a given rewrite rule *) -fun prep_meta_eq ctxt = - let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt) - in mk #> map Drule.zero_var_indexes end; - - - (* a type abriviation for match information *) - type match = - ((indexname * (sort * typ)) list (* type instantiations *) - * (indexname * (typ * term)) list) (* term instantiations *) - * (string * typ) list (* fake named type abs env *) - * (string * typ) list (* type abs env *) - * term (* outer term *) - - type searchinfo = - theory - * int (* maxidx *) - * Zipper.T (* focusterm to search under *) - - -(* skipping non-empty sub-sequences but when we reach the end - of the seq, remembering how much we have left to skip. *) -datatype 'a skipseq = SkipMore of int - | SkipSeq of 'a Seq.seq Seq.seq; -(* given a seqseq, skip the first m non-empty seq's, note deficit *) -fun skipto_skipseq m s = - let - fun skip_occs n sq = - case Seq.pull sq of - NONE => SkipMore n - | SOME (h,t) => - (case Seq.pull h of NONE => skip_occs n t - | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) - else skip_occs (n - 1) t) - in (skip_occs m s) end; - -(* note: outerterm is the taget with the match replaced by a bound - variable : ie: "P lhs" beocmes "%x. P x" - insts is the types of instantiations of vars in lhs - and typinsts is the type instantiations of types in the lhs - Note: Final rule is the rule lifted into the ontext of the - taget thm. *) -fun mk_foo_match mkuptermfunc Ts t = - let - val ty = Term.type_of t - val bigtype = (rev (map snd Ts)) ---> ty - fun mk_foo 0 t = t - | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) - val num_of_bnds = (length Ts) - (* foo_term = "fooabs y0 ... yn" where y's are local bounds *) - val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) - in Abs("fooabs", bigtype, mkuptermfunc foo_term) end; - -(* T is outer bound vars, n is number of locally bound vars *) -(* THINK: is order of Ts correct...? or reversed? *) -fun fakefree_badbounds Ts t = - let val (FakeTs,Ts,newnames) = - List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => - let val newname = Name.variant usednames n - in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs, - (newname,ty)::Ts, - newname::usednames) end) - ([],[],[]) - Ts - in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; - -(* before matching we need to fake the bound vars that are missing an -abstraction. In this function we additionally construct the -abstraction environment, and an outer context term (with the focus -abstracted out) for use in rewriting with RWInst.rw *) -fun prep_zipper_match z = - let - val t = Z.trm z - val c = Z.ctxt z - val Ts = Z.C.nty_ctxt c - val (FakeTs', Ts', t') = fakefree_badbounds Ts t - val absterm = mk_foo_match (Z.C.apply c) Ts' t' - in - (t', (FakeTs', Ts', absterm)) - end; - -(* Matching and Unification with exception handled *) -fun clean_match thy (a as (pat, t)) = - let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty) - in SOME (Vartab.dest tyenv, Vartab.dest tenv) - end handle Pattern.MATCH => NONE; - -(* given theory, max var index, pat, tgt; returns Seq of instantiations *) -fun clean_unify thry ix (a as (pat, tgt)) = - let - (* type info will be re-derived, maybe this can be cached - for efficiency? *) - val pat_ty = Term.type_of pat; - val tgt_ty = Term.type_of tgt; - (* is it OK to ignore the type instantiation info? - or should I be using it? *) - val typs_unify = - SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix)) - handle Type.TUNIFY => NONE; - in - case typs_unify of - SOME (typinsttab, ix2) => - let - (* is it right to throw away the flexes? - or should I be using them somehow? *) - fun mk_insts env = - (Vartab.dest (Envir.type_env env), - Envir.alist_of env); - val initenv = Envir.Envir {asol = Vartab.empty, - iTs = typinsttab, maxidx = ix2}; - val useq = Unify.smash_unifiers thry [a] initenv - handle UnequalLengths => Seq.empty - | Term.TERM _ => Seq.empty; - fun clean_unify' useq () = - (case (Seq.pull useq) of - NONE => NONE - | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t))) - handle UnequalLengths => NONE - | Term.TERM _ => NONE - in - (Seq.make (clean_unify' useq)) - end - | NONE => Seq.empty - end; - -(* Matching and Unification for zippers *) -(* Note: Ts is a modified version of the original names of the outer -bound variables. New names have been introduced to make sure they are -unique w.r.t all names in the term and each other. usednames' is -oldnames + new names. *) -fun clean_match_z thy pat z = - let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in - case clean_match thy (pat, t) of - NONE => NONE - | SOME insts => SOME (insts, FakeTs, Ts, absterm) end; -(* ix = max var index *) -fun clean_unify_z sgn ix pat z = - let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in - Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) - (clean_unify sgn ix (t, pat)) end; - - -(* FOR DEBUGGING... -type trace_subst_errT = int (* subgoal *) - * thm (* thm with all goals *) - * (Thm.cterm list (* certified free var placeholders for vars *) - * thm) (* trivial thm of goal concl *) - (* possible matches/unifiers *) - * thm (* rule *) - * (((indexname * typ) list (* type instantiations *) - * (indexname * term) list ) (* term instantiations *) - * (string * typ) list (* Type abs env *) - * term) (* outer term *); - -val trace_subst_err = (ref NONE : trace_subst_errT option ref); -val trace_subst_search = ref false; -exception trace_subst_exp of trace_subst_errT; -*) - - -fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l - | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t - | bot_left_leaf_of x = x; - -(* Avoid considering replacing terms which have a var at the head as - they always succeed trivially, and uninterestingly. *) -fun valid_match_start z = - (case bot_left_leaf_of (Z.trm z) of - Var _ => false - | _ => true); - -(* search from top, left to right, then down *) -val search_lr_all = ZipperSearch.all_bl_ur; - -(* search from top, left to right, then down *) -fun search_lr_valid validf = - let - fun sf_valid_td_lr z = - let val here = if validf z then [Z.Here z] else [] in - case Z.trm z - of _ $ _ => [Z.LookIn (Z.move_down_left z)] - @ here - @ [Z.LookIn (Z.move_down_right z)] - | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)] - | _ => here - end; - in Z.lzy_search sf_valid_td_lr end; - -(* search from bottom to top, left to right *) - -fun search_bt_valid validf = - let - fun sf_valid_td_lr z = - let val here = if validf z then [Z.Here z] else [] in - case Z.trm z - of _ $ _ => [Z.LookIn (Z.move_down_left z), - Z.LookIn (Z.move_down_right z)] @ here - | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here - | _ => here - end; - in Z.lzy_search sf_valid_td_lr end; - -fun searchf_unify_gen f (sgn, maxidx, z) lhs = - Seq.map (clean_unify_z sgn maxidx lhs) - (Z.limit_apply f z); - -(* search all unifications *) -val searchf_lr_unify_all = - searchf_unify_gen search_lr_all; - -(* search only for 'valid' unifiers (non abs subterms and non vars) *) -val searchf_lr_unify_valid = - searchf_unify_gen (search_lr_valid valid_match_start); - -val searchf_bt_unify_valid = - searchf_unify_gen (search_bt_valid valid_match_start); - -(* apply a substitution in the conclusion of the theorem th *) -(* cfvs are certified free var placeholders for goal params *) -(* conclthm is a theorem of for just the conclusion *) -(* m is instantiation/match information *) -(* rule is the equation for substitution *) -fun apply_subst_in_concl i th (cfvs, conclthm) rule m = - (RWInst.rw m rule conclthm) - |> IsaND.unfix_frees cfvs - |> RWInst.beta_eta_contract - |> (fn r => Tactic.rtac r i th); - -(* substitute within the conclusion of goal i of gth, using a meta -equation rule. Note that we assume rule has var indicies zero'd *) -fun prep_concl_subst i gth = - let - val th = Thm.incr_indexes 1 gth; - val tgt_term = Thm.prop_of th; - - val sgn = Thm.theory_of_thm th; - val ctermify = Thm.cterm_of sgn; - val trivify = Thm.trivial o ctermify; - - val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; - val cfvs = rev (map ctermify fvs); - - val conclterm = Logic.strip_imp_concl fixedbody; - val conclthm = trivify conclterm; - val maxidx = Thm.maxidx_of th; - val ft = ((Z.move_down_right (* ==> *) - o Z.move_down_left (* Trueprop *) - o Z.mktop - o Thm.prop_of) conclthm) - in - ((cfvs, conclthm), (sgn, maxidx, ft)) - end; - -(* substitute using an object or meta level equality *) -fun eqsubst_tac' ctxt searchf instepthm i th = - let - val (cvfsconclthm, searchinfo) = prep_concl_subst i th; - val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); - fun rewrite_with_thm r = - let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); - in searchf searchinfo lhs - |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end; - in stepthms |> Seq.maps rewrite_with_thm end; - - -(* distinct subgoals *) -fun distinct_subgoals th = - the_default th (SINGLE distinct_subgoals_tac th); - -(* General substitution of multiple occurances using one of - the given theorems*) - - -exception eqsubst_occL_exp of - string * (int list) * (thm list) * int * thm; -fun skip_first_occs_search occ srchf sinfo lhs = - case (skipto_skipseq occ (srchf sinfo lhs)) of - SkipMore _ => Seq.empty - | SkipSeq ss => Seq.flat ss; - -(* The occL is a list of integers indicating which occurence -w.r.t. the search order, to rewrite. Backtracking will also find later -occurences, but all earlier ones are skipped. Thus you can use [0] to -just find all rewrites. *) - -fun eqsubst_tac ctxt occL thms i th = - let val nprems = Thm.nprems_of th in - if nprems < i then Seq.empty else - let val thmseq = (Seq.of_list thms) - fun apply_occ occ th = - thmseq |> Seq.maps - (fn r => eqsubst_tac' - ctxt - (skip_first_occs_search - occ searchf_lr_unify_valid) r - (i + ((Thm.nprems_of th) - nprems)) - th); - val sortedoccL = - Library.sort (Library.rev_order o Library.int_ord) occL; - in - Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th) - end - end - handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); - - -(* inthms are the given arguments in Isar, and treated as eqstep with - the first one, then the second etc *) -fun eqsubst_meth ctxt occL inthms = - Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms); - -(* apply a substitution inside assumption j, keeps asm in the same place *) -fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) = - let - val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *) - val preelimrule = - (RWInst.rw m rule pth) - |> (Seq.hd o prune_params_tac) - |> Thm.permute_prems 0 ~1 (* put old asm first *) - |> IsaND.unfix_frees cfvs (* unfix any global params *) - |> RWInst.beta_eta_contract; (* normal form *) - (* val elimrule = - preelimrule - |> Tactic.make_elim (* make into elim rule *) - |> Thm.lift_rule (th2, i); (* lift into context *) - *) - in - (* ~j because new asm starts at back, thus we subtract 1 *) - Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i)) - (Tactic.dtac preelimrule i th2) - - (* (Thm.bicompose - false (* use unification *) - (true, (* elim resolution *) - elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems) - i th2) *) - end; - - -(* prepare to substitute within the j'th premise of subgoal i of gth, -using a meta-level equation. Note that we assume rule has var indicies -zero'd. Note that we also assume that premt is the j'th premice of -subgoal i of gth. Note the repetition of work done for each -assumption, i.e. this can be made more efficient for search over -multiple assumptions. *) -fun prep_subst_in_asm i gth j = - let - val th = Thm.incr_indexes 1 gth; - val tgt_term = Thm.prop_of th; - - val sgn = Thm.theory_of_thm th; - val ctermify = Thm.cterm_of sgn; - val trivify = Thm.trivial o ctermify; - - val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; - val cfvs = rev (map ctermify fvs); - - val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1); - val asm_nprems = length (Logic.strip_imp_prems asmt); - - val pth = trivify asmt; - val maxidx = Thm.maxidx_of th; - - val ft = ((Z.move_down_right (* trueprop *) - o Z.mktop - o Thm.prop_of) pth) - in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end; - -(* prepare subst in every possible assumption *) -fun prep_subst_in_asms i gth = - map (prep_subst_in_asm i gth) - ((fn l => Library.upto (1, length l)) - (Logic.prems_of_goal (Thm.prop_of gth) i)); - - -(* substitute in an assumption using an object or meta level equality *) -fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th = - let - val asmpreps = prep_subst_in_asms i th; - val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); - fun rewrite_with_thm r = - let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) - fun occ_search occ [] = Seq.empty - | occ_search occ ((asminfo, searchinfo)::moreasms) = - (case searchf searchinfo occ lhs of - SkipMore i => occ_search i moreasms - | SkipSeq ss => - Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss)) - (occ_search 1 moreasms)) - (* find later substs also *) - in - occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r) - end; - in stepthms |> Seq.maps rewrite_with_thm end; - - -fun skip_first_asm_occs_search searchf sinfo occ lhs = - skipto_skipseq occ (searchf sinfo lhs); - -fun eqsubst_asm_tac ctxt occL thms i th = - let val nprems = Thm.nprems_of th - in - if nprems < i then Seq.empty else - let val thmseq = (Seq.of_list thms) - fun apply_occ occK th = - thmseq |> Seq.maps - (fn r => - eqsubst_asm_tac' ctxt (skip_first_asm_occs_search - searchf_lr_unify_valid) occK r - (i + ((Thm.nprems_of th) - nprems)) - th); - val sortedoccs = - Library.sort (Library.rev_order o Library.int_ord) occL - in - Seq.map distinct_subgoals - (Seq.EVERY (map apply_occ sortedoccs) th) - end - end - handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); - -(* inthms are the given arguments in Isar, and treated as eqstep with - the first one, then the second etc *) -fun eqsubst_asm_meth ctxt occL inthms = - Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms); - -(* syntax for options, given "(asm)" will give back true, without - gives back false *) -val options_syntax = - (Args.parens (Args.$$$ "asm") >> (K true)) || - (Scan.succeed false); - -val ith_syntax = - Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0]; - -(* combination method that takes a flag (true indicates that subst -should be done to an assumption, false = apply to the conclusion of -the goal) as well as the theorems to use *) -fun subst_meth src = - Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src - #> (fn (((asmflag, occL), inthms), ctxt) => - (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms); - - -val setup = - Method.add_method ("subst", subst_meth, "single-step substitution"); - -end; diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/Provers/project_rule.ML --- a/src/Provers/project_rule.ML Sat Feb 28 13:54:47 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,63 +0,0 @@ -(* Title: Provers/project_rule.ML - ID: $Id$ - Author: Makarius - -Transform mutual rule: - HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn) -into projection: - xi:Ai ==> HH ==> Pi xi -*) - -signature PROJECT_RULE_DATA = -sig - val conjunct1: thm - val conjunct2: thm - val mp: thm -end; - -signature PROJECT_RULE = -sig - val project: Proof.context -> int -> thm -> thm - val projects: Proof.context -> int list -> thm -> thm list - val projections: Proof.context -> thm -> thm list -end; - -functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE = -struct - -fun conj1 th = th RS Data.conjunct1; -fun conj2 th = th RS Data.conjunct2; -fun imp th = th RS Data.mp; - -fun projects ctxt is raw_rule = - let - fun proj 1 th = the_default th (try conj1 th) - | proj k th = proj (k - 1) (conj2 th); - fun prems k th = - (case try imp th of - NONE => (k, th) - | SOME th' => prems (k + 1) th'); - val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt; - fun result i = - rule - |> proj i - |> prems 0 |-> (fn k => - Thm.permute_prems 0 (~ k) - #> singleton (Variable.export ctxt' ctxt) - #> Drule.zero_var_indexes - #> RuleCases.save raw_rule - #> RuleCases.add_consumes k); - in map result is end; - -fun project ctxt i th = hd (projects ctxt [i] th); - -fun projections ctxt raw_rule = - let - fun projs k th = - (case try conj2 th of - NONE => k - | SOME th' => projs (k + 1) th'); - val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt; - in projects ctxt (1 upto projs 1 rule) raw_rule end; - -end; diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/Tools/coherent.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/coherent.ML Sat Feb 28 14:02:12 2009 +0100 @@ -0,0 +1,233 @@ +(* Title: Tools/coherent.ML + Author: Stefan Berghofer, TU Muenchen + Author: Marc Bezem, Institutt for Informatikk, Universitetet i Bergen + +Prover for coherent logic, see e.g. + + Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005 + +for a description of the algorithm. +*) + +signature COHERENT_DATA = +sig + val atomize_elimL: thm + val atomize_exL: thm + val atomize_conjL: thm + val atomize_disjL: thm + val operator_names: string list +end; + +signature COHERENT = +sig + val verbose: bool ref + val show_facts: bool ref + val coherent_tac: thm list -> Proof.context -> int -> tactic + val coherent_meth: thm list -> Proof.context -> Proof.method + val setup: theory -> theory +end; + +functor CoherentFun(Data: COHERENT_DATA) : COHERENT = +struct + +val verbose = ref false; + +fun message f = if !verbose then tracing (f ()) else (); + +datatype cl_prf = + ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list * + int list * (term list * cl_prf) list; + +val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1); + +local open Conv in + +fun rulify_elim_conv ct = + if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct + else concl_conv (length (Logic.strip_imp_prems (term_of ct))) + (rewr_conv (symmetric Data.atomize_elimL) then_conv + MetaSimplifier.rewrite true (map symmetric + [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct + +end; + +fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th); + +(* Decompose elimination rule of the form + A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P +*) +fun dest_elim prop = + let + val prems = Logic.strip_imp_prems prop; + val concl = Logic.strip_imp_concl prop; + val (prems1, prems2) = + take_suffix (fn t => Logic.strip_assums_concl t = concl) prems; + in + (prems1, + if null prems2 then [([], [concl])] + else map (fn t => + (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2) + end; + +fun mk_rule th = + let + val th' = rulify_elim th; + val (prems, cases) = dest_elim (prop_of th') + in (th', prems, cases) end; + +fun mk_dom ts = fold (fn t => + Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty; + +val empty_env = (Vartab.empty, Vartab.empty); + +(* Find matcher that makes conjunction valid in given state *) +fun valid_conj ctxt facts env [] = Seq.single (env, []) + | valid_conj ctxt facts env (t :: ts) = + Seq.maps (fn (u, x) => Seq.map (apsnd (cons x)) + (valid_conj ctxt facts + (Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts + handle Pattern.MATCH => Seq.empty)) + (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t))); + +(* Instantiate variables that only occur free in conlusion *) +fun inst_extra_vars ctxt dom cs = + let + val vs = fold Term.add_vars (maps snd cs) []; + fun insts [] inst = Seq.single inst + | insts ((ixn, T) :: vs') inst = Seq.maps + (fn t => insts vs' (((ixn, T), t) :: inst)) + (Seq.of_list (case Typtab.lookup dom T of + NONE => error ("Unknown domain: " ^ + Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^ + commas (maps (map (Syntax.string_of_term ctxt) o snd) cs)) + | SOME ts => ts)) + in Seq.map (fn inst => + (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs)) + (insts vs []) + end; + +(* Check whether disjunction is valid in given state *) +fun is_valid_disj ctxt facts [] = false + | is_valid_disj ctxt facts ((Ts, ts) :: ds) = + let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts) + in case Seq.pull (valid_conj ctxt facts empty_env + (map (fn t => subst_bounds (vs, t)) ts)) of + SOME _ => true + | NONE => is_valid_disj ctxt facts ds + end; + +val show_facts = ref false; + +fun string_of_facts ctxt s facts = space_implode "\n" + (s :: map (Syntax.string_of_term ctxt) + (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n"; + +fun print_facts ctxt facts = + if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts) + else (); + +fun valid ctxt rules goal dom facts nfacts nparams = + let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) => + valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) => + let val cs' = map (fn (Ts, ts) => + (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs + in + inst_extra_vars ctxt dom cs' |> + Seq.map_filter (fn (inst, cs'') => + if is_valid_disj ctxt facts cs'' then NONE + else SOME (th, env, inst, is, cs'')) + end)) + in + case Seq.pull seq of + NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE) + | SOME ((th, env, inst, is, cs), _) => + if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, [])) + else + (case valid_cases ctxt rules goal dom facts nfacts nparams cs of + NONE => NONE + | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))) + end + +and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME [] + | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) = + let + val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts)); + val params = rev (map_index (fn (i, T) => + Free ("par" ^ string_of_int (nparams + i), T)) Ts); + val ts' = map_index (fn (i, t) => + (subst_bounds (params, t), nfacts + i)) ts; + val dom' = fold (fn (T, p) => + Typtab.map_default (T, []) (fn ps => ps @ [p])) + (Ts ~~ params) dom; + val facts' = fold (fn (t, i) => Net.insert_term op = + (t, (t, i))) ts' facts + in + case valid ctxt rules goal dom' facts' + (nfacts + length ts) (nparams + length Ts) of + NONE => NONE + | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of + NONE => NONE + | SOME prfs => SOME ((params, prf) :: prfs)) + end; + +(** proof replaying **) + +fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) = + let + val _ = message (fn () => space_implode "\n" + ("asms:" :: map Display.string_of_thm asms) ^ "\n\n"); + val th' = Drule.implies_elim_list + (Thm.instantiate + (map (fn (ixn, (S, T)) => + (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T)) + (Vartab.dest tye), + map (fn (ixn, (T, t)) => + (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)), + Thm.cterm_of thy t)) (Vartab.dest env) @ + map (fn (ixnT, t) => + (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th) + (map (nth asms) is); + val (_, cases) = dest_elim (prop_of th') + in + case (cases, prfs) of + ([([], [_])], []) => th' + | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf + | _ => Drule.implies_elim_list + (Thm.instantiate (Thm.match + (Drule.strip_imp_concl (cprop_of th'), goal)) th') + (map (thm_of_case_prf thy goal asms) (prfs ~~ cases)) + end + +and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) = + let + val cparams = map (cterm_of thy) params; + val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms' + in + Drule.forall_intr_list cparams (Drule.implies_intr_list asms'' + (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf)) + end; + + +(** external interface **) + +fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} => + rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN + SUBPROOF (fn {prems = prems', concl, context, ...} => + let val xs = map term_of params @ + map (fn (_, s) => Free (s, the (Variable.default_type context s))) + (Variable.fixes_of context) + in + case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl) + (mk_dom xs) Net.empty 0 0 of + NONE => no_tac + | SOME prf => + rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1 + end) context 1) ctxt; + +fun coherent_meth rules ctxt = + Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1); + +val setup = Method.add_method + ("coherent", Method.thms_ctxt_args coherent_meth, "Prove coherent formula"); + +end; diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/Tools/eqsubst.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/eqsubst.ML Sat Feb 28 14:02:12 2009 +0100 @@ -0,0 +1,575 @@ +(* Title: Tools/eqsubst.ML + Author: Lucas Dixon, University of Edinburgh + +A proof method to perform a substiution using an equation. +*) + +signature EQSUBST = +sig + (* a type abbreviation for match information *) + type match = + ((indexname * (sort * typ)) list (* type instantiations *) + * (indexname * (typ * term)) list) (* term instantiations *) + * (string * typ) list (* fake named type abs env *) + * (string * typ) list (* type abs env *) + * term (* outer term *) + + type searchinfo = + theory + * int (* maxidx *) + * Zipper.T (* focusterm to search under *) + + exception eqsubst_occL_exp of + string * int list * Thm.thm list * int * Thm.thm + + (* low level substitution functions *) + val apply_subst_in_asm : + int -> + Thm.thm -> + Thm.thm -> + (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq + val apply_subst_in_concl : + int -> + Thm.thm -> + Thm.cterm list * Thm.thm -> + Thm.thm -> match -> Thm.thm Seq.seq + + (* matching/unification within zippers *) + val clean_match_z : + Context.theory -> Term.term -> Zipper.T -> match option + val clean_unify_z : + Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq + + (* skipping things in seq seq's *) + + (* skipping non-empty sub-sequences but when we reach the end + of the seq, remembering how much we have left to skip. *) + datatype 'a skipseq = SkipMore of int + | SkipSeq of 'a Seq.seq Seq.seq; + + val skip_first_asm_occs_search : + ('a -> 'b -> 'c Seq.seq Seq.seq) -> + 'a -> int -> 'b -> 'c skipseq + val skip_first_occs_search : + int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq + val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq + + (* tactics *) + val eqsubst_asm_tac : + Proof.context -> + int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + val eqsubst_asm_tac' : + Proof.context -> + (searchinfo -> int -> Term.term -> match skipseq) -> + int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq + val eqsubst_tac : + Proof.context -> + int list -> (* list of occurences to rewrite, use [0] for any *) + Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq + val eqsubst_tac' : + Proof.context -> (* proof context *) + (searchinfo -> Term.term -> match Seq.seq) (* search function *) + -> Thm.thm (* equation theorem to rewrite with *) + -> int (* subgoal number in goal theorem *) + -> Thm.thm (* goal theorem *) + -> Thm.thm Seq.seq (* rewritten goal theorem *) + + + val fakefree_badbounds : + (string * Term.typ) list -> + Term.term -> + (string * Term.typ) list * (string * Term.typ) list * Term.term + + val mk_foo_match : + (Term.term -> Term.term) -> + ('a * Term.typ) list -> Term.term -> Term.term + + (* preparing substitution *) + val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list + val prep_concl_subst : + int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo + val prep_subst_in_asm : + int -> Thm.thm -> int -> + (Thm.cterm list * int * int * Thm.thm) * searchinfo + val prep_subst_in_asms : + int -> Thm.thm -> + ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list + val prep_zipper_match : + Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term) + + (* search for substitutions *) + val valid_match_start : Zipper.T -> bool + val search_lr_all : Zipper.T -> Zipper.T Seq.seq + val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq + val searchf_lr_unify_all : + searchinfo -> Term.term -> match Seq.seq Seq.seq + val searchf_lr_unify_valid : + searchinfo -> Term.term -> match Seq.seq Seq.seq + val searchf_bt_unify_valid : + searchinfo -> Term.term -> match Seq.seq Seq.seq + + (* syntax tools *) + val ith_syntax : Args.T list -> int list * Args.T list + val options_syntax : Args.T list -> bool * Args.T list + + (* Isar level hooks *) + val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method + val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method + val subst_meth : Method.src -> Proof.context -> Proof.method + val setup : theory -> theory + +end; + +structure EqSubst +: EQSUBST += struct + +structure Z = Zipper; + +(* changes object "=" to meta "==" which prepares a given rewrite rule *) +fun prep_meta_eq ctxt = + let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt) + in mk #> map Drule.zero_var_indexes end; + + + (* a type abriviation for match information *) + type match = + ((indexname * (sort * typ)) list (* type instantiations *) + * (indexname * (typ * term)) list) (* term instantiations *) + * (string * typ) list (* fake named type abs env *) + * (string * typ) list (* type abs env *) + * term (* outer term *) + + type searchinfo = + theory + * int (* maxidx *) + * Zipper.T (* focusterm to search under *) + + +(* skipping non-empty sub-sequences but when we reach the end + of the seq, remembering how much we have left to skip. *) +datatype 'a skipseq = SkipMore of int + | SkipSeq of 'a Seq.seq Seq.seq; +(* given a seqseq, skip the first m non-empty seq's, note deficit *) +fun skipto_skipseq m s = + let + fun skip_occs n sq = + case Seq.pull sq of + NONE => SkipMore n + | SOME (h,t) => + (case Seq.pull h of NONE => skip_occs n t + | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t) + else skip_occs (n - 1) t) + in (skip_occs m s) end; + +(* note: outerterm is the taget with the match replaced by a bound + variable : ie: "P lhs" beocmes "%x. P x" + insts is the types of instantiations of vars in lhs + and typinsts is the type instantiations of types in the lhs + Note: Final rule is the rule lifted into the ontext of the + taget thm. *) +fun mk_foo_match mkuptermfunc Ts t = + let + val ty = Term.type_of t + val bigtype = (rev (map snd Ts)) ---> ty + fun mk_foo 0 t = t + | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1))) + val num_of_bnds = (length Ts) + (* foo_term = "fooabs y0 ... yn" where y's are local bounds *) + val foo_term = mk_foo num_of_bnds (Bound num_of_bnds) + in Abs("fooabs", bigtype, mkuptermfunc foo_term) end; + +(* T is outer bound vars, n is number of locally bound vars *) +(* THINK: is order of Ts correct...? or reversed? *) +fun fakefree_badbounds Ts t = + let val (FakeTs,Ts,newnames) = + List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => + let val newname = Name.variant usednames n + in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs, + (newname,ty)::Ts, + newname::usednames) end) + ([],[],[]) + Ts + in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end; + +(* before matching we need to fake the bound vars that are missing an +abstraction. In this function we additionally construct the +abstraction environment, and an outer context term (with the focus +abstracted out) for use in rewriting with RWInst.rw *) +fun prep_zipper_match z = + let + val t = Z.trm z + val c = Z.ctxt z + val Ts = Z.C.nty_ctxt c + val (FakeTs', Ts', t') = fakefree_badbounds Ts t + val absterm = mk_foo_match (Z.C.apply c) Ts' t' + in + (t', (FakeTs', Ts', absterm)) + end; + +(* Matching and Unification with exception handled *) +fun clean_match thy (a as (pat, t)) = + let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty) + in SOME (Vartab.dest tyenv, Vartab.dest tenv) + end handle Pattern.MATCH => NONE; + +(* given theory, max var index, pat, tgt; returns Seq of instantiations *) +fun clean_unify thry ix (a as (pat, tgt)) = + let + (* type info will be re-derived, maybe this can be cached + for efficiency? *) + val pat_ty = Term.type_of pat; + val tgt_ty = Term.type_of tgt; + (* is it OK to ignore the type instantiation info? + or should I be using it? *) + val typs_unify = + SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix)) + handle Type.TUNIFY => NONE; + in + case typs_unify of + SOME (typinsttab, ix2) => + let + (* is it right to throw away the flexes? + or should I be using them somehow? *) + fun mk_insts env = + (Vartab.dest (Envir.type_env env), + Envir.alist_of env); + val initenv = Envir.Envir {asol = Vartab.empty, + iTs = typinsttab, maxidx = ix2}; + val useq = Unify.smash_unifiers thry [a] initenv + handle UnequalLengths => Seq.empty + | Term.TERM _ => Seq.empty; + fun clean_unify' useq () = + (case (Seq.pull useq) of + NONE => NONE + | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t))) + handle UnequalLengths => NONE + | Term.TERM _ => NONE + in + (Seq.make (clean_unify' useq)) + end + | NONE => Seq.empty + end; + +(* Matching and Unification for zippers *) +(* Note: Ts is a modified version of the original names of the outer +bound variables. New names have been introduced to make sure they are +unique w.r.t all names in the term and each other. usednames' is +oldnames + new names. *) +fun clean_match_z thy pat z = + let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in + case clean_match thy (pat, t) of + NONE => NONE + | SOME insts => SOME (insts, FakeTs, Ts, absterm) end; +(* ix = max var index *) +fun clean_unify_z sgn ix pat z = + let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in + Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) + (clean_unify sgn ix (t, pat)) end; + + +(* FOR DEBUGGING... +type trace_subst_errT = int (* subgoal *) + * thm (* thm with all goals *) + * (Thm.cterm list (* certified free var placeholders for vars *) + * thm) (* trivial thm of goal concl *) + (* possible matches/unifiers *) + * thm (* rule *) + * (((indexname * typ) list (* type instantiations *) + * (indexname * term) list ) (* term instantiations *) + * (string * typ) list (* Type abs env *) + * term) (* outer term *); + +val trace_subst_err = (ref NONE : trace_subst_errT option ref); +val trace_subst_search = ref false; +exception trace_subst_exp of trace_subst_errT; +*) + + +fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l + | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t + | bot_left_leaf_of x = x; + +(* Avoid considering replacing terms which have a var at the head as + they always succeed trivially, and uninterestingly. *) +fun valid_match_start z = + (case bot_left_leaf_of (Z.trm z) of + Var _ => false + | _ => true); + +(* search from top, left to right, then down *) +val search_lr_all = ZipperSearch.all_bl_ur; + +(* search from top, left to right, then down *) +fun search_lr_valid validf = + let + fun sf_valid_td_lr z = + let val here = if validf z then [Z.Here z] else [] in + case Z.trm z + of _ $ _ => [Z.LookIn (Z.move_down_left z)] + @ here + @ [Z.LookIn (Z.move_down_right z)] + | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)] + | _ => here + end; + in Z.lzy_search sf_valid_td_lr end; + +(* search from bottom to top, left to right *) + +fun search_bt_valid validf = + let + fun sf_valid_td_lr z = + let val here = if validf z then [Z.Here z] else [] in + case Z.trm z + of _ $ _ => [Z.LookIn (Z.move_down_left z), + Z.LookIn (Z.move_down_right z)] @ here + | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here + | _ => here + end; + in Z.lzy_search sf_valid_td_lr end; + +fun searchf_unify_gen f (sgn, maxidx, z) lhs = + Seq.map (clean_unify_z sgn maxidx lhs) + (Z.limit_apply f z); + +(* search all unifications *) +val searchf_lr_unify_all = + searchf_unify_gen search_lr_all; + +(* search only for 'valid' unifiers (non abs subterms and non vars) *) +val searchf_lr_unify_valid = + searchf_unify_gen (search_lr_valid valid_match_start); + +val searchf_bt_unify_valid = + searchf_unify_gen (search_bt_valid valid_match_start); + +(* apply a substitution in the conclusion of the theorem th *) +(* cfvs are certified free var placeholders for goal params *) +(* conclthm is a theorem of for just the conclusion *) +(* m is instantiation/match information *) +(* rule is the equation for substitution *) +fun apply_subst_in_concl i th (cfvs, conclthm) rule m = + (RWInst.rw m rule conclthm) + |> IsaND.unfix_frees cfvs + |> RWInst.beta_eta_contract + |> (fn r => Tactic.rtac r i th); + +(* substitute within the conclusion of goal i of gth, using a meta +equation rule. Note that we assume rule has var indicies zero'd *) +fun prep_concl_subst i gth = + let + val th = Thm.incr_indexes 1 gth; + val tgt_term = Thm.prop_of th; + + val sgn = Thm.theory_of_thm th; + val ctermify = Thm.cterm_of sgn; + val trivify = Thm.trivial o ctermify; + + val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; + val cfvs = rev (map ctermify fvs); + + val conclterm = Logic.strip_imp_concl fixedbody; + val conclthm = trivify conclterm; + val maxidx = Thm.maxidx_of th; + val ft = ((Z.move_down_right (* ==> *) + o Z.move_down_left (* Trueprop *) + o Z.mktop + o Thm.prop_of) conclthm) + in + ((cfvs, conclthm), (sgn, maxidx, ft)) + end; + +(* substitute using an object or meta level equality *) +fun eqsubst_tac' ctxt searchf instepthm i th = + let + val (cvfsconclthm, searchinfo) = prep_concl_subst i th; + val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); + fun rewrite_with_thm r = + let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); + in searchf searchinfo lhs + |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end; + in stepthms |> Seq.maps rewrite_with_thm end; + + +(* distinct subgoals *) +fun distinct_subgoals th = + the_default th (SINGLE distinct_subgoals_tac th); + +(* General substitution of multiple occurances using one of + the given theorems*) + + +exception eqsubst_occL_exp of + string * (int list) * (thm list) * int * thm; +fun skip_first_occs_search occ srchf sinfo lhs = + case (skipto_skipseq occ (srchf sinfo lhs)) of + SkipMore _ => Seq.empty + | SkipSeq ss => Seq.flat ss; + +(* The occL is a list of integers indicating which occurence +w.r.t. the search order, to rewrite. Backtracking will also find later +occurences, but all earlier ones are skipped. Thus you can use [0] to +just find all rewrites. *) + +fun eqsubst_tac ctxt occL thms i th = + let val nprems = Thm.nprems_of th in + if nprems < i then Seq.empty else + let val thmseq = (Seq.of_list thms) + fun apply_occ occ th = + thmseq |> Seq.maps + (fn r => eqsubst_tac' + ctxt + (skip_first_occs_search + occ searchf_lr_unify_valid) r + (i + ((Thm.nprems_of th) - nprems)) + th); + val sortedoccL = + Library.sort (Library.rev_order o Library.int_ord) occL; + in + Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th) + end + end + handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); + + +(* inthms are the given arguments in Isar, and treated as eqstep with + the first one, then the second etc *) +fun eqsubst_meth ctxt occL inthms = + Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms); + +(* apply a substitution inside assumption j, keeps asm in the same place *) +fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) = + let + val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *) + val preelimrule = + (RWInst.rw m rule pth) + |> (Seq.hd o prune_params_tac) + |> Thm.permute_prems 0 ~1 (* put old asm first *) + |> IsaND.unfix_frees cfvs (* unfix any global params *) + |> RWInst.beta_eta_contract; (* normal form *) + (* val elimrule = + preelimrule + |> Tactic.make_elim (* make into elim rule *) + |> Thm.lift_rule (th2, i); (* lift into context *) + *) + in + (* ~j because new asm starts at back, thus we subtract 1 *) + Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i)) + (Tactic.dtac preelimrule i th2) + + (* (Thm.bicompose + false (* use unification *) + (true, (* elim resolution *) + elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems) + i th2) *) + end; + + +(* prepare to substitute within the j'th premise of subgoal i of gth, +using a meta-level equation. Note that we assume rule has var indicies +zero'd. Note that we also assume that premt is the j'th premice of +subgoal i of gth. Note the repetition of work done for each +assumption, i.e. this can be made more efficient for search over +multiple assumptions. *) +fun prep_subst_in_asm i gth j = + let + val th = Thm.incr_indexes 1 gth; + val tgt_term = Thm.prop_of th; + + val sgn = Thm.theory_of_thm th; + val ctermify = Thm.cterm_of sgn; + val trivify = Thm.trivial o ctermify; + + val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; + val cfvs = rev (map ctermify fvs); + + val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1); + val asm_nprems = length (Logic.strip_imp_prems asmt); + + val pth = trivify asmt; + val maxidx = Thm.maxidx_of th; + + val ft = ((Z.move_down_right (* trueprop *) + o Z.mktop + o Thm.prop_of) pth) + in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end; + +(* prepare subst in every possible assumption *) +fun prep_subst_in_asms i gth = + map (prep_subst_in_asm i gth) + ((fn l => Library.upto (1, length l)) + (Logic.prems_of_goal (Thm.prop_of gth) i)); + + +(* substitute in an assumption using an object or meta level equality *) +fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th = + let + val asmpreps = prep_subst_in_asms i th; + val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm); + fun rewrite_with_thm r = + let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) + fun occ_search occ [] = Seq.empty + | occ_search occ ((asminfo, searchinfo)::moreasms) = + (case searchf searchinfo occ lhs of + SkipMore i => occ_search i moreasms + | SkipSeq ss => + Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss)) + (occ_search 1 moreasms)) + (* find later substs also *) + in + occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r) + end; + in stepthms |> Seq.maps rewrite_with_thm end; + + +fun skip_first_asm_occs_search searchf sinfo occ lhs = + skipto_skipseq occ (searchf sinfo lhs); + +fun eqsubst_asm_tac ctxt occL thms i th = + let val nprems = Thm.nprems_of th + in + if nprems < i then Seq.empty else + let val thmseq = (Seq.of_list thms) + fun apply_occ occK th = + thmseq |> Seq.maps + (fn r => + eqsubst_asm_tac' ctxt (skip_first_asm_occs_search + searchf_lr_unify_valid) occK r + (i + ((Thm.nprems_of th) - nprems)) + th); + val sortedoccs = + Library.sort (Library.rev_order o Library.int_ord) occL + in + Seq.map distinct_subgoals + (Seq.EVERY (map apply_occ sortedoccs) th) + end + end + handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); + +(* inthms are the given arguments in Isar, and treated as eqstep with + the first one, then the second etc *) +fun eqsubst_asm_meth ctxt occL inthms = + Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms); + +(* syntax for options, given "(asm)" will give back true, without + gives back false *) +val options_syntax = + (Args.parens (Args.$$$ "asm") >> (K true)) || + (Scan.succeed false); + +val ith_syntax = + Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0]; + +(* combination method that takes a flag (true indicates that subst +should be done to an assumption, false = apply to the conclusion of +the goal) as well as the theorems to use *) +fun subst_meth src = + Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src + #> (fn (((asmflag, occL), inthms), ctxt) => + (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms); + + +val setup = + Method.add_method ("subst", subst_meth, "single-step substitution"); + +end; diff -r 7b55b6b5c0c2 -r 5f7b17941730 src/Tools/project_rule.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/project_rule.ML Sat Feb 28 14:02:12 2009 +0100 @@ -0,0 +1,65 @@ +(* Title: Tools/project_rule.ML + Author: Makarius + +Transform mutual rule: + + HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn) + +into projection: + + xi:Ai ==> HH ==> Pi xi +*) + +signature PROJECT_RULE_DATA = +sig + val conjunct1: thm + val conjunct2: thm + val mp: thm +end; + +signature PROJECT_RULE = +sig + val project: Proof.context -> int -> thm -> thm + val projects: Proof.context -> int list -> thm -> thm list + val projections: Proof.context -> thm -> thm list +end; + +functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE = +struct + +fun conj1 th = th RS Data.conjunct1; +fun conj2 th = th RS Data.conjunct2; +fun imp th = th RS Data.mp; + +fun projects ctxt is raw_rule = + let + fun proj 1 th = the_default th (try conj1 th) + | proj k th = proj (k - 1) (conj2 th); + fun prems k th = + (case try imp th of + NONE => (k, th) + | SOME th' => prems (k + 1) th'); + val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt; + fun result i = + rule + |> proj i + |> prems 0 |-> (fn k => + Thm.permute_prems 0 (~ k) + #> singleton (Variable.export ctxt' ctxt) + #> Drule.zero_var_indexes + #> RuleCases.save raw_rule + #> RuleCases.add_consumes k); + in map result is end; + +fun project ctxt i th = hd (projects ctxt [i] th); + +fun projections ctxt raw_rule = + let + fun projs k th = + (case try conj2 th of + NONE => k + | SOME th' => projs (k + 1) th'); + val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt; + in projects ctxt (1 upto projs 1 rule) raw_rule end; + +end;