--- a/NEWS Thu Jun 11 20:04:55 2009 -0700
+++ b/NEWS Thu Jun 11 20:19:26 2009 -0700
@@ -4,28 +4,38 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Discontinued old form of "escaped symbols" such as \\<forall>. Only
+one backslash should be used, even in ML sources.
+
+
*** Pure ***
-* On instantiation of classes, remaining undefined class parameters are
-formally declared. INCOMPATIBILITY.
+* On instantiation of classes, remaining undefined class parameters
+are formally declared. INCOMPATIBILITY.
*** HOL ***
-* Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1;
-theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
-div_mult_mult2 have been generalized to class semiring_div, subsuming former
-theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
-div_mult_mult1 is now [simp] by default. INCOMPATIBILITY.
-
-* Power operations on relations and functions are now one dedicate constant compow with
-infix syntax "^^". Power operations on multiplicative monoids retains syntax "^"
-and is now defined generic in class power. INCOMPATIBILITY.
-
-* ML antiquotation @{code_datatype} inserts definition of a datatype generated
-by the code generator; see Predicate.thy for an example.
-
-* New method "linarith" invokes existing linear arithmetic decision procedure only.
+* Class semiring_div requires superclass no_zero_divisors and proof of
+div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
+div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
+generalized to class semiring_div, subsuming former theorems
+zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
+zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
+INCOMPATIBILITY.
+
+* Power operations on relations and functions are now one dedicate
+constant compow with infix syntax "^^". Power operations on
+multiplicative monoids retains syntax "^" and is now defined generic
+in class power. INCOMPATIBILITY.
+
+* ML antiquotation @{code_datatype} inserts definition of a datatype
+generated by the code generator; see Predicate.thy for an example.
+
+* New method "linarith" invokes existing linear arithmetic decision
+procedure only.
*** ML ***
--- a/doc-src/Codegen/Thy/document/Introduction.tex Thu Jun 11 20:04:55 2009 -0700
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Thu Jun 11 20:19:26 2009 -0700
@@ -249,9 +249,9 @@
\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
-\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~(let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
-\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
+\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys) );\\
\hspace*{0pt}\\
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
--- a/doc-src/Codegen/Thy/document/Program.tex Thu Jun 11 20:04:55 2009 -0700
+++ b/doc-src/Codegen/Thy/document/Program.tex Thu Jun 11 20:19:26 2009 -0700
@@ -346,8 +346,8 @@
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}semigroup{\char95}monoid A{\char95};\\
\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
@@ -363,9 +363,8 @@
\hspace*{0pt}\\
\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat =\\
-\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\
-\hspace*{0pt} ~nat monoid;\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
+\hspace*{0pt} ~:~nat monoid;\\
\hspace*{0pt}\\
\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
\hspace*{0pt}\\
@@ -967,9 +966,9 @@
\noindent%
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~(let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys) );\\
\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/examples/Example.hs Thu Jun 11 20:04:55 2009 -0700
+++ b/doc-src/Codegen/Thy/examples/Example.hs Thu Jun 11 20:19:26 2009 -0700
@@ -23,9 +23,9 @@
dequeue (AQueue [] []) = (Nothing, AQueue [] []);
dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
dequeue (AQueue (v : va) []) =
- let {
+ (let {
(y : ys) = rev (v : va);
- } in (Just y, AQueue [] ys);
+ } in (Just y, AQueue [] ys) );
enqueue :: forall a. a -> Queue a -> Queue a;
enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
--- a/doc-src/antiquote_setup.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/doc-src/antiquote_setup.ML Thu Jun 11 20:19:26 2009 -0700
@@ -19,16 +19,16 @@
| "{" => "\\{"
| "|" => "$\\mid$"
| "}" => "\\}"
- | "\\<dash>" => "-"
+ | "\<dash>" => "-"
| c => c);
-fun clean_name "\\<dots>" = "dots"
+fun clean_name "\<dots>" = "dots"
| clean_name ".." = "ddot"
| clean_name "." = "dot"
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
- | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
+ | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
(* verbatim text *)
--- a/lib/scripts/getsettings Thu Jun 11 20:04:55 2009 -0700
+++ b/lib/scripts/getsettings Thu Jun 11 20:19:26 2009 -0700
@@ -51,10 +51,8 @@
if [ "$OSTYPE" = cygwin ]; then
CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
function jvmpath() { cygpath -w -p "$@"; }
- ISABELLE_ROOT_JVM="$(jvmpath /)"
else
function jvmpath() { echo "$@"; }
- ISABELLE_ROOT_JVM=/
fi
HOME_JVM="$HOME"
--- a/src/HOL/List.thy Thu Jun 11 20:04:55 2009 -0700
+++ b/src/HOL/List.thy Thu Jun 11 20:19:26 2009 -0700
@@ -2931,7 +2931,7 @@
done
-subsubsection {* Infiniteness *}
+subsubsection {* (In)finiteness *}
lemma finite_maxlen:
"finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
@@ -2944,6 +2944,27 @@
thus ?case ..
qed
+lemma finite_lists_length_eq:
+assumes "finite A"
+shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
+proof(induct n)
+ case 0 show ?case by simp
+next
+ case (Suc n)
+ have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
+ by (auto simp:length_Suc_conv)
+ then show ?case using `finite A`
+ by (auto intro: finite_imageI Suc) (* FIXME metis? *)
+qed
+
+lemma finite_lists_length_le:
+ assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
+ (is "finite ?S")
+proof-
+ have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
+ thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
+qed
+
lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
apply(rule notI)
apply(drule finite_maxlen)
--- a/src/HOL/ex/Predicate_Compile_ex.thy Thu Jun 11 20:04:55 2009 -0700
+++ b/src/HOL/ex/Predicate_Compile_ex.thy Thu Jun 11 20:19:26 2009 -0700
@@ -8,11 +8,9 @@
| "odd n \<Longrightarrow> even (Suc n)"
-(*
-code_pred even
- using assms by (rule even.cases)
-*)
-setup {* Predicate_Compile.add_equations @{const_name even} *}
+
+code_pred even .
+
thm odd.equation
thm even.equation
@@ -31,15 +29,7 @@
"rev [] []"
| "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys"
-setup {* Predicate_Compile.add_equations @{const_name rev} *}
-
-thm rev.equation
-thm append.equation
-
-(*
-code_pred append
- using assms by (rule append.cases)
-*)
+code_pred rev .
thm append.equation
@@ -54,36 +44,41 @@
| "f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) (x # ys) zs"
| "\<not> f x \<Longrightarrow> partition f xs ys zs \<Longrightarrow> partition f (x # xs) ys (x # zs)"
-setup {* Predicate_Compile.add_equations @{const_name partition} *}
+(* FIXME: correct handling of parameters *)
(*
-code_pred partition
- using assms by (rule partition.cases)
-*)
+ML {* reset Predicate_Compile.do_proofs *}
+code_pred partition .
thm partition.equation
-
-(*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
- [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}"*)
-
-setup {* Predicate_Compile.add_equations @{const_name tranclp} *}
-(*
-code_pred tranclp
- using assms by (rule tranclp.cases)
+ML {* set Predicate_Compile.do_proofs *}
*)
+(* TODO: requires to handle abstractions in parameter positions correctly *)
+(*FIXME values 10 "{(ys, zs). partition (\<lambda>n. n mod 2 = 0)
+ [0, Suc 0, 2, 3, 4, 5, 6, 7] ys zs}" *)
+
+thm tranclp.intros
+
+(*
+lemma [code_pred_intros]:
+"r a b ==> tranclp r a b"
+"r a b ==> tranclp r b c ==> tranclp r a c"
+by auto
+*)
+(*
+code_pred tranclp .
+
thm tranclp.equation
-
+*)
inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
-setup {* Predicate_Compile.add_equations @{const_name succ} *}
-(*
-code_pred succ
- using assms by (rule succ.cases)
-*)
+code_pred succ .
+
thm succ.equation
+(* TODO: requires alternative rules for trancl *)
(*
values 20 "{n. tranclp succ 10 n}"
values "{n. tranclp succ n 10}"
--- a/src/HOL/ex/predicate_compile.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/src/HOL/ex/predicate_compile.ML Thu Jun 11 20:19:26 2009 -0700
@@ -37,13 +37,17 @@
fun tracing s = (if ! Toplevel.debug then Output.tracing s else ());
fun print_tac s = (if ! Toplevel.debug then Tactical.print_tac s else Seq.single);
-fun debug_tac msg = (fn st => (tracing msg; Seq.single st));
+fun new_print_tac s = Tactical.print_tac s
+fun debug_tac msg = (fn st => (Output.tracing msg; Seq.single st));
val do_proofs = ref true;
fun mycheat_tac thy i st =
(Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
+fun remove_last_goal thy st =
+ (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
+
(* reference to preprocessing of InductiveSet package *)
val ind_set_codegen_preproc = InductiveSetPackage.codegen_preproc;
@@ -175,7 +179,10 @@
(* queries *)
-val lookup_pred_data = try rep_pred_data oo Graph.get_node o PredData.get;
+fun lookup_pred_data thy name =
+ case try (Graph.get_node (PredData.get thy)) name of
+ SOME pred_data => SOME (rep_pred_data pred_data)
+ | NONE => NONE
fun the_pred_data thy name = case lookup_pred_data thy name
of NONE => error ("No such predicate " ^ quote name)
@@ -730,21 +737,27 @@
val args = map Free (argnames ~~ (Ts1' @ Ts2))
val (params, io_args) = chop nparams args
val (inargs, outargs) = get_args (snd mode) io_args
+ val param_names = Name.variant_list argnames
+ (map (fn i => "p" ^ string_of_int i) (1 upto nparams))
+ val param_vs = map Free (param_names ~~ Ts1)
val (params', names) = fold_map mk_Eval_of ((params ~~ Ts1) ~~ (fst mode)) []
- val predprop = HOLogic.mk_Trueprop (list_comb (pred, params' @ io_args))
+ val predpropI = HOLogic.mk_Trueprop (list_comb (pred, param_vs @ io_args))
+ val predpropE = HOLogic.mk_Trueprop (list_comb (pred, params' @ io_args))
+ val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
val funargs = params @ inargs
val funpropE = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
mk_tuple outargs))
- val introtrm = Logic.mk_implies (predprop, funpropI)
+ val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
+ val _ = Output.tracing (Syntax.string_of_term_global thy introtrm)
val simprules = [defthm, @{thm eval_pred},
@{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}]
val unfolddef_tac = (Simplifier.asm_full_simp_tac (HOL_basic_ss addsimps simprules) 1)
- val introthm = Goal.prove (ProofContext.init thy) (argnames @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
+ val introthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y"]) [] introtrm (fn {...} => unfolddef_tac)
val P = HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT));
- val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predprop, P)], P)
- val elimthm = Goal.prove (ProofContext.init thy) (argnames @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
+ val elimtrm = Logic.list_implies ([funpropE, Logic.mk_implies (predpropE, P)], P)
+ val elimthm = Goal.prove (ProofContext.init thy) (argnames @ param_names @ ["y", "P"]) [] elimtrm (fn {...} => unfolddef_tac)
in
(introthm, elimthm)
end;
@@ -789,6 +802,7 @@
in thy' |> add_predfun name mode (mode_id, definition, intro, elim)
|> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "I"), intro) |> snd
|> PureThy.store_thm (Binding.name (Long_Name.base_name mode_id ^ "E"), elim) |> snd
+ |> Theory.checkpoint
end;
in
fold create_definition modes thy
@@ -853,8 +867,19 @@
(* MAJOR FIXME: prove_params should be simple
- different form of introrule for parameters ? *)
-fun prove_param thy modes (NONE, t) = all_tac
- | prove_param thy modes (m as SOME (Mode (mode, is, ms)), t) = let
+fun prove_param thy modes (NONE, t) =
+ all_tac
+| prove_param thy modes (m as SOME (Mode (mode, is, ms)), t) =
+ REPEAT_DETERM (etac @{thm thin_rl} 1)
+ THEN REPEAT_DETERM (rtac @{thm ext} 1)
+ THEN (rtac @{thm iffI} 1)
+ THEN new_print_tac "prove_param"
+ (* proof in one direction *)
+ THEN (atac 1)
+ (* proof in the other direction *)
+ THEN (atac 1)
+ THEN new_print_tac "after prove_param"
+(* let
val (f, args) = strip_comb t
val (params, _) = chop (length ms) args
val f_tac = case f of
@@ -867,11 +892,10 @@
print_tac "before simplification in prove_args:"
THEN f_tac
THEN print_tac "after simplification in prove_args"
- (* work with parameter arguments *)
THEN (EVERY (map (prove_param thy modes) (ms ~~ params)))
THEN (REPEAT_DETERM (atac 1))
end
-
+*)
fun prove_expr thy modes (SOME (Mode (mode, is, ms)), t, us) (premposition : int) =
(case strip_comb t of
(Const (name, T), args) =>
@@ -892,8 +916,10 @@
(* for the right assumption in first position *)
THEN rotate_tac premposition 1
THEN rtac introrule 1
- THEN print_tac "after intro rule"
+ THEN new_print_tac "after intro rule"
(* work with parameter arguments *)
+ THEN (atac 1)
+ THEN (new_print_tac "parameter goal")
THEN (EVERY (map (prove_param thy modes) (ms ~~ args1)))
THEN (REPEAT_DETERM (atac 1)) end)
else error "Prove expr if case not implemented"
@@ -1027,7 +1053,7 @@
val nargs = length (binder_types T) - nparams_of thy pred
val pred_case_rule = singleton (ind_set_codegen_preproc thy)
(preprocess_elim thy nargs (the_elim_of thy pred))
- (* FIXME preprocessor |> Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}])*)
+ (* FIXME preprocessor |> Simplifier.full_simplify (HOL_basic_ss addsimps [@{thm Predicate.memb_code}])*)
in
REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
THEN etac (predfun_elim_of thy pred mode) 1
@@ -1036,6 +1062,7 @@
(fn i => EVERY' (select_sup (length clauses) i) i)
(1 upto (length clauses))))
THEN (EVERY (map (prove_clause thy nargs all_vs param_vs modes mode) clauses))
+ THEN new_print_tac "proved one direction"
end;
(*******************************************************************************************************)
@@ -1068,7 +1095,8 @@
(* VERY LARGE SIMILIRATIY to function prove_param
-- join both functions
-*)
+*)
+(*
fun prove_param2 thy modes (NONE, t) = all_tac
| prove_param2 thy modes (m as SOME (Mode (mode, is, ms)), t) = let
val (f, args) = strip_comb t
@@ -1082,9 +1110,9 @@
print_tac "before simplification in prove_args:"
THEN f_tac
THEN print_tac "after simplification in prove_args"
- (* work with parameter arguments *)
THEN (EVERY (map (prove_param2 thy modes) (ms ~~ params)))
end
+*)
fun prove_expr2 thy modes (SOME (Mode (mode, is, ms)), t) =
(case strip_comb t of
@@ -1092,8 +1120,14 @@
if AList.defined op = modes name then
etac @{thm bindE} 1
THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
+ THEN (debug_tac (Syntax.string_of_term_global thy
+ (prop_of (predfun_elim_of thy name mode))))
THEN (etac (predfun_elim_of thy name mode) 1)
- THEN (EVERY (map (prove_param2 thy modes) (ms ~~ args)))
+ THEN new_print_tac "prove_expr2"
+ (* TODO -- FIXME: replace remove_last_goal*)
+ THEN (EVERY (replicate (length args) (remove_last_goal thy)))
+ THEN new_print_tac "finished prove_expr2"
+ (* THEN (EVERY (map (prove_param thy modes) (ms ~~ args))) *)
else error "Prove expr2 if case not implemented"
| _ => etac @{thm bindE} 1)
| prove_expr2 _ _ _ = error "Prove expr2 not implemented"
@@ -1172,7 +1206,7 @@
THEN (if is_some name then
full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) (iss, js)]) 1
THEN etac @{thm not_predE} 1
- THEN (EVERY (map (prove_param2 thy modes) (param_modes ~~ params)))
+ THEN (EVERY (map (prove_param thy modes) (param_modes ~~ params)))
else
etac @{thm not_predE'} 1)
THEN rec_tac
@@ -1247,6 +1281,7 @@
fun prepare_intrs thy prednames =
let
+ (* FIXME: preprocessing moved to fetch_pred_data *)
val intrs = map (preprocess_intro thy) (maps (intros_of thy) prednames)
|> ind_set_codegen_preproc thy (*FIXME preprocessor
|> map (Simplifier.full_simplify (HOL_basic_ss addsimps [@ {thm Predicate.memb_code}]))*)
@@ -1309,11 +1344,13 @@
prepare_intrs thy prednames
val _ = tracing "Infering modes..."
val modes = infer_modes thy extra_modes arities param_vs clauses
+ val _ = print_modes modes
val _ = tracing "Defining executable functions..."
- val thy' = fold (create_definitions preds nparams) modes thy
+ val thy' = fold (create_definitions preds nparams) modes thy |> Theory.checkpoint
val clauses' = map (fn (s, cls) => (s, (the (AList.lookup (op =) preds s), cls))) clauses
val _ = tracing "Compiling equations..."
val ts = compile_preds thy' all_vs param_vs (extra_modes @ modes) clauses'
+ val _ = map (Output.tracing o (Syntax.string_of_term_global thy')) (flat ts)
val pred_mode =
maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses'
val _ = tracing "Proving equations..."
@@ -1323,13 +1360,14 @@
[((Binding.qualify true (Long_Name.base_name name) (Binding.name "equation"), result_thms),
[Attrib.attribute_i thy Code.add_default_eqn_attrib])] thy))
(arrange ((map (fn ((name, _), _) => name) pred_mode) ~~ result_thms)) thy'
+ |> Theory.checkpoint
in
thy''
end
(* generation of case rules from user-given introduction rules *)
-fun mk_casesrule introrules nparams ctxt =
+fun mk_casesrule ctxt nparams introrules =
let
val intros = map prop_of introrules
val (pred, (params, args)) = strip_intro_concl nparams (hd intros)
@@ -1349,10 +1387,7 @@
in fold Logic.all frees (Logic.list_implies (eqprems @ prems, prop)) end
val assm = HOLogic.mk_Trueprop (list_comb (pred, params @ argvs))
val cases = map mk_case intros
- val (_, ctxt3) = ProofContext.add_assms_i Assumption.assume_export
- [((Binding.name AutoBind.assmsN, []), map (fn t => (t, [])) (assm :: cases))]
- ctxt2
- in (pred, prop, ctxt3) end;
+ in Logic.list_implies (assm :: cases, prop) end;
(* code dependency graph *)
@@ -1364,7 +1399,7 @@
let
val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
in (fst (dest_Const const) = name) end;
- val intros = filter is_intro_of (#intrs result)
+ val intros = map (preprocess_intro thy) (filter is_intro_of (#intrs result))
val elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info)))
val nparams = length (InductivePackage.params_of (#raw_induct result))
in mk_pred_data ((intros, SOME elim, nparams), []) end
@@ -1384,7 +1419,7 @@
fun add_equations name thy =
let
- val thy' = PredData.map (Graph.extend (dependencies_of thy) [name]) thy;
+ val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy |> Theory.checkpoint;
(*val preds = Graph.all_preds (PredData.get thy') [name] |> filter_out (has_elim thy') *)
fun strong_conn_of gr keys =
Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
@@ -1392,7 +1427,7 @@
val thy'' = fold_rev
(fn preds => fn thy =>
if forall (null o modes_of thy) preds then add_equations_of preds thy else thy)
- scc thy'
+ scc thy' |> Theory.checkpoint
in thy'' end
(** user interface **)
@@ -1410,38 +1445,25 @@
(* TODO: must create state to prove multiple cases *)
fun generic_code_pred prep_const raw_const lthy =
let
- val thy = (ProofContext.theory_of lthy)
+
+ val thy = ProofContext.theory_of lthy
val const = prep_const thy raw_const
- val lthy' = lthy
- val thy' = PredData.map (Graph.extend (dependencies_of thy) [const]) thy
+
+ val lthy' = LocalTheory.theory (PredData.map (Graph.extend (dependencies_of thy) const)) lthy
+ |> LocalTheory.checkpoint
+ val thy' = ProofContext.theory_of lthy'
val preds = Graph.all_preds (PredData.get thy') [const] |> filter_out (has_elim thy')
- val _ = Output.tracing ("preds: " ^ commas preds)
- (*
- fun mk_elim pred =
+
+ fun mk_cases const =
let
- val nparams = nparams_of thy pred
- val intros = intros_of thy pred
- val (((tfrees, frees), fact), lthy'') =
- Variable.import_thms true intros lthy';
- val (pred, prop, lthy''') = mk_casesrule fact nparams lthy''
- in (pred, prop, lthy''') end;
-
- val (predname, _) = dest_Const pred
- *)
- val nparams = nparams_of thy' const
- val intros = intros_of thy' const
- val (((tfrees, frees), fact), lthy'') =
- Variable.import_thms true intros lthy';
- val (pred, prop, lthy''') = mk_casesrule fact nparams lthy''
- val (predname, _) = dest_Const pred
- fun after_qed [[th]] lthy''' =
- lthy'''
- |> LocalTheory.note Thm.generatedK
- ((Binding.empty, []), [th])
- |> snd
- |> LocalTheory.theory (add_equations_of [predname])
+ val nparams = nparams_of thy' const
+ val intros = intros_of thy' const
+ in mk_casesrule lthy' nparams intros end
+ val cases_rules = map mk_cases preds
+ fun after_qed thms =
+ LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations const)
in
- Proof.theorem_i NONE after_qed [[(prop, [])]] lthy'''
+ Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'
end;
structure P = OuterParse
--- a/src/Pure/General/graph.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/General/graph.ML Thu Jun 11 20:19:26 2009 -0700
@@ -48,8 +48,7 @@
val topological_order: 'a T -> key list
val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*)
val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*)
- val extend: (key -> 'a * key list) -> key list -> 'a T -> 'a T
- val make: (key -> 'a * key list) -> key list -> 'a T
+ val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
end;
functor GraphFun(Key: KEY): GRAPH =
@@ -277,24 +276,21 @@
|> fold add_edge_trans_acyclic (diff_edges G1 G2)
|> fold add_edge_trans_acyclic (diff_edges G2 G1);
-
+
(* constructing graphs *)
fun extend explore =
let
- fun contains_node gr key = member eq_key (keys gr) key
- fun extend' key gr =
- let
- val (node, preds) = explore key
- in
- gr |> (not (contains_node gr key)) ?
- (new_node (key, node)
- #> fold extend' preds
- #> fold (add_edge o (pair key)) preds)
- end
- in fold extend' end
-
-fun make explore keys = extend explore keys empty
+ fun ext x G =
+ if can (get_entry G) x then G
+ else
+ let val (info, ys) = explore x in
+ G
+ |> new_node (x, info)
+ |> fold ext ys
+ |> fold (fn y => add_edge (x, y)) ys
+ end
+ in ext end;
(*final declarations of this structure!*)
--- a/src/Pure/General/symbol.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/General/symbol.ML Thu Jun 11 20:19:26 2009 -0700
@@ -433,7 +433,7 @@
val scan_encoded_newline =
$$ "\^M" -- $$ "\n" >> K "\n" ||
$$ "\^M" >> K "\n" ||
- $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
+ Scan.this_string "\\<^newline>" >> K "\n";
val scan_raw =
Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
@@ -442,7 +442,7 @@
val scan =
Scan.one is_plain ||
scan_encoded_newline ||
- (($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
+ ($$ "\\" ^^ $$ "<" ^^
!! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
(($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
Scan.one not_eof;
@@ -453,7 +453,7 @@
Scan.this_string "{*" || Scan.this_string "*}";
val recover =
- (Scan.this (explode "\\\\<") || Scan.this (explode "\\<")) @@@
+ Scan.this ["\\", "<"] @@@
Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))
>> (fn ss => malformed :: ss @ [end_malformed]);
--- a/src/Pure/General/symbol.scala Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/General/symbol.scala Thu Jun 11 20:19:26 2009 -0700
@@ -6,37 +6,47 @@
package isabelle
-import java.util.regex.Pattern
-import java.io.File
import scala.io.Source
-import scala.collection.jcl.HashMap
+import scala.collection.jcl
+import scala.util.matching.Regex
-object Symbol {
+object Symbol
+{
/** Symbol regexps **/
- private def compile(s: String) =
- Pattern.compile(s, Pattern.COMMENTS | Pattern.DOTALL)
+ private val plain = new Regex("""(?xs)
+ [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
- private val plain_pattern = compile(""" [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
-
- private val symbol_pattern = compile(""" \\ \\? < (?:
+ private val symbol = new Regex("""(?xs)
+ \\ < (?:
\^? [A-Za-z][A-Za-z0-9_']* |
\^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
- private val bad_symbol_pattern = compile("(?!" + symbol_pattern + ")" +
- """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
+ private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
+ """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
// total pattern
- val pattern = compile(plain_pattern + "|" + symbol_pattern + "|" + bad_symbol_pattern + "| .")
+ val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
+ // prefix of another symbol
+ def is_open(s: String): Boolean =
+ {
+ val len = s.length
+ len == 1 && Character.isHighSurrogate(s(0)) ||
+ s == "\\" ||
+ s == "\\<" ||
+ len > 2 && s(len - 1) != '>'
+ }
/** Recoding **/
- private class Recoder(list: List[(String, String)]) {
- private val (min, max) = {
+ private class Recoder(list: List[(String, String)])
+ {
+ private val (min, max) =
+ {
var min = '\uffff'
var max = '\u0000'
for ((x, _) <- list) {
@@ -46,14 +56,16 @@
}
(min, max)
}
- private val table = {
- val table = new HashMap[String, String]
+ private val table =
+ {
+ val table = new jcl.HashMap[String, String] // reasonably efficient?
for ((x, y) <- list) table + (x -> y)
table
}
- def recode(text: String) = {
+ def recode(text: String): String =
+ {
val len = text.length
- val matcher = pattern.matcher(text)
+ val matcher = regex.pattern.matcher(text)
val result = new StringBuilder(len)
var i = 0
while (i < len) {
@@ -62,10 +74,7 @@
matcher.region(i, len)
matcher.lookingAt
val x = matcher.group
- table.get(x) match {
- case Some(y) => result.append(y)
- case None => result.append(x)
- }
+ result.append(table.get(x) getOrElse x)
i = matcher.end
}
else { result.append(c); i += 1 }
@@ -80,75 +89,56 @@
class Interpretation(symbol_decls: Iterator[String])
{
- private val symbols = new HashMap[String, HashMap[String, String]]
- private var decoder: Recoder = null
- private var encoder: Recoder = null
+ /* read symbols */
+
+ private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
+ private val key = new Regex("""(?xs) (.+): """)
+
+ private def read_decl(decl: String): (String, Map[String, String]) =
+ {
+ def err() = error("Bad symbol declaration: " + decl)
+
+ def read_props(props: List[String]): Map[String, String] =
+ {
+ props match {
+ case Nil => Map()
+ case _ :: Nil => err()
+ case key(x) :: y :: rest => read_props(rest) + (x -> y)
+ case _ => err()
+ }
+ }
+ decl.split("\\s+").toList match {
+ case Nil => err()
+ case sym :: props => (sym, read_props(props))
+ }
+ }
+
+ private val symbols: List[(String, Map[String, String])] =
+ for (decl <- symbol_decls.toList if !empty.pattern.matcher(decl).matches)
+ yield read_decl(decl)
+
+
+ /* main recoder methods */
+
+ private val (decoder, encoder) =
+ {
+ val mapping =
+ for {
+ (sym, props) <- symbols
+ val code =
+ try { Integer.decode(props("code")).intValue }
+ catch {
+ case _: NoSuchElementException => error("Missing code for symbol " + sym)
+ case _: NumberFormatException => error("Bad code for symbol " + sym)
+ }
+ val ch = new String(Character.toChars(code))
+ } yield (sym, ch)
+ (new Recoder(mapping),
+ new Recoder(mapping map { case (x, y) => (y, x) }))
+ }
def decode(text: String) = decoder.recode(text)
def encode(text: String) = encoder.recode(text)
-
- /* read symbols */
-
- private val empty_pattern = compile(""" ^\s* (?: \#.* )? $ """)
- private val blank_pattern = compile(""" \s+ """)
- private val key_pattern = compile(""" (.+): """)
-
- private def read_decl(decl: String) = {
- def err() = error("Bad symbol declaration: " + decl)
-
- def read_props(props: List[String], tab: HashMap[String, String])
- {
- props match {
- case Nil => ()
- case _ :: Nil => err()
- case key :: value :: rest => {
- val key_matcher = key_pattern.matcher(key)
- if (key_matcher.matches) {
- tab + (key_matcher.group(1) -> value)
- read_props(rest, tab)
- }
- else err ()
- }
- }
- }
-
- if (!empty_pattern.matcher(decl).matches) {
- blank_pattern.split(decl).toList match {
- case Nil => err()
- case symbol :: props => {
- val tab = new HashMap[String, String]
- read_props(props, tab)
- symbols + (symbol -> tab)
- }
- }
- }
- }
-
-
- /* init tables */
-
- private def get_code(entry: (String, HashMap[String, String])) = {
- val (symbol, props) = entry
- val code =
- try { Integer.decode(props("code")).intValue }
- catch {
- case _: NoSuchElementException => error("Missing code for symbol " + symbol)
- case _: NumberFormatException => error("Bad code for symbol " + symbol)
- }
- (symbol, new String(Character.toChars(code)))
- }
-
- private def init_recoders() = {
- val list = symbols.elements.toList.map(get_code)
- decoder = new Recoder(list ++ (for ((x, y) <- list) yield ("\\" + x, y)))
- encoder = new Recoder(for ((x, y) <- list) yield (y, x))
- }
-
-
- /* constructor */
-
- symbol_decls.foreach(read_decl)
- init_recoders()
}
}
--- a/src/Pure/General/yxml.scala Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/General/yxml.scala Thu Jun 11 20:19:26 2009 -0700
@@ -6,8 +6,6 @@
package isabelle
-import java.util.regex.Pattern
-
object YXML {
--- a/src/Pure/ML/ml_lex.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/ML/ml_lex.ML Thu Jun 11 20:19:26 2009 -0700
@@ -247,7 +247,11 @@
Symbol_Pos.source (Position.line 1) src
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
-val tokenize = Source.of_string #> source #> Source.exhaust;
+val tokenize =
+ Source.of_string #>
+ Symbol.source {do_recover = true} #>
+ source #>
+ Source.exhaust;
fun read_antiq (syms, pos) =
(Source.of_list syms
--- a/src/Pure/ML/ml_syntax.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/ML/ml_syntax.ML Thu Jun 11 20:19:26 2009 -0700
@@ -58,7 +58,7 @@
| print_option f (SOME x) = "SOME (" ^ f x ^ ")";
fun print_char s =
- if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
+ if not (Symbol.is_char s) then s
else if s = "\"" then "\\\""
else if s = "\\" then "\\\\"
else
@@ -68,7 +68,7 @@
else "\\" ^ string_of_int c
end;
-val print_string = quote o translate_string print_char;
+val print_string = quote o implode o map print_char o Symbol.explode;
val print_strings = print_list print_string;
val print_properties = print_list (print_pair print_string print_string);
--- a/src/Pure/Syntax/syn_trans.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/Syntax/syn_trans.ML Thu Jun 11 20:19:26 2009 -0700
@@ -223,7 +223,7 @@
fun the_struct structs i =
if 1 <= i andalso i <= length structs then nth structs (i - 1)
- else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
+ else error ("Illegal reference to implicit structure #" ^ string_of_int i);
fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
Lexicon.free (the_struct structs 1)
@@ -503,7 +503,7 @@
val exn_results = map (Exn.capture ast_of) pts;
val exns = map_filter Exn.get_exn exn_results;
val results = map_filter Exn.get_result exn_results
- in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
+ in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
@@ -534,6 +534,6 @@
val exn_results = map (Exn.capture (term_of #> free_fixed)) asts;
val exns = map_filter Exn.get_exn exn_results;
val results = map_filter Exn.get_result exn_results
- in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
+ in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
end;
--- a/src/Pure/System/isabelle_system.scala Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/System/isabelle_system.scala Thu Jun 11 20:19:26 2009 -0700
@@ -6,10 +6,11 @@
package isabelle
-import java.util.regex.{Pattern, Matcher}
+import java.util.regex.Pattern
import java.io.{BufferedReader, InputStreamReader, FileInputStream, File, IOException}
import scala.io.Source
+import scala.util.matching.Regex
object IsabelleSystem
@@ -58,16 +59,15 @@
/* Isabelle settings environment */
- private val (cygdrive_pattern, cygwin_root, shell_prefix) =
+ private val (platform_root, drive_prefix, shell_prefix) =
{
if (IsabelleSystem.is_cygwin) {
- val cygdrive = Cygwin.cygdrive getOrElse "/cygdrive"
- val pattern = Pattern.compile(cygdrive + "/([a-zA-Z])($|/.*)")
- val root = Cygwin.root getOrElse "C:\\cygwin"
- val bash = List(root + "\\bin\\bash", "-l")
- (Some(pattern), Some(root), bash)
+ val root = Cygwin.root() getOrElse "C:\\cygwin"
+ val drive = Cygwin.cygdrive() getOrElse "/cygdrive"
+ val shell = List(root + "\\bin\\bash", "-l")
+ (root, drive, shell)
}
- else (None, None, Nil)
+ else ("/", "", Nil)
}
private val environment: Map[String, String] =
@@ -117,39 +117,33 @@
/* file path specifications */
+ private val Cygdrive = new Regex(
+ if (drive_prefix == "") "\0"
+ else Pattern.quote(drive_prefix) + "/([a-zA-Z])($|/.*)")
+
def platform_path(source_path: String): String =
{
val result_path = new StringBuilder
- def init_plain(path: String): String =
- {
- if (path.startsWith("/")) {
- result_path.length = 0
- result_path.append(getenv_strict("ISABELLE_ROOT_JVM"))
- path.substring(1)
- }
- else path
- }
def init(path: String): String =
{
- cygdrive_pattern match {
- case Some(pattern) =>
- val cygdrive = pattern.matcher(path)
- if (cygdrive.matches) {
- result_path.length = 0
- result_path.append(cygdrive.group(1))
- result_path.append(":")
- result_path.append(File.separator)
- cygdrive.group(2)
- }
- else init_plain(path)
- case None => init_plain(path)
+ path match {
+ case Cygdrive(drive, rest) =>
+ result_path.length = 0
+ result_path.append(drive)
+ result_path.append(":")
+ result_path.append(File.separator)
+ rest
+ case _ if (path.startsWith("/")) =>
+ result_path.length = 0
+ result_path.append(platform_root)
+ path.substring(1)
+ case _ => path
}
}
-
def append(path: String)
{
- for (p <- init(path).split("/")) {
+ for (p <- init(path) split "/") {
if (p != "") {
val len = result_path.length
if (len > 0 && result_path(len - 1) != File.separatorChar)
@@ -158,7 +152,7 @@
}
}
}
- for (p <- init(source_path).split("/")) {
+ for (p <- init(source_path) split "/") {
if (p.startsWith("$")) append(getenv_strict(p.substring(1)))
else if (p == "~") append(getenv_strict("HOME"))
else if (p == "~~") append(getenv_strict("ISABELLE_HOME"))
--- a/src/Pure/Thy/thy_info.ML Thu Jun 11 20:04:55 2009 -0700
+++ b/src/Pure/Thy/thy_info.ML Thu Jun 11 20:19:26 2009 -0700
@@ -387,7 +387,7 @@
(case Graph.get_node tasks name of
Task body =>
let val after_load = body ()
- in after_load () handle exn => (kill_thy name; raise exn) end
+ in after_load () handle exn => (kill_thy name; reraise exn) end
| _ => ()));
in