--- 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)";
--- 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
--- 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"];
--- 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
--- 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;