# HG changeset patch # User huffman # Date 1244776766 25200 # Node ID 809dfb3d9c76cb1571da166515bb96a7fdb2a79a # Parent fd09da74183392de9e40ef9f835e2286f0cef730# Parent 4e36f2f17c636479f821dc772d3ced5dbdf465f5 merged diff -r fd09da741833 -r 809dfb3d9c76 NEWS --- 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 \\. 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 *** diff -r fd09da741833 -r 809dfb3d9c76 doc-src/Codegen/Thy/document/Introduction.tex --- 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;\\ diff -r fd09da741833 -r 809dfb3d9c76 doc-src/Codegen/Thy/document/Program.tex --- 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% diff -r fd09da741833 -r 809dfb3d9c76 doc-src/Codegen/Thy/examples/Example.hs --- 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; diff -r fd09da741833 -r 809dfb3d9c76 doc-src/antiquote_setup.ML --- 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$" | "}" => "\\}" - | "\\" => "-" + | "\" => "-" | c => c); -fun clean_name "\\" = "dots" +fun clean_name "\" = "dots" | clean_name ".." = "ddot" | clean_name "." = "dot" | clean_name "_" = "underscore" | clean_name "{" = "braceleft" | clean_name "}" = "braceright" - | clean_name s = s |> translate (fn "_" => "-" | "\\" => "-" | c => c); + | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | c => c); (* verbatim text *) diff -r fd09da741833 -r 809dfb3d9c76 lib/scripts/getsettings --- 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" diff -r fd09da741833 -r 809dfb3d9c76 src/HOL/List.thy --- 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 \ A \ length xs = n}" (is "finite (?S n)") +proof(induct n) + case 0 show ?case by simp +next + case (Suc n) + have "?S (Suc n) = (\x\A. (\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 \ A \ length xs \ n}" + (is "finite ?S") +proof- + have "?S = (\n\{0..n}. {xs. set xs \ A \ 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) diff -r fd09da741833 -r 809dfb3d9c76 src/HOL/ex/Predicate_Compile_ex.thy --- 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 \ 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 \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ 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 (\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 (\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 \ nat \ bool" where "succ 0 1" | "succ m n \ 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}" diff -r fd09da741833 -r 809dfb3d9c76 src/HOL/ex/ROOT.ML diff -r fd09da741833 -r 809dfb3d9c76 src/HOL/ex/predicate_compile.ML --- 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 diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/General/graph.ML --- 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!*) diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/General/symbol.ML --- 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]); diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/General/symbol.scala --- 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() } } diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/General/yxml.scala --- 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 { diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/ML/ml_lex.ML --- 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 diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/ML/ml_syntax.ML --- 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); diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/Syntax/syn_trans.ML --- 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; diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/System/isabelle_system.scala --- 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")) diff -r fd09da741833 -r 809dfb3d9c76 src/Pure/Thy/thy_info.ML --- 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