use conjunction stuff from conjunction.ML;
authorwenzelm
Thu Apr 13 12:01:01 2006 +0200 (2006-04-13)
changeset 1942351eeee99bd8f
parent 19422 bba26da0f227
child 19424 b701ea590259
use conjunction stuff from conjunction.ML;
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_cases.ML
src/Pure/goal.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Apr 13 12:01:00 2006 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Apr 13 12:01:01 2006 +0200
     1.3 @@ -1620,12 +1620,12 @@
     1.4      val intro = Drule.standard (Goal.prove defs_thy [] norm_ts statement (fn _ =>
     1.5        Tactic.rewrite_goals_tac [pred_def] THEN
     1.6        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
     1.7 -      Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
     1.8 +      Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1));
     1.9  
    1.10      val conjuncts =
    1.11 -      (Drule.equal_elim_rule1 OF [Thm.symmetric body_eq,
    1.12 +      (Drule.equal_elim_rule2 OF [body_eq,
    1.13          Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))])
    1.14 -      |> Drule.conj_elim_precise [length ts] |> hd;
    1.15 +      |> Conjunction.elim_precise [length ts] |> hd;
    1.16      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    1.17        prove_protected defs_thy t
    1.18         (Tactic.rewrite_goals_tac defs THEN
     2.1 --- a/src/Pure/Isar/proof.ML	Thu Apr 13 12:01:00 2006 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Thu Apr 13 12:01:01 2006 +0200
     2.3 @@ -496,7 +496,7 @@
     2.4      val _ = conditional (not (Pattern.matches thy
     2.5          (Logic.mk_conjunction_list2 propss, Thm.prop_of th))) (fn () =>
     2.6        error ("Proved a different theorem:\n" ^ ProofContext.string_of_thm ctxt th));
     2.7 -  in Drule.conj_elim_precise (map length propss) th end;
     2.8 +  in Conjunction.elim_precise (map length propss) th end;
     2.9  
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/rule_cases.ML	Thu Apr 13 12:01:00 2006 +0200
     3.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu Apr 13 12:01:01 2006 +0200
     3.3 @@ -195,7 +195,7 @@
     3.4    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
     3.5    else
     3.6      Drule.fconv_rule
     3.7 -      (Drule.concl_conv ~1 (Drule.conjunction_conv ~1
     3.8 +      (Drule.concl_conv ~1 (Conjunction.conv ~1
     3.9          (K (Drule.prems_conv ~1 (K (Tactic.rewrite true defs)))))) th;
    3.10  
    3.11  in
    3.12 @@ -337,7 +337,7 @@
    3.13          else
    3.14            SOME (ns,
    3.15              ths
    3.16 -            |> foldr1 (uncurry Drule.conj_intr)
    3.17 +            |> foldr1 (uncurry Conjunction.intr)
    3.18              |> Drule.implies_intr_list prems
    3.19              |> Drule.standard'
    3.20              |> save (hd raw_rules)
     4.1 --- a/src/Pure/goal.ML	Thu Apr 13 12:01:00 2006 +0200
     4.2 +++ b/src/Pure/goal.ML	Thu Apr 13 12:01:01 2006 +0200
     4.3 @@ -147,7 +147,7 @@
     4.4      val _ = conditional (not (Pattern.matches thy (Envir.beta_norm prop, prop'))) (fn () =>
     4.5        err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
     4.6    in
     4.7 -    hd (Drule.conj_elim_precise [length props] raw_result)
     4.8 +    hd (Conjunction.elim_precise [length props] raw_result)
     4.9      |> map
    4.10        (Drule.implies_intr_list casms
    4.11          #> Drule.forall_intr_list cparams
    4.12 @@ -176,12 +176,12 @@
    4.13  fun extract i n st =
    4.14    (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    4.15     else if n = 1 then Seq.single (Thm.cprem_of st i)
    4.16 -   else Seq.single (foldr1 Drule.mk_conjunction (map (Thm.cprem_of st) (i upto (i + n - 1)))))
    4.17 +   else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
    4.18    |> Seq.map (Thm.adjust_maxidx #> init);
    4.19  
    4.20  fun retrofit i n st' st =
    4.21    (if n = 1 then st
    4.22 -   else st |> Drule.rotate_prems (i - 1) |> Drule.conj_uncurry n |> Drule.rotate_prems (1 - i))
    4.23 +   else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
    4.24    |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
    4.25  
    4.26  fun SELECT_GOAL tac i st =
     5.1 --- a/src/Pure/tactic.ML	Thu Apr 13 12:01:00 2006 +0200
     5.2 +++ b/src/Pure/tactic.ML	Thu Apr 13 12:01:01 2006 +0200
     5.3 @@ -642,7 +642,7 @@
     5.4  (* meta-level conjunction *)
     5.5  
     5.6  val conj_tac = SUBGOAL (fn (goal, i) =>
     5.7 -  if can Logic.dest_conjunction goal then rtac Drule.conjunctionI i
     5.8 +  if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
     5.9    else no_tac);
    5.10  
    5.11  val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac;
    5.12 @@ -657,12 +657,12 @@
    5.13  fun CONJUNCTS tac =
    5.14    SELECT_GOAL (conjunction_tac 1
    5.15      THEN tac
    5.16 -    THEN PRIMITIVE (Drule.conj_uncurry ~1));
    5.17 +    THEN PRIMITIVE (Conjunction.uncurry ~1));
    5.18  
    5.19  fun PRECISE_CONJUNCTS n tac =
    5.20    SELECT_GOAL (precise_conjunction_tac n 1
    5.21      THEN tac
    5.22 -    THEN PRIMITIVE (Drule.conj_uncurry ~1));
    5.23 +    THEN PRIMITIVE (Conjunction.uncurry ~1));
    5.24  
    5.25  end;
    5.26