# HG changeset patch # User haftmann # Date 1267997796 -3600 # Node ID adf888e0fb1a9eca7339575b23802fd777e4a6a8 # Parent e0b2a6e773db7d45fd842b76c9c779b942477a1d# Parent 50655e2ebc8589f8b2c6fe64d775f23033c2f5fb merged diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Boogie/Tools/boogie_loader.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Complete_Lattice.thy --- 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 @@ "\UNIV = top" by (simp add: Inf_Sup Inf_empty [symmetric]) +lemma Sup_le_iff: "Sup A \ b \ (\a\A. a \ b)" + by (auto intro: Sup_least dest: Sup_upper) + +lemma le_Inf_iff: "b \ Inf A \ (\a\A. b \ a)" + by (auto intro: Inf_greatest dest: Inf_lower) + definition SUPR :: "'b set \ ('b \ 'a) \ 'a" where "SUPR A f = \ (f ` A)" @@ -126,6 +132,12 @@ lemma le_INFI: "(\i. i : A \ u \ M i) \ u \ (INF i:A. M i)" by (auto simp add: INFI_def intro: Inf_greatest) +lemma SUP_le_iff: "(SUP i:A. M i) \ u \ (\i \ A. M i \ u)" + unfolding SUPR_def by (auto simp add: Sup_le_iff) + +lemma le_INF_iff: "u \ (INF i:A. M i) \ (\i \ A. u \ M i)" + unfolding INFI_def by (auto simp add: le_Inf_iff) + lemma SUP_const[simp]: "A \ {} \ (SUP i:A. M) = M" by (auto intro: antisym SUP_leI le_SUPI) @@ -384,7 +396,7 @@ by blast lemma UN_subset_iff: "((\i\I. A i) \ B) = (\i\I. A i \ B)" - by blast + by (fact SUP_le_iff) lemma image_Union: "f ` \S = (\x\S. f ` x)" by blast @@ -591,7 +603,7 @@ by blast lemma INT_subset_iff: "(B \ (\i\I. A i)) = (\i\I. B \ A i)" - by blast + by (fact le_INF_iff) lemma INT_insert [simp]: "(\x \ insert a A. B x) = B a \ INTER A B" by blast diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- 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) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Decision_Procs/cooper_tac.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Decision_Procs/ferrack_tac.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Decision_Procs/mir_tac.ML --- 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 => diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/HOL.thy --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Int.thy --- 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 ("\") +lemma Ints_of_int [simp]: "of_int z \ \" + by (simp add: Ints_def) + +lemma Ints_of_nat [simp]: "of_nat n \ \" +apply (simp add: Ints_def) +apply (rule range_eqI) +apply (rule of_int_of_nat_eq [symmetric]) +done + lemma Ints_0 [simp]: "0 \ \" 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 \ \ \ b \ \ \ a - b \ \" +apply (auto simp add: Ints_def) +apply (rule range_eqI) +apply (rule of_int_diff [symmetric]) +done + lemma Ints_mult [simp]: "a \ \ \ b \ \ \ a * b \ \" apply (auto simp add: Ints_def) apply (rule range_eqI) apply (rule of_int_mult [symmetric]) done +lemma Ints_power [simp]: "a \ \ \ a ^ n \ \" +by (induct n) simp_all + lemma Ints_cases [cases set: Ints]: assumes "q \ \" obtains (of_int) z where "q = of_int z" @@ -1308,12 +1326,6 @@ end -lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a-b \ \" -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) \ Ints" unfolding number_of_eq Ints_def by simp +lemma Nats_number_of [simp]: + "Int.Pls \ w \ (number_of w :: 'a::number_ring) \ 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 \ Ints" shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))" diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Library/Efficient_Nat.thy --- 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, diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Library/normarith.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Library/reflection.ML --- 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') = diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Mutabelle/mutabelle.ML --- 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 = diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Mutabelle/mutabelle_extra.ML --- 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 = diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/NSA/transfer.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Nat.thy --- 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 \ \" + obtains (of_nat) n where "x = of_nat n" + unfolding Nats_def +proof - + from `x \ \` have "x \ 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 \ \ \ (\n. P (of_nat n)) \ P x" + by (rule Nats_cases) auto + end diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Nat_Numeral.thy --- 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 @@ "\ 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 \ x = 0 \ 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 \ x \ 0 \ y \ 0" -proof - - have "x * x + y * y \ 0 \ x \ 0 \ y \ 0" - by (simp add: sum_squares_eq_zero_iff) - then have "0 \ x * x + y * y \ x \ 0 \ y \ 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Nominal/nominal_datatype.ML --- 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, diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Parity.thy --- 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) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/RealDef.thy --- 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) \ 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) \ Nats" +unfolding real_of_nat_def by (rule of_nat_in_Nats) + +lemma Ints_real_of_nat [simp]: "real (n::nat) \ Ints" +unfolding real_of_nat_def by (rule Ints_of_nat) + subsection{* Rationals *} diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/RealPow.thy --- 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 \ r; r \ (1::real) |] ==> r ^ Suc n \ r" +(* TODO: no longer real-specific; rename and move elsewhere *) +lemma realpow_Suc_le_self: + fixes r :: "'a::linordered_semidom" + shows "[| 0 \ r; r \ 1 |] ==> r ^ Suc n \ 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 \ 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 \ 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 \ 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 \ x = 1 \ x = - 1" +proof - + have "x * x = 1 \ (x + 1) * (x - 1) = 0" + by (simp add: algebra_simps) + also have "\ \ x = 1 \ 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) \ 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) \ 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) \ (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 \ x" and ygt0: "0 \ y" and sq: "x^2 \ y^2" shows "x \ 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Rings.thy --- 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 \ a * a" + using linear [of 0 a] + by (auto simp add: mult_nonneg_nonneg mult_nonpos_nonpos) + +lemma not_square_less_zero [simp]: "\ (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 \ a * a" -by (simp add: zero_le_mult_iff linear) - -lemma not_square_less_zero [simp]: "\ (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 "\"} and equality.*} diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Datatype/datatype.ML --- 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, diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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 [] [] diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Datatype/datatype_realizer.ML --- 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)]); diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Function/induction_schema.ML --- 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) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Function/mutual.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Function/scnp_reconstruct.ML --- 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) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Function/termination.ML --- 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 = diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Groebner_Basis/groebner.ML --- 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)) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Groebner_Basis/normalizer_data.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Nitpick/minipick.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Nitpick/nitpick_model.ML --- 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) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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)) = diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Qelim/ferrante_rackoff.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Qelim/langford.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Qelim/presburger.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/TFL/post.ML --- 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...? *) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/arith_data.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/choice_specification.ML --- 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) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/hologic.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/inductive.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/inductive_realizer.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/lin_arith.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/meson.ML --- 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, diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/record.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/res_axioms.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/sat_funcs.ML --- 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; (* ------------------------------------------------------------------------- *) diff -r 50655e2ebc85 -r adf888e0fb1a src/HOL/Tools/typedef.ML --- 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), diff -r 50655e2ebc85 -r adf888e0fb1a src/HOLCF/Tools/Domain/domain_isomorphism.ML --- 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)] diff -r 50655e2ebc85 -r adf888e0fb1a src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/HOLCF/Tools/fixrec.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Provers/blast.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Provers/classical.ML --- 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)); diff -r 50655e2ebc85 -r adf888e0fb1a src/Provers/splitter.ML --- 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"; diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/General/sha1.ML --- /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; diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/General/sha1_polyml.ML --- /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; diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/IsaMakefile --- 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 \ diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/attrib.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")); diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/auto_bind.ML --- 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)))]; diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/code.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/constdefs.ML --- 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 => () diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/element.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/expression.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/isar_syn.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/local_defs.ML --- 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 **) diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/method.ML --- 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 *) diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/object_logic.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/obtain.ML --- 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"; diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/proof.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/rule_cases.ML --- 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))); diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/specification.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/theory_target.ML --- 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]; diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Isar/typedecl.ML --- /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; + diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/ML-Systems/proper_int.ML --- 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 *) diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/ROOT.ML --- 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*) diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Thy/term_style.ML --- 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) diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/Tools/find_theorems.ML --- 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 []; diff -r 50655e2ebc85 -r adf888e0fb1a src/Pure/old_goals.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/Tools/Code/code_preproc.ML --- 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) => diff -r 50655e2ebc85 -r adf888e0fb1a src/Tools/atomize_elim.ML --- 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 diff -r 50655e2ebc85 -r adf888e0fb1a src/Tools/induct.ML --- 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); diff -r 50655e2ebc85 -r adf888e0fb1a src/Tools/induct_tacs.ML --- 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); diff -r 50655e2ebc85 -r adf888e0fb1a src/Tools/intuitionistic.ML --- 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; diff -r 50655e2ebc85 -r adf888e0fb1a src/Tools/quickcheck.ML --- 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."