--- a/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 22:36:36 2010 +0100
@@ -87,8 +87,8 @@
| NONE =>
let
val args = Name.variant_list [] (replicate arity "'")
- val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
- mk_syntax name arity) thy
+ val (T, thy') =
+ Typedecl.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
val type_name = fst (Term.dest_Type T)
in (((name, type_name), log_new name type_name), thy') end)
end
--- a/src/HOL/Complete_Lattice.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Complete_Lattice.thy Sun Mar 07 22:36:36 2010 +0100
@@ -82,6 +82,12 @@
"\<Squnion>UNIV = top"
by (simp add: Inf_Sup Inf_empty [symmetric])
+lemma Sup_le_iff: "Sup A \<sqsubseteq> b \<longleftrightarrow> (\<forall>a\<in>A. a \<sqsubseteq> b)"
+ by (auto intro: Sup_least dest: Sup_upper)
+
+lemma le_Inf_iff: "b \<sqsubseteq> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<sqsubseteq> a)"
+ by (auto intro: Inf_greatest dest: Inf_lower)
+
definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
"SUPR A f = \<Squnion> (f ` A)"
@@ -126,6 +132,12 @@
lemma le_INFI: "(\<And>i. i : A \<Longrightarrow> u \<sqsubseteq> M i) \<Longrightarrow> u \<sqsubseteq> (INF i:A. M i)"
by (auto simp add: INFI_def intro: Inf_greatest)
+lemma SUP_le_iff: "(SUP i:A. M i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i \<in> A. M i \<sqsubseteq> u)"
+ unfolding SUPR_def by (auto simp add: Sup_le_iff)
+
+lemma le_INF_iff: "u \<sqsubseteq> (INF i:A. M i) \<longleftrightarrow> (\<forall>i \<in> A. u \<sqsubseteq> M i)"
+ unfolding INFI_def by (auto simp add: le_Inf_iff)
+
lemma SUP_const[simp]: "A \<noteq> {} \<Longrightarrow> (SUP i:A. M) = M"
by (auto intro: antisym SUP_leI le_SUPI)
@@ -384,7 +396,7 @@
by blast
lemma UN_subset_iff: "((\<Union>i\<in>I. A i) \<subseteq> B) = (\<forall>i\<in>I. A i \<subseteq> B)"
- by blast
+ by (fact SUP_le_iff)
lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
by blast
@@ -591,7 +603,7 @@
by blast
lemma INT_subset_iff: "(B \<subseteq> (\<Inter>i\<in>I. A i)) = (\<forall>i\<in>I. B \<subseteq> A i)"
- by blast
+ by (fact le_INF_iff)
lemma INT_insert [simp]: "(\<Inter>x \<in> insert a A. B x) = B a \<inter> INTER A B"
by blast
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Mar 07 22:36:36 2010 +0100
@@ -3098,7 +3098,7 @@
struct
fun frpar_tac T ps ctxt i =
- (ObjectLogic.full_atomize_tac i)
+ Object_Logic.full_atomize_tac i
THEN (fn st =>
let
val g = List.nth (cprems_of st, i - 1)
@@ -3108,7 +3108,7 @@
in rtac (th RS iffD2) i st end);
fun frpar2_tac T ps ctxt i =
- (ObjectLogic.full_atomize_tac i)
+ Object_Logic.full_atomize_tac i
THEN (fn st =>
let
val g = List.nth (cprems_of st, i - 1)
--- a/src/HOL/Decision_Procs/cooper_tac.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Mar 07 22:36:36 2010 +0100
@@ -66,7 +66,7 @@
fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
-fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
+fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
let
val g = List.nth (prems_of st, i - 1)
val thy = ProofContext.theory_of ctxt
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Mar 07 22:36:36 2010 +0100
@@ -73,7 +73,7 @@
fun linr_tac ctxt q =
- ObjectLogic.atomize_prems_tac
+ Object_Logic.atomize_prems_tac
THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
THEN' SUBGOAL (fn (g, i) =>
let
--- a/src/HOL/Decision_Procs/mir_tac.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Mar 07 22:36:36 2010 +0100
@@ -88,7 +88,7 @@
fun mir_tac ctxt q i =
- ObjectLogic.atomize_prems_tac i
+ Object_Logic.atomize_prems_tac i
THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
THEN (fn st =>
--- a/src/HOL/HOL.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/HOL.thy Sun Mar 07 22:36:36 2010 +0100
@@ -44,7 +44,7 @@
classes type
defaultsort type
-setup {* ObjectLogic.add_base_sort @{sort type} *}
+setup {* Object_Logic.add_base_sort @{sort type} *}
arities
"fun" :: (type, type) type
--- a/src/HOL/Int.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Int.thy Sun Mar 07 22:36:36 2010 +0100
@@ -1262,6 +1262,15 @@
notation (xsymbols)
Ints ("\<int>")
+lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
+ by (simp add: Ints_def)
+
+lemma Ints_of_nat [simp]: "of_nat n \<in> \<int>"
+apply (simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_of_nat_eq [symmetric])
+done
+
lemma Ints_0 [simp]: "0 \<in> \<int>"
apply (simp add: Ints_def)
apply (rule range_eqI)
@@ -1286,12 +1295,21 @@
apply (rule of_int_minus [symmetric])
done
+lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a - b \<in> \<int>"
+apply (auto simp add: Ints_def)
+apply (rule range_eqI)
+apply (rule of_int_diff [symmetric])
+done
+
lemma Ints_mult [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a * b \<in> \<int>"
apply (auto simp add: Ints_def)
apply (rule range_eqI)
apply (rule of_int_mult [symmetric])
done
+lemma Ints_power [simp]: "a \<in> \<int> \<Longrightarrow> a ^ n \<in> \<int>"
+by (induct n) simp_all
+
lemma Ints_cases [cases set: Ints]:
assumes "q \<in> \<int>"
obtains (of_int) z where "q = of_int z"
@@ -1308,12 +1326,6 @@
end
-lemma Ints_diff [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a-b \<in> \<int>"
-apply (auto simp add: Ints_def)
-apply (rule range_eqI)
-apply (rule of_int_diff [symmetric])
-done
-
text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}
lemma Ints_double_eq_0_iff:
@@ -1350,10 +1362,15 @@
qed
qed
-lemma Ints_number_of:
+lemma Ints_number_of [simp]:
"(number_of w :: 'a::number_ring) \<in> Ints"
unfolding number_of_eq Ints_def by simp
+lemma Nats_number_of [simp]:
+ "Int.Pls \<le> w \<Longrightarrow> (number_of w :: 'a::number_ring) \<in> Nats"
+unfolding Int.Pls_def number_of_eq
+by (simp only: of_nat_nat [symmetric] of_nat_in_Nats)
+
lemma Ints_odd_less_0:
assumes in_Ints: "a \<in> Ints"
shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
--- a/src/HOL/Library/Efficient_Nat.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Sun Mar 07 22:36:36 2010 +0100
@@ -181,7 +181,7 @@
| find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
| find_var _ = NONE;
fun find_thm th =
- let val th' = Conv.fconv_rule ObjectLogic.atomize th
+ let val th' = Conv.fconv_rule Object_Logic.atomize th
in Option.map (pair (th, th')) (find_var (prop_of th')) end
in
case get_first find_thm thms of
@@ -189,7 +189,7 @@
| SOME ((th, th'), (Sucv, v)) =>
let
val cert = cterm_of (Thm.theory_of_thm th);
- val th'' = ObjectLogic.rulify (Thm.implies_elim
+ val th'' = Object_Logic.rulify (Thm.implies_elim
(Conv.fconv_rule (Thm.beta_conversion true)
(Drule.instantiate' []
[SOME (cert (lambda v (Abs ("x", HOLogic.natT,
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sun Mar 07 22:36:36 2010 +0100
@@ -1431,7 +1431,7 @@
fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
fun sos_tac print_cert prover ctxt =
- ObjectLogic.full_atomize_tac THEN'
+ Object_Logic.full_atomize_tac THEN'
elim_denom_tac ctxt THEN'
core_sos_tac print_cert prover ctxt;
--- a/src/HOL/Library/normarith.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Library/normarith.ML Sun Mar 07 22:36:36 2010 +0100
@@ -410,7 +410,7 @@
fun norm_arith_tac ctxt =
clarify_tac HOL_cs THEN'
- ObjectLogic.full_atomize_tac THEN'
+ Object_Logic.full_atomize_tac THEN'
CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
end;
--- a/src/HOL/Library/reflection.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Library/reflection.ML Sun Mar 07 22:36:36 2010 +0100
@@ -62,7 +62,7 @@
fun tryext x = (x RS ext2 handle THM _ => x)
val cong = (Goal.prove ctxt'' [] (map mk_def env)
(HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, replace_fterms rhs)))
- (fn x => LocalDefs.unfold_tac (#context x) (map tryext (#prems x))
+ (fn x => Local_Defs.unfold_tac (#context x) (map tryext (#prems x))
THEN rtac th' 1)) RS sym
val (cong' :: vars') =
--- a/src/HOL/Mutabelle/mutabelle.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Sun Mar 07 22:36:36 2010 +0100
@@ -494,7 +494,7 @@
fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
| inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
-fun preprocess thy insts t = ObjectLogic.atomize_term thy
+fun preprocess thy insts t = Object_Logic.atomize_term thy
(map_types (inst_type insts) (freeze t));
fun is_executable thy insts th =
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 07 22:36:36 2010 +0100
@@ -91,7 +91,7 @@
fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
| inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
-fun preprocess thy insts t = ObjectLogic.atomize_term thy
+fun preprocess thy insts t = Object_Logic.atomize_term thy
(map_types (inst_type insts) (Mutabelle.freeze t));
fun invoke_quickcheck quickcheck_generator thy t =
--- a/src/HOL/NSA/transfer.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/NSA/transfer.ML Sun Mar 07 22:36:36 2010 +0100
@@ -56,14 +56,14 @@
let
val thy = ProofContext.theory_of ctxt;
val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
- val meta = LocalDefs.meta_rewrite_rule ctxt;
+ val meta = Local_Defs.meta_rewrite_rule ctxt;
val ths' = map meta ths;
val unfolds' = map meta unfolds and refolds' = map meta refolds;
val (_$_$t') = concl_of (MetaSimplifier.rewrite true unfolds' (cterm_of thy t))
val u = unstar_term consts t'
val tac =
rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
- ALLGOALS ObjectLogic.full_atomize_tac THEN
+ ALLGOALS Object_Logic.full_atomize_tac THEN
match_tac [transitive_thm] 1 THEN
resolve_tac [@{thm transfer_start}] 1 THEN
REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
--- a/src/HOL/Nat.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Nat.thy Sun Mar 07 22:36:36 2010 +0100
@@ -1400,6 +1400,20 @@
apply (rule of_nat_mult [symmetric])
done
+lemma Nats_cases [cases set: Nats]:
+ assumes "x \<in> \<nat>"
+ obtains (of_nat) n where "x = of_nat n"
+ unfolding Nats_def
+proof -
+ from `x \<in> \<nat>` have "x \<in> range of_nat" unfolding Nats_def .
+ then obtain n where "x = of_nat n" ..
+ then show thesis ..
+qed
+
+lemma Nats_induct [case_names of_nat, induct set: Nats]:
+ "x \<in> \<nat> \<Longrightarrow> (\<And>n. P (of_nat n)) \<Longrightarrow> P x"
+ by (rule Nats_cases) auto
+
end
--- a/src/HOL/Nat_Numeral.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Nat_Numeral.thy Sun Mar 07 22:36:36 2010 +0100
@@ -113,7 +113,7 @@
end
-context linordered_ring_strict
+context linordered_ring
begin
lemma sum_squares_ge_zero:
@@ -124,6 +124,11 @@
"\<not> x * x + y * y < 0"
by (simp add: not_less sum_squares_ge_zero)
+end
+
+context linordered_ring_strict
+begin
+
lemma sum_squares_eq_zero_iff:
"x * x + y * y = 0 \<longleftrightarrow> x = 0 \<and> y = 0"
by (simp add: add_nonneg_eq_0_iff)
@@ -134,14 +139,7 @@
lemma sum_squares_gt_zero_iff:
"0 < x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
-proof -
- have "x * x + y * y \<noteq> 0 \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
- by (simp add: sum_squares_eq_zero_iff)
- then have "0 \<noteq> x * x + y * y \<longleftrightarrow> x \<noteq> 0 \<or> y \<noteq> 0"
- by auto
- then show ?thesis
- by (simp add: less_le sum_squares_ge_zero)
-qed
+ by (simp add: not_le [symmetric] sum_squares_le_zero_iff)
end
--- a/src/HOL/Nominal/nominal_datatype.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Mar 07 22:36:36 2010 +0100
@@ -1074,7 +1074,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
- (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+ (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms' 1),
simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
--- a/src/HOL/Parity.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Parity.thy Sun Mar 07 22:36:36 2010 +0100
@@ -218,7 +218,7 @@
done
lemma zero_le_even_power: "even n ==>
- 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n"
+ 0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
apply (simp add: even_nat_equiv_def2)
apply (erule exE)
apply (erule ssubst)
--- a/src/HOL/RealDef.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/RealDef.thy Sun Mar 07 22:36:36 2010 +0100
@@ -701,6 +701,9 @@
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
by (insert real_of_int_div2 [of n x], simp)
+lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
+unfolding real_of_int_def by (rule Ints_of_int)
+
subsection{*Embedding the Naturals into the Reals*}
@@ -852,6 +855,12 @@
apply (simp only: real_of_int_real_of_nat)
done
+lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
+unfolding real_of_nat_def by (rule of_nat_in_Nats)
+
+lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
+unfolding real_of_nat_def by (rule Ints_of_nat)
+
subsection{* Rationals *}
--- a/src/HOL/RealPow.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/RealPow.thy Sun Mar 07 22:36:36 2010 +0100
@@ -24,71 +24,76 @@
apply (rule two_realpow_ge_one)
done
-lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_Suc_le_self:
+ fixes r :: "'a::linordered_semidom"
+ shows "[| 0 \<le> r; r \<le> 1 |] ==> r ^ Suc n \<le> r"
by (insert power_decreasing [of 1 "Suc n" r], simp)
-lemma realpow_minus_mult [rule_format]:
- "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
-apply (simp split add: nat_diff_split)
-done
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_minus_mult:
+ fixes x :: "'a::monoid_mult"
+ shows "0 < n \<Longrightarrow> x ^ (n - 1) * x = x ^ n"
+by (simp add: power_commutes split add: nat_diff_split)
+(* TODO: no longer real-specific; rename and move elsewhere *)
lemma realpow_two_diff:
- "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
+ fixes x :: "'a::comm_ring_1"
+ shows "x^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
by (simp add: algebra_simps)
+(* TODO: move elsewhere *)
+lemma add_eq_0_iff:
+ fixes x y :: "'a::group_add"
+ shows "x + y = 0 \<longleftrightarrow> y = - x"
+by (auto dest: minus_unique)
+
+(* TODO: no longer real-specific; rename and move elsewhere *)
lemma realpow_two_disj:
- "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
-apply (cut_tac x = x and y = y in realpow_two_diff)
-apply auto
-done
+ fixes x :: "'a::idom"
+ shows "(x^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
+using realpow_two_diff [of x y]
+by (auto simp add: add_eq_0_iff)
subsection{* Squares of Reals *}
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma real_two_squares_add_zero_iff [simp]:
"(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)"
by (rule sum_squares_eq_zero_iff)
-lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)"
-by simp
-
-lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)"
-by simp
-
-lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
-by (simp add: real_add_eq_0_iff [symmetric])
-
-lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
-by (simp add: left_distrib right_diff_distrib)
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma real_squared_diff_one_factored:
+ fixes x :: "'a::ring_1"
+ shows "x * x - 1 = (x + 1) * (x - 1)"
+by (simp add: algebra_simps)
-lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
-apply auto
-apply (drule right_minus_eq [THEN iffD2])
-apply (auto simp add: real_squared_diff_one_factored)
-done
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma real_mult_is_one [simp]:
+ fixes x :: "'a::ring_1_no_zero_divisors"
+ shows "x * x = 1 \<longleftrightarrow> x = 1 \<or> x = - 1"
+proof -
+ have "x * x = 1 \<longleftrightarrow> (x + 1) * (x - 1) = 0"
+ by (simp add: algebra_simps)
+ also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
+ by (auto simp add: add_eq_0_iff minus_equation_iff [of _ 1])
+ finally show ?thesis .
+qed
-lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
-by simp
-
-lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
-by simp
-
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma realpow_two_sum_zero_iff [simp]:
"(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
by (rule sum_power2_eq_zero_iff)
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
by (rule sum_power2_ge_zero)
+(* FIXME: declare this [simp] for all types, or not at all *)
lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
by (intro add_nonneg_nonneg zero_le_power2)
-lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
-by (simp add: sum_squares_gt_zero_iff)
-
-lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
-by (simp add: sum_squares_gt_zero_iff)
-
lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
by (rule_tac j = 0 in real_le_trans, auto)
@@ -96,8 +101,9 @@
by (auto simp add: power2_eq_square)
(* The following theorem is by Benjamin Porter *)
+(* TODO: no longer real-specific; rename and move elsewhere *)
lemma real_sq_order:
- fixes x::real
+ fixes x :: "'a::linordered_semidom"
assumes xgt0: "0 \<le> x" and ygt0: "0 \<le> y" and sq: "x^2 \<le> y^2"
shows "x \<le> y"
proof -
@@ -150,8 +156,11 @@
apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
done
-lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
-by (case_tac "n", auto)
+(* TODO: no longer real-specific; rename and move elsewhere *)
+lemma realpow_num_eq_if:
+ fixes m :: "'a::power"
+ shows "m ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
+by (cases n, auto)
end
--- a/src/HOL/Rings.thy Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Rings.thy Sun Mar 07 22:36:36 2010 +0100
@@ -796,6 +796,13 @@
auto intro: add_nonneg_nonneg, auto intro!: less_imp_le add_neg_neg)
qed (auto simp add: abs_if)
+lemma zero_le_square [simp]: "0 \<le> a * a"
+ using linear [of 0 a]
+ by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos)
+
+lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
+ by (simp add: not_less)
+
end
(* The "strict" suffix can be seen as describing the combination of linordered_ring and no_zero_divisors.
@@ -873,12 +880,6 @@
apply force
done
-lemma zero_le_square [simp]: "0 \<le> a * a"
-by (simp add: zero_le_mult_iff linear)
-
-lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
-by (simp add: not_less)
-
text{*Cancellation laws for @{term "c*a < c*b"} and @{term "a*c < b*c"},
also with the relations @{text "\<le>"} and equality.*}
--- a/src/HOL/Tools/Datatype/datatype.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Mar 07 22:36:36 2010 +0100
@@ -417,7 +417,7 @@
val inj_thm = Skip_Proof.prove_global thy5 [] []
(HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
- [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+ [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (EVERY
[rtac allI 1, rtac impI 1,
exh_tac (exh_thm_of dt_info) 1,
@@ -443,7 +443,7 @@
val elem_thm =
Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
(fn _ =>
- EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+ EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
rewrite_goals_tac rewrites,
REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
@@ -479,7 +479,7 @@
val iso_thms = if length descr = 1 then [] else
drop (length newTs) (split_conj_thm
(Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
- [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+ [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
REPEAT (rtac TrueI 1),
rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
@@ -617,7 +617,7 @@
(Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
(fn {prems, ...} => EVERY
[rtac indrule_lemma' 1,
- (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+ (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
[REPEAT (eresolve_tac Abs_inverse_thms 1),
simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Mar 07 22:36:36 2010 +0100
@@ -209,7 +209,7 @@
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
(map cert insts)) induct;
val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
- (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
+ (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
in split_conj_thm (Skip_Proof.prove_global thy1 [] []
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sun Mar 07 22:36:36 2010 +0100
@@ -115,7 +115,7 @@
(fn prems =>
[rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
rtac (cterm_instantiate inst induct) 1,
- ALLGOALS ObjectLogic.atomize_prems_tac,
+ ALLGOALS Object_Logic.atomize_prems_tac,
rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
REPEAT (etac allE i) THEN atac i)) 1)]);
--- a/src/HOL/Tools/Function/induction_schema.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Sun Mar 07 22:36:36 2010 +0100
@@ -195,7 +195,7 @@
|> fold_rev (curry Logic.mk_implies) Cs
|> fold_rev (Logic.all o Free) ws
|> term_conv thy ind_atomize
- |> ObjectLogic.drop_judgment thy
+ |> Object_Logic.drop_judgment thy
|> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
in
SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
--- a/src/HOL/Tools/Function/mutual.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Sun Mar 07 22:36:36 2010 +0100
@@ -190,7 +190,7 @@
in
Goal.prove ctxt [] []
(HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
- (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
+ (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
|> restore_cond
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Mar 07 22:36:36 2010 +0100
@@ -123,7 +123,7 @@
(* General reduction pair application *)
fun rem_inv_img ctxt =
let
- val unfold_tac = LocalDefs.unfold_tac ctxt
+ val unfold_tac = Local_Defs.unfold_tac ctxt
in
rtac @{thm subsetI} 1
THEN etac @{thm CollectE} 1
@@ -259,7 +259,7 @@
THEN mset_pwleq_tac 1
THEN EVERY (map2 (less_proof false) qs ps)
THEN (if strict orelse qs <> lq
- then LocalDefs.unfold_tac ctxt set_of_simps
+ then Local_Defs.unfold_tac ctxt set_of_simps
THEN steps_tac MAX true
(subtract (op =) qs lq) (subtract (op =) ps lp)
else all_tac)
@@ -290,7 +290,7 @@
THEN (rtac (order_rpair ms_rp label) 1)
THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt)
- THEN LocalDefs.unfold_tac ctxt
+ THEN Local_Defs.unfold_tac ctxt
(@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
THEN EVERY (map (prove_lev true) sl)
--- a/src/HOL/Tools/Function/termination.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML Sun Mar 07 22:36:36 2010 +0100
@@ -282,7 +282,7 @@
let
val (vars, prems, lhs, rhs) = dest_term ineq
in
- mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
+ mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
end
val relation =
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Mar 07 22:36:36 2010 +0100
@@ -967,10 +967,11 @@
(semiring_normalize_wrapper ctxt res)) form));
fun ring_tac add_ths del_ths ctxt =
- ObjectLogic.full_atomize_tac
- THEN' asm_full_simp_tac (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
+ Object_Logic.full_atomize_tac
+ THEN' asm_full_simp_tac
+ (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
THEN' CSUBGOAL (fn (p, i) =>
- rtac (let val form = (ObjectLogic.dest_judgment p)
+ rtac (let val form = Object_Logic.dest_judgment p
in case get_ring_ideal_convs ctxt form of
NONE => reflexive form
| SOME thy => #ring_conv thy form
@@ -1008,7 +1009,7 @@
end
in
clarify_tac @{claset} i
- THEN ObjectLogic.full_atomize_tac i
+ THEN Object_Logic.full_atomize_tac i
THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i
THEN clarify_tac @{claset} i
THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Mar 07 22:36:36 2010 +0100
@@ -127,7 +127,7 @@
check_rules fieldN f_rules 2 andalso
check_rules idomN idom 2;
- val mk_meta = LocalDefs.meta_rewrite_rule ctxt;
+ val mk_meta = Local_Defs.meta_rewrite_rule ctxt;
val sr_rules' = map mk_meta sr_rules;
val r_rules' = map mk_meta r_rules;
val f_rules' = map mk_meta f_rules;
--- a/src/HOL/Tools/Nitpick/minipick.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML Sun Mar 07 22:36:36 2010 +0100
@@ -298,7 +298,7 @@
| card (Type ("*", [T1, T2])) = card T1 * card T2
| card @{typ bool} = 2
| card T = Int.max (1, raw_card T)
- val neg_t = @{const Not} $ ObjectLogic.atomize_term thy t
+ val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
val _ = fold_types (K o check_type ctxt) neg_t ()
val frees = Term.add_frees neg_t []
val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Mar 07 22:36:36 2010 +0100
@@ -1762,8 +1762,8 @@
(* theory -> styp -> term -> term list * term list * term *)
fun triple_for_intro_rule thy x t =
let
- val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
- val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
+ val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
+ val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
(* term -> bool *)
val is_good_head = curry (op =) (Const x) o head_of
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Mar 07 22:36:36 2010 +0100
@@ -807,7 +807,7 @@
fun try_out negate =
let
val concl = (negate ? curry (op $) @{const Not})
- (ObjectLogic.atomize_term thy prop)
+ (Object_Logic.atomize_term thy prop)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
|> map_types (map_type_tfree
(fn (s, []) => TFree (s, HOLogic.typeS)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Mar 07 22:36:36 2010 +0100
@@ -418,7 +418,7 @@
*)
fun prepare_split_thm ctxt split_thm =
(split_thm RS @{thm iffD2})
- |> LocalDefs.unfold ctxt [@{thm atomize_conjL[symmetric]},
+ |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
@{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
fun find_split_thm thy (Const (name, typ)) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Mar 07 22:36:36 2010 +0100
@@ -145,7 +145,7 @@
val t' = Pattern.rewrite_term thy rewr [] t
val tac = Skip_Proof.cheat_tac thy
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
- val th''' = LocalDefs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
+ val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
in
th'''
end;
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sun Mar 07 22:36:36 2010 +0100
@@ -225,9 +225,9 @@
(case dlo_instance ctxt p of
NONE => no_tac
| SOME instance =>
- ObjectLogic.full_atomize_tac i THEN
+ Object_Logic.full_atomize_tac i THEN
simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *)
- CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
+ CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
simp_tac (simpset_of ctxt) i)); (* FIXME really? *)
end;
--- a/src/HOL/Tools/Qelim/langford.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML Sun Mar 07 22:36:36 2010 +0100
@@ -234,11 +234,11 @@
(case dlo_instance ctxt p of
(ss, NONE) => simp_tac ss i
| (ss, SOME instance) =>
- ObjectLogic.full_atomize_tac i THEN
+ Object_Logic.full_atomize_tac i THEN
simp_tac ss i
THEN (CONVERSION Thm.eta_long_conversion) i
THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
- THEN ObjectLogic.full_atomize_tac i
- THEN CONVERSION (ObjectLogic.judgment_conv (raw_dlo_conv ss instance)) i
+ THEN Object_Logic.full_atomize_tac i
+ THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
THEN (simp_tac ss i)));
end;
\ No newline at end of file
--- a/src/HOL/Tools/Qelim/presburger.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML Sun Mar 07 22:36:36 2010 +0100
@@ -166,13 +166,13 @@
val aprems = Arith_Data.get_arith_facts ctxt
in
Method.insert_tac aprems
- THEN_ALL_NEW ObjectLogic.full_atomize_tac
+ THEN_ALL_NEW Object_Logic.full_atomize_tac
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW simp_tac ss
THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
- THEN_ALL_NEW ObjectLogic.full_atomize_tac
+ THEN_ALL_NEW Object_Logic.full_atomize_tac
THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
- THEN_ALL_NEW ObjectLogic.full_atomize_tac
+ THEN_ALL_NEW Object_Logic.full_atomize_tac
THEN_ALL_NEW div_mod_tac ctxt
THEN_ALL_NEW splits_tac ctxt
THEN_ALL_NEW simp_tac ss
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Mar 07 22:36:36 2010 +0100
@@ -63,7 +63,7 @@
val qconst_bname = Binding.name lhs_str
val absrep_trm = absrep_fun AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
- val (_, prop') = LocalDefs.cert_def lthy prop
+ val (_, prop') = Local_Defs.cert_def lthy prop
val (_, newrhs) = Primitive_Defs.abs_def prop'
val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Mar 07 22:36:36 2010 +0100
@@ -48,7 +48,7 @@
fun atomize_thm thm =
let
val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
- val thm'' = ObjectLogic.atomize (cprop_of thm')
+ val thm'' = Object_Logic.atomize (cprop_of thm')
in
@{thm equal_elim_rule1} OF [thm'', thm']
end
@@ -616,7 +616,7 @@
(* the tactic leaves three subgoals to be proved *)
fun procedure_tac ctxt rthm =
- ObjectLogic.full_atomize_tac
+ Object_Logic.full_atomize_tac
THEN' gen_frees_tac ctxt
THEN' SUBGOAL (fn (goal, i) =>
let
--- a/src/HOL/Tools/TFL/post.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML Sun Mar 07 22:36:36 2010 +0100
@@ -151,9 +151,9 @@
{f = f, R = R, rules = rules,
full_pats_TCs = full_pats_TCs,
TCs = TCs}
- val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
+ val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
(R.CONJUNCTS rules)
- in {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
+ in {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
rules = ListPair.zip(rules', rows),
tcs = (termination_goals rules') @ tcs}
end
@@ -180,7 +180,7 @@
| solve_eq (th, [a], i) = [(a, i)]
| solve_eq (th, splitths as (_ :: _), i) =
(writeln "Proving unsplit equation...";
- [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
+ [((Drule.export_without_context o Object_Logic.rulify_no_asm)
(CaseSplit.splitto splitths th), i)])
(* if there's an error, pretend nothing happened with this definition
We should probably print something out so that the user knows...? *)
--- a/src/HOL/Tools/arith_data.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/arith_data.ML Sun Mar 07 22:36:36 2010 +0100
@@ -55,7 +55,7 @@
let
val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
fun invoke (_, (name, tac)) k st = (if verbose
- then warning ("Trying " ^ name ^ "...") else ();
+ then priority ("Trying " ^ name ^ "...") else ();
tac verbose ctxt k st);
in FIRST' (map invoke (rev tactics)) end;
--- a/src/HOL/Tools/choice_specification.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML Sun Mar 07 22:36:36 2010 +0100
@@ -111,7 +111,7 @@
| myfoldr f [] = error "Choice_Specification.process_spec internal error"
val rew_imps = alt_props |>
- map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
+ map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
val props' = rew_imps |>
map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
--- a/src/HOL/Tools/hologic.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/hologic.ML Sun Mar 07 22:36:36 2010 +0100
@@ -190,14 +190,14 @@
fun conj_intr thP thQ =
let
- val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ)
+ val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
fun conj_elim thPQ =
let
- val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ))
+ val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
--- a/src/HOL/Tools/inductive.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Mar 07 22:36:36 2010 +0100
@@ -788,7 +788,7 @@
else if coind then
singleton (ProofContext.export
(snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
- (rotate_prems ~1 (ObjectLogic.rulify
+ (rotate_prems ~1 (Object_Logic.rulify
(fold_rule rec_preds_defs
(rewrite_rule simp_thms'''
(mono RS (fp_def RS @{thm def_coinduct}))))))
@@ -832,7 +832,7 @@
let
val _ = Binding.is_empty name andalso null atts orelse
error "Abbreviations may not have names or attributes";
- val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
+ val ((x, T), rhs) = Local_Defs.abs_def (snd (Local_Defs.cert_def ctxt1 t));
val var =
(case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
NONE => error ("Undeclared head of abbreviation " ^ quote x)
@@ -854,8 +854,8 @@
val ps = map Free pnames;
val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
- val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
- val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
+ val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
+ val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
fun close_rule r = list_all_free (rev (fold_aterms
--- a/src/HOL/Tools/inductive_realizer.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Mar 07 22:36:36 2010 +0100
@@ -395,7 +395,7 @@
[rtac (#raw_induct ind_info) 1,
rewrite_goals_tac rews,
REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
- [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
+ [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
(Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
@@ -454,7 +454,7 @@
etac elimR 1,
ALLGOALS (asm_simp_tac HOL_basic_ss),
rewrite_goals_tac rews,
- REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
+ REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
(name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
--- a/src/HOL/Tools/lin_arith.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Mar 07 22:36:36 2010 +0100
@@ -901,7 +901,7 @@
in
fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
- ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
+ Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
val tac = gen_tac true;
--- a/src/HOL/Tools/meson.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/meson.ML Sun Mar 07 22:36:36 2010 +0100
@@ -587,7 +587,7 @@
Function mkcl converts theorems to clauses.*)
fun MESON mkcl cltac ctxt i st =
SELECT_GOAL
- (EVERY [ObjectLogic.atomize_prems_tac 1,
+ (EVERY [Object_Logic.atomize_prems_tac 1,
rtac ccontr 1,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
EVERY1 [skolemize_prems_tac ctxt negs,
--- a/src/HOL/Tools/record.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/record.ML Sun Mar 07 22:36:36 2010 +0100
@@ -2214,7 +2214,7 @@
[(cterm_of defs_thy Pvar, cterm_of defs_thy
(lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
induct_scheme;
- in ObjectLogic.rulify (mp OF [ind, refl]) end;
+ in Object_Logic.rulify (mp OF [ind, refl]) end;
val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
--- a/src/HOL/Tools/res_axioms.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sun Mar 07 22:36:36 2010 +0100
@@ -276,7 +276,7 @@
let val th1 = th |> transform_elim |> zero_var_indexes
val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
val th3 = th2
- |> Conv.fconv_rule ObjectLogic.atomize
+ |> Conv.fconv_rule Object_Logic.atomize
|> Meson.make_nnf ctxt |> strip_lambdas ~1
in (th3, ctxt) end;
@@ -475,7 +475,7 @@
(map Thm.term_of hyps)
val fixed = OldTerm.term_frees (concl_of st) @
fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
- in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
+ in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
fun meson_general_tac ctxt ths i st0 =
@@ -493,7 +493,7 @@
(*** Converting a subgoal into negated conjecture clauses. ***)
fun neg_skolemize_tac ctxt =
- EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
+ EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
--- a/src/HOL/Tools/sat_funcs.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/sat_funcs.ML Sun Mar 07 22:36:36 2010 +0100
@@ -434,7 +434,7 @@
val pre_cnf_tac =
rtac ccontr THEN'
- ObjectLogic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac THEN'
CONVERSION Drule.beta_eta_conversion;
(* ------------------------------------------------------------------------- *)
--- a/src/HOL/Tools/typedef.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOL/Tools/typedef.ML Sun Mar 07 22:36:36 2010 +0100
@@ -130,7 +130,7 @@
in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
fun typedef_result inhabited =
- ObjectLogic.typedecl (tname, vs, mx)
+ Typedecl.typedecl (tname, vs, mx)
#> snd
#> Sign.add_consts_i
[(Rep_name, newT --> oldT, NoSyn),
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Mar 07 22:36:36 2010 +0100
@@ -174,7 +174,7 @@
(K (beta_tac 1));
val tuple_unfold_thm =
(@{thm def_cont_fix_eq} OF [tuple_fixdef_thm, cont_thm])
- |> LocalDefs.unfold (ProofContext.init thy) @{thms split_conv};
+ |> Local_Defs.unfold (ProofContext.init thy) @{thms split_conv};
fun mk_unfold_thms [] thm = []
| mk_unfold_thms (n::[]) thm = [(n, thm)]
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sun Mar 07 22:36:36 2010 +0100
@@ -168,13 +168,17 @@
val take_rews = ax_take_0 :: ax_take_strict :: take_apps;
end;
+val case_ns =
+ "bottom" :: map (fn (b,_,_) => Binding.name_of b) (snd dom_eqn);
+
in
thy
|> Sign.add_path (Long_Name.base_name dname)
|> snd o PureThy.add_thmss [
((Binding.name "iso_rews" , iso_rews ), [Simplifier.simp_add]),
((Binding.name "exhaust" , [exhaust] ), []),
- ((Binding.name "casedist" , [casedist] ), [Induct.cases_type dname]),
+ ((Binding.name "casedist" , [casedist] ),
+ [Rule_Cases.case_names case_ns, Induct.cases_type dname]),
((Binding.name "when_rews" , when_rews ), [Simplifier.simp_add]),
((Binding.name "compacts" , con_compacts), [Simplifier.simp_add]),
((Binding.name "con_rews" , con_rews ),
@@ -422,8 +426,20 @@
| ERROR _ =>
(warning "Cannot prove induction rule"; ([], TrueI));
+val case_ns =
+ let
+ val bottoms =
+ if length dnames = 1 then ["bottom"] else
+ map (fn s => "bottom_" ^ Long_Name.base_name s) dnames;
+ fun one_eq bot (_,cons) =
+ bot :: map (fn (c,_) => Long_Name.base_name c) cons;
+ in flat (map2 one_eq bottoms eqs) end;
+
val inducts = Project_Rule.projections (ProofContext.init thy) ind;
-fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
+fun ind_rule (dname, rule) =
+ ((Binding.empty, [rule]),
+ [Rule_Cases.case_names case_ns, Induct.induct_type dname]);
+
val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
in thy |> Sign.add_path comp_dnam
--- a/src/HOLCF/Tools/fixrec.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/HOLCF/Tools/fixrec.ML Sun Mar 07 22:36:36 2010 +0100
@@ -146,9 +146,9 @@
val predicate = lambda_tuple lhss (list_comb (P, lhss));
val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
|> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
- |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
+ |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict};
val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
- |> LocalDefs.unfold lthy' @{thms split_conv};
+ |> Local_Defs.unfold lthy' @{thms split_conv};
fun unfolds [] thm = []
| unfolds (n::[]) thm = [(n, thm)]
| unfolds (n::ns) thm = let
--- a/src/Provers/blast.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Provers/blast.ML Sun Mar 07 22:36:36 2010 +0100
@@ -181,7 +181,7 @@
fun isGoal (Const ("*Goal*", _) $ _) = true
| isGoal _ = false;
-val TruepropC = ObjectLogic.judgment_name Data.thy;
+val TruepropC = Object_Logic.judgment_name Data.thy;
val TruepropT = Sign.the_const_type Data.thy TruepropC;
fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
@@ -1251,7 +1251,7 @@
fun timing_depth_tac start cs lim i st0 =
let val thy = Thm.theory_of_thm st0
val state = initialize thy
- val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
+ val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
val hyps = strip_imp_prems skoprem
and concl = strip_imp_concl skoprem
--- a/src/Provers/classical.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Provers/classical.ML Sun Mar 07 22:36:36 2010 +0100
@@ -153,7 +153,7 @@
*)
fun classical_rule rule =
- if ObjectLogic.is_elim rule then
+ if Object_Logic.is_elim rule then
let
val rule' = rule RS classical;
val concl' = Thm.concl_of rule';
@@ -173,7 +173,7 @@
else rule;
(*flatten nested meta connectives in prems*)
-val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
+val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
(*** Useful tactics for classical reasoning ***)
@@ -724,24 +724,24 @@
(*Dumb but fast*)
fun fast_tac cs =
- ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+ Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
(*Slower but smarter than fast_tac*)
fun best_tac cs =
- ObjectLogic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
(*even a bit smarter than best_tac*)
fun first_best_tac cs =
- ObjectLogic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
fun slow_tac cs =
- ObjectLogic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
fun slow_best_tac cs =
- ObjectLogic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
@@ -749,13 +749,13 @@
val weight_ASTAR = Unsynchronized.ref 5;
fun astar_tac cs =
- ObjectLogic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
(step_tac cs 1));
fun slow_astar_tac cs =
- ObjectLogic.atomize_prems_tac THEN'
+ Object_Logic.atomize_prems_tac THEN'
SELECT_GOAL
(ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
(slow_step_tac cs 1));
--- a/src/Provers/splitter.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Provers/splitter.ML Sun Mar 07 22:36:36 2010 +0100
@@ -46,14 +46,14 @@
struct
val Const (const_not, _) $ _ =
- ObjectLogic.drop_judgment Data.thy
+ Object_Logic.drop_judgment Data.thy
(#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
val Const (const_or , _) $ _ $ _ =
- ObjectLogic.drop_judgment Data.thy
+ Object_Logic.drop_judgment Data.thy
(#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
-val const_Trueprop = ObjectLogic.judgment_name Data.thy;
+val const_Trueprop = Object_Logic.judgment_name Data.thy;
fun split_format_err () = error "Wrong format for split rule";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sha1.ML Sun Mar 07 22:36:36 2010 +0100
@@ -0,0 +1,129 @@
+(* Title: Pure/General/sha1.ML
+ Author: Makarius
+
+Digesting strings according to SHA-1 (see RFC 3174) -- relatively slow
+version in pure ML.
+*)
+
+signature SHA1 =
+sig
+ val digest: string -> string
+end;
+
+structure SHA1: SHA1 =
+struct
+
+(* 32bit words *)
+
+infix 4 << >>;
+infix 3 andb;
+infix 2 orb xorb;
+
+val op << = Word32.<<;
+val op >> = Word32.>>;
+val op andb = Word32.andb;
+val op orb = Word32.orb;
+val op xorb = Word32.xorb;
+val notb = Word32.notb;
+
+fun rotate k w = w << k orb w >> (0w32 - k);
+
+
+(* hexadecimal words *)
+
+fun hex_digit (text, w: Word32.word) =
+ let
+ val d = Word32.toInt (w andb 0wxf);
+ val dig = if d < 10 then chr (ord "0" + d) else chr (ord "a" + d - 10);
+ in (dig ^ text, w >> 0w4) end;
+
+fun hex_word w = #1 (funpow 8 hex_digit ("", w));
+
+
+(* padding *)
+
+fun pack_bytes 0 n = ""
+ | pack_bytes k n = pack_bytes (k - 1) (n div 256) ^ chr (n mod 256);
+
+fun padded_text str =
+ let
+ val len = size str;
+ val padding = chr 128 ^ replicate_string (~ (len + 9) mod 64) (chr 0) ^ pack_bytes 8 (len * 8);
+ fun byte i = Char.ord (String.sub (if i < len then (str, i) else (padding, (i - len))));
+ fun word i =
+ Word32.fromInt (byte (4 * i)) << 0w24 orb
+ Word32.fromInt (byte (4 * i + 1)) << 0w16 orb
+ Word32.fromInt (byte (4 * i + 2)) << 0w8 orb
+ Word32.fromInt (byte (4 * i + 3));
+ in ((len + size padding) div 4, word) end;
+
+
+(* digest *)
+
+fun digest_word (i, w, {a, b, c, d, e}) =
+ let
+ val {f, k} =
+ if i < 20 then
+ {f = (b andb c) orb (notb b andb d),
+ k = 0wx5A827999}
+ else if i < 40 then
+ {f = b xorb c xorb d,
+ k = 0wx6ED9EBA1}
+ else if i < 60 then
+ {f = (b andb c) orb (b andb d) orb (c andb d),
+ k = 0wx8F1BBCDC}
+ else
+ {f = b xorb c xorb d,
+ k = 0wxCA62C1D6};
+ val op + = Word32.+;
+ in
+ {a = rotate 0w5 a + f + e + w + k,
+ b = a,
+ c = rotate 0w30 b,
+ d = c,
+ e = d}
+ end;
+
+fun digest str =
+ let
+ val (text_len, text) = padded_text str;
+
+ (*hash result -- 5 words*)
+ val hash_array : Word32.word Array.array =
+ Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0];
+ fun hash i = Array.sub (hash_array, i);
+ fun add_hash x i = Array.update (hash_array, i, hash i + x);
+
+ (*current chunk -- 80 words*)
+ val chunk_array = Array.array (80, 0w0: Word32.word);
+ fun chunk i = Array.sub (chunk_array, i);
+ fun init_chunk pos =
+ Array.modifyi (fn (i, _) =>
+ if i < 16 then text (pos + i)
+ else rotate 0w1 (chunk (i - 3) xorb chunk (i - 8) xorb chunk (i - 14) xorb chunk (i - 16)))
+ chunk_array;
+
+ fun digest_chunks pos =
+ if pos < text_len then
+ let
+ val _ = init_chunk pos;
+ val {a, b, c, d, e} = Array.foldli digest_word
+ {a = hash 0,
+ b = hash 1,
+ c = hash 2,
+ d = hash 3,
+ e = hash 4}
+ chunk_array;
+ val _ = add_hash a 0;
+ val _ = add_hash b 1;
+ val _ = add_hash c 2;
+ val _ = add_hash d 3;
+ val _ = add_hash e 4;
+ in digest_chunks (pos + 16) end
+ else ();
+ val _ = digest_chunks 0;
+
+ val hex = hex_word o hash;
+ in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/sha1_polyml.ML Sun Mar 07 22:36:36 2010 +0100
@@ -0,0 +1,29 @@
+(* Title: Pure/General/sha1_polyml.ML
+ Author: Sascha Boehme, TU Muenchen
+
+Digesting strings according to SHA-1 (see RFC 3174) -- based on an
+external implementation in C with a fallback to an internal
+implementation.
+*)
+
+structure SHA1: SHA1 =
+struct
+
+fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10);
+
+fun hex_string arr i =
+ let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr)
+ in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
+
+fun digest_external str =
+ let
+ val digest = CInterface.alloc 20 CInterface.Cchar;
+ val _ = CInterface.call3 (CInterface.get_sym "sha1" "sha1_buffer")
+ (CInterface.STRING, CInterface.INT, CInterface.POINTER)
+ CInterface.POINTER (str, size str, CInterface.address digest);
+ in fold (suffix o hex_string digest) (0 upto 19) "" end;
+
+fun digest str = digest_external str
+ handle CInterface.Foreign _ => SHA1.digest str;
+
+end;
--- a/src/Pure/IsaMakefile Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/IsaMakefile Sun Mar 07 22:36:36 2010 +0100
@@ -57,8 +57,9 @@
General/markup.ML General/name_space.ML General/ord_list.ML \
General/output.ML General/path.ML General/position.ML \
General/pretty.ML General/print_mode.ML General/properties.ML \
- General/queue.ML General/same.ML General/scan.ML General/secure.ML \
- General/seq.ML General/source.ML General/stack.ML General/symbol.ML \
+ General/queue.ML General/same.ML General/scan.ML General/sha1.ML \
+ General/sha1_polyml.ML General/secure.ML General/seq.ML \
+ General/source.ML General/stack.ML General/symbol.ML \
General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \
General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \
@@ -72,18 +73,19 @@
Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML \
Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML \
- Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \
- ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML \
- ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML \
- ML/ml_syntax.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
- ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML \
- Proof/extraction.ML Proof/proof_rewrite_rules.ML \
- Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
- ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
- ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML \
- ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML \
- ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML \
- ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML \
+ Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML \
+ Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML \
+ ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML \
+ ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML \
+ ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML \
+ ML-Systems/use_context.ML Proof/extraction.ML \
+ Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
+ Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML \
+ ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML \
+ ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML \
+ ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML \
+ ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML \
+ ProofGeneral/proof_general_emacs.ML \
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
--- a/src/Pure/Isar/attrib.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/attrib.ML Sun Mar 07 22:36:36 2010 +0100
@@ -245,14 +245,14 @@
fun unfolded_syntax rule =
thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
-val unfolded = unfolded_syntax LocalDefs.unfold;
-val folded = unfolded_syntax LocalDefs.fold;
+val unfolded = unfolded_syntax Local_Defs.unfold;
+val folded = unfolded_syntax Local_Defs.fold;
(* rule format *)
val rule_format = Args.mode "no_asm"
- >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format);
+ >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
val elim_format = Thm.rule_attribute (K Tactic.make_elim);
@@ -306,12 +306,12 @@
setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
setup (Binding.name "eta_long") (Scan.succeed eta_long)
"put theorem into eta long beta normal form" #>
- setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize)
+ setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
"declaration of atomize rule" #>
- setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
+ setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
"declaration of rulify rule" #>
setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
- setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del)
+ setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
"declaration of definitional transformations" #>
setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
"abstract over free variables of a definition"));
--- a/src/Pure/Isar/auto_bind.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/auto_bind.ML Sun Mar 07 22:36:36 2010 +0100
@@ -23,7 +23,7 @@
val thisN = "this";
val assmsN = "assms";
-fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
+fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
fun statement_binds thy name prop =
[((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
--- a/src/Pure/Isar/code.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/code.ML Sun Mar 07 22:36:36 2010 +0100
@@ -566,7 +566,7 @@
fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
-fun meta_rewrite thy = LocalDefs.meta_rewrite_rule (ProofContext.init thy);
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init thy);
fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
apfst (meta_rewrite thy);
@@ -810,7 +810,7 @@
val tyscm = typscheme_of_cert thy cert;
val thms = if null propers then [] else
cert_thm
- |> LocalDefs.expand [snd (get_head thy cert_thm)]
+ |> Local_Defs.expand [snd (get_head thy cert_thm)]
|> Thm.varifyT
|> Conjunction.elim_balanced (length propers);
in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
--- a/src/Pure/Isar/constdefs.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/constdefs.ML Sun Mar 07 22:36:36 2010 +0100
@@ -34,7 +34,7 @@
ProofContext.add_fixes [(x, T, mx)] #> snd #> pair (SOME x, mx)));
val prop = prep_prop var_ctxt raw_prop;
- val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
+ val (c, T) = #1 (Local_Defs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
val _ =
(case Option.map Name.of_binding d of
NONE => ()
--- a/src/Pure/Isar/element.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/element.ML Sun Mar 07 22:36:36 2010 +0100
@@ -223,12 +223,12 @@
val cert = Thm.cterm_of thy;
val th = MetaSimplifier.norm_hhf raw_th;
- val is_elim = ObjectLogic.is_elim th;
+ val is_elim = Object_Logic.is_elim th;
val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
val prop = Thm.prop_of th';
val (prems, concl) = Logic.strip_horn prop;
- val concl_term = ObjectLogic.drop_judgment thy concl;
+ val concl_term = Object_Logic.drop_judgment thy concl;
val fixes = fold_aterms (fn v as Free (x, T) =>
if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
@@ -499,11 +499,11 @@
let
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = LocalDefs.cert_def ctxt t (* FIXME adapt ps? *)
+ let val ((c, _), t') = Local_Defs.cert_def ctxt t (* FIXME adapt ps? *)
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
val (_, ctxt') = ctxt
|> fold Variable.auto_fixes (map #1 asms)
- |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
+ |> ProofContext.add_assms_i Local_Defs.def_export (map #2 asms);
in ctxt' end)
| init (Notes (kind, facts)) = (fn context =>
let
--- a/src/Pure/Isar/expression.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/expression.ML Sun Mar 07 22:36:36 2010 +0100
@@ -298,7 +298,7 @@
Assumes asms => Assumes (asms |> map (fn (a, propps) =>
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
| Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
+ let val ((c, _), t') = Local_Defs.cert_def ctxt (close_frees t)
in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end))
| e => e)
end;
@@ -513,8 +513,8 @@
fun bind_def ctxt eq (xs, env, eqs) =
let
- val _ = LocalDefs.cert_def ctxt eq;
- val ((y, T), b) = LocalDefs.abs_def eq;
+ val _ = Local_Defs.cert_def ctxt eq;
+ val ((y, T), b) = Local_Defs.abs_def eq;
val b' = norm_term env b;
fun err msg = error (msg ^ ": " ^ quote y);
in
@@ -595,11 +595,11 @@
fun atomize_spec thy ts =
let
val t = Logic.mk_conjunction_balanced ts;
- val body = ObjectLogic.atomize_term thy t;
+ val body = Object_Logic.atomize_term thy t;
val bodyT = Term.fastype_of body;
in
if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
- else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
+ else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
end;
(* achieve plain syntax for locale predicates (without "PROP") *)
@@ -634,7 +634,7 @@
val args = map Logic.mk_type extraTs @ map Free xs;
val head = Term.list_comb (Const (name, predT), args);
- val statement = ObjectLogic.ensure_propT thy head;
+ val statement = Object_Logic.ensure_propT thy head;
val ([pred_def], defs_thy) =
thy
@@ -808,8 +808,8 @@
val eqns = map (Morphism.thm (export' $> export)) raw_eqns;
val eqn_attrss = map2 (fn attrs => fn eqn =>
((apsnd o map) (Attrib.attribute_i thy) attrs, [([eqn], [])])) attrss eqns;
- fun meta_rewrite thy = map (LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
- Drule.abs_def) o maps snd;
+ fun meta_rewrite thy =
+ map (Local_Defs.meta_rewrite_rule (ProofContext.init thy) #> Drule.abs_def) o maps snd;
in
thy
|> PureThy.note_thmss Thm.lemmaK eqn_attrss
--- a/src/Pure/Isar/isar_syn.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Mar 07 22:36:36 2010 +0100
@@ -105,7 +105,7 @@
val _ =
OuterSyntax.command "typedecl" "type declaration" K.thy_decl
(P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
- Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
+ Toplevel.theory (Typedecl.typedecl (a, args, mx) #> snd)));
val _ =
OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
@@ -127,7 +127,7 @@
val _ =
OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
- (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
+ (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
val _ =
OuterSyntax.command "consts" "declare constants" K.thy_decl
--- a/src/Pure/Isar/local_defs.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/local_defs.ML Sun Mar 07 22:36:36 2010 +0100
@@ -34,7 +34,7 @@
((string * typ) * term) * (Proof.context -> thm -> thm)
end;
-structure LocalDefs: LOCAL_DEFS =
+structure Local_Defs: LOCAL_DEFS =
struct
(** primitive definitions **)
--- a/src/Pure/Isar/method.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/method.ML Sun Mar 07 22:36:36 2010 +0100
@@ -165,14 +165,14 @@
(* unfold/fold definitions *)
-fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.unfold_tac ctxt ths));
-fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (LocalDefs.fold_tac ctxt ths));
+fun unfold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.unfold_tac ctxt ths));
+fun fold_meth ths ctxt = SIMPLE_METHOD (CHANGED_PROP (Local_Defs.fold_tac ctxt ths));
(* atomize rule statements *)
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
- | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
+fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
+ | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
(* this -- resolve facts directly *)
--- a/src/Pure/Isar/object_logic.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/object_logic.ML Sun Mar 07 22:36:36 2010 +0100
@@ -8,7 +8,6 @@
sig
val get_base_sort: theory -> sort option
val add_base_sort: sort -> theory -> theory
- val typedecl: binding * string list * mixfix -> theory -> typ * theory
val add_judgment: binding * typ * mixfix -> theory -> theory
val add_judgment_cmd: binding * string * mixfix -> theory -> theory
val judgment_name: theory -> string
@@ -34,7 +33,7 @@
val rule_format_no_asm: attribute
end;
-structure ObjectLogic: OBJECT_LOGIC =
+structure Object_Logic: OBJECT_LOGIC =
struct
(** theory data **)
@@ -82,24 +81,6 @@
else (SOME S, judgment, atomize_rulify));
-(* typedecl *)
-
-fun typedecl (b, vs, mx) thy =
- let
- val base_sort = get_base_sort thy;
- val _ = has_duplicates (op =) vs andalso
- error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
- val name = Sign.full_name thy b;
- val n = length vs;
- val T = Type (name, map (fn v => TFree (v, [])) vs);
- in
- thy
- |> Sign.add_types [(b, n, mx)]
- |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
- |> pair T
- end;
-
-
(* add judgment *)
local
--- a/src/Pure/Isar/obtain.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/obtain.ML Sun Mar 07 22:36:36 2010 +0100
@@ -76,7 +76,7 @@
val thy = ProofContext.theory_of fix_ctxt;
val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
- val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
+ val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
error "Conclusion in obtained context must be object-logic judgment";
val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
@@ -100,7 +100,7 @@
fun bind_judgment ctxt name =
let
val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
- val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
+ val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
in ((v, t), ctxt') end;
val thatN = "that";
--- a/src/Pure/Isar/proof.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/proof.ML Sun Mar 07 22:36:36 2010 +0100
@@ -599,7 +599,7 @@
|>> map (fn (x, _, mx) => (x, mx))
|-> (fn vars =>
map_context_result (prep_binds false (map swap raw_rhss))
- #-> (fn rhss => map_context_result (LocalDefs.add_defs (vars ~~ (name_atts ~~ rhss)))))
+ #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
|-> (put_facts o SOME o map (#2 o #2))
end;
@@ -681,8 +681,8 @@
in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end));
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
-fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths);
-val unfold_goals = LocalDefs.unfold_goals;
+fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
+val unfold_goals = Local_Defs.unfold_goals;
in
--- a/src/Pure/Isar/rule_cases.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/rule_cases.ML Sun Mar 07 22:36:36 2010 +0100
@@ -110,7 +110,7 @@
val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
|> pairself (map (apsnd (maps Logic.dest_conjunctions)));
- val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
+ val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
val binds =
(case_conclN, concl) :: dest_binops concls concl
|> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
--- a/src/Pure/Isar/specification.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/specification.ML Sun Mar 07 22:36:36 2010 +0100
@@ -193,7 +193,7 @@
fun gen_def do_print prep (raw_var, raw_spec) lthy =
let
val (vars, [((raw_name, atts), prop)]) = fst (prep (the_list raw_var) [raw_spec] lthy);
- val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
+ val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
val var as (b, _) =
(case vars of
[] => (Binding.name x, NoSyn)
@@ -232,7 +232,7 @@
val ((vars, [(_, prop)]), _) =
prep (the_list raw_var) [(Attrib.empty_binding, raw_prop)]
(lthy |> ProofContext.set_mode ProofContext.mode_abbrev);
- val ((x, T), rhs) = LocalDefs.abs_def (#2 (LocalDefs.cert_def lthy prop));
+ val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy prop));
val var =
(case vars of
[] => (Binding.name x, NoSyn)
@@ -316,7 +316,7 @@
val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
- val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
+ val thesis = Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
fun assume_case ((name, (vars, _)), asms) ctxt' =
let
--- a/src/Pure/Isar/theory_target.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML Sun Mar 07 22:36:36 2010 +0100
@@ -121,7 +121,7 @@
(*export assumes/defines*)
val th = Goal.norm_result raw_th;
- val (defs, th') = LocalDefs.export ctxt thy_ctxt th;
+ val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
val concl_conv = MetaSimplifier.rewrite true defs (Thm.cprop_of th);
val assms = map (MetaSimplifier.rewrite_rule defs o Thm.assume) (Assumption.all_assms_of ctxt);
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
@@ -152,7 +152,7 @@
val result'' =
(case SINGLE (Seq.INTERVAL assm_tac 1 nprems) result' of
NONE => raise THM ("Failed to re-import result", 0, [result'])
- | SOME res => LocalDefs.trans_props ctxt [res, Thm.symmetric concl_conv])
+ | SOME res => Local_Defs.trans_props ctxt [res, Thm.symmetric concl_conv])
|> Goal.norm_result
|> PureThy.name_thm false false name;
@@ -235,7 +235,7 @@
lthy'
|> is_locale ? term_syntax ta false (locale_const ta Syntax.mode_default ((b, mx2), t))
|> is_class ? class_target ta (Class_Target.declare target ((b, mx1), t))
- |> LocalDefs.add_def ((b, NoSyn), t)
+ |> Local_Defs.add_def ((b, NoSyn), t)
end;
@@ -266,7 +266,7 @@
(Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
Sign.notation true prmode [(lhs, mx3)])))
|> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
- |> LocalDefs.fixed_abbrev ((b, NoSyn), t)
+ |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
end;
@@ -279,7 +279,7 @@
val name' = Thm.def_binding_optional b name;
val (rhs', rhs_conv) =
- LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
+ Local_Defs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
val xs = Variable.add_fixed (Local_Theory.target_of lthy) rhs' [];
val T = Term.fastype_of rhs;
@@ -296,7 +296,7 @@
if is_none (Class_Target.instantiation_param lthy b)
then Thm.add_def false false (name', Logic.mk_equals (lhs', rhs'))
else AxClass.define_overloaded name' (fst (dest_Const lhs'), rhs'));
- val def = LocalDefs.trans_terms lthy3
+ val def = Local_Defs.trans_terms lthy3
[(*c == global.c xs*) local_def,
(*global.c xs == rhs'*) global_def,
(*rhs' == rhs*) Thm.symmetric rhs_conv];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/typedecl.ML Sun Mar 07 22:36:36 2010 +0100
@@ -0,0 +1,31 @@
+(* Title: Pure/Isar/typedecl.ML
+ Author: Makarius
+
+Type declarations (within the object logic).
+*)
+
+signature TYPEDECL =
+sig
+ val typedecl: binding * string list * mixfix -> theory -> typ * theory
+end;
+
+structure Typedecl: TYPEDECL =
+struct
+
+fun typedecl (b, vs, mx) thy =
+ let
+ val base_sort = Object_Logic.get_base_sort thy;
+ val _ = has_duplicates (op =) vs andalso
+ error ("Duplicate parameters in type declaration " ^ quote (Binding.str_of b));
+ val name = Sign.full_name thy b;
+ val n = length vs;
+ val T = Type (name, map (fn v => TFree (v, [])) vs);
+ in
+ thy
+ |> Sign.add_types [(b, n, mx)]
+ |> (case base_sort of NONE => I | SOME S => AxClass.axiomatize_arity (name, replicate n S, S))
+ |> pair T
+ end;
+
+end;
+
--- a/src/Pure/ML-Systems/proper_int.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/ML-Systems/proper_int.ML Sun Mar 07 22:36:36 2010 +0100
@@ -165,6 +165,15 @@
val fromInt = Word.fromInt o dest_int;
end;
+structure Word32 =
+struct
+ open Word32;
+ val wordSize = mk_int Word32.wordSize;
+ val toInt = mk_int o Word32.toInt;
+ val toIntX = mk_int o Word32.toIntX;
+ val fromInt = Word32.fromInt o dest_int;
+end;
+
(* Real *)
--- a/src/Pure/ROOT.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/ROOT.ML Sun Mar 07 22:36:36 2010 +0100
@@ -52,6 +52,11 @@
use "General/xml.ML";
use "General/yxml.ML";
+use "General/sha1.ML";
+if String.isPrefix "polyml" ml_system
+then use "General/sha1_polyml.ML"
+else ();
+
(* concurrency within the ML runtime *)
@@ -218,6 +223,7 @@
use "Isar/spec_parse.ML";
use "Isar/spec_rules.ML";
use "Isar/specification.ML";
+use "Isar/typedecl.ML";
use "Isar/constdefs.ML";
(*toplevel transactions*)
--- a/src/Pure/Thy/term_style.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Thy/term_style.ML Sun Mar 07 22:36:36 2010 +0100
@@ -64,8 +64,8 @@
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
let
- val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
- (Logic.strip_imp_concl t)
+ val concl =
+ Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
in
case concl of (_ $ l $ r) => proj (l, r)
| _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
--- a/src/Pure/Tools/find_theorems.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sun Mar 07 22:36:36 2010 +0100
@@ -93,7 +93,7 @@
(* matching theorems *)
-fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
+fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
(*educated guesses on HOL*) (* FIXME broken *)
val boolT = Type ("bool", []);
@@ -110,13 +110,13 @@
fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
fun matches pat =
let
- val jpat = ObjectLogic.drop_judgment thy pat;
+ val jpat = Object_Logic.drop_judgment thy pat;
val c = Term.head_of jpat;
val pats =
if Term.is_Const c
then
if doiff andalso c = iff_const then
- (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
+ (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
|> filter (is_nontrivial thy)
else [pat]
else [];
--- a/src/Pure/old_goals.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Pure/old_goals.ML Sun Mar 07 22:36:36 2010 +0100
@@ -606,11 +606,11 @@
fun qed_goalw name thy rews goal tacsf =
ML_Context.ml_store_thm (name, prove_goalw thy rews goal tacsf);
fun qed_spec_mp name =
- ML_Context.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ()));
+ ML_Context.ml_store_thm (name, Object_Logic.rulify_no_asm (result ()));
fun qed_goal_spec_mp name thy s p =
- bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
+ bind_thm (name, Object_Logic.rulify_no_asm (prove_goal thy s p));
fun qed_goalw_spec_mp name thy defs s p =
- bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
+ bind_thm (name, Object_Logic.rulify_no_asm (prove_goalw thy defs s p));
end;
--- a/src/Tools/Code/code_preproc.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Sun Mar 07 22:36:36 2010 +0100
@@ -87,7 +87,7 @@
fun add_unfold_post raw_thm thy =
let
- val thm = LocalDefs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
+ val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm;
val thm_sym = Thm.symmetric thm;
in
thy |> map_pre_post (fn (pre, post) =>
--- a/src/Tools/atomize_elim.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Tools/atomize_elim.ML Sun Mar 07 22:36:36 2010 +0100
@@ -59,9 +59,9 @@
(EX x y z. ...) | ... | (EX a b c. ...)
*)
fun atomize_elim_conv ctxt ct =
- (forall_conv (K (prems_conv ~1 ObjectLogic.atomize_prems)) ctxt
+ (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
- then_conv (fn ct' => if can ObjectLogic.dest_judgment ct'
+ then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
then all_conv ct'
else raise CTERM ("atomize_elim", [ct', ct])))
ct
--- a/src/Tools/induct.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Tools/induct.ML Sun Mar 07 22:36:36 2010 +0100
@@ -137,7 +137,7 @@
Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
Conv.rewr_conv Drule.swap_prems_eq
-fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt);
+fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
fun find_eq ctxt t =
let
@@ -511,7 +511,7 @@
fun atomize_term thy =
MetaSimplifier.rewrite_term thy Data.atomize []
- #> ObjectLogic.drop_judgment thy;
+ #> Object_Logic.drop_judgment thy;
val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
@@ -683,14 +683,14 @@
fun add (SOME (_, (t, true))) ctxt = ((SOME t, []), ctxt)
| add (SOME (SOME x, (t, _))) ctxt =
let val ([(lhs, (_, th))], ctxt') =
- LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
+ Local_Defs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add (SOME (NONE, (t as Free _, _))) ctxt = ((SOME t, []), ctxt)
| add (SOME (NONE, (t, _))) ctxt =
let
val ([s], _) = Name.variants ["x"] (Variable.names_of ctxt);
val ([(lhs, (_, th))], ctxt') =
- LocalDefs.add_defs [((Binding.name s, NoSyn),
+ Local_Defs.add_defs [((Binding.name s, NoSyn),
(Thm.empty_binding, t))] ctxt
in ((SOME lhs, [th]), ctxt') end
| add NONE ctxt = ((NONE, []), ctxt);
--- a/src/Tools/induct_tacs.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Tools/induct_tacs.ML Sun Mar 07 22:36:36 2010 +0100
@@ -92,7 +92,7 @@
(_, rule) :: _ => rule
| [] => raise THM ("No induction rules", 0, [])));
- val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
+ val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
val _ = Method.trace ctxt [rule'];
val concls = Logic.dest_conjunctions (Thm.concl_of rule);
--- a/src/Tools/intuitionistic.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Tools/intuitionistic.ML Sun Mar 07 22:36:36 2010 +0100
@@ -89,7 +89,7 @@
Method.setup name
(Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
(fn opt_lim => fn ctxt =>
- SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
+ SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
"intuitionistic proof search";
end;
--- a/src/Tools/quickcheck.ML Sun Mar 07 08:46:12 2010 +0100
+++ b/src/Tools/quickcheck.ML Sun Mar 07 22:36:36 2010 +0100
@@ -199,7 +199,7 @@
val gi' = Logic.list_implies (if no_assms then [] else assms,
subst_bounds (frees, strip gi))
|> monomorphic_term thy insts default_T
- |> ObjectLogic.atomize_term thy;
+ |> Object_Logic.atomize_term thy;
in gen_test_term ctxt quiet report generator_name size iterations gi' end;
fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."