# HG changeset patch
# User paulson
# Date 909834154 -3600
# Node ID 7559f116cb100ca0271316782bb0b5fc75ca5f1d
# Parent  d37380544c398428a2f4ad8e4f22f017fc99ee41
locales now implicitly quantify over free variables

diff -r d37380544c39 -r 7559f116cb10 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Oct 30 15:59:51 1998 +0100
+++ b/src/HOL/Finite.ML	Sat Oct 31 12:42:34 1998 +0100
@@ -591,8 +591,7 @@
 
 Open_locale "LC"; 
 
-(*Strip meta-quantifiers: perhaps the locale should do this?*)
-val f_lcomm = forall_elim_vars 0 (thm "lcomm");
+val f_lcomm = thm "lcomm";
 
 
 Goal "ALL A x. card(A) < n --> (A, x) : foldSet f e --> \
@@ -680,10 +679,9 @@
 
 Open_locale "ACe"; 
 
-(*Strip meta-quantifiers: perhaps the locale should do this?*)
-val f_ident   = forall_elim_vars 0 (thm "ident");
-val f_commute = forall_elim_vars 0 (thm "commute");
-val f_assoc   = forall_elim_vars 0 (thm "assoc");
+val f_ident   = thm "ident";
+val f_commute = thm "commute";
+val f_assoc   = thm "assoc";
 
 
 Goal "f x (f y z) = f y (f x z)";
diff -r d37380544c39 -r 7559f116cb10 src/HOL/Finite.thy
--- a/src/HOL/Finite.thy	Fri Oct 30 15:59:51 1998 +0100
+++ b/src/HOL/Finite.thy	Sat Oct 31 12:42:34 1998 +0100
@@ -62,7 +62,7 @@
   fixes
     f    :: ['b,'a] => 'a
   assumes
-    lcomm    "!! x y z. f x (f y z) = f y (f x z)"
+    lcomm    "f x (f y z) = f y (f x z)"
   defines
     (*nothing*)
 
@@ -71,9 +71,9 @@
     f    :: ['a,'a] => 'a
     e    :: 'a
   assumes
-    ident    "!! x. f x e = x"
-    commute  "!! x y. f x y = f y x"
-    assoc    "!! x y z. f (f x y) z = f x (f y z)"
+    ident    "f x e = x"
+    commute  "f x y = f y x"
+    assoc    "f (f x y) z = f x (f y z)"
   defines
 
 end
diff -r d37380544c39 -r 7559f116cb10 src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Fri Oct 30 15:59:51 1998 +0100
+++ b/src/HOL/UNITY/Token.ML	Sat Oct 31 12:42:34 1998 +0100
@@ -22,15 +22,14 @@
 
 Open_locale "Token";
 
-(*Strip meta-quantifiers: perhaps the locale should do this?*)
-val TR2   = forall_elim_vars 0 (thm "TR2");
-val TR3   = forall_elim_vars 0 (thm "TR3");
-val TR4   = forall_elim_vars 0 (thm "TR4");
-val TR5   = forall_elim_vars 0 (thm "TR5");
-val TR6   = forall_elim_vars 0 (thm "TR6");
-val TR7   = forall_elim_vars 0 (thm "TR7");
-val nodeOrder_def   = (thm "nodeOrder_def");
-val next_def   = (thm "next_def");
+val TR2 = thm "TR2";
+val TR3 = thm "TR3";
+val TR4 = thm "TR4";
+val TR5 = thm "TR5";
+val TR6 = thm "TR6";
+val TR7 = thm "TR7";
+val nodeOrder_def = thm "nodeOrder_def";
+val next_def = thm "next_def";
 
 AddIffs [thm "N_positive"];
 
diff -r d37380544c39 -r 7559f116cb10 src/HOL/UNITY/Token.thy
--- a/src/HOL/UNITY/Token.thy	Fri Oct 30 15:59:51 1998 +0100
+++ b/src/HOL/UNITY/Token.thy	Sat Oct 31 12:42:34 1998 +0100
@@ -43,17 +43,17 @@
   assumes
     N_positive "0<N"
 
-    TR2  "!!i. F : constrains (T i) (T i Un H i)"
+    TR2  "F : constrains (T i) (T i Un H i)"
 
-    TR3  "!!i. F : constrains (H i) (H i Un E i)"
+    TR3  "F : constrains (H i) (H i Un E i)"
 
-    TR4  "!!i. F : constrains (H i - HasTok i) (H i)"
+    TR4  "F : constrains (H i - HasTok i) (H i)"
 
-    TR5  "!!i. F : constrains (HasTok i) (HasTok i Un Compl(E i))"
+    TR5  "F : constrains (HasTok i) (HasTok i Un Compl(E i))"
 
-    TR6  "!!i. F : leadsTo (H i Int HasTok i) (E i)"
+    TR6  "F : leadsTo (H i Int HasTok i) (E i)"
 
-    TR7  "!!i. F : leadsTo (HasTok i) (HasTok (next i))"
+    TR7  "F : leadsTo (HasTok i) (HasTok (next i))"
 
   defines
     nodeOrder_def
diff -r d37380544c39 -r 7559f116cb10 src/Pure/locale.ML
--- a/src/Pure/locale.ML	Fri Oct 30 15:59:51 1998 +0100
+++ b/src/Pure/locale.ML	Sat Oct 31 12:42:34 1998 +0100
@@ -2,17 +2,19 @@
     ID:         $Id$
     Author:     Florian Kammueller, University of Cambridge
 
-Locales. (* FIXME description *)
+Locales. The theory section 'locale' declarings constants, assumptions and
+definitions that have local scope.  Typical form is
+
+    locale Locale_name =
+      fixes   (*variables that are fixed in the locale's scope*)
+	v :: T
+      assumes (*meta-hypothesis that hold in the locale*)
+	Asm_name "meta-formula"  
+      defines (*local definitions of fixed variables in terms of others*)
+	v_def "v x == ...x..."
 
 TODO:
-  - cleanup this TODO list;
-  - read_cterm, pretty_cterm etc. wrt. current scope: collect defaults;
-  - inner locale name space for rules / defs (?!);
-  - attributes for assumptions (??!);
-  - logical aspects of locales:
-      . unfold / fold defs for in/out (use simplifier);
-      . discharge assumptions and eliminate defs for result;
-  - improve error msgs: more checks, at very beginning;
+  - operations on locales: extension, renaming.
 *)
 
 signature BASIC_LOCALE =
@@ -307,16 +309,20 @@
             end;
     in distinct(builddiff flist clist) end;
 
-(* Bind a term with !! over a list of "free" Free's *)
-fun abs_over_free clist term =
+(* Bind a term with !! over a list of "free" Free's.
+   To enable definitions like x + y == .... (without quantifier).
+   Complications, because x and y have to be removed from defaults *)
+fun abs_over_free clist ((defaults: (string * sort) list * (string * typ) list * string list), (s, term)) =
     let val diffl = rev(difflist term clist);
         fun abs_o (t, (x as Free(v,T))) = all(T) $ Abs(v, T, abstract_over (x,t))
           | abs_o (_ , _) = error ("Can't be: abs_over_free");
-    in foldl abs_o (term, diffl) end;
+        val diffl' = map (fn (Free (s, T)) => s) diffl;
+        val defaults' = (#1 defaults, filter (fn x => not((fst x) mem diffl')) (#2 defaults), #3 defaults)
+    in (defaults', (s, foldl abs_o (term, diffl))) end;
 
 (* assume a definition, i.e assume the cterm of a definiton term and then eliminate
    the binding !!, so that the def can be applied as rewrite. The meta hyp will still contain !! *)
-fun prep_def clist sg = forall_elim_vars(0) o assume o (cterm_of sg);
+fun prep_hyps clist sg = forall_elim_vars(0) o Thm.assume o (Thm.cterm_of sg);
 
 
 (* concrete syntax *)
@@ -379,9 +385,11 @@
     val new_loc_consts = (map #1 loc_consts);
     val all_loc_consts = old_loc_consts @ new_loc_consts;
 
-    val loc_defs_terms = map (apsnd (abs_over_free (all_loc_consts))) loc_defs;
-    val loc_defs_thms = map (apsnd (prep_def (map #1 loc_consts) syntax_sign)) loc_defs_terms;
-    val loc_thms = (map (apsnd (Thm.assume o Thm.cterm_of syntax_sign)) (loc_rules)) @ loc_defs_thms;
+    val (defaults, loc_defs_terms) = foldl_map (abs_over_free all_loc_consts) (defaults, loc_defs);
+    val loc_defs_thms = map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) loc_defs_terms;
+    val (defaults, loc_thms_terms) = foldl_map (abs_over_free all_loc_consts) (defaults, loc_rules);
+    val loc_thms = (map (apsnd (prep_hyps (map #1 loc_consts) syntax_sign)) (loc_thms_terms)) 
+                   @ loc_defs_thms;
 
 
     (* error messages *)        (* FIXME improve *)
@@ -390,7 +398,7 @@
       if is_none (get_locale thy name) then []
       else ["Duplicate definition of locale " ^ quote name];
 
-    (* check if definientes are local constants (in the same locale, so no redefining!) *)
+    (* check if definientes are locale constants (in the same locale, so no redefining!) *)
     val err_def_head =
       let fun peal_appl t = 
             case t of 
@@ -405,14 +413,27 @@
          else ["defined item not declared fixed in locale " ^ quote name]
       end; 
 
-    val errs = err_dup_locale @ err_def_head;
+    (* check that variables on rhs of definitions are either fixed or on lhs *)
+    val err_var_rhs = 
+      let fun compare_var_sides (t, (_, Const ("==", _) $ d1 $ d2)) = 
+            let val varl1 = difflist d1 all_loc_consts;
+                val varl2 = difflist d2 all_loc_consts
+            in t andalso (varl2 subset varl1)
+            end
+            | compare_var_sides (_,_) = error ("an illegal definition");
+          val check = foldl compare_var_sides (true, loc_defs)
+      in if check then []
+         else ["nonfixed variable on right hand side of a locale definition in locale" ^ quote name]
+      end;
+
+    val errs = err_dup_locale @ err_def_head @ err_var_rhs;
   in
     if null errs then ()
     else error (cat_lines errs);
 
     syntax_thy
     |> put_locale (name, 
-		   make_locale loc_consts nosyn loc_rules loc_defs_terms
+		   make_locale loc_consts nosyn loc_thms_terms loc_defs_terms
 		               loc_thms defaults)
   end;