tuned signature -- more explicit flags for low-level Thm.bicompose;
authorwenzelm
Wed May 29 18:25:11 2013 +0200 (2013-05-29)
changeset 522235bb6ae8acb87
parent 52222 0fa3b456a267
child 52224 6ba76ad4e679
tuned signature -- more explicit flags for low-level Thm.bicompose;
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/rule_insts.ML
src/Pure/drule.ML
src/Pure/goal.ML
src/Pure/subgoal.ML
src/Pure/tactic.ML
src/Pure/thm.ML
src/Tools/eqsubst.ML
src/Tools/misc_legacy.ML
     1.1 --- a/src/HOL/Tools/Function/function_core.ML	Wed May 29 16:12:05 2013 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_core.ML	Wed May 29 18:25:11 2013 +0200
     1.3 @@ -351,7 +351,8 @@
     1.4        map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas
     1.5  
     1.6      fun elim_implies_eta A AB =
     1.7 -      Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single
     1.8 +      Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB
     1.9 +      |> Seq.list_of |> the_single
    1.10  
    1.11      val uniqueness = G_cases
    1.12        |> Thm.forall_elim (cterm_of thy lhs)
     2.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 16:12:05 2013 +0200
     2.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Wed May 29 18:25:11 2013 +0200
     2.3 @@ -385,7 +385,8 @@
     2.4      val nbranches = length branches
     2.5      val npres = length pres
     2.6    in
     2.7 -    Thm.compose_no_flatten false (res, length newgoals) i
     2.8 +    Thm.bicompose {flatten = false, match = false, incremented = false}
     2.9 +      (false, res, length newgoals) i
    2.10      THEN term_tac (i + nbranches + npres)
    2.11      THEN (EVERY (map (TRY o pres_tac) ((i + nbranches + npres - 1) downto (i + nbranches))))
    2.12      THEN (EVERY (map (TRY o comp_tac) ((i + nbranches - 1) downto i)))
     3.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 29 16:12:05 2013 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 29 18:25:11 2013 +0200
     3.3 @@ -185,14 +185,15 @@
     3.4    let
     3.5      val tha = incr_type_indexes (1 + Thm.maxidx_of thb) tha
     3.6      fun aux (tha, thb) =
     3.7 -      case Thm.bicompose false (false, tha, nprems_of tha) i thb
     3.8 +      case Thm.bicompose {flatten = true, match = false, incremented = false}
     3.9 +            (false, tha, nprems_of tha) i thb
    3.10             |> Seq.list_of |> distinct Thm.eq_thm of
    3.11          [th] => th
    3.12        | _ => raise THM ("resolve_inc_tyvars: unique result expected", i,
    3.13                          [tha, thb])
    3.14    in
    3.15      aux (tha, thb)
    3.16 -    handle TERM z =>
    3.17 +    handle TERM z =>  (* FIXME obsolete!? *)
    3.18             (* The unifier, which is invoked from "Thm.bicompose", will sometimes
    3.19                refuse to unify "?a::?'a" with "?a::?'b" or "?a::nat" and throw a
    3.20                "TERM" exception (with "add_ffpair" as first argument). We then
     4.1 --- a/src/Pure/Isar/proof_context.ML	Wed May 29 16:12:05 2013 +0200
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Wed May 29 18:25:11 2013 +0200
     4.3 @@ -869,9 +869,17 @@
     4.4  
     4.5  (* fact_tac *)
     4.6  
     4.7 +local
     4.8 +
     4.9 +fun comp_hhf_tac th i st =
    4.10 +  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = true}
    4.11 +    (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
    4.12 +
    4.13  fun comp_incr_tac [] _ = no_tac
    4.14    | comp_incr_tac (th :: ths) i =
    4.15 -      (fn st => Goal.compose_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
    4.16 +      (fn st => comp_hhf_tac (Drule.incr_indexes st th) i st) APPEND comp_incr_tac ths i;
    4.17 +
    4.18 +in
    4.19  
    4.20  fun fact_tac facts = Goal.norm_hhf_tac THEN' comp_incr_tac facts;
    4.21  
    4.22 @@ -880,6 +888,8 @@
    4.23  
    4.24  fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => fact_tac (potential_facts ctxt goal) i);
    4.25  
    4.26 +end;
    4.27 +
    4.28  
    4.29  (* get_thm(s) *)
    4.30  
     5.1 --- a/src/Pure/Isar/rule_insts.ML	Wed May 29 16:12:05 2013 +0200
     5.2 +++ b/src/Pure/Isar/rule_insts.ML	Wed May 29 18:25:11 2013 +0200
     5.3 @@ -287,7 +287,10 @@
     5.4        Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
     5.5          (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
     5.6    in
     5.7 -    (case Seq.list_of (Thm.bicompose false (false, rl, Thm.nprems_of rl) 1 revcut_rl') of
     5.8 +    (case Seq.list_of
     5.9 +      (Thm.bicompose {flatten = true, match = false, incremented = false}
    5.10 +        (false, rl, Thm.nprems_of rl) 1 revcut_rl')
    5.11 +     of
    5.12        [th] => th
    5.13      | _ => raise THM ("make_elim_preserve", 1, [rl]))
    5.14    end;
     6.1 --- a/src/Pure/drule.ML	Wed May 29 16:12:05 2013 +0200
     6.2 +++ b/src/Pure/drule.ML	Wed May 29 18:25:11 2013 +0200
     6.3 @@ -359,7 +359,9 @@
     6.4    with no lifting or renaming!  Q may contain ==> or meta-quants
     6.5    ALWAYS deletes premise i *)
     6.6  fun compose(tha,i,thb) =
     6.7 -  distinct Thm.eq_thm (Seq.list_of (Thm.bicompose false (false,tha,0) i thb));
     6.8 +  distinct Thm.eq_thm
     6.9 +    (Seq.list_of
    6.10 +      (Thm.bicompose {flatten = true, match = false, incremented = false} (false, tha, 0) i thb));
    6.11  
    6.12  fun compose_single (tha,i,thb) =
    6.13    (case compose (tha,i,thb) of
    6.14 @@ -743,7 +745,8 @@
    6.15  
    6.16  fun comp_no_flatten (th, n) i rule =
    6.17    (case distinct Thm.eq_thm (Seq.list_of
    6.18 -      (Thm.compose_no_flatten false (th, n) i (incr_indexes th rule))) of
    6.19 +      (Thm.bicompose {flatten = false, match = false, incremented = true}
    6.20 +        (false, th, n) i (incr_indexes th rule))) of
    6.21      [th'] => th'
    6.22    | [] => raise THM ("comp_no_flatten", i, [th, rule])
    6.23    | _ => raise THM ("comp_no_flatten: unique result expected", i, [th, rule]));
     7.1 --- a/src/Pure/goal.ML	Wed May 29 16:12:05 2013 +0200
     7.2 +++ b/src/Pure/goal.ML	Wed May 29 18:25:11 2013 +0200
     7.3 @@ -56,7 +56,6 @@
     7.4    val precise_conjunction_tac: int -> int -> tactic
     7.5    val recover_conjunction_tac: tactic
     7.6    val norm_hhf_tac: int -> tactic
     7.7 -  val compose_hhf_tac: thm -> int -> tactic
     7.8    val assume_rule_tac: Proof.context -> int -> tactic
     7.9  end;
    7.10  
    7.11 @@ -359,7 +358,8 @@
    7.12  fun retrofit i n st' st =
    7.13    (if n = 1 then st
    7.14     else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
    7.15 -  |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
    7.16 +  |> Thm.bicompose {flatten = false, match = false, incremented = false}
    7.17 +      (false, conclude st', Thm.nprems_of st') i;
    7.18  
    7.19  fun SELECT_GOAL tac i st =
    7.20    if Thm.nprems_of st = 1 andalso i = 1 then tac st
    7.21 @@ -403,9 +403,6 @@
    7.22      if Drule.is_norm_hhf t then all_tac
    7.23      else rewrite_goal_tac Drule.norm_hhf_eqs i);
    7.24  
    7.25 -fun compose_hhf_tac th i st =
    7.26 -  PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
    7.27 -
    7.28  
    7.29  (* non-atomic goal assumptions *)
    7.30  
     8.1 --- a/src/Pure/subgoal.ML	Wed May 29 16:12:05 2013 +0200
     8.2 +++ b/src/Pure/subgoal.ML	Wed May 29 18:25:11 2013 +0200
     8.3 @@ -125,7 +125,10 @@
     8.4        |> fold (Thm.forall_elim o #2) subgoal_inst
     8.5        |> Thm.adjust_maxidx_thm idx
     8.6        |> singleton (Variable.export ctxt2 ctxt0);
     8.7 -  in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end;
     8.8 +  in
     8.9 +    Thm.bicompose {flatten = true, match = false, incremented = false}
    8.10 +      (false, result, Thm.nprems_of st1) i st0
    8.11 +  end;
    8.12  
    8.13  
    8.14  (* tacticals *)
     9.1 --- a/src/Pure/tactic.ML	Wed May 29 16:12:05 2013 +0200
     9.2 +++ b/src/Pure/tactic.ML	Wed May 29 18:25:11 2013 +0200
     9.3 @@ -111,7 +111,8 @@
     9.4  
     9.5  (*The composition rule/state: no lifting or var renaming.
     9.6    The arg = (bires_flg, orule, m);  see Thm.bicompose for explanation.*)
     9.7 -fun compose_tac arg i = PRIMSEQ (Thm.bicompose false arg i);
     9.8 +fun compose_tac arg i =
     9.9 +  PRIMSEQ (Thm.bicompose {flatten = true, match = false, incremented = false} arg i);
    9.10  
    9.11  (*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
    9.12    like [| P&Q; P==>R |] ==> R *)
    10.1 --- a/src/Pure/thm.ML	Wed May 29 16:12:05 2013 +0200
    10.2 +++ b/src/Pure/thm.ML	Wed May 29 18:25:11 2013 +0200
    10.3 @@ -144,8 +144,8 @@
    10.4    val permute_prems: int -> int -> thm -> thm
    10.5    val rename_params_rule: string list * int -> thm -> thm
    10.6    val rename_boundvars: term -> term -> thm -> thm
    10.7 -  val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
    10.8 -  val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    10.9 +  val bicompose: {flatten: bool, match: bool, incremented: bool} ->
   10.10 +    bool * thm * int -> int -> thm -> thm Seq.seq
   10.11    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
   10.12    val extern_oracles: Proof.context -> (Markup.T * xstring) list
   10.13    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   10.14 @@ -1615,7 +1615,7 @@
   10.15  *)
   10.16  local exception COMPOSE
   10.17  in
   10.18 -fun bicompose_aux flatten match (state, (stpairs, Bs, Bi, C), lifted)
   10.19 +fun bicompose_aux {flatten, match, incremented} (state, (stpairs, Bs, Bi, C), lifted)
   10.20                          (eres_flg, orule, nsubgoal) =
   10.21   let val Thm (sder, {maxidx=smax, shyps=sshyps, hyps=shyps, ...}) = state
   10.22       and Thm (rder, {maxidx=rmax, shyps=rshyps, hyps=rhyps,
   10.23 @@ -1705,17 +1705,14 @@
   10.24  
   10.25       val env0 = Envir.empty (Int.max (rmax, smax));
   10.26   in
   10.27 -   (case if lifted then SOME env0 else unify_var_types thy (state, orule) env0 of
   10.28 +   (case if incremented then SOME env0 else unify_var_types thy (state, orule) env0 of
   10.29       NONE => Seq.empty
   10.30     | SOME env => if eres_flg then eres env (rev rAs) else res env)
   10.31   end;
   10.32  end;
   10.33  
   10.34 -fun compose_no_flatten match (orule, nsubgoal) i state =
   10.35 -  bicompose_aux false match (state, dest_state (state, i), false) (false, orule, nsubgoal);
   10.36 -
   10.37 -fun bicompose match arg i state =
   10.38 -  bicompose_aux true match (state, dest_state (state,i), false) arg;
   10.39 +fun bicompose flags arg i state =
   10.40 +  bicompose_aux flags (state, dest_state (state,i), false) arg;
   10.41  
   10.42  (*Quick test whether rule is resolvable with the subgoal with hyps Hs
   10.43    and conclusion B.  If eres_flg then checks 1st premise of rule also*)
   10.44 @@ -1733,7 +1730,9 @@
   10.45          val lift = lift_rule (cprem_of state i);
   10.46          val B = Logic.strip_assums_concl Bi;
   10.47          val Hs = Logic.strip_assums_hyp Bi;
   10.48 -        val compose = bicompose_aux true match (state, (stpairs, Bs, Bi, C), true);
   10.49 +        val compose =
   10.50 +          bicompose_aux {flatten = true, match = match, incremented = true}
   10.51 +            (state, (stpairs, Bs, Bi, C), true);
   10.52          fun res [] = Seq.empty
   10.53            | res ((eres_flg, rule)::brules) =
   10.54                if !Pattern.trace_unify_fail orelse
    11.1 --- a/src/Tools/eqsubst.ML	Wed May 29 16:12:05 2013 +0200
    11.2 +++ b/src/Tools/eqsubst.ML	Wed May 29 18:25:11 2013 +0200
    11.3 @@ -365,12 +365,6 @@
    11.4        (* ~j because new asm starts at back, thus we subtract 1 *)
    11.5        Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
    11.6        (Tactic.dtac preelimrule i th2)
    11.7 -
    11.8 -      (* (Thm.bicompose
    11.9 -                 false (* use unification *)
   11.10 -                 (true, (* elim resolution *)
   11.11 -                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   11.12 -                 i th2) *)
   11.13      end;
   11.14  
   11.15  
    12.1 --- a/src/Tools/misc_legacy.ML	Wed May 29 16:12:05 2013 +0200
    12.2 +++ b/src/Tools/misc_legacy.ML	Wed May 29 18:25:11 2013 +0200
    12.3 @@ -203,7 +203,9 @@
    12.4                    (forall_intr_list cparams (implies_intr_list chyps Cth)))
    12.5          end
    12.6        (*function to replace the current subgoal*)
    12.7 -      fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state
    12.8 +      fun next st =
    12.9 +        Thm.bicompose {flatten = true, match = false, incremented = false}
   12.10 +          (false, relift st, nprems_of st) gno state
   12.11    in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end;
   12.12  
   12.13  fun print_vars_terms n thm =