--- 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 <martin@von-gagern.net>
*)
--- 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/
--- 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,
--- 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.
--- 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
--- 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])
--- 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"
--- 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
--- 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.
--- /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"
--- /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"
--- 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: "\<And> 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) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R"
by (blast elim: tranclE intro: trancl_into_rtrancl)
--- 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 \<Longrightarrow> odd (Suc n)"
| "odd n \<Longrightarrow> even (Suc n)"
-
-
code_pred even .
thm odd.equation
@@ -57,19 +55,23 @@
(*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
-*)
+
+(* 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 \<Rightarrow> nat \<Rightarrow> bool" where
"succ 0 1"
| "succ m n \<Longrightarrow> 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}"
--- 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