# HG changeset patch # User huffman # Date 1244901831 25200 # Node ID dc65b2f786647a68f1dad36adc84c78592197488 # Parent 61ee6256d863254f510c3e5a4daa6920ab667c84# Parent 91644309417c805f48ae181737588953775052dd merged diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/annomaly.ML --- a/Admin/isatest/annomaly.ML Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/annomaly.ML Sat Jun 13 07:03:51 2009 -0700 @@ -1,5 +1,4 @@ (* Title: Admin/isatest/annomaly.ML - ID: $Id$ Author: Martin von Gagern *) diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/isatest-annomaly --- a/Admin/isatest/isatest-annomaly Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/isatest-annomaly Sat Jun 13 07:03:51 2009 -0700 @@ -1,7 +1,5 @@ #!/usr/bin/env bash # -# $Id$ -# # Create AnnoMaLy documentation for Isabelle # # Based on http://martin.von-gagern.net/projects/annomaly/ diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/isatest-check --- a/Admin/isatest/isatest-check Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/isatest-check Sat Jun 13 07:03:51 2009 -0700 @@ -1,6 +1,5 @@ #!/usr/bin/env bash # -# $Id$ # Author: Gerwin Klein, TU Muenchen # # DESCRIPTION: sends email for failed tests, checks for error.log, diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/isatest-doc --- a/Admin/isatest/isatest-doc Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/isatest-doc Sat Jun 13 07:03:51 2009 -0700 @@ -1,6 +1,5 @@ #!/usr/bin/env bash # -# $Id$ # Author: Gerwin Klein, NICTA # # Run IsaMakefile for every Doc/ subdirectory. diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/isatest-lint --- a/Admin/isatest/isatest-lint Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/isatest-lint Sat Jun 13 07:03:51 2009 -0700 @@ -1,6 +1,5 @@ #!/usr/bin/env perl # -# $Id$ # Author: Florian Haftmann, TUM # # Do consistency and quality checks on the isabelle sources diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/isatest-makeall --- a/Admin/isatest/isatest-makeall Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/isatest-makeall Sat Jun 13 07:03:51 2009 -0700 @@ -1,6 +1,5 @@ #!/usr/bin/env bash # -# $Id$ # Author: Gerwin Klein, TU Muenchen # # DESCRIPTION: Run isabelle makeall from specified distribution and settings. @@ -71,14 +70,19 @@ NICE="nice" ;; + macbroy2) + MFLAGS="" + NICE="" + ;; + macbroy5) MFLAGS="-j 2" NICE="" ;; macbroy23) - MFLAGS="" - NICE="" + MFLAGS="-j 2" + NICE="nice" ;; macbroy2[0-9]) diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/isatest-makedist --- a/Admin/isatest/isatest-makedist Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/isatest-makedist Sat Jun 13 07:03:51 2009 -0700 @@ -1,6 +1,5 @@ #!/usr/bin/env bash # -# $Id$ # Author: Gerwin Klein, TU Muenchen # # DESCRIPTION: Build distribution and run isatest-make for lots of platforms. @@ -14,7 +13,6 @@ MAKEDIST=$HOME/bin/makedist MAKEALL=$HOME/bin/isatest-makeall TAR=tar -CVS2CL="$HOME/bin/cvs2cl --follow-only TRUNK" SSH="ssh -f" @@ -46,7 +44,6 @@ rm -f $RUNNING/*.runnning export DISTPREFIX -export CVS2CL DATE=$(date "+%Y-%m-%d") DISTLOG=$LOGPREFIX/isatest-makedist-$DATE.log @@ -109,9 +106,11 @@ sleep 15 $SSH atbroy101 "$MAKEALL $HOME/settings/at64-poly" sleep 15 +$SSH macbroy2 "$MAKEALL $HOME/settings/at-mac-poly-5.1-para; $MAKEALL $HOME/settings/mac-poly-M8" +sleep 15 $SSH macbroy5 "$MAKEALL $HOME/settings/mac-poly" sleep 15 -$SSH macbroy6 "/usr/stud/isatest/bin/isatest-makeall $HOME/settings/at-mac-poly-5.1-para" +$SSH macbroy6 "$MAKEALL $HOME/settings/mac-poly-M4" sleep 15 $SSH atbroy51 "$HOME/admin/isatest/isatest-annomaly" diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/isatest-settings --- a/Admin/isatest/isatest-settings Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/isatest-settings Sat Jun 13 07:03:51 2009 -0700 @@ -1,5 +1,5 @@ # -*- shell-script -*- :mode=shellscript: -# $Id$ +# # Author: Gerwin Klein, NICTA # # DESCRIPTION: common settings for the isatest-* scripts diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/pmail --- a/Admin/isatest/pmail Fri Jun 12 22:30:37 2009 -0700 +++ b/Admin/isatest/pmail Sat Jun 13 07:03:51 2009 -0700 @@ -1,6 +1,5 @@ #!/usr/bin/env bash # -# $Id$ # Author: Gerwin Klein, TU Muenchen # # DESCRIPTION: send email with text attachments. diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/settings/mac-poly-M4 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/mac-poly-M4 Sat Jun 13 07:03:51 2009 -0700 @@ -0,0 +1,28 @@ +# -*- shell-script -*- :mode=shellscript: + + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-experimental" + ML_PLATFORM="x86-darwin" + ML_HOME="$POLYML_HOME/$ML_PLATFORM" + ML_OPTIONS="--mutable 800 --immutable 2000" + + +ISABELLE_HOME_USER=~/isabelle-mac-poly-M4 + +# Where to look for isabelle tools (multiple dirs separated by ':'). +ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" + +# Location for temporary files (should be on a local file system). +ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" + + +# Heap input locations. ML system identifier is included in lookup. +ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" + +# Heap output location. ML system identifier is appended automatically later on. +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" + +ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4" + +HOL_USEDIR_OPTIONS="-p 2 -Q false" diff -r 61ee6256d863 -r dc65b2f78664 Admin/isatest/settings/mac-poly-M8 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/isatest/settings/mac-poly-M8 Sat Jun 13 07:03:51 2009 -0700 @@ -0,0 +1,28 @@ +# -*- shell-script -*- :mode=shellscript: + + POLYML_HOME="/home/polyml/polyml-svn" + ML_SYSTEM="polyml-experimental" + ML_PLATFORM="x86-darwin" + ML_HOME="$POLYML_HOME/$ML_PLATFORM" + ML_OPTIONS="--mutable 800 --immutable 2000" + + +ISABELLE_HOME_USER=~/isabelle-mac-poly-M8 + +# Where to look for isabelle tools (multiple dirs separated by ':'). +ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" + +# Location for temporary files (should be on a local file system). +ISABELLE_TMP_PREFIX="/tmp/isabelle-$USER" + + +# Heap input locations. ML system identifier is included in lookup. +ISABELLE_PATH="$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps" + +# Heap output location. ML system identifier is appended automatically later on. +ISABELLE_OUTPUT="$ISABELLE_HOME_USER/heaps" +ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info" + +ISABELLE_USEDIR_OPTIONS="-i false -d false -M 8" + +HOL_USEDIR_OPTIONS="-p 2 -Q false" diff -r 61ee6256d863 -r dc65b2f78664 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Jun 12 22:30:37 2009 -0700 +++ b/src/HOL/Transitive_Closure.thy Sat Jun 13 07:03:51 2009 -0700 @@ -486,6 +486,28 @@ lemmas tranclD = tranclpD [to_set] +lemma converse_tranclpE: + assumes major: "tranclp r x z" + assumes base: "r x z ==> P" + assumes step: "\ y. [| r x y; tranclp r y z |] ==> P" + shows P +proof - + from tranclpD[OF major] + obtain y where "r x y" and "rtranclp r y z" by iprover + from this(2) show P + proof (cases rule: rtranclp.cases) + case rtrancl_refl + with `r x y` base show P by iprover + next + case rtrancl_into_rtrancl + from this have "tranclp r y z" + by (iprover intro: rtranclp_into_tranclp1) + with `r x y` step show P by iprover + qed +qed + +lemmas converse_tranclE = converse_tranclpE [to_set] + lemma tranclD2: "(x, y) \ R\<^sup>+ \ \z. (x, z) \ R\<^sup>* \ (z, y) \ R" by (blast elim: tranclE intro: trancl_into_rtrancl) diff -r 61ee6256d863 -r dc65b2f78664 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Fri Jun 12 22:30:37 2009 -0700 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Jun 13 07:03:51 2009 -0700 @@ -7,8 +7,6 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" - - code_pred even . thm odd.equation @@ -57,19 +55,23 @@ (*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 -*) + +(* Setup requires quick and dirty proof *) (* -code_pred tranclp . +code_pred tranclp +proof - + case tranclp + from this converse_tranclpE[OF this(1)] show thesis by metis +qed thm tranclp.equation *) + inductive succ :: "nat \ nat \ bool" where "succ 0 1" | "succ m n \ succ (Suc m) (Suc n)" @@ -77,8 +79,7 @@ code_pred succ . thm succ.equation - -(* TODO: requires alternative rules for trancl *) +(* FIXME: why does this not terminate? *) (* values 20 "{n. tranclp succ 10 n}" values "{n. tranclp succ n 10}" diff -r 61ee6256d863 -r dc65b2f78664 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Fri Jun 12 22:30:37 2009 -0700 +++ b/src/HOL/ex/predicate_compile.ML Sat Jun 13 07:03:51 2009 -0700 @@ -135,6 +135,7 @@ cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map string_of_mode ms)) modes)); + datatype predfun_data = PredfunData of { name : string, definition : thm, @@ -180,9 +181,7 @@ (* queries *) 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 + Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name) fun the_pred_data thy name = case lookup_pred_data thy name of NONE => error ("No such predicate " ^ quote name) @@ -243,16 +242,73 @@ in thy end; *) + +fun imp_prems_conv cv ct = + case Thm.term_of ct of + Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct + | _ => Conv.all_conv ct + +fun Trueprop_conv cv ct = + case Thm.term_of ct of + Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct + | _ => error "Trueprop_conv" + +fun preprocess_intro thy rule = + Conv.fconv_rule + (imp_prems_conv + (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) + (Thm.transfer thy rule) + +fun preprocess_elim thy nargs elimrule = let + fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = + HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) + | replace_eqs t = t + fun preprocess_case t = let + val params = Logic.strip_params t + val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) + val assums_hyp' = assums1 @ (map replace_eqs assums2) + in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) end + val prems = Thm.prems_of elimrule + val cases' = map preprocess_case (tl prems) + val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) + in + Thm.equal_elim + (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}]) + (cterm_of thy elimrule'))) + elimrule + end; + +fun fetch_pred_data thy name = + case try (InductivePackage.the_inductive (ProofContext.init thy)) name of + SOME (info as (_, result)) => + let + fun is_intro_of intro = + let + val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) + in (fst (dest_Const const) = name) end; + 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 (intros, elim, nparams) end + | NONE => error ("No such predicate: " ^ quote name) + (* updaters *) fun add_predfun name mode data = let val add = apsnd (cons (mode, mk_predfun_data data)) in PredData.map (Graph.map_node name (map_pred_data add)) end -fun add_intro thm = let +fun add_intro thm thy = let val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm))) - fun set (intros, elim, nparams) = (thm::intros, elim, nparams) - in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end + fun cons_intro gr = + case try (Graph.get_node gr) name of + SOME pred_data => Graph.map_node name (map_pred_data + (apfst (fn (intro, elim, nparams) => (thm::intro, elim, nparams)))) gr + | NONE => + let + val nparams = the_default 0 (try (#3 o fetch_pred_data thy) name) + in Graph.new_node (name, mk_pred_data (([thm], NONE, nparams), [])) gr end; + in PredData.map cons_intro thy end fun set_elim thm = let val (name, _) = dest_Const (fst @@ -814,42 +870,6 @@ fun is_Type (Type _) = true | is_Type _ = false -fun imp_prems_conv cv ct = - case Thm.term_of ct of - Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct - | _ => Conv.all_conv ct - -fun Trueprop_conv cv ct = - case Thm.term_of ct of - Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct - | _ => error "Trueprop_conv" - -fun preprocess_intro thy rule = - Conv.fconv_rule - (imp_prems_conv - (Trueprop_conv (Conv.try_conv (Conv.rewr_conv (Thm.symmetric @{thm Predicate.eq_is_eq}))))) - (Thm.transfer thy rule) - -fun preprocess_elim thy nargs elimrule = let - fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = - HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) - | replace_eqs t = t - fun preprocess_case t = let - val params = Logic.strip_params t - val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) - val assums_hyp' = assums1 @ (map replace_eqs assums2) - in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) end - val prems = Thm.prems_of elimrule - val cases' = map preprocess_case (tl prems) - val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) - in - Thm.equal_elim - (Thm.symmetric (Conv.implies_concl_conv (MetaSimplifier.rewrite true [@{thm eq_is_eq}]) - (cterm_of thy elimrule'))) - elimrule - end; - - (* returns true if t is an application of an datatype constructor *) (* which then consequently would be splitted *) (* else false *) @@ -1369,7 +1389,7 @@ fun mk_casesrule ctxt nparams introrules = let - val intros = map prop_of introrules + val intros = map (Logic.unvarify o prop_of) introrules val (pred, (params, args)) = strip_intro_concl nparams (hd intros) val ([propname], ctxt1) = Variable.variant_fixes ["thesis"] ctxt val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT)) @@ -1390,26 +1410,13 @@ in Logic.list_implies (assm :: cases, prop) end; (* code dependency graph *) - -fun fetch_pred_data thy name = - case try (InductivePackage.the_inductive (ProofContext.init thy)) name of - SOME (info as (_, result)) => - let - fun is_intro_of intro = - let - val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) - in (fst (dest_Const const) = name) end; - 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 - | NONE => error ("No such predicate: " ^ quote name) -fun dependencies_of (thy : theory) name = +fun dependencies_of thy name = let fun is_inductive_predicate thy name = is_some (try (InductivePackage.the_inductive (ProofContext.init thy)) name) - val data = fetch_pred_data thy name + val (intro, elim, nparams) = fetch_pred_data thy name + val data = mk_pred_data ((intro, SOME elim, nparams), []) val intros = map Thm.prop_of (#intros (rep_pred_data data)) val keys = fold Term.add_consts intros [] |> map fst |> filter (is_inductive_predicate thy) @@ -1458,12 +1465,20 @@ let val nparams = nparams_of thy' const val intros = intros_of thy' const - in mk_casesrule lthy' nparams intros end + in mk_casesrule lthy' nparams intros end val cases_rules = map mk_cases preds + val cases = + map (fn case_rule => RuleCases.Case {fixes = [], + assumes = [("", Logic.strip_imp_prems case_rule)], + binds = [], cases = []}) cases_rules + val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases + val _ = Output.tracing (commas (map fst case_env)) + val lthy'' = ProofContext.add_cases true case_env lthy' + fun after_qed thms = LocalTheory.theory (fold set_elim (map the_single thms) #> add_equations const) in - Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy' + Proof.theorem_i NONE after_qed (map (single o (rpair [])) cases_rules) lthy'' end; structure P = OuterParse