# HG changeset patch # User dixon # Date 1116008501 -7200 # Node ID 366d39e95d3c1b71d4b442316a6647b01586a3ee # Parent b4ea8bf8e2f7de23b9ed929f4fc41d89d6284825 lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints) diff -r b4ea8bf8e2f7 -r 366d39e95d3c src/Provers/eqsubst.ML --- a/src/Provers/eqsubst.ML Fri May 13 19:55:09 2005 +0200 +++ b/src/Provers/eqsubst.ML Fri May 13 20:21:41 2005 +0200 @@ -27,6 +27,9 @@ signature EQSUBST_TAC = sig + exception eqsubst_occL_exp of + string * (int list) * (Thm.thm list) * int * Thm.thm; + type match = ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *) * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *) @@ -273,9 +276,29 @@ in (stepthms :-> rewrite_with_thm) end; +(* Tactic.distinct_subgoals_tac *) + +(* custom version of distinct subgoals that works with term and + type variables. Asssumes th is in beta-eta normal form. + Also, does nothing if flexflex contraints are present. *) +fun distinct_subgoals th = + if List.null (Thm.tpairs_of th) then + let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th + val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm + in + IsaND.unfix_frees_and_tfrees + fixes + (Drule.implies_intr_list + (Library.gen_distinct + (fn (x, y) => Thm.term_of x = Thm.term_of y) + cprems) fixedthconcl) + end + else th; (* General substiuttion of multiple occurances using one of the given theorems*) +exception eqsubst_occL_exp of + string * (int list) * (Thm.thm list) * int * Thm.thm; fun eqsubst_occL tac occL thms i th = let val nprems = Thm.nprems_of th in if nprems < i then Seq.empty else @@ -287,10 +310,15 @@ (i + ((Thm.nprems_of th) - nprems)) th); in - Seq.EVERY (map apply_occ (Library.sort (Library.rev_order o Library.int_ord) occL)) - th + Seq.map distinct_subgoals + (Seq.EVERY (map apply_occ + (Library.sort (Library.rev_order + o Library.int_ord) occL)) th) end - end; + end + handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); + + (* implicit argus: occL thms i th *) val eqsubst_tac = eqsubst_occL eqsubst_tac'; diff -r b4ea8bf8e2f7 -r 366d39e95d3c src/Pure/IsaPlanner/isand.ML --- a/src/Pure/IsaPlanner/isand.ML Fri May 13 19:55:09 2005 +0200 +++ b/src/Pure/IsaPlanner/isand.ML Fri May 13 20:21:41 2005 +0200 @@ -208,7 +208,9 @@ let val sign = Thm.sign_of_thm th; val ctypify = Thm.ctyp_of sign; - val renamings = fix_tvars_to_tfrees_in_terms [] [Thm.prop_of th]; + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); + val renamings = fix_tvars_to_tfrees_in_terms + [] ((Thm.prop_of th) :: tpairs); val crenamings = map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f))) renamings; @@ -237,7 +239,9 @@ fun fix_vars_to_frees th = let val ctermify = Thm.cterm_of (Thm.sign_of_thm th) - val renamings = fix_vars_to_frees_in_terms [] [Thm.prop_of th]; + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); + val renamings = fix_vars_to_frees_in_terms + [] ([Thm.prop_of th] @ tpairs); val crenamings = map (fn (v,f) => (ctermify (Var v), ctermify (Free f))) renamings; @@ -248,8 +252,9 @@ let val sgn = Thm.sign_of_thm th; val ctypify = Thm.ctyp_of sgn + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); val prop = (Thm.prop_of th); - val tvars = Term.term_tvars prop; + val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs); val ctyfixes = Library.mapfilter (fn (v as ((s,i),ty)) => @@ -260,8 +265,10 @@ let val sgn = Thm.sign_of_thm th; val ctermify = Thm.cterm_of sgn + val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th); val prop = (Thm.prop_of th); - val vars = map Term.dest_Var (Term.term_vars prop); + val vars = map Term.dest_Var (List.foldr Term.add_term_vars + [] (prop :: tpairs)); val cfixes = Library.mapfilter (fn (v as ((s,i),ty)) => @@ -282,8 +289,10 @@ in ((vars, tvars), th'') end; (* implicit Thm.thm argument *) +(* assumes: vars may contain fixed versions of the frees *) +(* THINK: what if vs already has types varified? *) fun unfix_frees_and_tfrees (vs,tvs) = - (unfix_frees vs o unfix_tfrees tvs); + (unfix_tfrees tvs o unfix_frees vs); (* datatype to capture an exported result, ie a fix or assume. *) datatype export = diff -r b4ea8bf8e2f7 -r 366d39e95d3c src/Pure/IsaPlanner/rw_inst.ML --- a/src/Pure/IsaPlanner/rw_inst.ML Fri May 13 19:55:09 2005 +0200 +++ b/src/Pure/IsaPlanner/rw_inst.ML Fri May 13 20:21:41 2005 +0200 @@ -201,13 +201,15 @@ in cross_instL (insts, []) end; -(* assume that rule and target_thm have distinct var names *) -(* THINK: efficient version with tables for vars for: target vars, -introduced vars, and rule vars, for quicker instantiation? *) -(* The outerterm defines which part of the target_thm was modified *) -(* Note: we take Ts in the upterm order, ie last abstraction first., -and with an outeterm where the abstracted subterm has the arguments in -the revered order, ie first abstraction first. *) +(* assume that rule and target_thm have distinct var names. THINK: +efficient version with tables for vars for: target vars, introduced +vars, and rule vars, for quicker instantiation? The outerterm defines +which part of the target_thm was modified. Note: we take Ts in the +upterm order, ie last abstraction first., and with an outeterm where +the abstracted subterm has the arguments in the revered order, ie +first abstraction first. FakeTs has abstractions using the fake name +- ie the name distinct from all other abstractions. *) + fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = let (* general signature info *) @@ -219,12 +221,14 @@ val (fixtyinsts, othertfrees) = mk_fixtvar_tyinsts nonfixed_typinsts [Thm.prop_of rule, Thm.prop_of target_thm]; - + val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty)) + fixtyinsts; val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts); (* certified instantiations for types *) val ctyp_insts = - map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) typinsts; + map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) + typinsts; (* type instantiated versions *) val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm; @@ -234,6 +238,11 @@ (* type instanitated outer term *) val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm; + val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) + FakeTs; + val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) + Ts; + (* type-instantiate the var instantiations *) val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => (ix, (Term.typ_subst_TVars term_typ_inst ty, @@ -268,7 +277,7 @@ val couter_inst = Thm.reflexive (ctermify outerterm_inst); val (cprems, abstract_rule_inst) = rule_inst |> Thm.instantiate ([], cterm_renamings) - |> mk_abstractedrule FakeTs Ts; + |> mk_abstractedrule FakeTs_tyinst Ts_tyinst; val specific_tgt_rule = beta_eta_contract (Thm.combination couter_inst abstract_rule_inst);