--- a/src/FOL/ex/NewLocaleSetup.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy Thu Dec 11 08:59:03 2008 +0100
@@ -16,7 +16,7 @@
val opt_bang = Scan.optional (P.$$$ "!" >> K true) false;
val locale_val =
- Expression.parse_expression --
+ SpecParse.locale_expression --
Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
Scan.repeat1 SpecParse.context_element >> pair ([], []);
@@ -27,7 +27,9 @@
(P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
- (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin)));
+ (Expression.add_locale_cmd name name expr elems #>
+ (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |>
+ fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes))));
val _ =
OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag
@@ -42,7 +44,7 @@
val _ =
OuterSyntax.command "interpretation"
"prove interpretation of locale expression in theory" K.thy_goal
- (P.!!! Expression.parse_expression
+ (P.!!! SpecParse.locale_expression
>> (fn expr => Toplevel.print o
Toplevel.theory_to_proof (Expression.interpretation_cmd expr)));
@@ -50,7 +52,7 @@
OuterSyntax.command "interpret"
"prove interpretation of locale expression in proof context"
(K.tag_proof K.prf_goal)
- (P.!!! Expression.parse_expression
+ (P.!!! SpecParse.locale_expression
>> (fn expr => Toplevel.print o
Toplevel.proof' (fn int => Expression.interpret_cmd expr int)));
--- a/src/FOL/ex/NewLocaleTest.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Thu Dec 11 08:59:03 2008 +0100
@@ -113,6 +113,12 @@
print_locale! use_decl thm use_decl_def
+text {* Foundational versions of theorems *}
+
+thm logic.assoc
+thm logic.lor_def
+
+
text {* Defines *}
locale logic_def =
@@ -124,12 +130,45 @@
defines "x || y == --(-- x && -- y)"
begin
+thm lor_def
+(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *)
+
+lemma "x || y = --(-- x && --y)"
+ by (unfold lor_def) (rule refl)
+
+end
+
+(* Inheritance of defines *)
+
+locale logic_def2 = logic_def
+begin
+
lemma "x || y = --(-- x && --y)"
by (unfold lor_def) (rule refl)
end
+text {* Notes *}
+
+(* A somewhat arcane homomorphism example *)
+
+definition semi_hom where
+ "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
+
+lemma semi_hom_mult:
+ "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
+ by (simp add: semi_hom_def)
+
+locale semi_hom_loc = prod: semi prod + sum: semi sum
+ for prod and sum and h +
+ assumes semi_homh: "semi_hom(prod, sum, h)"
+ notes semi_hom_mult = semi_hom_mult [OF semi_homh]
+
+lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
+ by (rule semi_hom_mult)
+
+
text {* Theorem statements *}
lemma (in lgrp) lcancel:
--- a/src/HOL/Groebner_Basis.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy Thu Dec 11 08:59:03 2008 +0100
@@ -178,7 +178,8 @@
lemma not_iszero_Numeral1: "\<not> iszero (Numeral1::'a::number_ring)"
by (simp add: numeral_1_eq_1)
-lemmas comp_arith = Let_def arith_simps nat_arith rel_simps if_False
+lemmas comp_arith =
+ Let_def arith_simps nat_arith rel_simps neg_simps if_False
if_True add_0 add_Suc add_number_of_left mult_number_of_left
numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
numeral_0_eq_0[symmetric] numerals[symmetric]
--- a/src/HOL/Import/HOL4Compat.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Import/HOL4Compat.thy Thu Dec 11 08:59:03 2008 +0100
@@ -3,7 +3,7 @@
Author: Sebastian Skalberg (TU Muenchen)
*)
-theory HOL4Compat imports HOL4Setup Divides Primes Real
+theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
begin
lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
--- a/src/HOL/Int.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Int.thy Thu Dec 11 08:59:03 2008 +0100
@@ -761,41 +761,18 @@
text {* Subtraction *}
-lemma diff_Pls:
- "Pls - k = - k"
- unfolding numeral_simps by simp
-
-lemma diff_Min:
- "Min - k = pred (- k)"
- unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit0:
+lemma diff_bin_simps [simp]:
+ "k - Pls = k"
+ "k - Min = succ k"
+ "Pls - (Bit0 l) = Bit0 (Pls - l)"
+ "Pls - (Bit1 l) = Bit1 (Min - l)"
+ "Min - (Bit0 l) = Bit1 (Min - l)"
+ "Min - (Bit1 l) = Bit0 (Min - l)"
"(Bit0 k) - (Bit0 l) = Bit0 (k - l)"
- unfolding numeral_simps by simp
-
-lemma diff_Bit0_Bit1:
"(Bit0 k) - (Bit1 l) = Bit1 (pred k - l)"
- unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit0:
"(Bit1 k) - (Bit0 l) = Bit1 (k - l)"
- unfolding numeral_simps by simp
-
-lemma diff_Bit1_Bit1:
"(Bit1 k) - (Bit1 l) = Bit0 (k - l)"
- unfolding numeral_simps by simp
-
-lemma diff_Pls_right:
- "k - Pls = k"
- unfolding numeral_simps by simp
-
-lemma diff_Min_right:
- "k - Min = succ k"
- unfolding numeral_simps by simp
-
-lemmas diff_bin_simps [simp] =
- diff_Pls diff_Min diff_Pls_right diff_Min_right
- diff_Bit0_Bit0 diff_Bit0_Bit1 diff_Bit1_Bit0 diff_Bit1_Bit1
+ unfolding numeral_simps by simp_all
text {* Multiplication *}
@@ -1076,47 +1053,17 @@
text {* First version by Norbert Voelker *}
-definition
- neg :: "'a\<Colon>ordered_idom \<Rightarrow> bool"
-where
- "neg Z \<longleftrightarrow> Z < 0"
-
definition (*for simplifying equalities*)
iszero :: "'a\<Colon>semiring_1 \<Rightarrow> bool"
where
"iszero z \<longleftrightarrow> z = 0"
-lemma not_neg_int [simp]: "~ neg (of_nat n)"
-by (simp add: neg_def)
-
-lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
-by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
-
-lemmas neg_eq_less_0 = neg_def
-
-lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
-by (simp add: neg_def linorder_not_less)
-
-text{*To simplify inequalities when Numeral1 can get simplified to 1*}
-
-lemma not_neg_0: "~ neg 0"
-by (simp add: One_int_def neg_def)
-
-lemma not_neg_1: "~ neg 1"
-by (simp add: neg_def linorder_not_less zero_le_one)
-
lemma iszero_0: "iszero 0"
by (simp add: iszero_def)
lemma not_iszero_1: "~ iszero 1"
by (simp add: iszero_def eq_commute)
-lemma neg_nat: "neg z ==> nat z = 0"
-by (simp add: neg_def order_less_imp_le)
-
-lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
-by (simp add: linorder_not_less neg_def)
-
lemma eq_number_of_eq:
"((number_of x::'a::number_ring) = number_of y) =
iszero (number_of (x + uminus y) :: 'a)"
@@ -1196,26 +1143,6 @@
subsubsection {* The Less-Than Relation *}
-lemma less_number_of_eq_neg:
- "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
- = neg (number_of (x + uminus y) :: 'a)"
-apply (subst less_iff_diff_less_0)
-apply (simp add: neg_def diff_minus number_of_add number_of_minus)
-done
-
-text {*
- If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
- @{term Numeral0} IS @{term "number_of Pls"}
-*}
-
-lemma not_neg_number_of_Pls:
- "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
- by (simp add: neg_def numeral_0_eq_0)
-
-lemma neg_number_of_Min:
- "neg (number_of Min ::'a::{ordered_idom,number_ring})"
- by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)
-
lemma double_less_0_iff:
"(a + a < 0) = (a < (0::'a::ordered_idom))"
proof -
@@ -1238,27 +1165,6 @@
add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
qed
-lemma neg_number_of_Bit0:
- "neg (number_of (Bit0 w)::'a) =
- neg (number_of w :: 'a::{ordered_idom,number_ring})"
-by (simp add: neg_def number_of_eq numeral_simps double_less_0_iff)
-
-lemma neg_number_of_Bit1:
- "neg (number_of (Bit1 w)::'a) =
- neg (number_of w :: 'a::{ordered_idom,number_ring})"
-proof -
- have "((1::'a) + of_int w + of_int w < 0) = (of_int (1 + w + w) < (of_int 0 :: 'a))"
- by simp
- also have "... = (w < 0)" by (simp only: of_int_less_iff odd_less_0)
- finally show ?thesis
- by (simp add: neg_def number_of_eq numeral_simps)
-qed
-
-lemmas neg_simps =
- not_neg_0 not_neg_1
- not_neg_number_of_Pls neg_number_of_Min
- neg_number_of_Bit0 neg_number_of_Bit1
-
text {* Less-Than or Equals *}
text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
@@ -1267,11 +1173,6 @@
linorder_not_less [of "number_of w" "number_of v", symmetric,
standard]
-lemma le_number_of_eq:
- "((number_of x::'a::{ordered_idom,number_ring}) \<le> number_of y)
- = (~ (neg (number_of (y + uminus x) :: 'a)))"
-by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)
-
text {* Absolute value (@{term abs}) *}
@@ -1325,7 +1226,7 @@
less_number_of less_bin_simps
le_number_of le_bin_simps
eq_number_of_eq eq_bin_simps
- iszero_simps neg_simps
+ iszero_simps
subsubsection {* Simplification of arithmetic when nested to the right. *}
--- a/src/HOL/IntDiv.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/IntDiv.thy Thu Dec 11 08:59:03 2008 +0100
@@ -1472,6 +1472,29 @@
IntDiv.zpower_zmod
zminus_zmod zdiff_zmod_left zdiff_zmod_right
+text {* Distributive laws for function @{text nat}. *}
+
+lemma nat_div_distrib: "0 \<le> x \<Longrightarrow> nat (x div y) = nat x div nat y"
+apply (rule linorder_cases [of y 0])
+apply (simp add: div_nonneg_neg_le0)
+apply simp
+apply (simp add: nat_eq_iff pos_imp_zdiv_nonneg_iff zdiv_int)
+done
+
+(*Fails if y<0: the LHS collapses to (nat z) but the RHS doesn't*)
+lemma nat_mod_distrib:
+ "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x mod y) = nat x mod nat y"
+apply (case_tac "y = 0", simp add: DIVISION_BY_ZERO)
+apply (simp add: nat_eq_iff zmod_int)
+done
+
+text{*Suggested by Matthias Daum*}
+lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
+apply (subgoal_tac "nat x div nat k < nat x")
+ apply (simp (asm_lr) add: nat_div_distrib [symmetric])
+apply (rule Divides.div_less_dividend, simp_all)
+done
+
text {* code generator setup *}
context ring_1
--- a/src/HOL/Library/Float.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Library/Float.thy Thu Dec 11 08:59:03 2008 +0100
@@ -514,7 +514,7 @@
by simp
lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (x + (uminus y)))::int)"
- by (rule less_number_of_eq_neg)
+ unfolding neg_def number_of_is_id by simp
lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
by simp
--- a/src/HOL/NatBin.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/NatBin.thy Thu Dec 11 08:59:03 2008 +0100
@@ -39,6 +39,63 @@
square ("(_\<twosuperior>)" [1000] 999)
+subsection {* Predicate for negative binary numbers *}
+
+definition
+ neg :: "int \<Rightarrow> bool"
+where
+ "neg Z \<longleftrightarrow> Z < 0"
+
+lemma not_neg_int [simp]: "~ neg (of_nat n)"
+by (simp add: neg_def)
+
+lemma neg_zminus_int [simp]: "neg (- (of_nat (Suc n)))"
+by (simp add: neg_def neg_less_0_iff_less del: of_nat_Suc)
+
+lemmas neg_eq_less_0 = neg_def
+
+lemma not_neg_eq_ge_0: "(~neg x) = (0 \<le> x)"
+by (simp add: neg_def linorder_not_less)
+
+text{*To simplify inequalities when Numeral1 can get simplified to 1*}
+
+lemma not_neg_0: "~ neg 0"
+by (simp add: One_int_def neg_def)
+
+lemma not_neg_1: "~ neg 1"
+by (simp add: neg_def linorder_not_less zero_le_one)
+
+lemma neg_nat: "neg z ==> nat z = 0"
+by (simp add: neg_def order_less_imp_le)
+
+lemma not_neg_nat: "~ neg z ==> of_nat (nat z) = z"
+by (simp add: linorder_not_less neg_def)
+
+text {*
+ If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
+ @{term Numeral0} IS @{term "number_of Pls"}
+*}
+
+lemma not_neg_number_of_Pls: "~ neg (number_of Int.Pls)"
+ by (simp add: neg_def)
+
+lemma neg_number_of_Min: "neg (number_of Int.Min)"
+ by (simp add: neg_def)
+
+lemma neg_number_of_Bit0:
+ "neg (number_of (Int.Bit0 w)) = neg (number_of w)"
+ by (simp add: neg_def)
+
+lemma neg_number_of_Bit1:
+ "neg (number_of (Int.Bit1 w)) = neg (number_of w)"
+ by (simp add: neg_def)
+
+lemmas neg_simps [simp] =
+ not_neg_0 not_neg_1
+ not_neg_number_of_Pls neg_number_of_Min
+ neg_number_of_Bit0 neg_number_of_Bit1
+
+
subsection{*Function @{term nat}: Coercion from Type @{typ int} to @{typ nat}*}
declare nat_0 [simp] nat_1 [simp]
@@ -61,52 +118,8 @@
done
-text{*Distributive laws for type @{text nat}. The others are in theory
- @{text IntArith}, but these require div and mod to be defined for type
- "int". They also need some of the lemmas proved above.*}
-
-lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
-apply (case_tac "0 <= z'")
-apply (auto simp add: div_nonneg_neg_le0)
-apply (case_tac "z' = 0", simp)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m div int m'")
- prefer 2 apply (simp add: nat_numeral_0_eq_0 pos_imp_zdiv_nonneg_iff)
-apply (rule of_nat_eq_iff [where 'a=int, THEN iffD1], simp)
-apply (rule_tac r = "int (m mod m') " in quorem_div)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
- of_nat_add [symmetric] of_nat_mult [symmetric]
- del: of_nat_add of_nat_mult)
-done
-
-(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-lemma nat_mod_distrib:
- "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
-apply (case_tac "z' = 0", simp add: DIVISION_BY_ZERO)
-apply (auto elim!: nonneg_eq_int)
-apply (rename_tac m m')
-apply (subgoal_tac "0 <= int m mod int m'")
- prefer 2 apply (simp add: nat_less_iff nat_numeral_0_eq_0 pos_mod_sign)
-apply (rule int_int_eq [THEN iffD1], simp)
-apply (rule_tac q = "int (m div m') " in quorem_mod)
- prefer 2 apply force
-apply (simp add: nat_less_iff [symmetric] quorem_def nat_numeral_0_eq_0
- of_nat_add [symmetric] of_nat_mult [symmetric]
- del: of_nat_add of_nat_mult)
-done
-
-text{*Suggested by Matthias Daum*}
-lemma int_div_less_self: "\<lbrakk>0 < x; 1 < k\<rbrakk> \<Longrightarrow> x div k < (x::int)"
-apply (subgoal_tac "nat x div nat k < nat x")
- apply (simp (asm_lr) add: nat_div_distrib [symmetric])
-apply (rule Divides.div_less_dividend, simp_all)
-done
-
subsection{*Function @{term int}: Coercion from Type @{typ nat} to @{typ int}*}
-(*"neg" is used in rewrite rules for binary comparisons*)
lemma int_nat_number_of [simp]:
"int (number_of v) =
(if neg (number_of v :: int) then 0
@@ -138,7 +151,6 @@
subsubsection{*Addition *}
-(*"neg" is used in rewrite rules for binary comparisons*)
lemma add_nat_number_of [simp]:
"(number_of v :: nat) + number_of v' =
(if v < Int.Pls then number_of v'
@@ -246,7 +258,6 @@
"[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')"
by (auto elim!: nonneg_eq_int)
-(*"neg" is used in rewrite rules for binary comparisons*)
lemma eq_nat_number_of [simp]:
"((number_of v :: nat) = number_of v') =
(if neg (number_of v :: int) then (number_of v' :: int) \<le> 0
@@ -627,9 +638,8 @@
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
lessD = lessD, neqE = neqE,
- simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
- @{thm not_neg_number_of_Pls}, @{thm neg_number_of_Min},
- @{thm neg_number_of_Bit0}, @{thm neg_number_of_Bit1}]})
+ simpset = simpset addsimps @{thms neg_simps} @
+ [@{thm Suc_nat_number_of}, @{thm int_nat_number_of}]})
*}
declaration {* K nat_bin_arith_setup *}
--- a/src/HOL/Real/HahnBanach/Bounds.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Bounds.thy Thu Dec 11 08:59:03 2008 +0100
@@ -6,7 +6,7 @@
header {* Bounds *}
theory Bounds
-imports Main Real
+imports Main ContNotDenum
begin
locale lub =
--- a/src/HOL/Tools/ComputeNumeral.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Tools/ComputeNumeral.thy Thu Dec 11 08:59:03 2008 +0100
@@ -29,63 +29,13 @@
lemmas bitlezero = lezero1 lezero2 lezero3 lezero4
(* equality for bit strings *)
-lemma biteq1: "(Int.Pls = Int.Pls) = True" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq2: "(Int.Min = Int.Min) = True" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq3: "(Int.Pls = Int.Min) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq4: "(Int.Min = Int.Pls) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq5: "(Int.Bit0 x = Int.Bit0 y) = (x = y)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq6: "(Int.Bit1 x = Int.Bit1 y) = (x = y)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq7: "(Int.Bit0 x = Int.Bit1 y) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq8: "(Int.Bit1 x = Int.Bit0 y) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq9: "(Int.Pls = Int.Bit0 x) = (Int.Pls = x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq10: "(Int.Pls = Int.Bit1 x) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq11: "(Int.Min = Int.Bit0 x) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq12: "(Int.Min = Int.Bit1 x) = (Int.Min = x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq13: "(Int.Bit0 x = Int.Pls) = (x = Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq14: "(Int.Bit1 x = Int.Pls) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq15: "(Int.Bit0 x = Int.Min) = False" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma biteq16: "(Int.Bit1 x = Int.Min) = (x = Int.Min)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemmas biteq = biteq1 biteq2 biteq3 biteq4 biteq5 biteq6 biteq7 biteq8 biteq9 biteq10 biteq11 biteq12 biteq13 biteq14 biteq15 biteq16
+lemmas biteq = eq_bin_simps
(* x < y for bit strings *)
-lemma bitless1: "(Int.Pls < Int.Min) = False" by (simp add: less_int_code)
-lemma bitless2: "(Int.Pls < Int.Pls) = False" by (simp add: less_int_code)
-lemma bitless3: "(Int.Min < Int.Pls) = True" by (simp add: less_int_code)
-lemma bitless4: "(Int.Min < Int.Min) = False" by (simp add: less_int_code)
-lemma bitless5: "(Int.Bit0 x < Int.Bit0 y) = (x < y)" by (simp add: less_int_code)
-lemma bitless6: "(Int.Bit1 x < Int.Bit1 y) = (x < y)" by (simp add: less_int_code)
-lemma bitless7: "(Int.Bit0 x < Int.Bit1 y) = (x \<le> y)" by (simp add: less_int_code)
-lemma bitless8: "(Int.Bit1 x < Int.Bit0 y) = (x < y)" by (simp add: less_int_code)
-lemma bitless9: "(Int.Pls < Int.Bit0 x) = (Int.Pls < x)" by (simp add: less_int_code)
-lemma bitless10: "(Int.Pls < Int.Bit1 x) = (Int.Pls \<le> x)" by (simp add: less_int_code)
-lemma bitless11: "(Int.Min < Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma bitless12: "(Int.Min < Int.Bit1 x) = (Int.Min < x)" by (simp add: less_int_code)
-lemma bitless13: "(Int.Bit0 x < Int.Pls) = (x < Int.Pls)" by (simp add: less_int_code)
-lemma bitless14: "(Int.Bit1 x < Int.Pls) = (x < Int.Pls)" by (simp add: less_int_code)
-lemma bitless15: "(Int.Bit0 x < Int.Min) = (x < Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma bitless16: "(Int.Bit1 x < Int.Min) = (x < Int.Min)" by (simp add: less_int_code)
-lemmas bitless = bitless1 bitless2 bitless3 bitless4 bitless5 bitless6 bitless7 bitless8
- bitless9 bitless10 bitless11 bitless12 bitless13 bitless14 bitless15 bitless16
+lemmas bitless = less_bin_simps
(* x \<le> y for bit strings *)
-lemma bitle1: "(Int.Pls \<le> Int.Min) = False" by (simp add: less_eq_int_code)
-lemma bitle2: "(Int.Pls \<le> Int.Pls) = True" by (simp add: less_eq_int_code)
-lemma bitle3: "(Int.Min \<le> Int.Pls) = True" by (simp add: less_eq_int_code)
-lemma bitle4: "(Int.Min \<le> Int.Min) = True" by (simp add: less_eq_int_code)
-lemma bitle5: "(Int.Bit0 x \<le> Int.Bit0 y) = (x \<le> y)" by (simp add: less_eq_int_code)
-lemma bitle6: "(Int.Bit1 x \<le> Int.Bit1 y) = (x \<le> y)" by (simp add: less_eq_int_code)
-lemma bitle7: "(Int.Bit0 x \<le> Int.Bit1 y) = (x \<le> y)" by (simp add: less_eq_int_code)
-lemma bitle8: "(Int.Bit1 x \<le> Int.Bit0 y) = (x < y)" by (simp add: less_eq_int_code)
-lemma bitle9: "(Int.Pls \<le> Int.Bit0 x) = (Int.Pls \<le> x)" by (simp add: less_eq_int_code)
-lemma bitle10: "(Int.Pls \<le> Int.Bit1 x) = (Int.Pls \<le> x)" by (simp add: less_eq_int_code)
-lemma bitle11: "(Int.Min \<le> Int.Bit0 x) = (Int.Pls \<le> x)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma bitle12: "(Int.Min \<le> Int.Bit1 x) = (Int.Min \<le> x)" by (simp add: less_eq_int_code)
-lemma bitle13: "(Int.Bit0 x \<le> Int.Pls) = (x \<le> Int.Pls)" by (simp add: less_eq_int_code)
-lemma bitle14: "(Int.Bit1 x \<le> Int.Pls) = (x < Int.Pls)" by (simp add: less_eq_int_code)
-lemma bitle15: "(Int.Bit0 x \<le> Int.Min) = (x < Int.Pls)" unfolding Pls_def Min_def Bit0_def Bit1_def by presburger
-lemma bitle16: "(Int.Bit1 x \<le> Int.Min) = (x \<le> Int.Min)" by (simp add: less_eq_int_code)
-lemmas bitle = bitle1 bitle2 bitle3 bitle4 bitle5 bitle6 bitle7 bitle8
- bitle9 bitle10 bitle11 bitle12 bitle13 bitle14 bitle15 bitle16
+lemmas bitle = le_bin_simps
(* succ for bit strings *)
lemmas bitsucc = succ_bin_simps
--- a/src/HOL/Tools/int_factor_simprocs.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML Thu Dec 11 08:59:03 2008 +0100
@@ -19,7 +19,7 @@
and d = gcd(m,m') and n=m/d and n'=m'/d.
*)
-val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of_eq_neg}, @{thm le_number_of_eq}];
+val rel_number_of = [@{thm eq_number_of_eq}, @{thm less_number_of}, @{thm le_number_of}];
local
open Int_Numeral_Simprocs
--- a/src/HOL/Tools/nat_simprocs.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/Tools/nat_simprocs.ML Thu Dec 11 08:59:03 2008 +0100
@@ -53,7 +53,7 @@
@{thm mult_nat_number_of}, @{thm nat_number_of_mult_left},
@{thm less_nat_number_of},
@{thm Let_number_of}, @{thm nat_number_of}] @
- @{thms arith_simps} @ @{thms rel_simps};
+ @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
fun prep_simproc (name, pats, proc) =
Simplifier.simproc (the_context ()) name pats proc;
--- a/src/HOL/ex/MIR.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOL/ex/MIR.thy Thu Dec 11 08:59:03 2008 +0100
@@ -1,9 +1,9 @@
-(* Title: Complex/ex/MIR.thy
+(* Title: HOL/ex/MIR.thy
Author: Amine Chaieb
*)
theory MIR
-imports List Real Code_Integer Efficient_Nat
+imports Main RComplete Code_Integer Efficient_Nat
uses ("mirtac.ML")
begin
--- a/src/HOLCF/Cfun.thy Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOLCF/Cfun.thy Thu Dec 11 08:59:03 2008 +0100
@@ -303,31 +303,34 @@
text {* cont2cont lemma for @{term Rep_CFun} *}
lemma cont2cont_Rep_CFun:
- "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x)\<cdot>(t x))"
-by (best intro: cont2cont_app2 cont_const cont_Rep_CFun cont_Rep_CFun2)
+ assumes f: "cont (\<lambda>x. f x)"
+ assumes t: "cont (\<lambda>x. t x)"
+ shows "cont (\<lambda>x. (f x)\<cdot>(t x))"
+proof -
+ have "cont (\<lambda>x. Rep_CFun (f x))"
+ using cont_Rep_CFun f by (rule cont2cont_app3)
+ thus "cont (\<lambda>x. (f x)\<cdot>(t x))"
+ using cont_Rep_CFun2 t by (rule cont2cont_app2)
+qed
text {* cont2mono Lemma for @{term "%x. LAM y. c1(x)(y)"} *}
lemma cont2mono_LAM:
-assumes p1: "!!x. cont(c1 x)"
-assumes p2: "!!y. monofun(%x. c1 x y)"
-shows "monofun(%x. LAM y. c1 x y)"
-apply (rule monofunI)
-apply (rule less_cfun_ext)
-apply (simp add: p1)
-apply (erule p2 [THEN monofunE])
-done
+ "\<lbrakk>\<And>x. cont (\<lambda>y. f x y); \<And>y. monofun (\<lambda>x. f x y)\<rbrakk>
+ \<Longrightarrow> monofun (\<lambda>x. \<Lambda> y. f x y)"
+ unfolding monofun_def expand_cfun_less by simp
-text {* cont2cont Lemma for @{term "%x. LAM y. c1 x y"} *}
+text {* cont2cont Lemma for @{term "%x. LAM y. f x y"} *}
lemma cont2cont_LAM:
-assumes p1: "!!x. cont(c1 x)"
-assumes p2: "!!y. cont(%x. c1 x y)"
-shows "cont(%x. LAM y. c1 x y)"
-apply (rule cont_Abs_CFun)
-apply (simp add: p1 CFun_def)
-apply (simp add: p2 cont2cont_lambda)
-done
+ assumes f1: "\<And>x. cont (\<lambda>y. f x y)"
+ assumes f2: "\<And>y. cont (\<lambda>x. f x y)"
+ shows "cont (\<lambda>x. \<Lambda> y. f x y)"
+proof (rule cont_Abs_CFun)
+ fix x
+ from f1 show "f x \<in> CFun" by (simp add: CFun_def)
+ from f2 show "cont f" by (rule cont2cont_lambda)
+qed
text {* continuity simplification procedure *}
--- a/src/HOLCF/Tools/cont_proc.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML Thu Dec 11 08:59:03 2008 +0100
@@ -1,5 +1,4 @@
(* Title: HOLCF/Tools/cont_proc.ML
- ID: $Id$
Author: Brian Huffman
*)
@@ -8,7 +7,7 @@
val is_lcf_term: term -> bool
val cont_thms: term -> thm list
val all_cont_thms: term -> thm list
- val cont_tac: int -> tactic
+ val cont_tac: thm list ref -> int -> tactic
val cont_proc: theory -> simproc
val setup: theory -> theory
end;
@@ -16,13 +15,22 @@
structure ContProc: CONT_PROC =
struct
+structure ContProcData = TheoryDataFun
+(
+ type T = thm list ref;
+ val empty = ref [];
+ val copy = I;
+ val extend = I;
+ fun merge _ _ = ref [];
+)
+
(** theory context references **)
-val cont_K = thm "cont_const";
-val cont_I = thm "cont_id";
-val cont_A = thm "cont2cont_Rep_CFun";
-val cont_L = thm "cont2cont_LAM";
-val cont_R = thm "cont_Rep_CFun2";
+val cont_K = @{thm cont_const};
+val cont_I = @{thm cont_id};
+val cont_A = @{thm cont2cont_Rep_CFun};
+val cont_L = @{thm cont2cont_LAM};
+val cont_R = @{thm cont_Rep_CFun2};
(* checks whether a term contains no dangling bound variables *)
val is_closed_term =
@@ -35,10 +43,11 @@
in bound_less 0 end;
(* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) =
+fun is_lcf_term (Const (@{const_name Rep_CFun}, _) $ t $ u) =
is_lcf_term t andalso is_lcf_term u
- | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t
- | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false
+ | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+ is_lcf_term t
+ | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ _) = false
| is_lcf_term (Bound _) = true
| is_lcf_term t = is_closed_term t;
@@ -73,12 +82,12 @@
(* first list: cont thm for each dangling bound variable *)
(* second list: cont thm for each LAM in t *)
(* if b = false, only return cont thm for outermost LAMs *)
- fun cont_thms1 b (Const ("Cfun.Rep_CFun", _) $ f $ t) =
+ fun cont_thms1 b (Const (@{const_name Rep_CFun}, _) $ f $ t) =
let
val (cs1,ls1) = cont_thms1 b f;
val (cs2,ls2) = cont_thms1 b t;
in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
- | cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) =
+ | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
let
val (cs, ls) = cont_thms1 b t;
val (cs', l) = lam cs;
@@ -98,41 +107,40 @@
conditional rewrite rule with the unsolved subgoals as premises.
*)
-local
- val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
+fun cont_tac prev_cont_thms =
+ let
+ val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
- (* FIXME proper cache as theory data!? *)
- val prev_cont_thms : thm list ref = ref [];
+ fun old_cont_tac i thm =
+ case !prev_cont_thms of
+ [] => no_tac thm
+ | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
- fun old_cont_tac i thm = CRITICAL (fn () =>
- case !prev_cont_thms of
- [] => no_tac thm
- | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
+ fun new_cont_tac f' i thm =
+ case all_cont_thms f' of
+ [] => no_tac thm
+ | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
- fun new_cont_tac f' i thm = CRITICAL (fn () =>
- case all_cont_thms f' of
- [] => no_tac thm
- | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
-
- fun cont_tac_of_term (Const ("Cont.cont", _) $ f) =
- let
- val f' = Const ("Cfun.Abs_CFun", dummyT) $ f;
- in
- if is_lcf_term f'
- then old_cont_tac ORELSE' new_cont_tac f'
- else REPEAT_ALL_NEW (resolve_tac rules)
- end
- | cont_tac_of_term _ = K no_tac;
-in
- val cont_tac =
- SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
-end;
+ fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
+ let
+ val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
+ in
+ if is_lcf_term f'
+ then old_cont_tac ORELSE' new_cont_tac f'
+ else REPEAT_ALL_NEW (resolve_tac rules)
+ end
+ | cont_tac_of_term _ = K no_tac;
+ in
+ SUBGOAL (fn (t, i) =>
+ cont_tac_of_term (HOLogic.dest_Trueprop t) i)
+ end;
local
fun solve_cont thy _ t =
let
val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
- in Option.map fst (Seq.pull (cont_tac 1 tr)) end
+ val prev_thms = ContProcData.get thy
+ in Option.map fst (Seq.pull (cont_tac prev_thms 1 tr)) end
in
fun cont_proc thy =
Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
--- a/src/Pure/Isar/class.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/Pure/Isar/class.ML Thu Dec 11 08:59:03 2008 +0100
@@ -394,7 +394,8 @@
end;
fun default_intro_tac ctxt [] =
- intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
+ intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE
+ Locale.intro_locales_tac true ctxt []
| default_intro_tac _ _ = no_tac;
fun default_tac rules ctxt facts =
--- a/src/Pure/Isar/expression.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/Pure/Isar/expression.ML Thu Dec 11 08:59:03 2008 +0100
@@ -19,9 +19,11 @@
(* Declaring locales *)
val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory ->
- string * Proof.context
+ (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
+ Proof.context
val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory ->
- string * Proof.context
+ (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
+ Proof.context
(* Interpretation *)
val sublocale_cmd: string -> expression -> theory -> Proof.state;
@@ -30,10 +32,6 @@
val interpretation: expression_i -> theory -> Proof.state;
val interpret_cmd: expression -> bool -> Proof.state -> Proof.state;
val interpret: expression_i -> bool -> Proof.state -> Proof.state;
-
- (* Debugging and development *)
- val parse_expression: OuterParse.token list -> expression * OuterParse.token list
- (* FIXME to spec_parse.ML *)
end;
@@ -55,63 +53,6 @@
type expression_i = term expr * (Binding.T * typ option * mixfix) list;
-(** Parsing and printing **)
-
-local
-
-structure P = OuterParse;
-
-val loc_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
- P.$$$ "defines" || P.$$$ "notes";
-fun plus1_unless test scan =
- scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan));
-
-val prefix = P.name --| P.$$$ ":";
-val named = P.name -- (P.$$$ "=" |-- P.term);
-val position = P.maybe P.term;
-val instance = P.$$$ "where" |-- P.and_list1 named >> Named ||
- Scan.repeat1 position >> Positional;
-
-in
-
-val parse_expression =
- let
- fun expr2 x = P.xname x;
- fun expr1 x = (Scan.optional prefix "" -- expr2 --
- Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
- fun expr0 x = (plus1_unless loc_keyword expr1) x;
- in expr0 -- P.for_fixes end;
-
-end;
-
-fun pretty_expr thy expr =
- let
- fun pretty_pos NONE = Pretty.str "_"
- | pretty_pos (SOME x) = Pretty.str x;
- fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=",
- Pretty.brk 1, Pretty.str y] |> Pretty.block;
- fun pretty_ren (Positional ps) = take_suffix is_none ps |> snd |>
- map pretty_pos |> Pretty.breaks
- | pretty_ren (Named []) = []
- | pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 ::
- (ps |> map pretty_named |> Pretty.separate "and");
- fun pretty_rename (loc, ("", ren)) =
- Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren)
- | pretty_rename (loc, (prfx, ren)) =
- Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) ::
- Pretty.brk 1 :: pretty_ren ren);
- in Pretty.separate "+" (map pretty_rename expr) |> Pretty.block end;
-
-fun err_in_expr thy msg expr =
- let
- val err_msg =
- if null expr then msg
- else msg ^ "\n" ^ Pretty.string_of (Pretty.block
- [Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1,
- pretty_expr thy expr])
- in error err_msg end;
-
-
(** Internalise locale names in expr **)
fun intern thy instances = map (apfst (NewLocale.intern thy)) instances;
@@ -133,6 +74,13 @@
end;
fun match_bind (n, b) = (n = Binding.base_name b);
+ fun parm_eq ((b1, mx1), (b2, mx2)) =
+ (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
+ (Binding.base_name b1 = Binding.base_name b2) andalso
+ (if mx1 = mx2 then true
+ else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^
+ " in expression."));
+
fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
(* FIXME: cannot compare bindings for equality. *)
@@ -164,12 +112,7 @@
val (is', ps') = fold_map (fn i => fn ps =>
let
val (ps', i') = params_inst i;
- val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
- (* FIXME: should check for bindings being the same.
- Instead we check for equal name and syntax. *)
- if mx1 = mx2 then mx1
- else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^
- " in expression.")) (ps, ps')
+ val ps'' = distinct parm_eq (ps @ ps');
in (i', ps'') end) is []
in (ps', is') end;
@@ -329,21 +272,18 @@
val norm_term = Envir.beta_norm oo Term.subst_atomic;
-fun abstract_thm thy eq =
- Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
-
-fun bind_def ctxt eq (xs, env, ths) =
+fun bind_def ctxt eq (xs, env, eqs) =
let
+ val _ = LocalDefs.cert_def ctxt eq;
val ((y, T), b) = LocalDefs.abs_def eq;
val b' = norm_term env b;
- val th = abstract_thm (ProofContext.theory_of ctxt) eq;
fun err msg = error (msg ^ ": " ^ quote y);
in
exists (fn (x, _) => x = y) xs andalso
err "Attempt to define previously specified variable";
exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
err "Attempt to redefine variable";
- (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
+ (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
end;
fun eval_text _ _ (Fixes _) text = text
@@ -494,8 +434,7 @@
env: list of term pairs encoding substitutions, where the first term
is a free variable; substitutions represent defines elements and
the rhs is normalised wrt. the previous env
- defs: theorems representing the substitutions from defines elements
- (thms are normalised wrt. env).
+ defs: the equations from the defines elements
elems is an updated version of raw_elems:
- type info added to Fixes and modified in Constrains
- axiom and definition statement replaced by corresponding one
@@ -548,7 +487,6 @@
NewLocale.clear_local_idents |> fold NewLocale.activate_local_facts deps;
val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
in ((fixed, deps, elems'), (parms, spec, defs)) end;
- (* FIXME check if defs used somewhere *)
in
@@ -583,7 +521,6 @@
val export = Variable.export_morphism goal_ctxt context;
val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
-(* val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *)
val exp_term = Drule.term_rule thy (singleton exp_fact);
val exp_typ = Logic.type_map exp_term;
val export' =
@@ -687,6 +624,8 @@
fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
let
+ val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
+
val (a_pred, a_intro, a_axioms, thy'') =
if null exts then (NONE, NONE, [], thy)
else
@@ -694,7 +633,7 @@
val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
val ((statement, intro, axioms), thy') =
thy
- |> def_pred aname parms defs exts exts';
+ |> def_pred aname parms defs' exts exts';
val (_, thy'') =
thy'
|> Sign.add_path aname
@@ -709,7 +648,7 @@
let
val ((statement, intro, axioms), thy''') =
thy''
- |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred);
+ |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
val (_, thy'''') =
thy'''
|> Sign.add_path pname
@@ -734,15 +673,10 @@
|> apfst (curry Notes Thm.assumptionK)
| assumes_to_notes e axms = (e, axms);
-fun defines_to_notes thy (Defines defs) defns =
- let
- val defs' = map (fn (_, (def, _)) => def) defs
- val notes = map (fn (a, (def, _)) =>
- (a, [([Assumption.assume (cterm_of thy def)], [])])) defs
- in
- (Notes (Thm.definitionK, notes), defns @ defs')
- end
- | defines_to_notes _ e defns = (e, defns);
+fun defines_to_notes thy (Defines defs) =
+ Notes (Thm.definitionK, map (fn (a, (def, _)) =>
+ (a, [([Assumption.assume (cterm_of thy def)], [])])) defs)
+ | defines_to_notes _ e = e;
fun gen_add_locale prep_decl
bname predicate_name raw_imprt raw_body thy =
@@ -751,7 +685,7 @@
val _ = NewLocale.test_locale thy name andalso
error ("Duplicate definition of locale " ^ quote name);
- val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), _)) =
+ val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
prep_decl raw_imprt raw_body (ProofContext.init thy);
val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
define_preds predicate_name text thy;
@@ -760,29 +694,39 @@
val _ = if null extraTs then ()
else warning ("Additional type variable(s) in locale specification " ^ quote bname);
- val satisfy = Element.satisfy_morphism b_axioms;
+ val a_satisfy = Element.satisfy_morphism a_axioms;
+ val b_satisfy = Element.satisfy_morphism b_axioms;
val params = fixed @
(body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
val asm = if is_some b_statement then b_statement else a_statement;
- val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems [];
- val notes = body_elems' |>
+
+ (* These are added immediately. *)
+ val notes =
+ if is_some asm
+ then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
+ [([Assumption.assume (cterm_of thy' (the asm))],
+ [(Attrib.internal o K) NewLocale.witness_attrib])])])]
+ else [];
+
+ (* These will be added in the local theory. *)
+ val notes' = body_elems |>
+ map (defines_to_notes thy') |>
+ map (Element.morph_ctxt a_satisfy) |>
(fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
- fst |> map (Element.morph_ctxt satisfy) |>
- map_filter (fn Notes notes => SOME notes | _ => NONE) |>
- (if is_some asm
- then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
- [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
- else I);
+ fst |>
+ map (Element.morph_ctxt b_satisfy) |>
+ map_filter (fn Notes notes => SOME notes | _ => NONE);
- val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
+ val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps;
val loc_ctxt = thy' |>
NewLocale.register_locale bname (extraTs, params)
- (asm, defns) ([], [])
+ (asm, rev defs) ([], [])
(map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
- NewLocale.init name
- in (name, loc_ctxt) end;
+ NewLocale.init name;
+
+ in ((name, notes'), loc_ctxt) end;
in
--- a/src/Pure/Isar/isar_syn.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Dec 11 08:59:03 2008 +0100
@@ -401,7 +401,7 @@
val _ =
OuterSyntax.command "sublocale"
"prove sublocale relation between a locale and a locale expression" K.thy_goal
- (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
+ (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expression
>> (fn (loc, expr) =>
Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
--- a/src/Pure/Isar/new_locale.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML Thu Dec 11 08:59:03 2008 +0100
@@ -39,7 +39,6 @@
Proof.context -> Proof.context
val activate_global_facts: string * Morphism.morphism -> theory -> theory
val activate_local_facts: string * Morphism.morphism -> Proof.context -> Proof.context
-(* val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
val init: string -> theory -> Proof.context
(* Reasoning about locales *)
--- a/src/Pure/Isar/spec_parse.ML Thu Dec 11 08:56:02 2008 +0100
+++ b/src/Pure/Isar/spec_parse.ML Thu Dec 11 08:59:03 2008 +0100
@@ -26,6 +26,7 @@
val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
val class_expr: token list -> string list * token list
val locale_expr: token list -> Locale.expr * token list
+ val locale_expression: OuterParse.token list -> Expression.expression * OuterParse.token list
val locale_keyword: token list -> string * token list
val context_element: token list -> Element.context * token list
val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
@@ -103,6 +104,12 @@
val rename = P.name -- Scan.option P.mixfix;
+val prefix = P.name --| P.$$$ ":";
+val named = P.name -- (P.$$$ "=" |-- P.term);
+val position = P.maybe P.term;
+val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named ||
+ Scan.repeat1 position >> Expression.Positional;
+
in
val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" ||
@@ -117,6 +124,14 @@
and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Locale.Merge es)) x;
in expr0 end;
+val locale_expression =
+ let
+ fun expr2 x = P.xname x;
+ fun expr1 x = (Scan.optional prefix "" -- expr2 --
+ Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x;
+ fun expr0 x = (plus1_unless locale_keyword expr1) x;
+ in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end;
+
val context_element = P.group "context element" loc_element;
end;