--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/PLATFORMS Sun Mar 07 10:03:16 2010 -0800
@@ -0,0 +1,81 @@
+Some notes on platform support of Isabelle
+==========================================
+
+Preamble
+--------
+
+The general programming model is that of a stylized ML + Scala + POSIX
+environment, with hardly any system specific code in user-space tools
+and packages.
+
+The basic Isabelle system infrastructure provides some facilities to
+make this work, e.g. see the ML structures File and Path, or functions
+like bash_output. The settings environment also provides some means
+for portability, e.g. jvm_path to hold up the impression that even
+Java on Windows/Cygwin adheres to Isabelle/POSIX standards.
+
+When producing add-on tools, it is important to stay within this clean
+room of Isabelle, and refrain from overly ambitious system hacking.
+
+
+Supported platforms
+-------------------
+
+The following hardware and operating system platforms are officially
+supported by the Isabelle distribution (and bundled tools):
+
+ x86-linux
+ x86-darwin
+ x86-cygwin
+ x86_64-linux
+ x86_64-darwin
+
+As of Cygwin 1.7 there is only a 32 bit version of that platform. The
+other 64 bit platforms become more and more important for power users
+and always need to be taken into account when testing tools.
+
+All of the above platforms are 100% supported -- end-users should not
+have to care about the differences at all. There are also some
+secondary platforms where Poly/ML also happens to work:
+
+ ppc-darwin
+ sparc-solaris
+ x86-solaris
+ x86-bsd
+
+There is no guarantee that Isabelle add-ons work on these fringe
+platforms. Even Isabelle/Scala already fails on ppc-darwin due to
+lack of JVM 1.6 support on that platform.
+
+
+Dependable system tools
+-----------------------
+
+The following portable system tools can be taken for granted:
+
+ * GNU bash as uniform shell on all platforms. Note that the POSIX
+ "standard" shell /bin/sh is *not* appropriate, because there are
+ too many different implementations of it.
+
+ * Perl as largely portable system programming language. In some
+ situations Python may as an alternative, but it usually performs
+ not as well in addressing various delicate details of basic
+ operating system concepts (processes, signals, sockets etc.).
+
+ * Scala with Java Runtime 1.6. The Isabelle/Pure.jar library irons
+ out many oddities and portability problems of the Java platform.
+
+
+Known problems
+--------------
+
+* Mac OS: If MacPorts is installed and its version of Perl takes
+ precedence over /usr/bin/perl in the PATH, then the end-user needs
+ to take care of installing add-on modules, e.g. HTTP support. Such
+ add-ons are usually included in Apple's /usr/bin/perl by default.
+
+* The Java runtime has its own idea about the underlying platform,
+ e.g. on 64 bit machine Isabelle/ML could be x86-linux, but the JVM
+ could be x86_64-linux. This affects Java native libraries in
+ particular -- which are very hard to support in a platform
+ independent manner, and should be avoided in the first place.
--- a/NEWS Sun Mar 07 09:57:30 2010 -0800
+++ b/NEWS Sun Mar 07 10:03:16 2010 -0800
@@ -58,6 +58,9 @@
* Type constructors admit general mixfix syntax, not just infix.
+* Use of cumulative prems via "!" in some proof methods has been
+discontinued (legacy feature).
+
*** Pure ***
--- a/doc-src/IsarRef/Thy/Generic.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/doc-src/IsarRef/Thy/Generic.thy Sun Mar 07 10:03:16 2010 -0800
@@ -364,7 +364,7 @@
\indexouternonterm{simpmod}
\begin{rail}
- ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
+ ('simp' | 'simp\_all') opt? (simpmod *)
;
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
@@ -404,9 +404,7 @@
proofs this is usually quite well behaved in practice: just the
local premises of the actual goal are involved, additional facts may
be inserted via explicit forward-chaining (via @{command "then"},
- @{command "from"}, @{command "using"} etc.). The full context of
- premises is only included if the ``@{text "!"}'' (bang) argument is
- given, which should be used with some care, though.
+ @{command "from"}, @{command "using"} etc.).
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -603,9 +601,9 @@
\indexouternonterm{clamod}
\begin{rail}
- 'blast' ('!' ?) nat? (clamod *)
+ 'blast' nat? (clamod *)
;
- ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
+ ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
;
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
@@ -629,9 +627,7 @@
Any of the above methods support additional modifiers of the context
of classical rules. Their semantics is analogous to the attributes
given before. Facts provided by forward chaining are inserted into
- the goal before commencing proof search. The ``@{text
- "!"}''~argument causes the full context of assumptions to be
- included as well.
+ the goal before commencing proof search.
*}
@@ -649,9 +645,9 @@
\indexouternonterm{clasimpmod}
\begin{rail}
- 'auto' '!'? (nat nat)? (clasimpmod *)
+ 'auto' (nat nat)? (clasimpmod *)
;
- ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
+ ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
;
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
@@ -674,8 +670,7 @@
here.
Facts provided by forward chaining are inserted into the goal before
- doing the search. The ``@{text "!"}'' argument causes the full
- context of assumptions to be included as well.
+ doing the search.
\end{description}
*}
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Sun Mar 07 10:03:16 2010 -0800
@@ -795,16 +795,15 @@
\end{matharray}
\begin{rail}
- 'iprover' ('!' ?) ( rulemod * )
+ 'iprover' ( rulemod * )
;
\end{rail}
The @{method (HOL) iprover} method performs intuitionistic proof
search, depending on specifically declared rules from the context,
or given as explicit arguments. Chained facts are inserted into the
- goal before commencing proof search; ``@{method (HOL) iprover}@{text
- "!"}'' means to include the current @{fact prems} as well.
-
+ goal before commencing proof search.
+
Rules need to be classified as @{attribute (Pure) intro},
@{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
``@{text "!"}'' indicator refers to ``safe'' rules, which may be
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sun Mar 07 09:57:30 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sun Mar 07 10:03:16 2010 -0800
@@ -384,7 +384,7 @@
\indexouternonterm{simpmod}
\begin{rail}
- ('simp' | 'simp\_all') ('!' ?) opt? (simpmod *)
+ ('simp' | 'simp\_all') opt? (simpmod *)
;
opt: '(' ('no\_asm' | 'no\_asm\_simp' | 'no\_asm\_use' | 'asm\_lr' ) ')'
@@ -424,9 +424,7 @@
proofs this is usually quite well behaved in practice: just the
local premises of the actual goal are involved, additional facts may
be inserted via explicit forward-chaining (via \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}},
- \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.). The full context of
- premises is only included if the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' (bang) argument is
- given, which should be used with some care, though.
+ \hyperlink{command.from}{\mbox{\isa{\isacommand{from}}}}, \hyperlink{command.using}{\mbox{\isa{\isacommand{using}}}} etc.).
Additional Simplifier options may be specified to tune the behavior
further (mostly for unstructured scripts with many accidental local
@@ -626,9 +624,9 @@
\indexouternonterm{clamod}
\begin{rail}
- 'blast' ('!' ?) nat? (clamod *)
+ 'blast' nat? (clamod *)
;
- ('fast' | 'slow' | 'best' | 'safe' | 'clarify') ('!' ?) (clamod *)
+ ('fast' | 'slow' | 'best' | 'safe' | 'clarify') (clamod *)
;
clamod: (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' thmrefs
@@ -650,8 +648,7 @@
Any of the above methods support additional modifiers of the context
of classical rules. Their semantics is analogous to the attributes
given before. Facts provided by forward chaining are inserted into
- the goal before commencing proof search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}''~argument causes the full context of assumptions to be
- included as well.%
+ the goal before commencing proof search.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -671,9 +668,9 @@
\indexouternonterm{clasimpmod}
\begin{rail}
- 'auto' '!'? (nat nat)? (clasimpmod *)
+ 'auto' (nat nat)? (clasimpmod *)
;
- ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') '!'? (clasimpmod *)
+ ('force' | 'clarsimp' | 'fastsimp' | 'slowsimp' | 'bestsimp') (clasimpmod *)
;
clasimpmod: ('simp' (() | 'add' | 'del' | 'only') |
@@ -694,8 +691,7 @@
here.
Facts provided by forward chaining are inserted into the goal before
- doing the search. The ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' argument causes the full
- context of assumptions to be included as well.
+ doing the search.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sun Mar 07 09:57:30 2010 -0800
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Sun Mar 07 10:03:16 2010 -0800
@@ -805,15 +805,15 @@
\end{matharray}
\begin{rail}
- 'iprover' ('!' ?) ( rulemod * )
+ 'iprover' ( rulemod * )
;
\end{rail}
The \hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}} method performs intuitionistic proof
search, depending on specifically declared rules from the context,
or given as explicit arguments. Chained facts are inserted into the
- goal before commencing proof search; ``\hyperlink{method.HOL.iprover}{\mbox{\isa{iprover}}}\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' means to include the current \hyperlink{fact.prems}{\mbox{\isa{prems}}} as well.
-
+ goal before commencing proof search.
+
Rules need to be classified as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}},
\hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, or \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}}; here the
``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' indicator refers to ``safe'' rules, which may be
--- a/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/HOL.thy Sun Mar 07 10:03:16 2010 -0800
@@ -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/Induct/Comb.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Induct/Comb.thy Sun Mar 07 10:03:16 2010 -0800
@@ -1,5 +1,4 @@
(* Title: HOL/Induct/Comb.thy
- ID: $Id$
Author: Lawrence C Paulson
Copyright 1996 University of Cambridge
*)
@@ -134,21 +133,10 @@
apply (blast intro: rtrancl_trans)+
done
-(** Counterexample to the diamond property for -1-> **)
-
-lemma KIII_contract1: "K##I##(I##I) -1-> I"
-by (rule contract.K)
-
-lemma KIII_contract2: "K##I##(I##I) -1-> K##I##((K##I)##(K##I))"
-by (unfold I_def, blast)
-
-lemma KIII_contract3: "K##I##((K##I)##(K##I)) -1-> I"
-by blast
+text {*Counterexample to the diamond property for @{term "x -1-> y"}*}
lemma not_diamond_contract: "~ diamond(contract)"
-apply (unfold diamond_def)
-apply (best intro: KIII_contract1 KIII_contract2 KIII_contract3)
-done
+by (unfold diamond_def, metis S_contractE contract.K)
subsection {* Results about Parallel Contraction *}
@@ -190,10 +178,7 @@
*}
lemma contract_subset_parcontract: "contract <= parcontract"
-apply (rule subsetI)
-apply (simp only: split_tupled_all)
-apply (erule contract.induct, blast+)
-done
+by (auto, erule contract.induct, blast+)
text{*Reductions: simply throw together reflexivity, transitivity and
the one-step reductions*}
@@ -205,16 +190,12 @@
by (unfold I_def, blast)
lemma parcontract_subset_reduce: "parcontract <= contract^*"
-apply (rule subsetI)
-apply (simp only: split_tupled_all)
-apply (erule parcontract.induct, blast+)
-done
+by (auto, erule parcontract.induct, blast+)
lemma reduce_eq_parreduce: "contract^* = parcontract^*"
-by (rule equalityI contract_subset_parcontract [THEN rtrancl_mono]
- parcontract_subset_reduce [THEN rtrancl_subset_rtrancl])+
+by (metis contract_subset_parcontract parcontract_subset_reduce rtrancl_subset)
-lemma diamond_reduce: "diamond(contract^*)"
+theorem diamond_reduce: "diamond(contract^*)"
by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract)
end
--- a/src/HOL/IsaMakefile Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/IsaMakefile Sun Mar 07 10:03:16 2010 -0800
@@ -401,7 +401,7 @@
Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML \
Library/Library/document/root.tex Library/Library/document/root.bib \
Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
- Library/Product_ord.thy Library/Char_nat.thy \
+ Library/Product_ord.thy Library/Char_nat.thy Library/Table.thy \
Library/Sublist_Order.thy Library/List_lexord.thy \
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Formal_Power_Series.thy Library/Binomial.thy \
--- a/src/HOL/Library/Efficient_Nat.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Library/Efficient_Nat.thy Sun Mar 07 10:03:16 2010 -0800
@@ -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/Library.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Library/Library.thy Sun Mar 07 10:03:16 2010 -0800
@@ -58,6 +58,7 @@
SML_Quickcheck
State_Monad
Sum_Of_Squares
+ Table
Transitive_Closure_Table
Univ_Poly
While_Combinator
--- a/src/HOL/Library/RBT.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Library/RBT.thy Sun Mar 07 10:03:16 2010 -0800
@@ -151,8 +151,8 @@
lemma lookup_Empty: "lookup Empty = empty"
by (rule ext) simp
-lemma lookup_map_of_entries:
- "sorted t \<Longrightarrow> lookup t = map_of (entries t)"
+lemma map_of_entries:
+ "sorted t \<Longrightarrow> map_of (entries t) = lookup t"
proof (induct t)
case Empty thus ?case by (simp add: lookup_Empty)
next
@@ -213,11 +213,11 @@
} ultimately show ?thesis using less_linear by blast
qed
also from Branch have "lookup t2 ++ [k \<mapsto> v] ++ lookup t1 = map_of (entries (Branch c t1 k v t2))" by simp
- finally show ?case .
+ finally show ?case by simp
qed
lemma lookup_in_tree: "sorted t \<Longrightarrow> lookup t k = Some v \<longleftrightarrow> (k, v) \<in> set (entries t)"
- by (simp_all add: lookup_map_of_entries distinct_entries)
+ by (simp add: map_of_entries [symmetric] distinct_entries)
lemma set_entries_inject:
assumes sorted: "sorted t1" "sorted t2"
@@ -236,7 +236,7 @@
shows "entries t1 = entries t2"
proof -
from sorted lookup have "map_of (entries t1) = map_of (entries t2)"
- by (simp add: lookup_map_of_entries)
+ by (simp add: map_of_entries)
with sorted have "set (entries t1) = set (entries t2)"
by (simp add: map_of_inject_set distinct_entries)
with sorted show ?thesis by (simp add: set_entries_inject)
@@ -245,7 +245,7 @@
lemma entries_lookup:
assumes "sorted t1" "sorted t2"
shows "entries t1 = entries t2 \<longleftrightarrow> lookup t1 = lookup t2"
- using assms by (auto intro: entries_eqI simp add: lookup_map_of_entries)
+ using assms by (auto intro: entries_eqI simp add: map_of_entries [symmetric])
lemma lookup_from_in_tree:
assumes "sorted t1" "sorted t2"
@@ -1013,11 +1013,9 @@
theorem map_entry_is_rbt [simp]: "is_rbt (map_entry k f t) = is_rbt t"
unfolding is_rbt_def by (simp add: map_entry_inv2 map_entry_color_of map_entry_sorted map_entry_inv1 )
-theorem map_entry_map [simp]:
- "lookup (map_entry k f t) x =
- (if x = k then case lookup t x of None \<Rightarrow> None | Some y \<Rightarrow> Some (f y)
- else lookup t x)"
- by (induct t arbitrary: x) (auto split:option.splits)
+theorem lookup_map_entry:
+ "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
+ by (induct t) (auto split: option.splits simp add: expand_fun_eq)
subsection {* Mapping all entries *}
@@ -1040,8 +1038,8 @@
theorem map_is_rbt [simp]: "is_rbt (map f t) = is_rbt t"
unfolding is_rbt_def by (simp add: map_inv1 map_inv2 map_sorted map_color_of)
-theorem lookup_map [simp]: "lookup (map f t) x = Option.map (f x) (lookup t x)"
-by (induct t) auto
+theorem lookup_map: "lookup (map f t) x = Option.map (f x) (lookup t x)"
+ by (induct t) auto
subsection {* Folding over entries *}
@@ -1057,7 +1055,7 @@
subsection {* Bulkloading a tree *}
-definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where (*FIXME move*)
+definition bulkload :: "('a \<times> 'b) list \<Rightarrow> ('a\<Colon>linorder, 'b) rbt" where
"bulkload xs = foldr (\<lambda>(k, v). RBT.insert k v) xs RBT.Empty"
lemma bulkload_is_rbt [simp, intro]:
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Table.thy Sun Mar 07 10:03:16 2010 -0800
@@ -0,0 +1,139 @@
+(* Author: Florian Haftmann, TU Muenchen *)
+
+header {* Tables: finite mappings implemented by red-black trees *}
+
+theory Table
+imports Main RBT
+begin
+
+subsection {* Type definition *}
+
+typedef (open) ('a, 'b) table = "{t :: ('a\<Colon>linorder, 'b) rbt. is_rbt t}"
+ morphisms tree_of Table
+proof -
+ have "RBT.Empty \<in> ?table" by simp
+ then show ?thesis ..
+qed
+
+lemma is_rbt_tree_of [simp, intro]:
+ "is_rbt (tree_of t)"
+ using tree_of [of t] by simp
+
+lemma table_eq:
+ "t1 = t2 \<longleftrightarrow> tree_of t1 = tree_of t2"
+ by (simp add: tree_of_inject)
+
+code_abstype Table tree_of
+ by (simp add: tree_of_inverse)
+
+
+subsection {* Primitive operations *}
+
+definition lookup :: "('a\<Colon>linorder, 'b) table \<Rightarrow> 'a \<rightharpoonup> 'b" where
+ [code]: "lookup t = RBT.lookup (tree_of t)"
+
+definition empty :: "('a\<Colon>linorder, 'b) table" where
+ "empty = Table RBT.Empty"
+
+lemma tree_of_empty [code abstract]:
+ "tree_of empty = RBT.Empty"
+ by (simp add: empty_def Table_inverse)
+
+definition update :: "'a\<Colon>linorder \<Rightarrow> 'b \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "update k v t = Table (RBT.insert k v (tree_of t))"
+
+lemma tree_of_update [code abstract]:
+ "tree_of (update k v t) = RBT.insert k v (tree_of t)"
+ by (simp add: update_def Table_inverse)
+
+definition delete :: "'a\<Colon>linorder \<Rightarrow> ('a, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "delete k t = Table (RBT.delete k (tree_of t))"
+
+lemma tree_of_delete [code abstract]:
+ "tree_of (delete k t) = RBT.delete k (tree_of t)"
+ by (simp add: delete_def Table_inverse)
+
+definition entries :: "('a\<Colon>linorder, 'b) table \<Rightarrow> ('a \<times> 'b) list" where
+ [code]: "entries t = RBT.entries (tree_of t)"
+
+definition bulkload :: "('a\<Colon>linorder \<times> 'b) list \<Rightarrow> ('a, 'b) table" where
+ "bulkload xs = Table (RBT.bulkload xs)"
+
+lemma tree_of_bulkload [code abstract]:
+ "tree_of (bulkload xs) = RBT.bulkload xs"
+ by (simp add: bulkload_def Table_inverse)
+
+definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "map_entry k f t = Table (RBT.map_entry k f (tree_of t))"
+
+lemma tree_of_map_entry [code abstract]:
+ "tree_of (map_entry k f t) = RBT.map_entry k f (tree_of t)"
+ by (simp add: map_entry_def Table_inverse)
+
+definition map :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> ('a, 'b) table" where
+ "map f t = Table (RBT.map f (tree_of t))"
+
+lemma tree_of_map [code abstract]:
+ "tree_of (map f t) = RBT.map f (tree_of t)"
+ by (simp add: map_def Table_inverse)
+
+definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a\<Colon>linorder, 'b) table \<Rightarrow> 'c \<Rightarrow> 'c" where
+ [code]: "fold f t = RBT.fold f (tree_of t)"
+
+
+subsection {* Derived operations *}
+
+definition is_empty :: "('a\<Colon>linorder, 'b) table \<Rightarrow> bool" where
+ [code]: "is_empty t = (case tree_of t of RBT.Empty \<Rightarrow> True | _ \<Rightarrow> False)"
+
+
+subsection {* Abstract lookup properties *}
+
+lemma lookup_Table:
+ "is_rbt t \<Longrightarrow> lookup (Table t) = RBT.lookup t"
+ by (simp add: lookup_def Table_inverse)
+
+lemma lookup_tree_of:
+ "RBT.lookup (tree_of t) = lookup t"
+ by (simp add: lookup_def)
+
+lemma entries_tree_of:
+ "RBT.entries (tree_of t) = entries t"
+ by (simp add: entries_def)
+
+lemma lookup_empty [simp]:
+ "lookup empty = Map.empty"
+ by (simp add: empty_def lookup_Table expand_fun_eq)
+
+lemma lookup_update [simp]:
+ "lookup (update k v t) = (lookup t)(k \<mapsto> v)"
+ by (simp add: update_def lookup_Table lookup_insert lookup_tree_of)
+
+lemma lookup_delete [simp]:
+ "lookup (delete k t) = (lookup t)(k := None)"
+ by (simp add: delete_def lookup_Table lookup_delete lookup_tree_of restrict_complement_singleton_eq)
+
+lemma map_of_entries [simp]:
+ "map_of (entries t) = lookup t"
+ by (simp add: entries_def map_of_entries lookup_tree_of)
+
+lemma lookup_bulkload [simp]:
+ "lookup (bulkload xs) = map_of xs"
+ by (simp add: bulkload_def lookup_Table lookup_bulkload)
+
+lemma lookup_map_entry [simp]:
+ "lookup (map_entry k f t) = (lookup t)(k := Option.map f (lookup t k))"
+ by (simp add: map_entry_def lookup_Table lookup_map_entry lookup_tree_of)
+
+lemma lookup_map [simp]:
+ "lookup (map f t) k = Option.map (f k) (lookup t k)"
+ by (simp add: map_def lookup_Table lookup_map lookup_tree_of)
+
+lemma fold_fold:
+ "fold f t = (\<lambda>s. foldl (\<lambda>s (k, v). f k v s) s (entries t))"
+ by (simp add: fold_def expand_fun_eq RBT.fold_def entries_tree_of)
+
+hide (open) const tree_of lookup empty update delete
+ entries bulkload map_entry map fold
+
+end
--- a/src/HOL/Library/normarith.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Library/normarith.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Library/reflection.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/Map.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Map.thy Sun Mar 07 10:03:16 2010 -0800
@@ -398,6 +398,10 @@
"map_of (map (\<lambda>k. (k, f k)) ks) = (Some \<circ> f) |` set ks"
by (induct ks) (simp_all add: expand_fun_eq restrict_map_insert)
+lemma restrict_complement_singleton_eq:
+ "f |` (- {x}) = f(x := None)"
+ by (simp add: restrict_map_def expand_fun_eq)
+
subsection {* @{term [source] map_upds} *}
@@ -707,4 +711,3 @@
qed
end
-
--- a/src/HOL/Matrix/Matrix.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Matrix/Matrix.thy Sun Mar 07 10:03:16 2010 -0800
@@ -32,7 +32,7 @@
lemma nrows:
assumes hyp: "nrows A \<le> m"
- shows "(Rep_matrix A m n) = 0" (is ?concl)
+ shows "(Rep_matrix A m n) = 0"
proof cases
assume "nonzero_positions(Rep_matrix A) = {}"
then show "(Rep_matrix A m n) = 0" by (simp add: nonzero_positions_def)
@@ -157,13 +157,13 @@
ultimately show "False" using b by (simp)
qed
-lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
+lemma less_ncols: "(n < ncols A) = (? j i. n <= i & (Rep_matrix A j i) \<noteq> 0)"
proof -
have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
- show ?concl by (simp add: a ncols_le)
+ show ?thesis by (simp add: a ncols_le)
qed
-lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
+lemma le_ncols: "(n <= ncols A) = (\<forall> m. (\<forall> j i. m <= i \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)"
apply (auto)
apply (subgoal_tac "ncols A <= m")
apply (simp)
@@ -179,13 +179,13 @@
finally show "(nrows A <= n) = (! j i. n <= j \<longrightarrow> (Rep_matrix A j i) = 0)" by (auto)
qed
-lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)" (is ?concl)
+lemma less_nrows: "(m < nrows A) = (? j i. m <= j & (Rep_matrix A j i) \<noteq> 0)"
proof -
have a: "!! (a::nat) b. (a < b) = (~(b <= a))" by arith
- show ?concl by (simp add: a nrows_le)
+ show ?thesis by (simp add: a nrows_le)
qed
-lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)" (is ?concl)
+lemma le_nrows: "(n <= nrows A) = (\<forall> m. (\<forall> j i. m <= j \<longrightarrow> (Rep_matrix A j i) = 0) \<longrightarrow> n <= m)"
apply (auto)
apply (subgoal_tac "nrows A <= m")
apply (simp)
@@ -479,7 +479,7 @@
lemma foldseq_significant_positions:
assumes p: "! i. i <= N \<longrightarrow> S i = T i"
- shows "foldseq f S N = foldseq f T N" (is ?concl)
+ shows "foldseq f S N = foldseq f T N"
proof -
have "!! m . ! s t. (! i. i<=m \<longrightarrow> s i = t i) \<longrightarrow> foldseq f s m = foldseq f t m"
apply (induct_tac m)
@@ -496,10 +496,12 @@
have d:"!! s t. (\<forall>i\<le>n. s i = t i) \<Longrightarrow> foldseq f s n = foldseq f t n" by (simp add: a)
show "f (t 0) (foldseq f (\<lambda>k. s (Suc k)) n) = f (t 0) (foldseq f (\<lambda>k. t (Suc k)) n)" by (rule c, simp add: d b)
qed
- with p show ?concl by simp
+ with p show ?thesis by simp
qed
-lemma foldseq_tail: "M <= N \<Longrightarrow> foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M" (is "?p \<Longrightarrow> ?concl")
+lemma foldseq_tail:
+ assumes "M <= N"
+ shows "foldseq f S N = foldseq f (% k. (if k < M then (S k) else (foldseq f (% k. S(k+M)) (N-M)))) M"
proof -
have suc: "!! a b. \<lbrakk>a <= Suc b; a \<noteq> Suc b\<rbrakk> \<Longrightarrow> a <= b" by arith
have a:"!! a b c . a = b \<Longrightarrow> f c a = f c b" by blast
@@ -533,7 +535,7 @@
apply (rule a)
by (simp add: subc if_def)
qed
- then show "?p \<Longrightarrow> ?concl" by simp
+ then show ?thesis using assms by simp
qed
lemma foldseq_zerotail:
@@ -556,14 +558,13 @@
assumes "! x. f x 0 = x"
and "! i. n < i \<longrightarrow> s i = 0"
and nm: "n <= m"
- shows
- "foldseq f s n = foldseq f s m" (is ?concl)
+ shows "foldseq f s n = foldseq f s m"
proof -
- have "f 0 0 = 0" by (simp add: prems)
+ have "f 0 0 = 0" by (simp add: assms)
have b:"!! m n. n <= m \<Longrightarrow> m \<noteq> n \<Longrightarrow> ? k. m-n = Suc k" by arith
have c: "0 <= m" by simp
have d: "!! k. k \<noteq> 0 \<Longrightarrow> ? l. k = Suc l" by arith
- show ?concl
+ show ?thesis
apply (subst foldseq_tail[OF nm])
apply (rule foldseq_significant_positions)
apply (auto)
@@ -572,10 +573,11 @@
apply (drule b[OF nm])
apply (auto)
apply (case_tac "k=0")
- apply (simp add: prems)
+ apply (simp add: assms)
apply (drule d)
apply (auto)
- by (simp add: prems foldseq_zero)
+ apply (simp add: assms foldseq_zero)
+ done
qed
lemma foldseq_zerostart:
@@ -623,11 +625,11 @@
lemma foldseq_almostzero:
assumes f0x:"! x. f 0 x = x" and fx0: "! x. f x 0 = x" and s0:"! i. i \<noteq> j \<longrightarrow> s i = 0"
- shows "foldseq f s n = (if (j <= n) then (s j) else 0)" (is ?concl)
+ shows "foldseq f s n = (if (j <= n) then (s j) else 0)"
proof -
from s0 have a: "! i. i < j \<longrightarrow> s i = 0" by simp
from s0 have b: "! i. j < i \<longrightarrow> s i = 0" by simp
- show ?concl
+ show ?thesis
apply auto
apply (subst foldseq_zerotail2[of f, OF fx0, of j, OF b, of n, THEN sym])
apply simp
@@ -639,7 +641,7 @@
lemma foldseq_distr_unary:
assumes "!! a b. g (f a b) = f (g a) (g b)"
- shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n" (is ?concl)
+ shows "g(foldseq f s n) = foldseq f (% x. g(s x)) n"
proof -
have "! s. g(foldseq f s n) = foldseq f (% x. g(s x)) n"
apply (induct_tac n)
@@ -647,8 +649,8 @@
apply (simp)
apply (auto)
apply (drule_tac x="% k. s (Suc k)" in spec)
- by (simp add: prems)
- then show ?concl by simp
+ by (simp add: assms)
+ then show ?thesis by simp
qed
definition mult_matrix_n :: "nat \<Rightarrow> (('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> ('c \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> 'a matrix \<Rightarrow> 'b matrix \<Rightarrow> 'c matrix" where
@@ -658,21 +660,24 @@
"mult_matrix fmul fadd A B == mult_matrix_n (max (ncols A) (nrows B)) fmul fadd A B"
lemma mult_matrix_n:
- assumes prems: "ncols A \<le> n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
- shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B" (is ?concl)
+ assumes "ncols A \<le> n" (is ?An) "nrows B \<le> n" (is ?Bn) "fadd 0 0 = 0" "fmul 0 0 = 0"
+ shows c:"mult_matrix fmul fadd A B = mult_matrix_n n fmul fadd A B"
proof -
- show ?concl using prems
+ show ?thesis using assms
apply (simp add: mult_matrix_def mult_matrix_n_def)
apply (rule comb[of "Abs_matrix" "Abs_matrix"], simp, (rule ext)+)
- by (rule foldseq_zerotail, simp_all add: nrows_le ncols_le prems)
+ apply (rule foldseq_zerotail, simp_all add: nrows_le ncols_le assms)
+ done
qed
lemma mult_matrix_nm:
- assumes prems: "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
+ assumes "ncols A <= n" "nrows B <= n" "ncols A <= m" "nrows B <= m" "fadd 0 0 = 0" "fmul 0 0 = 0"
shows "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B"
proof -
- from prems have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B" by (simp add: mult_matrix_n)
- also from prems have "\<dots> = mult_matrix_n m fmul fadd A B" by (simp add: mult_matrix_n[THEN sym])
+ from assms have "mult_matrix_n n fmul fadd A B = mult_matrix fmul fadd A B"
+ by (simp add: mult_matrix_n)
+ also from assms have "\<dots> = mult_matrix_n m fmul fadd A B"
+ by (simp add: mult_matrix_n[THEN sym])
finally show "mult_matrix_n n fmul fadd A B = mult_matrix_n m fmul fadd A B" by simp
qed
@@ -689,23 +694,23 @@
lemma max2: "!! b x y. (b::nat) <= y \<Longrightarrow> b <= max x y" by (arith)
lemma r_distributive_matrix:
- assumes prems:
+ assumes
"r_distributive fmul fadd"
"associative fadd"
"commutative fadd"
"fadd 0 0 = 0"
"! a. fmul a 0 = 0"
"! a. fmul 0 a = 0"
- shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
+ shows "r_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"
proof -
- from prems show ?concl
+ from assms show ?thesis
apply (simp add: r_distributive_def mult_matrix_def, auto)
proof -
fix a::"'a matrix"
fix u::"'b matrix"
fix v::"'b matrix"
let ?mx = "max (ncols a) (max (nrows u) (nrows v))"
- from prems show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
+ from assms show "mult_matrix_n (max (ncols a) (nrows (combine_matrix fadd u v))) fmul fadd a (combine_matrix fadd u v) =
combine_matrix fadd (mult_matrix_n (max (ncols a) (nrows u)) fmul fadd a u) (mult_matrix_n (max (ncols a) (nrows v)) fmul fadd a v)"
apply (subst mult_matrix_nm[of _ _ _ ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
@@ -729,23 +734,23 @@
qed
lemma l_distributive_matrix:
- assumes prems:
+ assumes
"l_distributive fmul fadd"
"associative fadd"
"commutative fadd"
"fadd 0 0 = 0"
"! a. fmul a 0 = 0"
"! a. fmul 0 a = 0"
- shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)" (is ?concl)
+ shows "l_distributive (mult_matrix fmul fadd) (combine_matrix fadd)"
proof -
- from prems show ?concl
+ from assms show ?thesis
apply (simp add: l_distributive_def mult_matrix_def, auto)
proof -
fix a::"'b matrix"
fix u::"'a matrix"
fix v::"'a matrix"
let ?mx = "max (nrows a) (max (ncols u) (ncols v))"
- from prems show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
+ from assms show "mult_matrix_n (max (ncols (combine_matrix fadd u v)) (nrows a)) fmul fadd (combine_matrix fadd u v) a =
combine_matrix fadd (mult_matrix_n (max (ncols u) (nrows a)) fmul fadd u a) (mult_matrix_n (max (ncols v) (nrows a)) fmul fadd v a)"
apply (subst mult_matrix_nm[of v _ _ ?mx fadd fmul])
apply (simp add: max1 max2 combine_nrows combine_ncols)+
@@ -995,7 +1000,7 @@
by (simp add: nrows)
lemma mult_matrix_singleton_right[simp]:
- assumes prems:
+ assumes
"! x. fmul x 0 = 0"
"! x. fmul 0 x = 0"
"! x. fadd 0 x = x"
@@ -1004,11 +1009,11 @@
apply (simp add: mult_matrix_def)
apply (subst mult_matrix_nm[of _ _ _ "max (ncols A) (Suc j)"])
apply (auto)
- apply (simp add: prems)+
+ apply (simp add: assms)+
apply (simp add: mult_matrix_n_def apply_matrix_def apply_infmatrix_def)
apply (rule comb[of "Abs_matrix" "Abs_matrix"], auto, (rule ext)+)
apply (subst foldseq_almostzero[of _ j])
- apply (simp add: prems)+
+ apply (simp add: assms)+
apply (auto)
apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
done
@@ -1038,7 +1043,7 @@
let ?S = "singleton_matrix I 0 e"
let ?comp = "mult_matrix fmul fadd"
have d: "!!x f g. f = g \<Longrightarrow> f x = g x" by blast
- have e: "(% x. fmul x e) 0 = 0" by (simp add: prems)
+ have e: "(% x. fmul x e) 0 = 0" by (simp add: assms)
have "~(?comp A ?S = ?comp B ?S)"
apply (rule notI)
apply (simp add: fprems eprops)
@@ -1058,12 +1063,12 @@
assumes
"! a b c d. g(f a b) (f c d) = f (g a c) (g b d)"
shows
- "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m" (is ?concl)
+ "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
proof -
have forall:"!! P x. (! x. P x) \<Longrightarrow> P x" by auto
have tworows:"! A. foldmatrix f g A 1 n = foldmatrix_transposed g f (transpose_infmatrix A) n 1"
apply (induct n)
- apply (simp add: foldmatrix_def foldmatrix_transposed_def prems)+
+ apply (simp add: foldmatrix_def foldmatrix_transposed_def assms)+
apply (auto)
by (drule_tac x="(% j i. A j (Suc i))" in forall, simp)
show "foldmatrix f g A m n = foldmatrix_transposed g f (transpose_infmatrix A) n m"
@@ -1083,7 +1088,7 @@
shows
"foldseq g (% j. foldseq f (A j) n) m = foldseq f (% j. foldseq g ((transpose_infmatrix A) j) m) n"
apply (insert foldmatrix_transpose[of g f A m n])
- by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] prems)
+ by (simp add: foldmatrix_def foldmatrix_transposed_def foldseq_assoc[THEN sym] assms)
lemma mult_n_nrows:
assumes
@@ -1095,10 +1100,11 @@
apply (simp add: mult_matrix_n_def)
apply (subst RepAbs_matrix)
apply (rule_tac x="nrows A" in exI)
-apply (simp add: nrows prems foldseq_zero)
+apply (simp add: nrows assms foldseq_zero)
apply (rule_tac x="ncols B" in exI)
-apply (simp add: ncols prems foldseq_zero)
-by (simp add: nrows prems foldseq_zero)
+apply (simp add: ncols assms foldseq_zero)
+apply (simp add: nrows assms foldseq_zero)
+done
lemma mult_n_ncols:
assumes
@@ -1110,10 +1116,11 @@
apply (simp add: mult_matrix_n_def)
apply (subst RepAbs_matrix)
apply (rule_tac x="nrows A" in exI)
-apply (simp add: nrows prems foldseq_zero)
+apply (simp add: nrows assms foldseq_zero)
apply (rule_tac x="ncols B" in exI)
-apply (simp add: ncols prems foldseq_zero)
-by (simp add: ncols prems foldseq_zero)
+apply (simp add: ncols assms foldseq_zero)
+apply (simp add: ncols assms foldseq_zero)
+done
lemma mult_nrows:
assumes
@@ -1121,7 +1128,7 @@
"! a. fmul a 0 = 0"
"fadd 0 0 = 0"
shows "nrows (mult_matrix fmul fadd A B) \<le> nrows A"
-by (simp add: mult_matrix_def mult_n_nrows prems)
+by (simp add: mult_matrix_def mult_n_nrows assms)
lemma mult_ncols:
assumes
@@ -1129,7 +1136,7 @@
"! a. fmul a 0 = 0"
"fadd 0 0 = 0"
shows "ncols (mult_matrix fmul fadd A B) \<le> ncols B"
-by (simp add: mult_matrix_def mult_n_ncols prems)
+by (simp add: mult_matrix_def mult_n_ncols assms)
lemma nrows_move_matrix_le: "nrows (move_matrix A j i) <= nat((int (nrows A)) + j)"
apply (auto simp add: nrows_le)
@@ -1144,7 +1151,7 @@
done
lemma mult_matrix_assoc:
- assumes prems:
+ assumes
"! a. fmul1 0 a = 0"
"! a. fmul1 a 0 = 0"
"! a. fmul2 0 a = 0"
@@ -1157,50 +1164,52 @@
"! a b c. fmul2 (fmul1 a b) c = fmul1 a (fmul2 b c)"
"! a b c. fmul2 (fadd1 a b) c = fadd1 (fmul2 a c) (fmul2 b c)"
"! a b c. fmul1 c (fadd2 a b) = fadd2 (fmul1 c a) (fmul1 c b)"
- shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)" (is ?concl)
+ shows "mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B) C = mult_matrix fmul1 fadd1 A (mult_matrix fmul2 fadd2 B C)"
proof -
have comb_left: "!! A B x y. A = B \<Longrightarrow> (Rep_matrix (Abs_matrix A)) x y = (Rep_matrix(Abs_matrix B)) x y" by blast
have fmul2fadd1fold: "!! x s n. fmul2 (foldseq fadd1 s n) x = foldseq fadd1 (% k. fmul2 (s k) x) n"
- by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], simp_all!)
+ by (rule_tac g1 = "% y. fmul2 y x" in ssubst [OF foldseq_distr_unary], insert assms, simp_all)
have fmul1fadd2fold: "!! x s n. fmul1 x (foldseq fadd2 s n) = foldseq fadd2 (% k. fmul1 x (s k)) n"
- by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all!)
+ using assms by (rule_tac g1 = "% y. fmul1 x y" in ssubst [OF foldseq_distr_unary], simp_all)
let ?N = "max (ncols A) (max (ncols B) (max (nrows B) (nrows C)))"
- show ?concl
+ show ?thesis
apply (simp add: Rep_matrix_inject[THEN sym])
apply (rule ext)+
apply (simp add: mult_matrix_def)
apply (simplesubst mult_matrix_nm[of _ "max (ncols (mult_matrix_n (max (ncols A) (nrows B)) fmul1 fadd1 A B)) (nrows C)" _ "max (ncols B) (nrows C)"])
- apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
- apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"]) apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+ apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
+ apply (simplesubst mult_matrix_nm[of _ "max (ncols A) (nrows (mult_matrix_n (max (ncols B) (nrows C)) fmul2 fadd2 B C))" _ "max (ncols A) (nrows B)"])
+ apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
- apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+ apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
- apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+ apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
- apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+ apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
apply (simplesubst mult_matrix_nm[of _ _ _ "?N"])
- apply (simp add: max1 max2 mult_n_ncols mult_n_nrows prems)+
+ apply (simp add: max1 max2 mult_n_ncols mult_n_nrows assms)+
apply (simp add: mult_matrix_n_def)
apply (rule comb_left)
apply ((rule ext)+, simp)
apply (simplesubst RepAbs_matrix)
apply (rule exI[of _ "nrows B"])
- apply (simp add: nrows prems foldseq_zero)
+ apply (simp add: nrows assms foldseq_zero)
apply (rule exI[of _ "ncols C"])
- apply (simp add: prems ncols foldseq_zero)
+ apply (simp add: assms ncols foldseq_zero)
apply (subst RepAbs_matrix)
apply (rule exI[of _ "nrows A"])
- apply (simp add: nrows prems foldseq_zero)
+ apply (simp add: nrows assms foldseq_zero)
apply (rule exI[of _ "ncols B"])
- apply (simp add: prems ncols foldseq_zero)
- apply (simp add: fmul2fadd1fold fmul1fadd2fold prems)
+ apply (simp add: assms ncols foldseq_zero)
+ apply (simp add: fmul2fadd1fold fmul1fadd2fold assms)
apply (subst foldseq_foldseq)
- apply (simp add: prems)+
- by (simp add: transpose_infmatrix)
+ apply (simp add: assms)+
+ apply (simp add: transpose_infmatrix)
+ done
qed
lemma
- assumes prems:
+ assumes
"! a. fmul1 0 a = 0"
"! a. fmul1 a 0 = 0"
"! a. fmul2 0 a = 0"
@@ -1217,10 +1226,11 @@
"(mult_matrix fmul1 fadd1 A) o (mult_matrix fmul2 fadd2 B) = mult_matrix fmul2 fadd2 (mult_matrix fmul1 fadd1 A B)"
apply (rule ext)+
apply (simp add: comp_def )
-by (simp add: mult_matrix_assoc prems)
+apply (simp add: mult_matrix_assoc assms)
+done
lemma mult_matrix_assoc_simple:
- assumes prems:
+ assumes
"! a. fmul 0 a = 0"
"! a. fmul a 0 = 0"
"fadd 0 0 = 0"
@@ -1228,14 +1238,16 @@
"commutative fadd"
"associative fmul"
"distributive fmul fadd"
- shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)" (is ?concl)
+ shows "mult_matrix fmul fadd (mult_matrix fmul fadd A B) C = mult_matrix fmul fadd A (mult_matrix fmul fadd B C)"
proof -
have "!! a b c d. fadd (fadd a b) (fadd c d) = fadd (fadd a c) (fadd b d)"
- by (simp! add: associative_def commutative_def)
- then show ?concl
+ using assms by (simp add: associative_def commutative_def)
+ then show ?thesis
apply (subst mult_matrix_assoc)
- apply (simp_all!)
- by (simp add: associative_def distributive_def l_distributive_def r_distributive_def)+
+ using assms
+ apply simp_all
+ apply (simp_all add: associative_def distributive_def l_distributive_def r_distributive_def)
+ done
qed
lemma transpose_apply_matrix: "f 0 = 0 \<Longrightarrow> transpose_matrix (apply_matrix f A) = apply_matrix f (transpose_matrix A)"
@@ -1258,9 +1270,10 @@
foldseq fadd (% k. fmul (Rep_matrix A j k) (Rep_matrix B k i)) (max (ncols A) (nrows B))"
apply (simp add: mult_matrix_def mult_matrix_n_def)
apply (subst RepAbs_matrix)
-apply (rule exI[of _ "nrows A"], simp! add: nrows foldseq_zero)
-apply (rule exI[of _ "ncols B"], simp! add: ncols foldseq_zero)
-by simp
+apply (rule exI[of _ "nrows A"], insert assms, simp add: nrows foldseq_zero)
+apply (rule exI[of _ "ncols B"], insert assms, simp add: ncols foldseq_zero)
+apply simp
+done
lemma transpose_mult_matrix:
assumes
@@ -1272,7 +1285,9 @@
"transpose_matrix (mult_matrix fmul fadd A B) = mult_matrix fmul fadd (transpose_matrix B) (transpose_matrix A)"
apply (simp add: Rep_matrix_inject[THEN sym])
apply (rule ext)+
- by (simp! add: Rep_mult_matrix max_ac)
+ using assms
+ apply (simp add: Rep_mult_matrix max_ac)
+ done
lemma column_transpose_matrix: "column_of_matrix (transpose_matrix A) n = transpose_matrix (row_of_matrix A n)"
apply (simp add: Rep_matrix_inject[THEN sym])
@@ -1318,7 +1333,7 @@
"(a::('a::{ord, zero}) matrix) <= b"
shows
"apply_matrix f a <= apply_matrix f b"
- by (simp! add: le_matrix_def)
+ using assms by (simp add: le_matrix_def)
lemma le_combine_matrix:
assumes
@@ -1328,7 +1343,7 @@
"C <= D"
shows
"combine_matrix f A C <= combine_matrix f B D"
-by (simp! add: le_matrix_def)
+ using assms by (simp add: le_matrix_def)
lemma le_left_combine_matrix:
assumes
@@ -1337,7 +1352,7 @@
"A <= B"
shows
"combine_matrix f C A <= combine_matrix f C B"
- by (simp! add: le_matrix_def)
+ using assms by (simp add: le_matrix_def)
lemma le_right_combine_matrix:
assumes
@@ -1346,7 +1361,7 @@
"A <= B"
shows
"combine_matrix f A C <= combine_matrix f B C"
- by (simp! add: le_matrix_def)
+ using assms by (simp add: le_matrix_def)
lemma le_transpose_matrix: "(A <= B) = (transpose_matrix A <= transpose_matrix B)"
by (simp add: le_matrix_def, auto)
@@ -1358,8 +1373,9 @@
shows
"foldseq f s n <= foldseq f t n"
proof -
- have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n" by (induct_tac n, simp_all!)
- then show "foldseq f s n <= foldseq f t n" by (simp!)
+ have "! s t. (! i. i<=n \<longrightarrow> s i <= t i) \<longrightarrow> foldseq f s n <= foldseq f t n"
+ by (induct n) (simp_all add: assms)
+ then show "foldseq f s n <= foldseq f t n" using assms by simp
qed
lemma le_left_mult:
@@ -1373,11 +1389,13 @@
"A <= B"
shows
"mult_matrix fmul fadd C A <= mult_matrix fmul fadd C B"
- apply (simp! add: le_matrix_def Rep_mult_matrix)
+ using assms
+ apply (simp add: le_matrix_def Rep_mult_matrix)
apply (auto)
apply (simplesubst foldseq_zerotail[of _ _ _ "max (ncols C) (max (nrows A) (nrows B))"], simp_all add: nrows ncols max1 max2)+
apply (rule le_foldseq)
- by (auto)
+ apply (auto)
+ done
lemma le_right_mult:
assumes
@@ -1390,11 +1408,13 @@
"A <= B"
shows
"mult_matrix fmul fadd A C <= mult_matrix fmul fadd B C"
- apply (simp! add: le_matrix_def Rep_mult_matrix)
+ using assms
+ apply (simp add: le_matrix_def Rep_mult_matrix)
apply (auto)
apply (simplesubst foldseq_zerotail[of _ _ _ "max (nrows C) (max (ncols A) (ncols B))"], simp_all add: nrows ncols max1 max2)+
apply (rule le_foldseq)
- by (auto)
+ apply (auto)
+ done
lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast
lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast
@@ -1720,15 +1740,16 @@
proof -
have "Y = Y * one_matrix (nrows A)"
apply (subst one_matrix_mult_right)
- apply (insert prems)
- by (simp_all add: left_inverse_matrix_def)
+ using assms
+ apply (simp_all add: left_inverse_matrix_def)
+ done
also have "\<dots> = Y * (A * X)"
- apply (insert prems)
+ apply (insert assms)
apply (frule right_inverse_matrix_dim)
by (simp add: right_inverse_matrix_def)
also have "\<dots> = (Y * A) * X" by (simp add: mult_assoc)
also have "\<dots> = X"
- apply (insert prems)
+ apply (insert assms)
apply (frule left_inverse_matrix_dim)
apply (simp_all add: left_inverse_matrix_def right_inverse_matrix_def one_matrix_mult_left)
done
--- a/src/HOL/Mutabelle/mutabelle.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Mutabelle/mutabelle.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/NSA/transfer.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/Nominal/nominal_datatype.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/Tools/Datatype/datatype.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Function/induction_schema.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Function/mutual.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Function/termination.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Nitpick/minipick.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Qelim/langford.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Qelim/presburger.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/TFL/post.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/choice_specification.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/Tools/choice_specification.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/hologic.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/inductive.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/lin_arith.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/meson.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/record.ML Sun Mar 07 10:03:16 2010 -0800
@@ -859,12 +859,12 @@
fun strip_fields T =
(case T of
- Type (ext, args) =>
+ Type (ext, args as _ :: _) =>
(case try (unsuffix ext_typeN) ext of
SOME ext' =>
(case get_extfields thy ext' of
- SOME fields =>
- (case get_fieldext thy (fst (hd fields)) of
+ SOME (fields as (x, _) :: _) =>
+ (case get_fieldext thy x of
SOME (_, alphas) =>
(let
val f :: fs = but_last fields;
@@ -877,9 +877,9 @@
in fields'' @ strip_fields more end
handle Type.TYPE_MATCH => [("", T)]
| Library.UnequalLengths => [("", T)])
- | NONE => [("", T)])
- | NONE => [("", T)])
- | NONE => [("", T)])
+ | _ => [("", T)])
+ | _ => [("", T)])
+ | _ => [("", T)])
| _ => [("", T)]);
val (fields, (_, moreT)) = split_last (strip_fields T);
@@ -896,25 +896,7 @@
fun record_type_abbr_tr' abbr alphas zeta last_ext schemeT ctxt tm =
let
val thy = ProofContext.theory_of ctxt;
-
- (*tm is term representation of a (nested) field type. We first reconstruct the
- type from tm so that we can continue on the type level rather then the term level*)
-
- (* FIXME !??? *)
- (*WORKAROUND:
- If a record type occurs in an error message of type inference there
- may be some internal frees donoted by ??:
- (Const "_tfree",_) $ Free ("??'a", _).
-
- This will unfortunately be translated to Type ("??'a", []) instead of
- TFree ("??'a", _) by typ_of_term, which will confuse unify below.
- fixT works around.*)
- fun fixT (T as Type (x, [])) =
- if String.isPrefix "??'" x then TFree (x, Sign.defaultS thy) else T
- | fixT (Type (x, xs)) = Type (x, map fixT xs)
- | fixT T = T;
-
- val T = fixT (decode_type thy tm);
+ val T = decode_type thy tm;
val midx = maxidx_of_typ T;
val varifyT = varifyT midx;
@@ -2232,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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/res_axioms.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/sat_funcs.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/HOL/Tools/typedef.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/HOL/ex/Codegenerator_Candidates.thy Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOL/ex/Codegenerator_Candidates.thy Sun Mar 07 10:03:16 2010 -0800
@@ -21,6 +21,7 @@
Product_ord
"~~/src/HOL/ex/Records"
SetsAndFunctions
+ Table
Tree
While_Combinator
Word
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/fixrec.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/HOLCF/Tools/fixrec.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Provers/blast.ML Sun Mar 07 10:03:16 2010 -0800
@@ -57,7 +57,7 @@
safe0_netpair: netpair, safep_netpair: netpair,
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
val cla_modifiers: Method.modifier parser list
- val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
+ val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
end;
signature BLAST =
@@ -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
@@ -1309,10 +1309,9 @@
val setup =
setup_depth_limit #>
Method.setup @{binding blast}
- (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
- Method.sections Data.cla_modifiers >>
- (fn (prems, NONE) => Data.cla_meth' blast_tac prems
- | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
+ (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
+ (fn NONE => Data.cla_meth' blast_tac
+ | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
"classical tableau prover";
end;
--- a/src/Provers/clasimp.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Provers/clasimp.ML Sun Mar 07 10:03:16 2010 -0800
@@ -258,21 +258,21 @@
(* methods *)
-fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (clasimpset_of ctxt));
+fun clasimp_meth tac ctxt = METHOD (fn facts =>
+ ALLGOALS (Method.insert_tac facts) THEN tac (clasimpset_of ctxt));
-fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
+fun clasimp_meth' tac ctxt = METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac facts THEN' tac (clasimpset_of ctxt)));
fun clasimp_method' tac =
- Args.bang_facts --| Method.sections clasimp_modifiers >> (clasimp_meth' tac);
+ Method.sections clasimp_modifiers >> K (clasimp_meth' tac);
val auto_method =
- Args.bang_facts -- Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
- Method.sections clasimp_modifiers >>
- (fn (prems, NONE) => clasimp_meth (CHANGED_PROP o auto_tac) prems
- | (prems, SOME (m, n)) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)) prems);
+ Scan.lift (Scan.option (OuterParse.nat -- OuterParse.nat)) --|
+ Method.sections clasimp_modifiers >>
+ (fn NONE => clasimp_meth (CHANGED_PROP o auto_tac)
+ | SOME (m, n) => clasimp_meth (CHANGED_PROP o (fn css => mk_auto_tac css m n)));
(* theory setup *)
--- a/src/Provers/classical.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Provers/classical.ML Sun Mar 07 10:03:16 2010 -0800
@@ -125,8 +125,8 @@
val haz_intro: int option -> attribute
val rule_del: attribute
val cla_modifiers: Method.modifier parser list
- val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
- val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
+ val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
+ val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
val setup: theory -> theory
@@ -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));
@@ -969,14 +969,14 @@
Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
Args.del -- Args.colon >> K (I, rule_del)];
-fun cla_meth tac prems ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
+fun cla_meth tac ctxt = METHOD (fn facts =>
+ ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
-fun cla_meth' tac prems ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
+fun cla_meth' tac ctxt = METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
-fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
-fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
+fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
+fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
--- a/src/Provers/splitter.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Provers/splitter.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 10:03:16 2010 -0800
@@ -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 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/IsaMakefile Sun Mar 07 10:03:16 2010 -0800
@@ -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/args.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Pure/Isar/args.ML Sun Mar 07 10:03:16 2010 -0800
@@ -57,7 +57,6 @@
val type_name: bool -> string context_parser
val const: bool -> string context_parser
val const_proper: bool -> string context_parser
- val bang_facts: thm list context_parser
val goal_spec: ((int -> tactic) -> tactic) context_parser
val parse: token list parser
val parse1: (string -> bool) -> token list parser
@@ -224,11 +223,6 @@
(* improper method arguments *)
-val bang_facts = Scan.peek (fn context =>
- P.position ($$$ "!") >> (fn (_, pos) =>
- (legacy_feature ("use of cumulative prems (!) in proof method" ^ Position.str_of pos);
- Assumption.all_prems_of (Context.proof_of context))) || Scan.succeed []);
-
val from_to =
P.nat -- ($$$ "-" |-- P.nat) >> (fn (i, j) => fn tac => Seq.INTERVAL tac i j) ||
P.nat --| $$$ "-" >> (fn i => fn tac => fn st => Seq.INTERVAL tac i (Thm.nprems_of st) st) ||
--- a/src/Pure/Isar/attrib.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Pure/Isar/attrib.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/auto_bind.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/code.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/constdefs.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/element.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/expression.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/isar_syn.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/local_defs.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/method.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/object_logic.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/obtain.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/proof.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/proof_context.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 07 10:03:16 2010 -0800
@@ -64,6 +64,7 @@
val expand_abbrevs: Proof.context -> term -> term
val cert_term: Proof.context -> term -> term
val cert_prop: Proof.context -> term -> term
+ val def_type: Proof.context -> indexname -> typ option
val goal_export: Proof.context -> Proof.context -> thm list -> thm list
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
@@ -628,13 +629,15 @@
(* type checking/inference *)
+fun def_type ctxt =
+ let val Mode {pattern, ...} = get_mode ctxt
+ in Variable.def_type ctxt pattern end;
+
fun standard_infer_types ctxt ts =
- let val Mode {pattern, ...} = get_mode ctxt in
- TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
- (try (Consts.the_constraint (consts_of ctxt))) (Variable.def_type ctxt pattern)
- (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
- handle TYPE (msg, _, _) => error msg
- end;
+ TypeInfer.infer_types (Syntax.pp ctxt) (tsig_of ctxt) (Syntax.check_typs ctxt)
+ (try (Consts.the_constraint (consts_of ctxt))) (def_type ctxt)
+ (Variable.names_of ctxt) (Variable.maxidx_of ctxt) ts
+ handle TYPE (msg, _, _) => error msg;
local
--- a/src/Pure/Isar/rule_cases.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Pure/Isar/rule_cases.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/specification.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Isar/theory_target.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/ML-Systems/proper_int.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/ROOT.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Thy/term_style.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/Tools/find_theorems.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Pure/old_goals.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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/Pure/simplifier.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Pure/simplifier.ML Sun Mar 07 10:03:16 2010 -0800
@@ -15,15 +15,15 @@
val simpset_of: Proof.context -> simpset
val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
val safe_asm_full_simp_tac: simpset -> int -> tactic
- val simp_tac: simpset -> int -> tactic
- val asm_simp_tac: simpset -> int -> tactic
- val full_simp_tac: simpset -> int -> tactic
- val asm_lr_simp_tac: simpset -> int -> tactic
- val asm_full_simp_tac: simpset -> int -> tactic
- val simplify: simpset -> thm -> thm
- val asm_simplify: simpset -> thm -> thm
- val full_simplify: simpset -> thm -> thm
- val asm_lr_simplify: simpset -> thm -> thm
+ val simp_tac: simpset -> int -> tactic
+ val asm_simp_tac: simpset -> int -> tactic
+ val full_simp_tac: simpset -> int -> tactic
+ val asm_lr_simp_tac: simpset -> int -> tactic
+ val asm_full_simp_tac: simpset -> int -> tactic
+ val simplify: simpset -> thm -> thm
+ val asm_simplify: simpset -> thm -> thm
+ val full_simplify: simpset -> thm -> thm
+ val asm_lr_simplify: simpset -> thm -> thm
val asm_full_simplify: simpset -> thm -> thm
end;
@@ -41,10 +41,10 @@
-> (theory -> simpset -> term -> thm option) -> simproc
val simproc: theory -> string -> string list
-> (theory -> simpset -> term -> thm option) -> simproc
- val rewrite: simpset -> conv
- val asm_rewrite: simpset -> conv
- val full_rewrite: simpset -> conv
- val asm_lr_rewrite: simpset -> conv
+ val rewrite: simpset -> conv
+ val asm_rewrite: simpset -> conv
+ val full_rewrite: simpset -> conv
+ val asm_lr_rewrite: simpset -> conv
val asm_full_rewrite: simpset -> conv
val get_ss: Context.generic -> simpset
val map_ss: (simpset -> simpset) -> Context.generic -> Context.generic
@@ -371,9 +371,9 @@
Scan.succeed asm_full_simp_tac);
fun simp_method more_mods meth =
- Args.bang_facts -- Scan.lift simp_options --|
+ Scan.lift simp_options --|
Method.sections (more_mods @ simp_modifiers') >>
- (fn (prems, tac) => fn ctxt => METHOD (fn facts => meth ctxt tac (prems @ facts)));
+ (fn tac => fn ctxt => METHOD (fn facts => meth ctxt tac facts));
--- a/src/Pure/tactic.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Pure/tactic.ML Sun Mar 07 10:03:16 2010 -0800
@@ -63,8 +63,6 @@
sig
include BASIC_TACTIC
val innermost_params: int -> thm -> (string * typ) list
- val term_lift_inst_rule:
- thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
val insert_tagged_brl: 'a * (bool * thm) ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
@@ -193,40 +191,6 @@
(*params of subgoal i as they are printed*)
fun params_of_state i st = rev (innermost_params i st);
-(*
-Like lift_inst_rule but takes terms, not strings, where the terms may contain
-Bounds referring to parameters of the subgoal.
-
-insts: [...,(vj,tj),...]
-
-The tj may contain references to parameters of subgoal i of the state st
-in the form of Bound k, i.e. the tj may be subterms of the subgoal.
-To saturate the lose bound vars, the tj are enclosed in abstractions
-corresponding to the parameters of subgoal i, thus turning them into
-functions. At the same time, the types of the vj are lifted.
-
-NB: the types in insts must be correctly instantiated already,
- i.e. Tinsts is not applied to insts.
-*)
-fun term_lift_inst_rule (st, i, Tinsts, insts, rule) =
-let
- val thy = Thm.theory_of_thm st
- val cert = Thm.cterm_of thy
- val certT = Thm.ctyp_of thy
- val maxidx = Thm.maxidx_of st
- val paramTs = map #2 (params_of_state i st)
- val inc = maxidx+1
- fun liftvar ((a,j), T) = Var((a, j+inc), paramTs---> Logic.incr_tvar inc T)
- (*lift only Var, not term, which must be lifted already*)
- fun liftpair (v,t) = (cert (liftvar v), cert t)
- fun liftTpair (((a, i), S), T) =
- (certT (TVar ((a, i + inc), S)),
- certT (Logic.incr_tvar inc T))
-in Drule.instantiate (map liftTpair Tinsts, map liftpair insts)
- (Thm.lift_rule (Thm.cprem_of st i) rule)
-end;
-
-
(*** Applications of cut_rl ***)
--- a/src/Tools/Code/code_preproc.ML Sun Mar 07 09:57:30 2010 -0800
+++ b/src/Tools/Code/code_preproc.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Tools/atomize_elim.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Tools/induct.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Tools/induct_tacs.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Tools/intuitionistic.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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 09:57:30 2010 -0800
+++ b/src/Tools/quickcheck.ML Sun Mar 07 10:03:16 2010 -0800
@@ -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."