src/Pure/thm.ML
changeset 52223 5bb6ae8acb87
parent 52222 0fa3b456a267
child 52470 dedd7952a62c
equal deleted inserted replaced
52222:0fa3b456a267 52223:5bb6ae8acb87
   142   val eq_assumption: int -> thm -> thm
   142   val eq_assumption: int -> thm -> thm
   143   val rotate_rule: int -> int -> thm -> thm
   143   val rotate_rule: int -> int -> thm -> thm
   144   val permute_prems: int -> int -> thm -> thm
   144   val permute_prems: int -> int -> thm -> thm
   145   val rename_params_rule: string list * int -> thm -> thm
   145   val rename_params_rule: string list * int -> thm -> thm
   146   val rename_boundvars: term -> term -> thm -> thm
   146   val rename_boundvars: term -> term -> thm -> thm
   147   val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   147   val bicompose: {flatten: bool, match: bool, incremented: bool} ->
   148   val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   148     bool * thm * int -> int -> thm -> thm Seq.seq
   149   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   149   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   150   val extern_oracles: Proof.context -> (Markup.T * xstring) list
   150   val extern_oracles: Proof.context -> (Markup.T * xstring) list
   151   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   151   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   152 end;
   152 end;
   153 
   153 
  1613   nsubgoal is the number of new subgoals (written m above).
  1613   nsubgoal is the number of new subgoals (written m above).
  1614   Curried so that resolution calls dest_state only once.
  1614   Curried so that resolution calls dest_state only once.
  1615 *)
  1615 *)
  1616 local exception COMPOSE
  1616 local exception COMPOSE
  1617 in
  1617 in
  1618 fun bicompose_aux flatten match (state, (stpairs, Bs, Bi, C), lifted)
  1618 fun bicompose_aux {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
  1619                         (eres_flg, orule, nsubgoal) =
  1619                         (eres_flg, orule, nsubgoal) =
  1620  let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
  1620  let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
  1621      and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
  1621      and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
  1622              tpairs=rtpairs, prop=rprop,...}) = orule
  1622              tpairs=rtpairs, prop=rprop,...}) = orule
  1623          (*How many hyps to skip over during normalization*)
  1623          (*How many hyps to skip over during normalization*)
  1703            Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
  1703            Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs)))
  1704              (Seq.make (fn () => cell), Seq.empty));
  1704              (Seq.make (fn () => cell), Seq.empty));
  1705 
  1705 
  1706      val env0 = Envir.empty (Int.max (rmax, smax));
  1706      val env0 = Envir.empty (Int.max (rmax, smax));
  1707  in
  1707  in
  1708    (case if lifted then SOME env0 else unify_var_types thy (state, orule) env0 of
  1708    (case if incremented then SOME env0 else unify_var_types thy (state, orule) env0 of
  1709      NONE => Seq.empty
  1709      NONE => Seq.empty
  1710    | SOME env => if eres_flg then eres env (rev rAs) else res env)
  1710    | SOME env => if eres_flg then eres env (rev rAs) else res env)
  1711  end;
  1711  end;
  1712 end;
  1712 end;
  1713 
  1713 
  1714 fun compose_no_flatten match (orule, nsubgoal) i state =
  1714 fun bicompose flags arg i state =
  1715   bicompose_aux false match (state, dest_state (state, i), false) (false, orule, nsubgoal);
  1715   bicompose_aux flags (state, dest_state (state,i), false) arg;
  1716 
       
  1717 fun bicompose match arg i state =
       
  1718   bicompose_aux true match (state, dest_state (state,i), false) arg;
       
  1719 
  1716 
  1720 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  1717 (*Quick test whether rule is resolvable with the subgoal with hyps Hs
  1721   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  1718   and conclusion B.  If eres_flg then checks 1st premise of rule also*)
  1722 fun could_bires (Hs, B, eres_flg, rule) =
  1719 fun could_bires (Hs, B, eres_flg, rule) =
  1723     let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
  1720     let fun could_reshyp (A1::_) = exists (fn H => Term.could_unify (A1, H)) Hs
  1731 fun biresolution match brules i state =
  1728 fun biresolution match brules i state =
  1732     let val (stpairs, Bs, Bi, C) = dest_state(state,i);
  1729     let val (stpairs, Bs, Bi, C) = dest_state(state,i);
  1733         val lift = lift_rule (cprem_of state i);
  1730         val lift = lift_rule (cprem_of state i);
  1734         val B = Logic.strip_assums_concl Bi;
  1731         val B = Logic.strip_assums_concl Bi;
  1735         val Hs = Logic.strip_assums_hyp Bi;
  1732         val Hs = Logic.strip_assums_hyp Bi;
  1736         val compose = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true);
  1733         val compose =
       
  1734           bicompose_aux {flatten = true, match = match, incremented = true}
       
  1735             (state, (stpairs, Bs, Bi, C), true);
  1737         fun res [] = Seq.empty
  1736         fun res [] = Seq.empty
  1738           | res ((eres_flg, rule)::brules) =
  1737           | res ((eres_flg, rule)::brules) =
  1739               if !Pattern.trace_unify_fail orelse
  1738               if !Pattern.trace_unify_fail orelse
  1740                  could_bires (Hs, B, eres_flg, rule)
  1739                  could_bires (Hs, B, eres_flg, rule)
  1741               then Seq.make (*delay processing remainder till needed*)
  1740               then Seq.make (*delay processing remainder till needed*)