--- a/Admin/makedist Tue Nov 16 16:36:57 2010 -0800
+++ b/Admin/makedist Wed Nov 17 06:49:23 2010 -0800
@@ -108,7 +108,7 @@
if [ -z "$RELEASE" ]; then
DISTNAME="Isabelle_$DATE"
- DISTVERSION="Isabelle repository snapshot $IDENT ($DATE)"
+ DISTVERSION="Isabelle repository snapshot $IDENT $DATE"
else
DISTNAME="$RELEASE"
DISTVERSION="$DISTNAME: $DISTDATE"
--- a/Isabelle Tue Nov 16 16:36:57 2010 -0800
+++ b/Isabelle Wed Nov 17 06:49:23 2010 -0800
@@ -24,6 +24,6 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
CLASSPATH="$(jvmpath "$CLASSPATH")"
-exec "$ISABELLE_JAVA" \
+exec "$ISABELLE_TOOL" java \
"-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
-jar "$(jvmpath "$ISABELLE_HOME/lib/classes/isabelle-scala.jar")" "$@"
--- a/NEWS Tue Nov 16 16:36:57 2010 -0800
+++ b/NEWS Wed Nov 17 06:49:23 2010 -0800
@@ -355,6 +355,9 @@
cvc3_options
yices_options
+* Boogie output files (.b2i files) need to be declared in the
+theory header.
+
* Removed [split_format ... and ... and ...] version of
[split_format]. Potential INCOMPATIBILITY.
--- a/doc-src/System/Thy/Basics.thy Tue Nov 16 16:36:57 2010 -0800
+++ b/doc-src/System/Thy/Basics.thy Wed Nov 17 06:49:23 2010 -0800
@@ -309,12 +309,18 @@
The root of component initialization is @{setting ISABELLE_HOME}
itself. After initializing all of its sub-components recursively,
@{setting ISABELLE_HOME_USER} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to @{verbatim "$ISABELLE_HOME_USER/etc/components"}.
-
- It is also possible to initialize components programmatically via
- the \verb,init_component, shell function, say within the
- \verb,settings, script of another component.
+ that directory exists). This allows to install private components
+ via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+ often more convenient to do that programmatically via the
+ \verb,init_component, shell function in the \verb,etc/settings,
+ script of \verb,$ISABELLE_HOME_USER, (or any other component
+ directory). For example:
+ \begin{verbatim}
+ if [ -d "$HOME/screwdriver-2.0" ]
+ then
+ init_component "$HOME/screwdriver-2.0"
+ else
+ \end{verbatim}
*}
--- a/doc-src/System/Thy/document/Basics.tex Tue Nov 16 16:36:57 2010 -0800
+++ b/doc-src/System/Thy/document/Basics.tex Wed Nov 17 06:49:23 2010 -0800
@@ -318,12 +318,18 @@
The root of component initialization is \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}
itself. After initializing all of its sub-components recursively,
\hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}} is included in the same manner (if
- that directory exists). Thus users can easily add private
- components to \verb|$ISABELLE_HOME_USER/etc/components|.
-
- It is also possible to initialize components programmatically via
- the \verb,init_component, shell function, say within the
- \verb,settings, script of another component.%
+ that directory exists). This allows to install private components
+ via \verb|$ISABELLE_HOME_USER/etc/components|, although it is
+ often more convenient to do that programmatically via the
+ \verb,init_component, shell function in the \verb,etc/settings,
+ script of \verb,$ISABELLE_HOME_USER, (or any other component
+ directory). For example:
+ \begin{verbatim}
+ if [ -d "$HOME/screwdriver-2.0" ]
+ then
+ init_component "$HOME/screwdriver-2.0"
+ else
+ \end{verbatim}%
\end{isamarkuptext}%
\isamarkuptrue%
%
--- a/etc/isar-keywords.el Tue Nov 16 16:36:57 2010 -0800
+++ b/etc/isar-keywords.el Wed Nov 17 06:49:23 2010 -0800
@@ -81,6 +81,7 @@
"display_drafts"
"domain"
"domain_isomorphism"
+ "domaindef"
"done"
"enable_pr"
"end"
@@ -207,7 +208,6 @@
"refute_params"
"remove_thy"
"rep_datatype"
- "repdef"
"schematic_corollary"
"schematic_lemma"
"schematic_theorem"
@@ -247,6 +247,7 @@
"txt"
"txt_raw"
"typ"
+ "type_mapper"
"type_notation"
"typed_print_translation"
"typedecl"
@@ -460,6 +461,7 @@
"defs"
"domain"
"domain_isomorphism"
+ "domaindef"
"equivariance"
"extract"
"extract_type"
@@ -501,7 +503,6 @@
"recdef"
"record"
"refute_params"
- "repdef"
"setup"
"simproc_setup"
"sledgehammer_params"
@@ -548,6 +549,7 @@
"sublocale"
"termination"
"theorem"
+ "type_mapper"
"typedef"))
(defconst isar-keywords-qed
--- a/etc/settings Tue Nov 16 16:36:57 2010 -0800
+++ b/etc/settings Wed Nov 17 06:49:23 2010 -0800
@@ -55,7 +55,11 @@
### JVM components (Scala or Java)
###
-ISABELLE_JAVA="java"
+if [ -n "$JAVA_HOME" ]; then
+ ISABELLE_JAVA="$JAVA_HOME/bin/java"
+else
+ ISABELLE_JAVA="java"
+fi
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/lib/scripts/getsettings Tue Nov 16 16:36:57 2010 -0800
+++ b/lib/scripts/getsettings Wed Nov 17 06:49:23 2010 -0800
@@ -72,6 +72,7 @@
CLASSPATH="$CLASSPATH:$X"
fi
done
+ export CLASSPATH
}
#arrays
@@ -90,6 +91,13 @@
function init_component ()
{
local COMPONENT="$1"
+ case "$COMPONENT" in
+ /*) ;;
+ *)
+ echo >&2 "Absolute component path required: \"$COMPONENT\""
+ exit 2
+ ;;
+ esac
if [ ! -d "$COMPONENT" ]; then
echo >&2 "Bad Isabelle component: \"$COMPONENT\""
--- a/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/Boogie_Dijkstra.thy Wed Nov 17 06:49:23 2010 -0800
@@ -80,7 +80,7 @@
*}
-boogie_open "Boogie_Dijkstra"
+boogie_open "Boogie_Dijkstra.b2i"
declare [[smt_certificates="Boogie_Dijkstra.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/Boogie/Examples/Boogie_Max.thy Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/Boogie_Max.thy Wed Nov 17 06:49:23 2010 -0800
@@ -37,7 +37,7 @@
\end{verbatim}
*}
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
declare [[smt_certificates="Boogie_Max.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy Wed Nov 17 06:49:23 2010 -0800
@@ -37,7 +37,7 @@
\end{verbatim}
*}
-boogie_open "Boogie_Max"
+boogie_open "Boogie_Max.b2i"
boogie_status -- {* gives an overview of all verification conditions *}
--- a/src/HOL/Boogie/Examples/VCC_Max.thy Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Examples/VCC_Max.thy Wed Nov 17 06:49:23 2010 -0800
@@ -45,7 +45,7 @@
\end{verbatim}
*}
-boogie_open (quiet) "VCC_Max"
+boogie_open (quiet) "VCC_Max.b2i"
declare [[smt_certificates="VCC_Max.certs"]]
declare [[smt_fixed=true]]
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Wed Nov 17 06:49:23 2010 -0800
@@ -17,8 +17,11 @@
fun boogie_open ((quiet, base_name), offsets) thy =
let
val ext = "b2i"
- fun add_ext path = path |> snd (Path.split_ext path) <> ext ? Path.ext ext
- val base_path = add_ext (Path.explode base_name)
+ fun check_ext path = snd (Path.split_ext path) = ext orelse
+ error ("Bad file ending of file " ^ quote (Path.implode path) ^ ", " ^
+ "expected file ending " ^ quote ext)
+
+ val base_path = Path.explode base_name |> tap check_ext
val (full_path, _) =
Thy_Load.check_file [Thy_Load.master_directory thy] base_path
--- a/src/HOL/HOL.thy Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/HOL.thy Wed Nov 17 06:49:23 2010 -0800
@@ -32,6 +32,7 @@
"Tools/async_manager.ML"
"Tools/try.ML"
("Tools/cnf_funcs.ML")
+ ("Tools/functorial_mappers.ML")
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -708,6 +709,7 @@
and [Pure.elim?] = iffD1 iffD2 impE
use "Tools/hologic.ML"
+use "Tools/functorial_mappers.ML"
subsubsection {* Atomizing meta-level connectives *}
--- a/src/HOL/IsaMakefile Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/IsaMakefile Wed Nov 17 06:49:23 2010 -0800
@@ -136,6 +136,7 @@
$(SRC)/Tools/solve_direct.ML \
$(SRC)/Tools/value.ML \
HOL.thy \
+ Tools/functorial_mappers.ML \
Tools/hologic.ML \
Tools/recfun_codegen.ML \
Tools/simpdata.ML
--- a/src/HOL/Tools/SMT/smt_config.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_config.ML Wed Nov 17 06:49:23 2010 -0800
@@ -25,6 +25,7 @@
val monomorph_limit: int Config.T
val drop_bad_facts: bool Config.T
val filter_only_facts: bool Config.T
+ val debug_files: string Config.T
(*tools*)
val with_timeout: Proof.context -> ('a -> 'b) -> 'a -> 'b
@@ -131,6 +132,10 @@
val (filter_only_facts, setup_filter_only_facts) =
Attrib.config_bool filter_only_factsN (K false)
+val debug_filesN = "smt_debug_files"
+val (debug_files, setup_debug_files) =
+ Attrib.config_string debug_filesN (K "")
+
val setup_options =
setup_oracle #>
setup_datatypes #>
@@ -141,7 +146,8 @@
setup_monomorph_limit #>
setup_drop_bad_facts #>
setup_filter_only_facts #>
- setup_trace_used_facts
+ setup_trace_used_facts #>
+ setup_debug_files
(* diagnostics *)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Wed Nov 17 06:49:23 2010 -0800
@@ -162,10 +162,12 @@
addsimps [@{thm Nat_Numeral.int_nat_number_of}]
addsimps @{thms neg_simps}
+ val int_eq = Thm.cterm_of @{theory} @{const "==" (int)}
+
fun cancel_int_nat_simproc _ ss ct =
let
val num = Thm.dest_arg (Thm.dest_arg ct)
- val goal = Thm.mk_binop @{cterm "op == :: int => _"} ct num
+ val goal = Thm.mk_binop int_eq ct num
val simpset = Simplifier.inherit_context ss cancel_int_nat_ss
fun tac _ = Simplifier.simp_tac simpset 1
in on_positive num (Goal.prove_internal [] goal) tac end
@@ -180,8 +182,8 @@
fun conv ctxt = Simplifier.rewrite (Simplifier.context ctxt nat_ss)
val uses_nat_type = Term.exists_type (Term.exists_subtype (equal @{typ nat}))
- val uses_nat_int =
- Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
+ val uses_nat_int = Term.exists_subterm (member (op aconv)
+ [@{const of_nat (int)}, @{const nat}])
in
fun nat_as_int ctxt =
map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
@@ -285,7 +287,7 @@
fun norm_def ctxt thm =
(case Thm.prop_of thm of
- @{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
+ @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Abs _) =>
norm_def ctxt (thm RS @{thm fun_cong})
| Const (@{const_name "=="}, _) $ _ $ Abs _ =>
norm_def ctxt (thm RS @{thm meta_eq_to_obj_eq})
@@ -293,7 +295,7 @@
fun atomize_conv ctxt ct =
(case Thm.term_of ct of
- @{term "op ==>"} $ _ $ _ =>
+ @{const "==>"} $ _ $ _ =>
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_imp}
| Const (@{const_name "=="}, _) $ _ $ _ =>
--- a/src/HOL/Tools/SMT/smt_real.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_real.ML Wed Nov 17 06:49:23 2010 -0800
@@ -63,7 +63,7 @@
(* Z3 builtins *)
local
- fun z3_builtin_fun @{term "op / :: real => _"} ts = SOME ("/", ts)
+ fun z3_builtin_fun @{const divide (real)} ts = SOME ("/", ts)
| z3_builtin_fun _ _ = NONE
in
@@ -86,13 +86,13 @@
if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
else NONE
- val mk_uminus = Thm.capply @{cterm "uminus :: real => _"}
- val mk_add = Thm.mk_binop @{cterm "op + :: real => _"}
- val mk_sub = Thm.mk_binop @{cterm "op - :: real => _"}
- val mk_mul = Thm.mk_binop @{cterm "op * :: real => _"}
- val mk_div = Thm.mk_binop @{cterm "op / :: real => _"}
- val mk_lt = Thm.mk_binop @{cterm "op < :: real => _"}
- val mk_le = Thm.mk_binop @{cterm "op <= :: real => _"}
+ val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
+ val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
+ val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
+ val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
+ val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
+ val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)})
+ val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
fun z3_mk_builtin_fun (I.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
| z3_mk_builtin_fun (I.Sym ("+", _)) [ct, cu] = SOME (mk_add ct cu)
--- a/src/HOL/Tools/SMT/smt_solver.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_solver.ML Wed Nov 17 06:49:23 2010 -0800
@@ -108,7 +108,17 @@
fun run ctxt cmd args input =
(case C.certificates_of ctxt of
- NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+ NONE =>
+ if Config.get ctxt C.debug_files = "" then
+ Cache_IO.run (make_cmd (choose cmd) args) input
+ else
+ let
+ val base_path = Path.explode (Config.get ctxt C.debug_files)
+ val in_path = Path.ext "smt_in" base_path
+ val out_path = Path.ext "smt_out" base_path
+ in
+ Cache_IO.raw_run (make_cmd (choose cmd) args) input in_path out_path
+ end
| SOME certs =>
(case Cache_IO.lookup certs input of
(NONE, key) =>
@@ -254,6 +264,8 @@
in
raise SMT_Failure.SMT (SMT_Failure.Counterexample (result = Sat, ts))
end)
+
+ val cfalse = Thm.cterm_of @{theory} (@{const Trueprop} $ @{const False})
in
fun add_solver cfg =
@@ -261,7 +273,7 @@
val {name, env_var, is_remote, options, interface, outcome, cex_parser,
reconstruct} = cfg
- fun core_oracle () = @{cprop False}
+ fun core_oracle () = cfalse
fun solver ocl = { env_var=env_var, is_remote=is_remote, options=options,
interface=interface,
@@ -302,6 +314,8 @@
"contains the universal sort {}"))
else solver_of ctxt rm ctxt irules
+val cnot = Thm.cterm_of @{theory} @{const Not}
+
fun smt_filter run_remote time_limit st xrules i =
let
val {facts, goal, ...} = Proof.goal st
@@ -312,10 +326,8 @@
|> Config.put C.drop_bad_facts true
|> Config.put C.filter_only_facts true
val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
- val cprop =
- concl
- |> Thm.rhs_of o SMT_Normalize.atomize_conv ctxt'
- |> Thm.capply @{cterm Trueprop} o Thm.capply @{cterm Not} o Thm.dest_arg
+ fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
+ val cprop = negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl))
val irs = map (pair ~1) (Thm.assume cprop :: prems @ facts)
val rm = SOME run_remote
in
--- a/src/HOL/Tools/SMT/smt_translate.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Nov 17 06:49:23 2010 -0800
@@ -134,7 +134,7 @@
| (ps, [false]) => cons (SNoPat ps)
| _ => raise TERM ("dest_pats", ts))
-fun dest_trigger (@{term trigger} $ tl $ t) =
+fun dest_trigger (@{const trigger} $ tl $ t) =
(rev (fold (dest_pats o HOLogic.dest_list) (HOLogic.dest_list tl) []), t)
| dest_trigger t = ([], t)
@@ -161,8 +161,8 @@
val needs_rewrite = Thm.prop_of #> Term.exists_subterm (fn
Const (@{const_name Let}, _) => true
- | @{term "op = :: bool => _"} $ _ $ @{term True} => true
- | Const (@{const_name If}, _) $ _ $ @{term True} $ @{term False} => true
+ | @{const HOL.eq (bool)} $ _ $ @{const True} => true
+ | Const (@{const_name If}, _) $ _ $ @{const True} $ @{const False} => true
| _ => false)
val rewrite_rules = [
@@ -199,11 +199,11 @@
fun conn (n, T) = (n, mapTs as_propT as_propT T)
fun pred (n, T) = (n, mapTs I as_propT T)
- val term_eq = @{term "op = :: bool => _"} |> Term.dest_Const |> pred
- fun as_term t = Const term_eq $ t $ @{term True}
+ val term_eq = @{const HOL.eq (bool)} |> Term.dest_Const |> pred
+ fun as_term t = Const term_eq $ t $ @{const True}
val if_term = Const (@{const_name If}, [propT, boolT, boolT] ---> boolT)
- fun wrap_in_if t = if_term $ t $ @{term True} $ @{term False}
+ fun wrap_in_if t = if_term $ t $ @{const True} $ @{const False}
fun in_list T f t = HOLogic.mk_list T (map f (HOLogic.dest_list t))
@@ -225,7 +225,7 @@
and in_pats ps =
in_list @{typ "pattern list"} (in_list @{typ pattern} in_pat) ps
- and in_trig ((c as @{term trigger}) $ p $ t) = c $ in_pats p $ in_form t
+ and in_trig ((c as @{const trigger}) $ p $ t) = c $ in_pats p $ in_form t
| in_trig t = in_form t
and in_form t =
--- a/src/HOL/Tools/SMT/smt_word.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_word.ML Wed Nov 17 06:49:23 2010 -0800
@@ -60,7 +60,7 @@
fun dest_word_funT (Type ("fun", [T, U])) = (dest_wordT T, dest_wordT U)
| dest_word_funT T = raise TYPE ("dest_word_funT", [T], [])
- fun dest_nat (@{term nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
+ fun dest_nat (@{const nat} $ n :: ts) = (snd (HOLogic.dest_number n), ts)
| dest_nat ts = raise TERM ("dest_nat", ts)
fun dest_nat_word_funT (T, ts) =
(dest_word_funT (Term.range_type T), dest_nat ts)
--- a/src/HOL/Tools/SMT/z3_interface.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_interface.ML Wed Nov 17 06:49:23 2010 -0800
@@ -70,8 +70,8 @@
val {is_builtin_pred, ...}= the strict
val {builtin_typ, builtin_num, builtin_fun, ...} = builtins
- fun is_int_div_mod @{term "op div :: int => _"} = true
- | is_int_div_mod @{term "op mod :: int => _"} = true
+ fun is_int_div_mod @{const div (int)} = true
+ | is_int_div_mod @{const mod (int)} = true
| is_int_div_mod _ = false
fun add_div_mod irules =
@@ -170,11 +170,13 @@
val destT1 = hd o Thm.dest_ctyp
val destT2 = hd o tl o Thm.dest_ctyp
-val mk_true = @{cterm "~False"}
-val mk_false = @{cterm False}
-val mk_not = Thm.capply @{cterm Not}
-val mk_implies = Thm.mk_binop @{cterm HOL.implies}
-val mk_iff = Thm.mk_binop @{cterm "op = :: bool => _"}
+val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+val mk_false = Thm.cterm_of @{theory} @{const False}
+val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies})
+val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)})
+val conj = Thm.cterm_of @{theory} @{const HOL.conj}
+val disj = Thm.cterm_of @{theory} @{const HOL.disj}
fun mk_nary _ cu [] = cu
| mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
@@ -205,22 +207,22 @@
let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
in Thm.capply (Thm.mk_binop (instTs cTs update) array index) value end
-val mk_uminus = Thm.capply @{cterm "uminus :: int => _"}
-val mk_add = Thm.mk_binop @{cterm "op + :: int => _"}
-val mk_sub = Thm.mk_binop @{cterm "op - :: int => _"}
-val mk_mul = Thm.mk_binop @{cterm "op * :: int => _"}
-val mk_div = Thm.mk_binop @{cterm "z3div :: int => _"}
-val mk_mod = Thm.mk_binop @{cterm "z3mod :: int => _"}
-val mk_lt = Thm.mk_binop @{cterm "op < :: int => _"}
-val mk_le = Thm.mk_binop @{cterm "op <= :: int => _"}
+val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
+val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
+val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
+val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
+val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3div})
+val mk_mod = Thm.mk_binop (Thm.cterm_of @{theory} @{const z3mod})
+val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (int)})
+val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (int)})
fun mk_builtin_fun ctxt sym cts =
(case (sym, cts) of
(Sym ("true", _), []) => SOME mk_true
| (Sym ("false", _), []) => SOME mk_false
| (Sym ("not", _), [ct]) => SOME (mk_not ct)
- | (Sym ("and", _), _) => SOME (mk_nary @{cterm HOL.conj} mk_true cts)
- | (Sym ("or", _), _) => SOME (mk_nary @{cterm HOL.disj} mk_false cts)
+ | (Sym ("and", _), _) => SOME (mk_nary conj mk_true cts)
+ | (Sym ("or", _), _) => SOME (mk_nary disj mk_false cts)
| (Sym ("implies", _), [ct, cu]) => SOME (mk_implies ct cu)
| (Sym ("iff", _), [ct, cu]) => SOME (mk_iff ct cu)
| (Sym ("~", _), [ct, cu]) => SOME (mk_iff ct cu)
--- a/src/HOL/Tools/SMT/z3_model.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_model.ML Wed Nov 17 06:49:23 2010 -0800
@@ -115,7 +115,7 @@
fun match ts ((n, _), _) = matches terms (member (op aconv) ts) n
val (default_int, ints) =
- (case find_first (match [@{term int}]) vs of
+ (case find_first (match [@{const of_nat (int)}]) vs of
NONE => (NONE, [])
| SOME (_, cases) =>
let val (cs, (_, e)) = split_last cases
@@ -138,7 +138,7 @@
| SOME t => ((n, k), map (subst_nat (Term.fastype_of t) k) cases))
in
map subst_nats vs
- |> filter_out (match [@{term int}, @{term nat}])
+ |> filter_out (match [@{const of_nat (int)}, @{const nat}])
end
fun filter_valid_valuations terms = map_filter (fn
@@ -179,8 +179,8 @@
fun get_term n (cx as (_, terms, _)) = (the (Symtab.lookup terms n), cx)
-fun trans_expr _ True = pair @{term True}
- | trans_expr _ False = pair @{term False}
+fun trans_expr _ True = pair @{const True}
+ | trans_expr _ False = pair @{const False}
| trans_expr T (Number (i, NONE)) = pair (HOLogic.mk_number T i)
| trans_expr T (Number (i, SOME j)) =
pair (Const (@{const_name divide}, [T, T] ---> T) $
--- a/src/HOL/Tools/SMT/z3_proof_literals.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_literals.ML Wed Nov 17 06:49:23 2010 -0800
@@ -22,6 +22,7 @@
val is_conj: term -> bool
val is_disj: term -> bool
val exists_lit: bool -> (term -> bool) -> term -> bool
+ val negate: cterm -> cterm
(* proof tools *)
val explode: bool -> bool -> bool -> term list -> thm -> thm list
@@ -59,19 +60,19 @@
(** properties and term operations **)
-val is_neg = (fn @{term Not} $ _ => true | _ => false)
-fun is_neg' f = (fn @{term Not} $ t => f t | _ => false)
+val is_neg = (fn @{const Not} $ _ => true | _ => false)
+fun is_neg' f = (fn @{const Not} $ t => f t | _ => false)
val is_dneg = is_neg' is_neg
-val is_conj = (fn @{term HOL.conj} $ _ $ _ => true | _ => false)
-val is_disj = (fn @{term HOL.disj} $ _ $ _ => true | _ => false)
+val is_conj = (fn @{const HOL.conj} $ _ $ _ => true | _ => false)
+val is_disj = (fn @{const HOL.disj} $ _ $ _ => true | _ => false)
fun dest_disj_term' f = (fn
- @{term Not} $ (@{term HOL.disj} $ t $ u) => SOME (f t, f u)
+ @{const Not} $ (@{const HOL.disj} $ t $ u) => SOME (f t, f u)
| _ => NONE)
-val dest_conj_term = (fn @{term HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
+val dest_conj_term = (fn @{const HOL.conj} $ t $ u => SOME (t, u) | _ => NONE)
val dest_disj_term =
- dest_disj_term' (fn @{term Not} $ t => t | t => @{term Not} $ t)
+ dest_disj_term' (fn @{const Not} $ t => t | t => @{const Not} $ t)
fun exists_lit is_conj P =
let
@@ -82,6 +83,8 @@
| NONE => false)
in exists end
+val negate = Thm.capply (Thm.cterm_of @{theory} @{const Not})
+
(** proof tools **)
@@ -135,7 +138,7 @@
end
| NONE => add (t, rev rules))
- fun explode0 (@{term Not} $ (@{term Not} $ t)) =
+ fun explode0 (@{const Not} $ (@{const Not} $ t)) =
Termtab.make [(t, [dneg_rule])]
| explode0 t = explode1 [] t Termtab.empty
@@ -202,23 +205,23 @@
| comp_disj ((true, thm1), (false, thm2)) = comp2 disj3 thm1 thm2
| comp_disj ((true, thm1), (true, thm2)) = comp2 disj4 thm1 thm2
- fun dest_conj (@{term HOL.conj} $ t $ u) = ((false, t), (false, u))
+ fun dest_conj (@{const HOL.conj} $ t $ u) = ((false, t), (false, u))
| dest_conj t = raise TERM ("dest_conj", [t])
- val neg = (fn @{term Not} $ t => (true, t) | t => (false, @{term Not} $ t))
- fun dest_disj (@{term Not} $ (@{term HOL.disj} $ t $ u)) = (neg t, neg u)
+ val neg = (fn @{const Not} $ t => (true, t) | t => (false, @{const Not} $ t))
+ fun dest_disj (@{const Not} $ (@{const HOL.disj} $ t $ u)) = (neg t, neg u)
| dest_disj t = raise TERM ("dest_disj", [t])
val dnegE = T.precompose (single o d2 o d1) @{thm notnotD}
val dnegI = T.precompose (single o d1) @{lemma "P ==> ~~P" by fast}
- fun as_dneg f t = f (@{term Not} $ (@{term Not} $ t))
+ fun as_dneg f t = f (@{const Not} $ (@{const Not} $ t))
fun dni f = apsnd f o Thm.dest_binop o f o d1
val negIffE = T.precompose2 (dni d1) @{lemma "~(P = (~Q)) ==> Q = P" by fast}
val negIffI = T.precompose2 (dni I) @{lemma "P = Q ==> ~(Q = (~P))" by fast}
- val iff_const = @{term "op = :: bool => _"}
- fun as_negIff f (@{term "op = :: bool => _"} $ t $ u) =
- f (@{term Not} $ (iff_const $ u $ (@{term Not} $ t)))
+ val iff_const = @{const HOL.eq (bool)}
+ fun as_negIff f (@{const HOL.eq (bool)} $ t $ u) =
+ f (@{const Not} $ (iff_const $ u $ (@{const Not} $ t)))
| as_negIff _ _ = NONE
in
@@ -231,12 +234,12 @@
fun lookup_rule t =
(case t of
- @{term Not} $ (@{term Not} $ t) => (T.compose dnegI, lookup t)
- | @{term Not} $ (@{term "op = :: bool => _"} $ t $ (@{term Not} $ u)) =>
- (T.compose negIffI, lookup (iff_const $ u $ t))
- | @{term Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
+ @{const Not} $ (@{const Not} $ t) => (T.compose dnegI, lookup t)
+ | @{const Not} $ (@{const HOL.eq (bool)} $ t $ (@{const Not} $ u)) =>
+ (T.compose negIffI, lookup (iff_const $ u $ t))
+ | @{const Not} $ ((eq as Const (@{const_name HOL.eq}, _)) $ t $ u) =>
let fun rewr lit = lit COMP @{thm not_sym}
- in (rewr, lookup (@{term Not} $ (eq $ u $ t))) end
+ in (rewr, lookup (@{const Not} $ (eq $ u $ t))) end
| _ =>
(case as_dneg lookup t of
NONE => (T.compose negIffE, as_negIff lookup t)
@@ -264,11 +267,10 @@
val cp1 = @{lemma "(~P) = (~Q) ==> P = Q" by simp}
val cp2 = @{lemma "(~P) = Q ==> P = (~Q)" by fastsimp}
val cp3 = @{lemma "P = (~Q) ==> (~P) = Q" by simp}
- val neg = Thm.capply @{cterm Not}
in
-fun contrapos1 prove (ct, cu) = prove (neg ct, neg cu) COMP cp1
-fun contrapos2 prove (ct, cu) = prove (neg ct, Thm.dest_arg cu) COMP cp2
-fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, neg cu) COMP cp3
+fun contrapos1 prove (ct, cu) = prove (negate ct, negate cu) COMP cp1
+fun contrapos2 prove (ct, cu) = prove (negate ct, Thm.dest_arg cu) COMP cp2
+fun contrapos3 prove (ct, cu) = prove (Thm.dest_arg ct, negate cu) COMP cp3
end
@@ -279,10 +281,10 @@
val rules = explode_term conj (T.prop_of thm)
fun contra_lits (t, rs) =
(case t of
- @{term Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
+ @{const Not} $ u => Termtab.lookup rules u |> Option.map (pair rs)
| _ => NONE)
in
- (case Termtab.lookup rules @{term False} of
+ (case Termtab.lookup rules @{const False} of
SOME rs => extract_lit thm rs
| NONE =>
the (Termtab.get_first contra_lits rules)
@@ -322,8 +324,9 @@
let val cp as (cl, cr) = Thm.dest_binop (Thm.dest_arg ct)
in
(case (kind_of (Thm.term_of cl), Thm.term_of cr) of
- (SOME CONJ, @{term False}) => contradict true cl
- | (SOME DISJ, @{term "~False"}) => contrapos2 (contradict false o fst) cp
+ (SOME CONJ, @{const False}) => contradict true cl
+ | (SOME DISJ, @{const Not} $ @{const False}) =>
+ contrapos2 (contradict false o fst) cp
| (kl, _) =>
(case (kl, kind_of (Thm.term_of cr)) of
(SOME CONJ, SOME CONJ) => prove_eq true true cp
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML Wed Nov 17 06:49:23 2010 -0800
@@ -113,10 +113,11 @@
fun mk (i, v) = (v, certify ctxt (Free (nth ns i, #T (Thm.rep_cterm v))))
in map mk vars end
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
+
fun close ctxt (ct, vars) =
let
val inst = mk_inst ctxt vars
- val mk_prop = Thm.capply @{cterm Trueprop}
val names = fold (Term.add_free_names o Thm.term_of o snd) inst []
in (mk_prop (Thm.instantiate_cterm ([], inst) ct), names) end
@@ -182,6 +183,8 @@
(* parser context *)
+val not_false = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
+
fun make_context ctxt typs terms =
let
val ctxt' =
@@ -189,7 +192,7 @@
|> Symtab.fold (Variable.declare_typ o snd) typs
|> Symtab.fold (Variable.declare_term o snd) terms
- fun cert @{term True} = @{cterm "~False"}
+ fun cert @{const True} = not_false
| cert t = certify ctxt' t
in (typs, Symtab.map (K cert) terms, Inttab.empty, Inttab.empty, [], ctxt') end
@@ -357,8 +360,10 @@
fun pats st = seps (par ((this ":pat" || this ":nopat") |-- seps1 id)) st
+val ctrue = Thm.cterm_of @{theory} @{const True}
+
fun pattern st = par (this "pattern" |-- Scan.repeat1 (sep arg) >>
- (the o mk_fun (K (SOME @{cterm True})))) st
+ (the o mk_fun (K (SOME ctrue)))) st
fun quant_kind st = st |> (
this "forall" >> K (mk_forall o theory_of) ||
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Wed Nov 17 06:49:23 2010 -0800
@@ -231,7 +231,7 @@
in
fun lemma thm ct =
let
- val cu = Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ val cu = L.negate (Thm.dest_arg ct)
val hyps = map_filter (try HOLogic.dest_Trueprop) (#hyps (Thm.rep_thm thm))
in Thm (T.compose ccontr (T.under_assumption (intro hyps thm) cu)) end
end
@@ -243,7 +243,7 @@
val explode_disj = L.explode false true false
val join_disj = L.join false
fun unit thm thms th =
- let val t = @{term Not} $ T.prop_of thm and ts = map T.prop_of thms
+ let val t = @{const Not} $ T.prop_of thm and ts = map T.prop_of thms
in join_disj (L.make_littab (thms @ explode_disj ts th)) t end
fun dest_arg2 ct = Thm.dest_arg (Thm.dest_arg ct)
@@ -251,7 +251,7 @@
val contrapos = T.precompose2 dest @{lemma "(~P ==> ~Q) ==> Q ==> P" by fast}
in
fun unit_resolution thm thms ct =
- Thm.capply @{cterm Not} (Thm.dest_arg ct)
+ L.negate (Thm.dest_arg ct)
|> T.under_assumption (unit thm thms)
|> Thm o T.discharge thm o T.compose contrapos
end
@@ -295,14 +295,14 @@
let val (ct1, ct2) = Thm.dest_binop (Thm.dest_arg ct)
in
(case Thm.term_of ct1 of
- @{term Not} $ (@{term HOL.conj} $ _ $ _) =>
+ @{const Not} $ (@{const HOL.conj} $ _ $ _) =>
prove disjI1 (Thm.dest_arg ct1, true) (ct2, true)
- | @{term HOL.conj} $ _ $ _ =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, true)
- | @{term Not} $ (@{term HOL.disj} $ _ $ _) =>
- prove disjI3 (Thm.capply @{cterm Not} ct2, false) (ct1, false)
- | @{term HOL.disj} $ _ $ _ =>
- prove disjI2 (Thm.capply @{cterm Not} ct1, false) (ct2, true)
+ | @{const HOL.conj} $ _ $ _ =>
+ prove disjI3 (L.negate ct2, false) (ct1, true)
+ | @{const Not} $ (@{const HOL.disj} $ _ $ _) =>
+ prove disjI3 (L.negate ct2, false) (ct1, false)
+ | @{const HOL.disj} $ _ $ _ =>
+ prove disjI2 (L.negate ct1, false) (ct2, true)
| Const (@{const_name SMT.distinct}, _) $ _ =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv cv)
@@ -310,7 +310,7 @@
let val (cu1, cu2) = Thm.dest_binop (Thm.dest_arg cu)
in prove disjI4 (Thm.dest_arg cu2, true) (cu1, true) end
in T.with_conv (dis_conv T.unfold_distinct_conv) prv ct end
- | @{term Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
+ | @{const Not} $ (Const (@{const_name SMT.distinct}, _) $ _) =>
let
fun dis_conv cv = Conv.arg_conv (Conv.arg1_conv (Conv.arg_conv cv))
fun prv cu =
@@ -392,7 +392,7 @@
if l aconv r
then MetaEq (Thm.reflexive (Thm.dest_arg (Thm.dest_arg ct)))
else MetaEq (nnf_quant vars quant_rules1 (hd ps) ct)
- | _ $ (@{term Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
+ | _ $ (@{const Not} $ (Const _ $ Abs _)) $ (Const _ $ Abs _) =>
MetaEq (nnf_quant vars quant_rules2 (hd ps) ct)
| _ =>
let
@@ -474,8 +474,8 @@
fun mono f (cp as (cl, _)) =
(case Term.head_of (Thm.term_of cl) of
- @{term HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
- | @{term HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
+ @{const HOL.conj} => prove_nary L.is_conj (prove_eq_exn f)
+ | @{const HOL.disj} => prove_nary L.is_disj (prove_eq_exn f)
| Const (@{const_name SMT.distinct}, _) => prove_distinct (prove_eq_safe f)
| _ => prove (prove_eq_safe f)) cp
in
@@ -589,8 +589,8 @@
|> Conv.fconv_rule (Thm.beta_conversion true)
fun kind (Const (@{const_name Ex}, _) $ _) = (sk_ex_rule, I, I)
- | kind (@{term Not} $ (Const (@{const_name All}, _) $ _)) =
- (sk_all_rule, Thm.dest_arg, Thm.capply @{cterm Not})
+ | kind (@{const Not} $ (Const (@{const_name All}, _) $ _)) =
+ (sk_all_rule, Thm.dest_arg, L.negate)
| kind t = raise TERM ("skolemize", [t])
fun dest_abs_type (Abs (_, T, _)) = T
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Wed Nov 17 06:49:23 2010 -0800
@@ -53,12 +53,12 @@
(* accessing terms *)
-val dest_prop = (fn @{term Trueprop} $ t => t | t => t)
+val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
fun term_of ct = dest_prop (Thm.term_of ct)
fun prop_of thm = dest_prop (Thm.prop_of thm)
-val mk_prop = Thm.capply @{cterm Trueprop}
+val mk_prop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
val eq = I.mk_inst_pair I.destT1 @{cpat "op =="}
fun mk_meta_eq_cterm ct cu = Thm.mk_binop (I.instT' ct eq) ct cu
@@ -195,14 +195,14 @@
and abstr cvs ct =
(case Thm.term_of ct of
- @{term Trueprop} $ _ => abstr1 cvs ct
- | @{term "op ==>"} $ _ $ _ => abstr2 cvs ct
- | @{term True} => pair ct
- | @{term False} => pair ct
- | @{term Not} $ _ => abstr1 cvs ct
- | @{term HOL.conj} $ _ $ _ => abstr2 cvs ct
- | @{term HOL.disj} $ _ $ _ => abstr2 cvs ct
- | @{term HOL.implies} $ _ $ _ => abstr2 cvs ct
+ @{const Trueprop} $ _ => abstr1 cvs ct
+ | @{const "==>"} $ _ $ _ => abstr2 cvs ct
+ | @{const True} => pair ct
+ | @{const False} => pair ct
+ | @{const Not} $ _ => abstr1 cvs ct
+ | @{const HOL.conj} $ _ $ _ => abstr2 cvs ct
+ | @{const HOL.disj} $ _ $ _ => abstr2 cvs ct
+ | @{const HOL.implies} $ _ $ _ => abstr2 cvs ct
| Const (@{const_name HOL.eq}, _) $ _ $ _ => abstr2 cvs ct
| Const (@{const_name SMT.distinct}, _) $ _ =>
if ext_logic then abs_arg (abs_list abstr fresh_abstraction) cvs ct
@@ -221,8 +221,10 @@
else fresh_abstraction cvs ct cx))
in abstr [] end
+val cimp = Thm.cterm_of @{theory} @{const "==>"}
+
fun with_prems thms f ct =
- fold_rev (Thm.mk_binop @{cterm "op ==>"} o Thm.cprop_of) thms ct
+ fold_rev (Thm.mk_binop cimp o Thm.cprop_of) thms ct
|> f
|> fold (fn prem => fn th => Thm.implies_elim th prem) thms
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/functorial_mappers.ML Wed Nov 17 06:49:23 2010 -0800
@@ -0,0 +1,210 @@
+(* Title: HOL/Tools/functorial_mappers.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Functorial mappers on types.
+*)
+
+signature FUNCTORIAL_MAPPERS =
+sig
+ val find_atomic: theory -> typ -> (typ * (bool * bool)) list
+ val construct_mapper: theory -> (string * bool -> term)
+ -> bool -> typ -> typ -> term
+ val register: string -> string -> (sort * (bool * bool)) list -> thm -> thm
+ -> theory -> theory
+ val type_mapper: term -> theory -> Proof.state
+ type entry
+ val entries: theory -> entry Symtab.table
+end;
+
+structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
+struct
+
+(** functorial mappers and their properties **)
+
+(* bookkeeping *)
+
+type entry = { mapper: string, variances: (sort * (bool * bool)) list,
+ concatenate: thm, identity: thm };
+
+structure Data = Theory_Data(
+ type T = entry Symtab.table
+ val empty = Symtab.empty
+ val merge = Symtab.merge (K true)
+ val extend = I
+);
+
+val entries = Data.get;
+
+
+(* type analysis *)
+
+fun find_atomic thy T =
+ let
+ val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
+ fun add_variance is_contra T =
+ AList.map_default (op =) (T, (false, false))
+ ((if is_contra then apsnd else apfst) (K true));
+ fun analyze' is_contra (_, (co, contra)) T =
+ (if co then analyze is_contra T else I)
+ #> (if contra then analyze (not is_contra) T else I)
+ and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
+ of NONE => add_variance is_contra T
+ | SOME variances => fold2 (analyze' is_contra) variances Ts)
+ | analyze is_contra T = add_variance is_contra T;
+ in analyze false T [] end;
+
+fun construct_mapper thy atomic =
+ let
+ val lookup = the o Symtab.lookup (Data.get thy);
+ fun constructs is_contra (_, (co, contra)) T T' =
+ (if co then [construct is_contra T T'] else [])
+ @ (if contra then [construct (not is_contra) T T'] else [])
+ and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
+ let
+ val { mapper, variances, ... } = lookup tyco;
+ val args = maps (fn (arg_pattern, (T, T')) =>
+ constructs is_contra arg_pattern T T')
+ (variances ~~ (Ts ~~ Ts'));
+ val (U, U') = if is_contra then (T', T) else (T, T');
+ in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
+ | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
+ in construct end;
+
+
+(* mapper properties *)
+
+fun make_concatenate_prop variances (tyco, mapper) =
+ let
+ fun invents n k nctxt =
+ let
+ val names = Name.invents nctxt n k;
+ in (names, fold Name.declare names nctxt) end;
+ val (((vs1, vs2), vs3), _) = Name.context
+ |> invents Name.aT (length variances)
+ ||>> invents Name.aT (length variances)
+ ||>> invents Name.aT (length variances);
+ fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
+ vs variances;
+ val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
+ fun mk_argT ((T, T'), (_, (co, contra))) =
+ (if co then [(T --> T')] else [])
+ @ (if contra then [(T' --> T)] else []);
+ val contras = maps (fn (_, (co, contra)) =>
+ (if co then [false] else []) @ (if contra then [true] else [])) variances;
+ val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
+ val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
+ val ((names21, names32), nctxt) = Name.context
+ |> invents "f" (length Ts21)
+ ||>> invents "f" (length Ts32);
+ val T1 = Type (tyco, Ts1);
+ val T2 = Type (tyco, Ts2);
+ val T3 = Type (tyco, Ts3);
+ val x = Free (the_single (Name.invents nctxt "a" 1), T3);
+ val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
+ val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
+ if not is_contra then
+ Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
+ else
+ Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
+ ) contras (args21 ~~ args32)
+ fun mk_mapper T T' args = list_comb (Const (mapper,
+ map fastype_of args ---> T --> T'), args);
+ val lhs = mk_mapper T2 T1 (map Free args21) $
+ (mk_mapper T3 T2 (map Free args32) $ x);
+ val rhs = mk_mapper T3 T1 args31 $ x;
+ in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
+
+fun make_identity_prop variances (tyco, mapper) =
+ let
+ val vs = Name.invents Name.context Name.aT (length variances);
+ val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
+ fun bool_num b = if b then 1 else 0;
+ fun mk_argT (T, (_, (co, contra))) =
+ replicate (bool_num co + bool_num contra) (T --> T)
+ val Ts' = maps mk_argT (Ts ~~ variances)
+ val T = Type (tyco, Ts);
+ val x = Free ("a", T);
+ val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
+ map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
+ in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
+
+
+(* registering mappers *)
+
+fun register tyco mapper variances raw_concatenate raw_identity thy =
+ let
+ val (_, concatenate_prop) = make_concatenate_prop variances (tyco, mapper);
+ val (_, identity_prop) = make_identity_prop variances (tyco, mapper);
+ val concatenate = Goal.prove_global thy
+ (Term.add_free_names concatenate_prop []) [] concatenate_prop
+ (K (ALLGOALS (ProofContext.fact_tac [raw_concatenate])));
+ val identity = Goal.prove_global thy
+ (Term.add_free_names identity_prop []) [] identity_prop
+ (K (ALLGOALS (ProofContext.fact_tac [raw_identity])));
+ in
+ thy
+ |> Data.map (Symtab.update (tyco, { mapper = mapper,
+ variances = variances,
+ concatenate = concatenate, identity = identity }))
+ end;
+
+fun split_mapper_typ "fun" T =
+ let
+ val (Ts', T') = strip_type T;
+ val (Ts'', T'') = split_last Ts';
+ val (Ts''', T''') = split_last Ts'';
+ in (Ts''', T''', T'' --> T') end
+ | split_mapper_typ tyco T =
+ let
+ val (Ts', T') = strip_type T;
+ val (Ts'', T'') = split_last Ts';
+ in (Ts'', T'', T') end;
+
+fun analyze_variances thy tyco T =
+ let
+ fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
+ val (Ts, T1, T2) = split_mapper_typ tyco T
+ handle List.Empty => bad_typ ();
+ val _ = pairself
+ ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
+ val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
+ handle TYPE _ => bad_typ ();
+ val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
+ then bad_typ () else ();
+ in [] end;
+
+fun gen_type_mapper prep_term raw_t thy =
+ let
+ val (mapper, T) = case prep_term thy raw_t
+ of Const cT => cT
+ | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
+ val _ = Type.no_tvars T;
+ fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
+ | add_tycos _ = I;
+ val tycos = add_tycos T [];
+ val tyco = if tycos = ["fun"] then "fun"
+ else case remove (op =) "fun" tycos
+ of [tyco] => tyco
+ | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
+ val variances = analyze_variances thy tyco T;
+ val (_, concatenate_prop) = make_concatenate_prop variances (tyco, mapper);
+ val (_, identity_prop) = make_identity_prop variances (tyco, mapper);
+ fun after_qed [[concatenate], [identity]] lthy =
+ lthy
+ |> (Local_Theory.background_theory o Data.map)
+ (Symtab.update (tyco, { mapper = mapper, variances = variances,
+ concatenate = concatenate, identity = identity }));
+ in
+ thy
+ |> Named_Target.theory_init
+ |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [concatenate_prop, identity_prop])
+ end
+
+val type_mapper = gen_type_mapper Sign.cert_term;
+val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
+
+val _ =
+ Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
+ (Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
+
+end;
--- a/src/Pure/PIDE/command.scala Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Pure/PIDE/command.scala Wed Nov 17 06:49:23 2010 -0800
@@ -54,7 +54,9 @@
val props = Position.purge(atts)
val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
- case _ => System.err.println("Ignored report message: " + msg); state
+ case _ =>
+ // FIXME System.err.println("Ignored report message: " + msg)
+ state
})
case XML.Elem(Markup(name, atts), body) =>
atts match {
--- a/src/Pure/System/gui_setup.scala Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Pure/System/gui_setup.scala Wed Nov 17 06:49:23 2010 -0800
@@ -39,6 +39,7 @@
// values
if (Platform.is_windows)
text.append("Cygwin root: " + Cygwin.check_root() + "\n")
+ text.append("JVM name: " + System.getProperty("java.vm.name") + "\n")
text.append("JVM platform: " + Platform.jvm_platform + "\n")
try {
val isabelle_system = new Isabelle_System
--- a/src/Tools/cache_io.ML Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Tools/cache_io.ML Wed Nov 17 06:49:23 2010 -0800
@@ -13,6 +13,8 @@
output: string list,
redirected_output: string list,
return_code: int}
+ val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T ->
+ result
val run: (Path.T -> Path.T -> string) -> string -> result
(*cache*)
@@ -52,14 +54,16 @@
redirected_output: string list,
return_code: int}
+fun raw_run make_cmd str in_path out_path =
+ let
+ val _ = File.write in_path str
+ val (out2, rc) = bash_output (make_cmd in_path out_path)
+ val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
+ in {output=split_lines out2, redirected_output=out1, return_code=rc} end
+
fun run make_cmd str =
with_tmp_file cache_io_prefix (fn in_path =>
- with_tmp_file cache_io_prefix (fn out_path =>
- let
- val _ = File.write in_path str
- val (out2, rc) = bash_output (make_cmd in_path out_path)
- val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
- in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
+ with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
(* cache *)
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Tue Nov 16 16:36:57 2010 -0800
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Wed Nov 17 06:49:23 2010 -0800
@@ -24,7 +24,6 @@
echo " -m MODE add print mode for output"
echo
echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
- echo "(default ~/Scratch.thy)."
echo
exit 1
}
@@ -93,14 +92,10 @@
# args
-if [ "$#" -eq 0 ]; then
- ARGS["${#ARGS[@]}"]="Scratch.thy"
-else
- while [ "$#" -gt 0 ]; do
- ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
- shift
- done
-fi
+while [ "$#" -gt 0 ]; do
+ ARGS["${#ARGS[@]}"]="$(jvmpath "$1")"
+ shift
+done
## default perspective