--- a/src/HOL/Nominal/nominal_primrec.ML Tue Jun 19 23:15:23 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Jun 19 23:15:27 2007 +0200
@@ -350,7 +350,7 @@
val rule_prems = cprems @ flat cpremss;
val rule = implies_intr_list rule_prems
- (foldr1 (uncurry Conjunction.intr) (map mk_eqn (rec_rewrites' ~~ asmss)));
+ (Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
val goals = map (fn ((cargs, _, _), (_, eqn)) =>
(list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns);
--- a/src/Pure/Isar/locale.ML Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Isar/locale.ML Tue Jun 19 23:15:27 2007 +0200
@@ -214,7 +214,7 @@
(* A registration is indexed by parameter instantiation. Its components are:
- parameters and prefix
(if the Boolean flag is set, only accesses containing the prefix are generated,
- otherwise the prefix may be omitted when accessing theorems etc.)
+ otherwise the prefix may be omitted when accessing theorems etc.)
- theorems (actually witnesses) instantiating locale assumptions
- theorems (equations, actually witnesses) interpreting derived concepts
and indexed by lhs
@@ -656,10 +656,10 @@
fun unify T U envir = Sign.typ_unify thy (U, T) envir
handle Type.TUNIFY =>
- let
+ let
val T' = Envir.norm_type (fst envir) T;
val U' = Envir.norm_type (fst envir) U;
- val prt = Sign.string_of_typ thy;
+ val prt = Sign.string_of_typ thy;
in
raise TYPE ("unify_parms: failed to unify types " ^
prt U' ^ " and " ^ prt T', [U', T'], [])
@@ -1660,7 +1660,7 @@
(axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
add_thmss loc Thm.internalK [(("", [Attrib.internal (decl_attrib decl)]), [([dummy_thm], [])])];
-in
+in
val add_type_syntax = add_decls (apfst o cons);
val add_term_syntax = add_decls (apsnd o cons);
@@ -1687,7 +1687,7 @@
fun atomize_spec thy ts =
let
- val t = Logic.mk_conjunction_list ts;
+ val t = Logic.mk_conjunction_balanced ts;
val body = ObjectLogic.atomize_term thy t;
val bodyT = Term.fastype_of body;
in
@@ -1737,12 +1737,13 @@
val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ =>
MetaSimplifier.rewrite_goals_tac [pred_def] THEN
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
- Tactic.compose_tac (false, Conjunction.intr_list (map (Thm.assume o cert) norm_ts), 0) 1);
+ Tactic.compose_tac (false,
+ Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
val conjuncts =
(Drule.equal_elim_rule2 OF [body_eq,
MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))])
- |> Conjunction.elim_precise [length ts] |> hd;
+ |> Conjunction.elim_balanced (length ts);
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
Element.prove_witness defs_ctxt t
(MetaSimplifier.rewrite_goals_tac defs THEN
@@ -2353,7 +2354,7 @@
#> after_qed;
in
thy
- |> ProofContext.init
+ |> ProofContext.init
|> Proof.theorem_i NONE after_qed' (prep_propp propss)
|> Element.refine_witness
|> Seq.hd
--- a/src/Pure/Isar/proof.ML Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Isar/proof.ML Tue Jun 19 23:15:27 2007 +0200
@@ -468,11 +468,22 @@
val _ = null extra_hyps orelse
error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
- val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal)
- handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal);
- val _ = Unify.matches_list thy (flat propss) (map Thm.prop_of (flat results)) orelse
+ fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
+
+ val th = Goal.conclude goal handle THM _ => lost_structure ();
+ val goal_propss = filter_out null propss;
+ val results =
+ Conjunction.elim_balanced (length goal_propss) th
+ |> map2 Conjunction.elim_balanced (map length goal_propss)
+ handle THM _ => lost_structure ();
+ val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
error ("Proved a different theorem:\n" ^ string_of_thm th);
- in results end;
+
+ fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
+ | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
+ | recover_result [] [] = []
+ | recover_result _ _ = lost_structure ();
+ in recover_result propss results end;
@@ -758,6 +769,7 @@
fun generic_goal prepp kind before_qed after_qed raw_propp state =
let
val thy = theory_of state;
+ val cert = Thm.cterm_of thy;
val chaining = can assert_chain state;
val ((propss, after_ctxt), goal_state) =
@@ -773,7 +785,9 @@
val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props';
val propss' = map (Logic.mk_term o Var) vars :: propss;
- val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss'));
+ val goal_propss = filter_out null propss';
+ val goal = Goal.init (cert
+ (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)));
val after_qed' = after_qed |>> (fn after_local =>
fn results => map_context after_ctxt #> after_local results);
in
@@ -787,7 +801,7 @@
|> open_block
|> put_goal NONE
|> enter_backward
- |> not (null vars) ? refine_terms (length propss')
+ |> not (null vars) ? refine_terms (length goal_propss)
|> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
end;
--- a/src/Pure/Isar/rule_cases.ML Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Isar/rule_cases.ML Tue Jun 19 23:15:27 2007 +0200
@@ -195,8 +195,8 @@
if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
else
Conv.fconv_rule
- (Conv.concl_conv ~1 (Conjunction.conv ~1
- (K (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
+ (Conv.concl_conv ~1 (Conjunction.convs
+ (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs))))) th;
in
@@ -338,7 +338,7 @@
else
SOME (ns,
rls
- |> foldr1 (uncurry Conjunction.intr)
+ |> Conjunction.intr_balanced
|> Drule.implies_intr_list prems
|> singleton (Variable.export ctxt' ctxt)
|> save th
--- a/src/Pure/Tools/codegen_func.ML Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML Tue Jun 19 23:15:27 2007 +0200
@@ -238,9 +238,9 @@
fun burrow_thms f [] = []
| burrow_thms f thms =
thms
- |> Conjunction.intr_list
+ |> Conjunction.intr_balanced
|> f
- |> Conjunction.elim_list;
+ |> Conjunction.elim_balanced (length thms)
in
thms
|> burrow_thms (canonical_tvars purify_tvar)
--- a/src/Pure/goal.ML Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/goal.ML Tue Jun 19 23:15:27 2007 +0200
@@ -8,8 +8,8 @@
signature BASIC_GOAL =
sig
val SELECT_GOAL: tactic -> int -> tactic
+ val CONJUNCTS: tactic -> int -> tactic
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
- val CONJUNCTS: tactic -> int -> tactic
end;
signature GOAL =
@@ -29,8 +29,9 @@
val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm
val extract: int -> int -> thm -> thm Seq.seq
val retrofit: int -> int -> thm -> thm -> thm Seq.seq
+ val conjunction_tac: int -> tactic
val precise_conjunction_tac: int -> int -> tactic
- val conjunction_tac: int -> tactic
+ val recover_conjunction_tac: tactic
val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic
val rewrite_goal_tac: thm list -> int -> tactic
val norm_hhf_tac: int -> tactic
@@ -132,12 +133,12 @@
|> fold Variable.declare_internal (asms @ props)
|> Assumption.add_assumes casms;
- val goal = init (Conjunction.mk_conjunction_list cprops);
+ val goal = init (Conjunction.mk_conjunction_balanced cprops);
val res =
(case SINGLE (tac {prems = prems, context = ctxt'}) goal of
NONE => err "Tactic failed."
| SOME res => res);
- val [results] = Conjunction.elim_precise [length props] (finish res)
+ val results = Conjunction.elim_balanced (length props) (finish res)
handle THM (msg, _, _) => err msg;
val _ = Unify.matches_list thy (map Thm.term_of cprops) (map Thm.prop_of results)
orelse err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res));
@@ -165,12 +166,13 @@
fun extract i n st =
(if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
else if n = 1 then Seq.single (Thm.cprem_of st i)
- else Seq.single (foldr1 Conjunction.mk_conjunction (map (Thm.cprem_of st) (i upto i + n - 1))))
+ else
+ Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
|> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
fun retrofit i n st' st =
(if n = 1 then st
- else st |> Drule.rotate_prems (i - 1) |> Conjunction.uncurry n |> Drule.rotate_prems (1 - i))
+ else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
|> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
fun SELECT_GOAL tac i st =
@@ -180,48 +182,31 @@
(* multiple goals *)
-local
-
-fun conj_intrs n =
- let
- val cert = Thm.cterm_of ProtoPure.thy;
- val names = Name.invents Name.context "A" n;
- val As = map (fn name => cert (Free (name, propT))) names;
- in
- Thm.generalize ([], names) 0
- (Drule.implies_intr_list As (Conjunction.intr_list (map Thm.assume As)))
- end;
+fun precise_conjunction_tac 0 i = eq_assume_tac i
+ | precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
+ | precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n));
-fun count_conjs A =
- (case try Logic.dest_conjunction A of
- NONE => 1
- | SOME (_, B) => count_conjs B + 1);
-
-in
+val adhoc_conjunction_tac = REPEAT_ALL_NEW
+ (SUBGOAL (fn (goal, i) =>
+ if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
+ else no_tac));
-val precise_conjunction_tac =
- let
- fun tac 0 i = eq_assume_tac i
- | tac 1 i = SUBGOAL (K all_tac) i
- | tac 2 i = rtac Conjunction.conjunctionI i
- | tac n i = rtac (conj_intrs n) i;
- in TRY oo tac end;
+val conjunction_tac = SUBGOAL (fn (goal, i) =>
+ precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
+ TRY (adhoc_conjunction_tac i));
-val conjunction_tac = TRY o REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) =>
- let val n = count_conjs goal
- in if n < 2 then no_tac else precise_conjunction_tac n i end));
+val recover_conjunction_tac = PRIMITIVE (fn th =>
+ Conjunction.uncurry_balanced (Thm.nprems_of th) th);
fun PRECISE_CONJUNCTS n tac =
SELECT_GOAL (precise_conjunction_tac n 1
THEN tac
- THEN PRIMITIVE (Conjunction.uncurry ~1));
+ THEN recover_conjunction_tac);
fun CONJUNCTS tac =
SELECT_GOAL (conjunction_tac 1
THEN tac
- THEN PRIMITIVE (Conjunction.uncurry ~1));
-
-end;
+ THEN recover_conjunction_tac);
(* rewriting *)
--- a/src/Pure/logic.ML Tue Jun 19 23:15:23 2007 +0200
+++ b/src/Pure/logic.ML Tue Jun 19 23:15:27 2007 +0200
@@ -19,12 +19,14 @@
val strip_prems: int * term list * term -> term list * term
val count_prems: term -> int
val nth_prem: int * term -> term
+ val true_prop: term
val conjunction: term
val mk_conjunction: term * term -> term
val mk_conjunction_list: term list -> term
- val mk_conjunction_list2: term list list -> term
+ val mk_conjunction_balanced: term list -> term
val dest_conjunction: term -> term * term
val dest_conjunction_list: term -> term list
+ val dest_conjunction_balanced: int -> term -> term list
val dest_conjunctions: term -> term list
val strip_horn: term -> term list * term
val mk_type: typ -> term
@@ -145,20 +147,24 @@
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+
(** conjunction **)
+val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0));
val conjunction = Const ("ProtoPure.conjunction", propT --> propT --> propT);
+
(*A && B*)
fun mk_conjunction (A, B) = conjunction $ A $ B;
(*A && B && C -- improper*)
-fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0))
+fun mk_conjunction_list [] = true_prop
| mk_conjunction_list ts = foldr1 mk_conjunction ts;
-(*(A1 && B1 && C1) && (A2 && B2 && C2 && D2) && A3 && B3 -- improper*)
-fun mk_conjunction_list2 tss =
- mk_conjunction_list (map mk_conjunction_list (filter_out null tss));
+(*(A && B) && (C && D) -- balanced*)
+fun mk_conjunction_balanced [] = true_prop
+ | mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts;
+
(*A && B*)
fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B)
@@ -170,6 +176,10 @@
NONE => [t]
| SOME (A, B) => A :: dest_conjunction_list B);
+(*(A && B) && (C && D) -- balanced*)
+fun dest_conjunction_balanced 0 _ = []
+ | dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t;
+
(*((A && B) && C) && D && E -- flat*)
fun dest_conjunctions t =
(case try dest_conjunction t of