balanced conjunctions;
authorwenzelm
Tue Jun 19 23:15:27 2007 +0200 (2007-06-19)
changeset 23418c195f6f13769
parent 23417 42c1a89b45c1
child 23419 8c30dd4b3b22
balanced conjunctions;
src/HOL/Nominal/nominal_primrec.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Tools/codegen_func.ML
src/Pure/goal.ML
src/Pure/logic.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Jun 19 23:15:23 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Jun 19 23:15:27 2007 +0200
     1.3 @@ -350,7 +350,7 @@
     1.4  
     1.5      val rule_prems = cprems @ flat cpremss;
     1.6      val rule = implies_intr_list rule_prems
     1.7 -      (foldr1 (uncurry Conjunction.intr) (map mk_eqn (rec_rewrites' ~~ asmss)));
     1.8 +      (Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
     1.9  
    1.10      val goals = map (fn ((cargs, _, _), (_, eqn)) =>
    1.11        (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns);
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Jun 19 23:15:23 2007 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Jun 19 23:15:27 2007 +0200
     2.3 @@ -214,7 +214,7 @@
     2.4    (* A registration is indexed by parameter instantiation.  Its components are:
     2.5       - parameters and prefix
     2.6         (if the Boolean flag is set, only accesses containing the prefix are generated,
     2.7 -        otherwise the prefix may be omitted when accessing theorems etc.) 
     2.8 +        otherwise the prefix may be omitted when accessing theorems etc.)
     2.9       - theorems (actually witnesses) instantiating locale assumptions
    2.10       - theorems (equations, actually witnesses) interpreting derived concepts
    2.11         and indexed by lhs
    2.12 @@ -656,10 +656,10 @@
    2.13  
    2.14      fun unify T U envir = Sign.typ_unify thy (U, T) envir
    2.15        handle Type.TUNIFY =>
    2.16 -        let 
    2.17 +        let
    2.18            val T' = Envir.norm_type (fst envir) T;
    2.19            val U' = Envir.norm_type (fst envir) U;
    2.20 -          val prt = Sign.string_of_typ thy; 
    2.21 +          val prt = Sign.string_of_typ thy;
    2.22          in
    2.23            raise TYPE ("unify_parms: failed to unify types " ^
    2.24              prt U' ^ " and " ^ prt T', [U', T'], [])
    2.25 @@ -1660,7 +1660,7 @@
    2.26        (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
    2.27    add_thmss loc Thm.internalK [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
    2.28  
    2.29 -in  
    2.30 +in
    2.31  
    2.32  val add_type_syntax = add_decls (apfst o cons);
    2.33  val add_term_syntax = add_decls (apsnd o cons);
    2.34 @@ -1687,7 +1687,7 @@
    2.35  
    2.36  fun atomize_spec thy ts =
    2.37    let
    2.38 -    val t = Logic.mk_conjunction_list ts;
    2.39 +    val t = Logic.mk_conjunction_balanced ts;
    2.40      val body = ObjectLogic.atomize_term thy t;
    2.41      val bodyT = Term.fastype_of body;
    2.42    in
    2.43 @@ -1737,12 +1737,13 @@
    2.44      val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
    2.45        MetaSimplifier.rewrite_goals_tac [pred_def] THEN
    2.46        Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
    2.47 -      Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
    2.48 +      Tactic.compose_tac (false,
    2.49 +        Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
    2.50  
    2.51      val conjuncts =
    2.52        (Drule.equal_elim_rule2 OF [body_eq,
    2.53          MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
    2.54 -      |> Conjunction.elim_precise [length ts] |> hd;
    2.55 +      |> Conjunction.elim_balanced (length ts);
    2.56      val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
    2.57        Element.prove_witness defs_ctxt t
    2.58         (MetaSimplifier.rewrite_goals_tac defs THEN
    2.59 @@ -2353,7 +2354,7 @@
    2.60        #> after_qed;
    2.61    in
    2.62      thy
    2.63 -    |> ProofContext.init 
    2.64 +    |> ProofContext.init
    2.65      |> Proof.theorem_i NONE after_qed' (prep_propp propss)
    2.66      |> Element.refine_witness
    2.67      |> Seq.hd
     3.1 --- a/src/Pure/Isar/proof.ML	Tue Jun 19 23:15:23 2007 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Tue Jun 19 23:15:27 2007 +0200
     3.3 @@ -468,11 +468,22 @@
     3.4      val _ = null extra_hyps orelse
     3.5        error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
     3.6  
     3.7 -    val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
     3.8 -      handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
     3.9 -    val _ = Unify.matches_list thy (flat propss) (map Thm.prop_of (flat results)) orelse
    3.10 +    fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
    3.11 +
    3.12 +    val th = Goal.conclude goal handle THM _ => lost_structure ();
    3.13 +    val goal_propss = filter_out null propss;
    3.14 +    val results =
    3.15 +      Conjunction.elim_balanced (length goal_propss) th
    3.16 +      |> map2 Conjunction.elim_balanced (map length goal_propss)
    3.17 +      handle THM _ => lost_structure ();
    3.18 +    val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
    3.19        error ("Proved a different theorem:\n" ^ string_of_thm th);
    3.20 -  in results end;
    3.21 +
    3.22 +    fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
    3.23 +      | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
    3.24 +      | recover_result [] [] = []
    3.25 +      | recover_result _ _ = lost_structure ();
    3.26 +  in recover_result propss results end;
    3.27  
    3.28  
    3.29  
    3.30 @@ -758,6 +769,7 @@
    3.31  fun generic_goal prepp kind before_qed after_qed raw_propp state =
    3.32    let
    3.33      val thy = theory_of state;
    3.34 +    val cert = Thm.cterm_of thy;
    3.35      val chaining = can assert_chain state;
    3.36  
    3.37      val ((propss, after_ctxt), goal_state) =
    3.38 @@ -773,7 +785,9 @@
    3.39      val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
    3.40  
    3.41      val propss' = map (Logic.mk_term o Var) vars :: propss;
    3.42 -    val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss'));
    3.43 +    val goal_propss = filter_out null propss';
    3.44 +    val goal = Goal.init (cert
    3.45 +      (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)));
    3.46      val after_qed' = after_qed |>> (fn after_local =>
    3.47        fn results => map_context after_ctxt #> after_local results);
    3.48    in
    3.49 @@ -787,7 +801,7 @@
    3.50      |> open_block
    3.51      |> put_goal NONE
    3.52      |> enter_backward
    3.53 -    |> not (null vars) ? refine_terms (length propss')
    3.54 +    |> not (null vars) ? refine_terms (length goal_propss)
    3.55      |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
    3.56    end;
    3.57  
     4.1 --- a/src/Pure/Isar/rule_cases.ML	Tue Jun 19 23:15:23 2007 +0200
     4.2 +++ b/src/Pure/Isar/rule_cases.ML	Tue Jun 19 23:15:27 2007 +0200
     4.3 @@ -195,8 +195,8 @@
     4.4    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
     4.5    else
     4.6      Conv.fconv_rule
     4.7 -      (Conv.concl_conv ~1 (Conjunction.conv ~1
     4.8 -        (K (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
     4.9 +      (Conv.concl_conv ~1 (Conjunction.convs
    4.10 +        (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs))))) th;
    4.11  
    4.12  in
    4.13  
    4.14 @@ -338,7 +338,7 @@
    4.15          else
    4.16            SOME (ns,
    4.17              rls
    4.18 -            |> foldr1 (uncurry Conjunction.intr)
    4.19 +            |> Conjunction.intr_balanced
    4.20              |> Drule.implies_intr_list prems
    4.21              |> singleton (Variable.export ctxt' ctxt)
    4.22              |> save th
     5.1 --- a/src/Pure/Tools/codegen_func.ML	Tue Jun 19 23:15:23 2007 +0200
     5.2 +++ b/src/Pure/Tools/codegen_func.ML	Tue Jun 19 23:15:27 2007 +0200
     5.3 @@ -238,9 +238,9 @@
     5.4      fun burrow_thms f [] = []
     5.5        | burrow_thms f thms =
     5.6            thms
     5.7 -          |> Conjunction.intr_list
     5.8 +          |> Conjunction.intr_balanced
     5.9            |> f
    5.10 -          |> Conjunction.elim_list;
    5.11 +          |> Conjunction.elim_balanced (length thms)
    5.12    in
    5.13      thms
    5.14      |> burrow_thms (canonical_tvars purify_tvar)
     6.1 --- a/src/Pure/goal.ML	Tue Jun 19 23:15:23 2007 +0200
     6.2 +++ b/src/Pure/goal.ML	Tue Jun 19 23:15:27 2007 +0200
     6.3 @@ -8,8 +8,8 @@
     6.4  signature BASIC_GOAL =
     6.5  sig
     6.6    val SELECT_GOAL: tactic -> int -> tactic
     6.7 +  val CONJUNCTS: tactic -> int -> tactic
     6.8    val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
     6.9 -  val CONJUNCTS: tactic -> int -> tactic
    6.10  end;
    6.11  
    6.12  signature GOAL =
    6.13 @@ -29,8 +29,9 @@
    6.14    val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
    6.15    val extract: int -> int -> thm -> thm Seq.seq
    6.16    val retrofit: int -> int -> thm -> thm -> thm Seq.seq
    6.17 +  val conjunction_tac: int -> tactic
    6.18    val precise_conjunction_tac: int -> int -> tactic
    6.19 -  val conjunction_tac: int -> tactic
    6.20 +  val recover_conjunction_tac: tactic
    6.21    val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
    6.22    val rewrite_goal_tac: thm list -> int -> tactic
    6.23    val norm_hhf_tac: int -> tactic
    6.24 @@ -132,12 +133,12 @@
    6.25        |> fold Variable.declare_internal (asms @ props)
    6.26        |> Assumption.add_assumes casms;
    6.27  
    6.28 -    val goal = init (Conjunction.mk_conjunction_list cprops);
    6.29 +    val goal = init (Conjunction.mk_conjunction_balanced cprops);
    6.30      val res =
    6.31        (case SINGLE (tac {prems = prems, context = ctxt'}) goal of
    6.32          NONE => err "Tactic failed."
    6.33        | SOME res => res);
    6.34 -    val [results] = Conjunction.elim_precise [length props] (finish res)
    6.35 +    val results = Conjunction.elim_balanced (length props) (finish res)
    6.36        handle THM (msg, _, _) => err msg;
    6.37      val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results)
    6.38        orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
    6.39 @@ -165,12 +166,13 @@
    6.40  fun extract i n st =
    6.41    (if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
    6.42     else if n = 1 then Seq.single (Thm.cprem_of st i)
    6.43 -   else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
    6.44 +   else
    6.45 +     Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
    6.46    |> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
    6.47  
    6.48  fun retrofit i n st' st =
    6.49    (if n = 1 then st
    6.50 -   else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
    6.51 +   else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
    6.52    |> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
    6.53  
    6.54  fun SELECT_GOAL tac i st =
    6.55 @@ -180,48 +182,31 @@
    6.56  
    6.57  (* multiple goals *)
    6.58  
    6.59 -local
    6.60 -
    6.61 -fun conj_intrs n =
    6.62 -  let
    6.63 -    val cert = Thm.cterm_of ProtoPure.thy;
    6.64 -    val names = Name.invents Name.context "A" n;
    6.65 -    val As = map (fn name => cert (Free (name, propT))) names;
    6.66 -  in
    6.67 -    Thm.generalize ([], names) 0
    6.68 -      (Drule.implies_intr_list As (Conjunction.intr_list (map Thm.assume As)))
    6.69 -  end;
    6.70 +fun precise_conjunction_tac 0 i = eq_assume_tac i
    6.71 +  | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
    6.72 +  | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n));
    6.73  
    6.74 -fun count_conjs A =
    6.75 -  (case try Logic.dest_conjunction A of
    6.76 -    NONE => 1
    6.77 -  | SOME (_, B) => count_conjs B + 1);
    6.78 -
    6.79 -in
    6.80 +val adhoc_conjunction_tac = REPEAT_ALL_NEW
    6.81 +  (SUBGOAL (fn (goal, i) =>
    6.82 +    if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
    6.83 +    else no_tac));
    6.84  
    6.85 -val precise_conjunction_tac =
    6.86 -  let
    6.87 -    fun tac 0 i = eq_assume_tac i
    6.88 -      | tac 1 i = SUBGOAL (K all_tac) i
    6.89 -      | tac 2 i = rtac Conjunction.conjunctionI i
    6.90 -      | tac n i = rtac (conj_intrs n) i;
    6.91 -  in TRY oo tac end;
    6.92 +val conjunction_tac = SUBGOAL (fn (goal, i) =>
    6.93 +  precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
    6.94 +  TRY (adhoc_conjunction_tac i));
    6.95  
    6.96 -val conjunction_tac = TRY o REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) =>
    6.97 -  let val n = count_conjs goal
    6.98 -  in if n < 2 then no_tac else precise_conjunction_tac n i end));
    6.99 +val recover_conjunction_tac = PRIMITIVE (fn th =>
   6.100 +  Conjunction.uncurry_balanced (Thm.nprems_of th) th);
   6.101  
   6.102  fun PRECISE_CONJUNCTS n tac =
   6.103    SELECT_GOAL (precise_conjunction_tac n 1
   6.104      THEN tac
   6.105 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
   6.106 +    THEN recover_conjunction_tac);
   6.107  
   6.108  fun CONJUNCTS tac =
   6.109    SELECT_GOAL (conjunction_tac 1
   6.110      THEN tac
   6.111 -    THEN PRIMITIVE (Conjunction.uncurry ~1));
   6.112 -
   6.113 -end;
   6.114 +    THEN recover_conjunction_tac);
   6.115  
   6.116  
   6.117  (* rewriting *)
     7.1 --- a/src/Pure/logic.ML	Tue Jun 19 23:15:23 2007 +0200
     7.2 +++ b/src/Pure/logic.ML	Tue Jun 19 23:15:27 2007 +0200
     7.3 @@ -19,12 +19,14 @@
     7.4    val strip_prems: int * term list * term -> term list * term
     7.5    val count_prems: term -> int
     7.6    val nth_prem: int * term -> term
     7.7 +  val true_prop: term
     7.8    val conjunction: term
     7.9    val mk_conjunction: term * term -> term
    7.10    val mk_conjunction_list: term list -> term
    7.11 -  val mk_conjunction_list2: term list list -> term
    7.12 +  val mk_conjunction_balanced: term list -> term
    7.13    val dest_conjunction: term -> term * term
    7.14    val dest_conjunction_list: term -> term list
    7.15 +  val dest_conjunction_balanced: int -> term -> term list
    7.16    val dest_conjunctions: term -> term list
    7.17    val strip_horn: term -> term list * term
    7.18    val mk_type: typ -> term
    7.19 @@ -145,20 +147,24 @@
    7.20  fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    7.21  
    7.22  
    7.23 +
    7.24  (** conjunction **)
    7.25  
    7.26 +val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
    7.27  val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
    7.28  
    7.29 +
    7.30  (*A && B*)
    7.31  fun mk_conjunction (A, B) = conjunction $ A $ B;
    7.32  
    7.33  (*A && B && C -- improper*)
    7.34 -fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
    7.35 +fun mk_conjunction_list [] = true_prop
    7.36    | mk_conjunction_list ts = foldr1 mk_conjunction ts;
    7.37  
    7.38 -(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
    7.39 -fun mk_conjunction_list2 tss =
    7.40 -  mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
    7.41 +(*(A && B) && (C && D) -- balanced*)
    7.42 +fun mk_conjunction_balanced [] = true_prop
    7.43 +  | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
    7.44 +
    7.45  
    7.46  (*A && B*)
    7.47  fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
    7.48 @@ -170,6 +176,10 @@
    7.49      NONE => [t]
    7.50    | SOME (A, B) => A :: dest_conjunction_list B);
    7.51  
    7.52 +(*(A && B) && (C && D) -- balanced*)
    7.53 +fun dest_conjunction_balanced 0 _ = []
    7.54 +  | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
    7.55 +
    7.56  (*((A && B) && C) && D && E -- flat*)
    7.57  fun dest_conjunctions t =
    7.58    (case try dest_conjunction t of