# HG changeset patch
# User ballarin
# Date 1118239869 -7200
# Node ID a6431098a92971fe8d791e1a163524c2f5bdfb82
# Parent  059caec54d911b11373c402b1e1c6133db9425d8
Fixed "axiom" generation for mixed locales with and without predicates.

diff -r 059caec54d91 -r a6431098a929 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Wed Jun 08 15:14:09 2005 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Wed Jun 08 16:11:09 2005 +0200
@@ -22,12 +22,10 @@
 
 locale (open) S = var mult +
   assumes "mult(x, y) = mult(y, x)"
-(* Making this declaration (open) reveals a problem when mixing open and
-   closed locales. *)
 
 print_locale S
 
-locale (open) S' = S mult (infixl "**" 60)
+locale S' = S mult (infixl "**" 60)
 
 print_locale S'
 
diff -r 059caec54d91 -r a6431098a929 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Jun 08 15:14:09 2005 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Wed Jun 08 16:11:09 2005 +0200
@@ -58,7 +58,7 @@
   join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   "x \<squnion> y == sup L {x, y}"
 
-  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
+  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   "x \<sqinter> y == inf L {x, y}"
 
 
diff -r 059caec54d91 -r a6431098a929 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Jun 08 15:14:09 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Jun 08 16:11:09 2005 +0200
@@ -21,7 +21,6 @@
 (* TODO:
 - beta-eta normalisation of interpretation parameters
 - no beta reduction of interpretation witnesses
-- mix of locales with and without open in activate_elems
 - dangling type frees in locales
 *)
 
@@ -855,7 +854,6 @@
     (* thy used for retrieval of locale info,
        ctxt for error messages, parameter unification and instantiation
        of axioms *)
-    (* TODO: consider err_in_locale with thy argument *)
 
     fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
       | renaming (NONE :: xs) (y :: ys) = renaming xs ys
@@ -1740,7 +1738,7 @@
         Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
       |> Drule.conj_elim_precise (length ts);
     val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
-      Tactic.prove defs_sign [] [] t (fn _ =>
+      Tactic.prove_plain defs_sign [] [] t (fn _ =>
         Tactic.rewrite_goals_tac defs THEN
         Tactic.compose_tac (false, ax, 0) 1));
   in (defs_thy, (statement, intro, axioms)) end;
@@ -1777,7 +1775,7 @@
           val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
           val (def_thy, (statement, intro, axioms)) =
             thy |> def_pred aname parms defs exts exts';
-          val elemss' = change_elemss axioms elemss @
+          val elemss' = change_elemss (map (Drule.zero_var_indexes o Drule.gen_all) axioms) elemss @
             [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
         in
           def_thy |> note_thmss_qualified "" aname
diff -r 059caec54d91 -r a6431098a929 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Jun 08 15:14:09 2005 +0200
+++ b/src/Pure/tactic.ML	Wed Jun 08 16:11:09 2005 +0200
@@ -111,10 +111,13 @@
   val simplify: bool -> thm list -> thm -> thm
   val conjunction_tac: tactic
   val smart_conjunction_tac: int -> tactic
+  val prove_multi_plain: Sign.sg -> string list -> term list -> term list ->
+    (thm list -> tactic) -> thm list
   val prove_multi: Sign.sg -> string list -> term list -> term list ->
     (thm list -> tactic) -> thm list
   val prove_multi_standard: Sign.sg -> string list -> term list -> term list ->
     (thm list -> tactic) -> thm list
+  val prove_plain: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
   val prove_standard: Sign.sg -> string list -> term list -> term ->
     (thm list -> tactic) -> thm
@@ -659,7 +662,7 @@
 
 (** minimal goal interface for programmed proofs *)
 
-fun prove_multi sign xs asms props tac =
+fun gen_prove_multi finish_thm sign xs asms props tac =
   let
     val prop = Logic.mk_conjunction_list props;
     val statement = Logic.list_implies (asms, prop);
@@ -700,14 +703,19 @@
     |> map (fn res => res
       |> Drule.implies_intr_list casms
       |> Drule.forall_intr_list cparams
-      |> norm_hhf_rule
-      |> (#1 o Thm.varifyT' fixed_tfrees)
-      |> Drule.zero_var_indexes)
+      |> finish_thm fixed_tfrees)
   end;
 
+fun prove_multi_plain sign xs asms prop tac =
+  gen_prove_multi (K norm_hhf_plain) sign xs asms prop tac;
+fun prove_multi sign xs asms prop tac =
+  gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
+      (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
+    sign xs asms prop tac;
 fun prove_multi_standard sign xs asms prop tac =
   map Drule.standard (prove_multi sign xs asms prop tac);
 
+fun prove_plain sign xs asms prop tac = hd (prove_multi_plain sign xs asms [prop] tac);
 fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac);
 fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac);