--- a/doc-src/System/Thy/Presentation.thy Fri Mar 05 17:55:30 2010 +0100
+++ b/doc-src/System/Thy/Presentation.thy Sat Mar 06 07:30:21 2010 +0100
@@ -183,14 +183,19 @@
Usage: browser [OPTIONS] [GRAPHFILE]
Options are:
+ -b Admin/build only
-c cleanup -- remove GRAPHFILE after use
-o FILE output to FILE (ps, eps, pdf)
\end{ttbox}
When no filename is specified, the browser automatically changes to
the directory @{setting ISABELLE_BROWSER_INFO}.
- \medskip The @{verbatim "-c"} option causes the input file to be
- removed after use.
+ \medskip The @{verbatim "-b"} option indicates that this is for
+ administrative build only, i.e.\ no browser popup if no files are
+ given.
+
+ The @{verbatim "-c"} option causes the input file to be removed
+ after use.
The @{verbatim "-o"} option indicates batch-mode operation, with the
output written to the indicated file; note that @{verbatim pdf}
--- a/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 17:55:30 2010 +0100
+++ b/doc-src/System/Thy/document/Presentation.tex Sat Mar 06 07:30:21 2010 +0100
@@ -198,14 +198,19 @@
Usage: browser [OPTIONS] [GRAPHFILE]
Options are:
+ -b Admin/build only
-c cleanup -- remove GRAPHFILE after use
-o FILE output to FILE (ps, eps, pdf)
\end{ttbox}
When no filename is specified, the browser automatically changes to
the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}.
- \medskip The \verb|-c| option causes the input file to be
- removed after use.
+ \medskip The \verb|-b| option indicates that this is for
+ administrative build only, i.e.\ no browser popup if no files are
+ given.
+
+ The \verb|-c| option causes the input file to be removed
+ after use.
The \verb|-o| option indicates batch-mode operation, with the
output written to the indicated file; note that \verb|pdf|
--- a/lib/Tools/browser Fri Mar 05 17:55:30 2010 +0100
+++ b/lib/Tools/browser Sat Mar 06 07:30:21 2010 +0100
@@ -13,6 +13,7 @@
echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
echo
echo " Options are:"
+ echo " -b Admin/build only"
echo " -c cleanup -- remove GRAPHFILE after use"
echo " -o FILE output to FILE (ps, eps, pdf)"
echo
@@ -30,12 +31,16 @@
# options
+ADMIN_BUILD=""
CLEAN=""
OUTFILE=""
-while getopts "co:" OPT
+while getopts "bco:" OPT
do
case "$OPT" in
+ b)
+ ADMIN_BUILD=true
+ ;;
c)
CLEAN=true
;;
@@ -64,10 +69,7 @@
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
-if [ -z "$GRAPHFILE" ]; then
- [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
- exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
-else
+if [ -n "$GRAPHFILE" ]; then
PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
@@ -95,6 +97,11 @@
fi
rm -f "$PRIVATE_FILE"
+elif [ -z "$ADMIN_BUILD" ]; then
+ [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
+ exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
+else
+ RC=0
fi
exit "$RC"
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sat Mar 06 07:30:21 2010 +0100
@@ -27,7 +27,6 @@
unit
(*utility functions*)
- val goal_thm_of : Proof.state -> thm
val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
Proof.state -> bool
val theorems_in_proof_term : thm -> thm list
@@ -155,11 +154,9 @@
(* Mirabelle utility functions *)
-val goal_thm_of = #goal o Proof.raw_goal (* FIXME ?? *)
-
fun can_apply time tac st =
let
- val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *)
+ val {context = ctxt, facts, goal} = Proof.goal st
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
in
(case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
@@ -201,7 +198,7 @@
NONE => []
| SOME st =>
if not (Toplevel.is_proof st) then []
- else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
+ else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st))))
fun get_setting settings (key, default) =
the_default default (AList.lookup (op =) settings key)
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Sat Mar 06 07:30:21 2010 +0100
@@ -10,8 +10,8 @@
fun refute_action args timeout {pre=st, ...} =
let
val subgoal = 1
- val thy = Proof.theory_of st
- val thm = goal_thm_of st
+ val thy = Proof.theory_of st
+ val thm = #goal (Proof.raw_goal st)
val refute = Refute.refute_goal thy args thm
val _ = TimeLimit.timeLimit timeout refute subgoal
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Mar 06 07:30:21 2010 +0100
@@ -307,7 +307,7 @@
fun run_sh prover hard_timeout timeout dir st =
let
- val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *)
+ val {context = ctxt, facts, goal} = Proof.goal st
val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
val ctxt' =
ctxt
@@ -434,39 +434,39 @@
end
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
- let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre)) (* FIXME ?? *) in
- if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
- then () else
- let
- val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
- val minimize = AList.defined (op =) args minimizeK
- val metis_ft = AList.defined (op =) args metis_ftK
-
- fun apply_metis m1 m2 =
- if metis_ft
- then
- if not (Mirabelle.catch_result metis_tag false
- (run_metis false m1 name (these (!named_thms))) id st)
+ let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
+ if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
+ then () else
+ let
+ val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
+ val minimize = AList.defined (op =) args minimizeK
+ val metis_ft = AList.defined (op =) args metis_ftK
+
+ fun apply_metis m1 m2 =
+ if metis_ft
then
+ if not (Mirabelle.catch_result metis_tag false
+ (run_metis false m1 name (these (!named_thms))) id st)
+ then
+ (Mirabelle.catch_result metis_tag false
+ (run_metis true m2 name (these (!named_thms))) id st; ())
+ else ()
+ else
(Mirabelle.catch_result metis_tag false
- (run_metis true m2 name (these (!named_thms))) id st; ())
- else ()
- else
- (Mirabelle.catch_result metis_tag false
- (run_metis false m1 name (these (!named_thms))) id st; ())
- in
- change_data id (set_mini minimize);
- Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
- if is_some (!named_thms)
- then
- (apply_metis Unminimized UnminimizedFT;
- if minimize andalso not (null (these (!named_thms)))
+ (run_metis false m1 name (these (!named_thms))) id st; ())
+ in
+ change_data id (set_mini minimize);
+ Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
+ if is_some (!named_thms)
then
- (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
- apply_metis Minimized MinimizedFT)
- else ())
- else ()
- end
+ (apply_metis Unminimized UnminimizedFT;
+ if minimize andalso not (null (these (!named_thms)))
+ then
+ (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
+ apply_metis Minimized MinimizedFT)
+ else ())
+ else ()
+ end
end
fun invoke args =
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sat Mar 06 07:30:21 2010 +0100
@@ -253,7 +253,7 @@
NONE => warning ("Unknown external prover: " ^ quote name)
| SOME prover =>
let
- val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
+ val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
"external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Sat Mar 06 07:30:21 2010 +0100
@@ -117,7 +117,7 @@
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
- val {context = ctxt, facts, goal} = Proof.raw_goal state (* FIXME ?? *)
+ val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{with_full_types = ! ATP_Manager.full_types,
subgoal = subgoalno,
--- a/src/HOLCF/Domain.thy Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOLCF/Domain.thy Sat Mar 06 07:30:21 2010 +0100
@@ -214,6 +214,102 @@
ssum_map_sinl ssum_map_sinr sprod_map_spair u_map_up
+subsection {* Take functions and finiteness *}
+
+lemma lub_ID_take_lemma:
+ assumes "chain t" and "(\<Squnion>n. t n) = ID"
+ assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
+proof -
+ have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
+ using assms(3) by simp
+ then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
+ using assms(1) by (simp add: lub_distribs)
+ then show "x = y"
+ using assms(2) by simp
+qed
+
+lemma lub_ID_reach:
+ assumes "chain t" and "(\<Squnion>n. t n) = ID"
+ shows "(\<Squnion>n. t n\<cdot>x) = x"
+using assms by (simp add: lub_distribs)
+
+text {*
+ Let a ``decisive'' function be a deflation that maps every input to
+ either itself or bottom. Then if a domain's take functions are all
+ decisive, then all values in the domain are finite.
+*}
+
+definition
+ decisive :: "('a::pcpo \<rightarrow> 'a) \<Rightarrow> bool"
+where
+ "decisive d \<longleftrightarrow> (\<forall>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>)"
+
+lemma decisiveI: "(\<And>x. d\<cdot>x = x \<or> d\<cdot>x = \<bottom>) \<Longrightarrow> decisive d"
+ unfolding decisive_def by simp
+
+lemma decisive_cases:
+ assumes "decisive d" obtains "d\<cdot>x = x" | "d\<cdot>x = \<bottom>"
+using assms unfolding decisive_def by auto
+
+lemma decisive_bottom: "decisive \<bottom>"
+ unfolding decisive_def by simp
+
+lemma decisive_ID: "decisive ID"
+ unfolding decisive_def by simp
+
+lemma decisive_ssum_map:
+ assumes f: "decisive f"
+ assumes g: "decisive g"
+ shows "decisive (ssum_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_sprod_map:
+ assumes f: "decisive f"
+ assumes g: "decisive g"
+ shows "decisive (sprod_map\<cdot>f\<cdot>g)"
+apply (rule decisiveI, rename_tac s)
+apply (case_tac s, simp_all)
+apply (rule_tac x=x in decisive_cases [OF f], simp_all)
+apply (rule_tac x=y in decisive_cases [OF g], simp_all)
+done
+
+lemma decisive_abs_rep:
+ fixes abs rep
+ assumes iso: "iso abs rep"
+ assumes d: "decisive d"
+ shows "decisive (abs oo d oo rep)"
+apply (rule decisiveI)
+apply (rule_tac x="rep\<cdot>x" in decisive_cases [OF d])
+apply (simp add: iso.rep_iso [OF iso])
+apply (simp add: iso.abs_strict [OF iso])
+done
+
+lemma lub_ID_finite:
+ assumes chain: "chain d"
+ assumes lub: "(\<Squnion>n. d n) = ID"
+ assumes decisive: "\<And>n. decisive (d n)"
+ shows "\<exists>n. d n\<cdot>x = x"
+proof -
+ have 1: "chain (\<lambda>n. d n\<cdot>x)" using chain by simp
+ have 2: "(\<Squnion>n. d n\<cdot>x) = x" using chain lub by (rule lub_ID_reach)
+ have "\<forall>n. d n\<cdot>x = x \<or> d n\<cdot>x = \<bottom>"
+ using decisive unfolding decisive_def by simp
+ hence "range (\<lambda>n. d n\<cdot>x) \<subseteq> {x, \<bottom>}"
+ by auto
+ hence "finite (range (\<lambda>n. d n\<cdot>x))"
+ by (rule finite_subset, simp)
+ with 1 have "finite_chain (\<lambda>n. d n\<cdot>x)"
+ by (rule finite_range_imp_finch)
+ then have "\<exists>n. (\<Squnion>n. d n\<cdot>x) = d n\<cdot>x"
+ unfolding finite_chain_def by (auto simp add: maxinch_is_thelub)
+ with 2 show "\<exists>n. d n\<cdot>x = x" by (auto elim: sym)
+qed
+
+
subsection {* Installing the domain package *}
lemmas con_strict_rules =
@@ -253,23 +349,6 @@
ID1 ssum_map_sinl' ssum_map_sinr' ssum_map_strict
sprod_map_spair' sprod_map_strict u_map_up u_map_strict
-lemma lub_ID_take_lemma:
- assumes "chain t" and "(\<Squnion>n. t n) = ID"
- assumes "\<And>n. t n\<cdot>x = t n\<cdot>y" shows "x = y"
-proof -
- have "(\<Squnion>n. t n\<cdot>x) = (\<Squnion>n. t n\<cdot>y)"
- using assms(3) by simp
- then have "(\<Squnion>n. t n)\<cdot>x = (\<Squnion>n. t n)\<cdot>y"
- using assms(1) by (simp add: lub_distribs)
- then show "x = y"
- using assms(2) by simp
-qed
-
-lemma lub_ID_reach:
- assumes "chain t" and "(\<Squnion>n. t n) = ID"
- shows "(\<Squnion>n. t n\<cdot>x) = x"
-using assms by (simp add: lub_distribs)
-
use "Tools/cont_consts.ML"
use "Tools/cont_proc.ML"
use "Tools/Domain/domain_library.ML"
--- a/src/HOLCF/Representable.thy Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOLCF/Representable.thy Sat Mar 06 07:30:21 2010 +0100
@@ -12,6 +12,44 @@
("Tools/Domain/domain_isomorphism.ML")
begin
+subsection {* Preliminaries: Take proofs *}
+
+text {*
+ This section contains lemmas that are used in a module that supports
+ the domain isomorphism package; the module contains proofs related
+ to take functions and the finiteness predicate.
+*}
+
+lemma deflation_abs_rep:
+ fixes abs and rep and d
+ assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
+ assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
+ shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
+by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
+
+lemma deflation_chain_min:
+ assumes chain: "chain d"
+ assumes defl: "\<And>n. deflation (d n)"
+ shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
+proof (rule linorder_le_cases)
+ assume "m \<le> n"
+ with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
+ by (rule deflation_below_comp1 [OF defl defl])
+ moreover from `m \<le> n` have "min m n = m" by simp
+ ultimately show ?thesis by simp
+next
+ assume "n \<le> m"
+ with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
+ then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
+ by (rule deflation_below_comp2 [OF defl defl])
+ moreover from `n \<le> m` have "min m n = n" by simp
+ ultimately show ?thesis by simp
+qed
+
+use "Tools/Domain/domain_take_proofs.ML"
+
+
subsection {* Class of representable types *}
text "Overloaded embedding and projection functions between
@@ -180,33 +218,6 @@
shows "abs\<cdot>(rep\<cdot>x) = x"
unfolding abs_def rep_def by (simp add: REP [symmetric])
-lemma deflation_abs_rep:
- fixes abs and rep and d
- assumes abs_iso: "\<And>x. rep\<cdot>(abs\<cdot>x) = x"
- assumes rep_iso: "\<And>y. abs\<cdot>(rep\<cdot>y) = y"
- shows "deflation d \<Longrightarrow> deflation (abs oo d oo rep)"
-by (rule ep_pair.deflation_e_d_p) (simp add: ep_pair.intro assms)
-
-lemma deflation_chain_min:
- assumes chain: "chain d"
- assumes defl: "\<And>n. deflation (d n)"
- shows "d m\<cdot>(d n\<cdot>x) = d (min m n)\<cdot>x"
-proof (rule linorder_le_cases)
- assume "m \<le> n"
- with chain have "d m \<sqsubseteq> d n" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d m\<cdot>x"
- by (rule deflation_below_comp1 [OF defl defl])
- moreover from `m \<le> n` have "min m n = m" by simp
- ultimately show ?thesis by simp
-next
- assume "n \<le> m"
- with chain have "d n \<sqsubseteq> d m" by (rule chain_mono)
- then have "d m\<cdot>(d n\<cdot>x) = d n\<cdot>x"
- by (rule deflation_below_comp2 [OF defl defl])
- moreover from `n \<le> m` have "min m n = n" by simp
- ultimately show ?thesis by simp
-qed
-
subsection {* Proving a subtype is representable *}
@@ -777,7 +788,6 @@
subsection {* Constructing Domain Isomorphisms *}
-use "Tools/Domain/domain_take_proofs.ML"
use "Tools/Domain/domain_isomorphism.ML"
setup {*
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Mar 06 07:30:21 2010 +0100
@@ -350,7 +350,7 @@
val goal = mk_eqs (mk_Rep_of lhsT, mk_Rep_of rhsT);
val REP_simps = RepData.get thy;
val tac =
- simp_tac (HOL_basic_ss addsimps REP_simps) 1
+ rewrite_goals_tac (map mk_meta_eq REP_simps)
THEN resolve_tac defl_unfold_thms 1;
in
Goal.prove_global thy [] [] goal (K tac)
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Mar 06 07:30:21 2010 +0100
@@ -99,26 +99,13 @@
infix -->>;
infix 9 `;
-val deflT = @{typ "udom alg_defl"};
-
fun mapT (T as Type (_, Ts)) =
(map (fn T => T ->> T) Ts) -->> (T ->> T)
| mapT T = T ->> T;
-fun mk_Rep_of T =
- Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
-
-fun coerce_const T = Const (@{const_name coerce}, T);
-
-fun isodefl_const T =
- Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
-
fun mk_deflation t =
Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
-(* splits a cterm into the right and lefthand sides of equality *)
-fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
-
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
(******************************************************************************)
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Sat Mar 06 07:30:21 2010 +0100
@@ -157,13 +157,11 @@
val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
val rhs = con_app2 con one_rhs args;
val goal = mk_trp (lhs === rhs);
- val rules = [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}];
- val rules2 =
- @{thms take_con_rules ID1 deflation_strict}
+ val rules =
+ [ax_take_Suc, ax_abs_iso, @{thm cfcomp2}]
+ @ @{thms take_con_rules ID1 deflation_strict}
@ deflation_thms @ axs_deflation_take;
- val tacs =
- [simp_tac (HOL_basic_ss addsimps rules) 1,
- asm_simp_tac (HOL_basic_ss addsimps rules2) 1];
+ val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1];
in pg con_appls goal (K tacs) end;
val take_apps = map one_take_app cons;
in
@@ -196,10 +194,256 @@
pat_rews @ dist_les @ dist_eqs)
end; (* let *)
+(******************************************************************************)
+(****************************** induction rules *******************************)
+(******************************************************************************)
+
+fun prove_induction
+ (comp_dnam, eqs : eq list)
+ (take_lemmas : thm list)
+ (axs_reach : thm list)
+ (take_rews : thm list)
+ (thy : theory) =
+let
+ val dnames = map (fst o fst) eqs;
+ val conss = map snd eqs;
+ fun dc_take dn = %%:(dn^"_take");
+ val x_name = idx_name dnames "x";
+ val P_name = idx_name dnames "P";
+ val pg = pg' thy;
+
+ local
+ fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
+ fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
+ in
+ val axs_rep_iso = map (ga "rep_iso") dnames;
+ val axs_abs_iso = map (ga "abs_iso") dnames;
+ val axs_chain_take = map (ga "chain_take") dnames;
+ val lub_take_thms = map (ga "lub_take") dnames;
+ val axs_finite_def = map (ga "finite_def") dnames;
+ val take_0_thms = map (ga "take_0") dnames;
+ val take_Suc_thms = map (ga "take_Suc") dnames;
+ val cases = map (ga "casedist" ) dnames;
+ val con_rews = maps (gts "con_rews" ) dnames;
+ end;
+
+ fun one_con p (con, args) =
+ let
+ val P_names = map P_name (1 upto (length dnames));
+ val vns = Name.variant_list P_names (map vname args);
+ val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
+ fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
+ val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
+ val t2 = lift ind_hyp (filter is_rec args, t1);
+ val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
+ in Library.foldr mk_All (vns, t3) end;
+
+ fun one_eq ((p, cons), concl) =
+ mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
+
+ fun ind_term concf = Library.foldr one_eq
+ (mapn (fn n => fn x => (P_name n, x)) 1 conss,
+ mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
+ val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
+ fun quant_tac ctxt i = EVERY
+ (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
+
+ fun ind_prems_tac prems = EVERY
+ (maps (fn cons =>
+ (resolve_tac prems 1 ::
+ maps (fn (_,args) =>
+ resolve_tac prems 1 ::
+ map (K(atac 1)) (nonlazy args) @
+ map (K(atac 1)) (filter is_rec args))
+ cons))
+ conss);
+ local
+ (* check whether every/exists constructor of the n-th part of the equation:
+ it has a possibly indirectly recursive argument that isn't/is possibly
+ indirectly lazy *)
+ fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg =>
+ is_rec arg andalso not(rec_of arg mem ns) andalso
+ ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
+ rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
+ (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
+ ) o snd) cons;
+ fun all_rec_to ns = rec_to forall not all_rec_to ns;
+ fun warn (n,cons) =
+ if all_rec_to [] false (n,cons)
+ then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
+ else false;
+ fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns;
+
+ in
+ val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
+ val is_emptys = map warn n__eqs;
+ val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
+ val _ = if is_finite
+ then message ("Proving finiteness rule for domain "^comp_dnam^" ...")
+ else ();
+ end;
+ val _ = trace " Proving finite_ind...";
+ val finite_ind =
+ let
+ fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
+ val goal = ind_term concf;
+
+ fun tacf {prems, context} =
+ let
+ val tacs1 = [
+ quant_tac context 1,
+ simp_tac HOL_ss 1,
+ InductTacs.induct_tac context [[SOME "n"]] 1,
+ simp_tac (take_ss addsimps prems) 1,
+ TRY (safe_tac HOL_cs)];
+ fun arg_tac arg =
+ (* FIXME! case_UU_tac *)
+ case_UU_tac context (prems @ con_rews) 1
+ (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
+ fun con_tacs (con, args) =
+ asm_simp_tac take_ss 1 ::
+ map arg_tac (filter is_nonlazy_rec args) @
+ [resolve_tac prems 1] @
+ map (K (atac 1)) (nonlazy args) @
+ map (K (etac spec 1)) (filter is_rec args);
+ fun cases_tacs (cons, cases) =
+ res_inst_tac context [(("y", 0), "x")] cases 1 ::
+ asm_simp_tac (take_ss addsimps prems) 1 ::
+ maps con_tacs cons;
+ in
+ tacs1 @ maps cases_tacs (conss ~~ cases)
+ end;
+ in pg'' thy [] goal tacf
+ handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI)
+ end;
+
+(* ----- theorems concerning finiteness and induction ----------------------- *)
+
+ val global_ctxt = ProofContext.init thy;
+
+ val _ = trace " Proving finites, ind...";
+ val (finites, ind) =
+ (
+ if is_finite
+ then (* finite case *)
+ let
+ val decisive_lemma =
+ let
+ val iso_locale_thms =
+ map2 (fn x => fn y => @{thm iso.intro} OF [x, y])
+ axs_abs_iso axs_rep_iso;
+ val decisive_abs_rep_thms =
+ map (fn x => @{thm decisive_abs_rep} OF [x])
+ iso_locale_thms;
+ val n = Free ("n", @{typ nat});
+ fun mk_decisive t = %%: @{const_name decisive} $ t;
+ fun f dn = mk_decisive (dc_take dn $ n);
+ val goal = mk_trp (foldr1 mk_conj (map f dnames));
+ val rules0 = @{thm decisive_bottom} :: take_0_thms;
+ val rules1 =
+ take_Suc_thms @ decisive_abs_rep_thms
+ @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
+ val tacs = [
+ rtac @{thm nat.induct} 1,
+ simp_tac (HOL_ss addsimps rules0) 1,
+ asm_simp_tac (HOL_ss addsimps rules1) 1];
+ in pg [] goal (K tacs) end;
+ fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
+ fun one_finite (dn, decisive_thm) =
+ let
+ val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
+ val tacs = [
+ rtac @{thm lub_ID_finite} 1,
+ resolve_tac axs_chain_take 1,
+ resolve_tac lub_take_thms 1,
+ rtac decisive_thm 1];
+ in pg axs_finite_def goal (K tacs) end;
+
+ val _ = trace " Proving finites";
+ val finites = map one_finite (dnames ~~ atomize global_ctxt decisive_lemma);
+ val _ = trace " Proving ind";
+ val ind =
+ let
+ fun concf n dn = %:(P_name n) $ %:(x_name n);
+ fun tacf {prems, context} =
+ let
+ fun finite_tacs (finite, fin_ind) = [
+ rtac(rewrite_rule axs_finite_def finite RS exE)1,
+ etac subst 1,
+ rtac fin_ind 1,
+ ind_prems_tac prems];
+ in
+ TRY (safe_tac HOL_cs) ::
+ maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
+ end;
+ in pg'' thy [] (ind_term concf) tacf end;
+ in (finites, ind) end (* let *)
+
+ else (* infinite case *)
+ let
+ fun one_finite n dn =
+ read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
+ val finites = mapn one_finite 1 dnames;
+
+ val goal =
+ let
+ fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
+ fun concf n dn = %:(P_name n) $ %:(x_name n);
+ in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
+ val cont_rules =
+ @{thms cont_id cont_const cont2cont_Rep_CFun
+ cont2cont_fst cont2cont_snd};
+ val subgoal =
+ let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n));
+ in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end;
+ val subgoal' = legacy_infer_term thy subgoal;
+ fun tacf {prems, context} =
+ let
+ val subtac =
+ EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
+ val subthm = Goal.prove context [] [] subgoal' (K subtac);
+ in
+ map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
+ cut_facts_tac (subthm :: take (length dnames) prems) 1,
+ REPEAT (rtac @{thm conjI} 1 ORELSE
+ EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
+ resolve_tac axs_chain_take 1,
+ asm_simp_tac HOL_basic_ss 1])
+ ]
+ end;
+ val ind = (pg'' thy [] goal tacf
+ handle ERROR _ =>
+ (warning "Cannot prove infinite induction rule"; TrueI)
+ );
+ in (finites, ind) end
+ )
+ handle THM _ =>
+ (warning "Induction proofs failed (THM raised)."; ([], TrueI))
+ | ERROR _ =>
+ (warning "Cannot prove induction rule"; ([], TrueI));
+
+val inducts = Project_Rule.projections (ProofContext.init thy) ind;
+fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
+val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
+
+in thy |> Sign.add_path comp_dnam
+ |> snd o PureThy.add_thmss [
+ ((Binding.name "finites" , finites ), []),
+ ((Binding.name "finite_ind" , [finite_ind]), []),
+ ((Binding.name "ind" , [ind] ), [])]
+ |> (if induct_failed then I
+ else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
+ |> Sign.parent_path
+end; (* prove_induction *)
+
+(******************************************************************************)
+(************************ bisimulation and coinduction ************************)
+(******************************************************************************)
+
fun prove_coinduction
(comp_dnam, eqs : eq list)
(take_lemmas : thm list)
- (thy : theory) : thm * theory =
+ (thy : theory) : theory =
let
val dnames = map (fst o fst) eqs;
@@ -339,312 +583,72 @@
in pg [] goal (K tacs) end;
end; (* local *)
-in
- (coind, thy)
-end;
+in thy |> Sign.add_path comp_dnam
+ |> snd o PureThy.add_thmss [((Binding.name "coind", [coind]), [])]
+ |> Sign.parent_path
+end; (* let *)
fun comp_theorems (comp_dnam, eqs: eq list) thy =
let
val map_tab = Domain_Take_Proofs.get_map_tab thy;
val dnames = map (fst o fst) eqs;
-val conss = map snd eqs;
val comp_dname = Sign.full_bname thy comp_dnam;
-val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+(* ----- getting the composite axiom and definitions ------------------------ *)
-val pg = pg' thy;
+(* Test for indirect recursion *)
+local
+ fun indirect_arg arg =
+ rec_of arg = ~1 andalso Datatype_Aux.is_rec_type (dtyp_of arg);
+ fun indirect_con (_, args) = exists indirect_arg args;
+ fun indirect_eq (_, cons) = exists indirect_con cons;
+in
+ val is_indirect = exists indirect_eq eqs;
+ val _ =
+ if is_indirect
+ then message "Indirect recursion detected, skipping proofs of (co)induction rules"
+ else message ("Proving induction properties of domain "^comp_dname^" ...");
+end;
-(* ----- getting the composite axiom and definitions ------------------------ *)
+(* theorems about take *)
local
fun ga s dn = PureThy.get_thm thy (dn ^ "." ^ s);
-in
- val axs_take_def = map (ga "take_def" ) dnames;
val axs_chain_take = map (ga "chain_take") dnames;
val axs_lub_take = map (ga "lub_take" ) dnames;
- val axs_finite_def = map (ga "finite_def") dnames;
-end;
-
-local
- fun gt s dn = PureThy.get_thm thy (dn ^ "." ^ s);
- fun gts s dn = PureThy.get_thms thy (dn ^ "." ^ s);
in
- val cases = map (gt "casedist" ) dnames;
- val con_rews = maps (gts "con_rews" ) dnames;
-end;
-
-fun dc_take dn = %%:(dn^"_take");
-val x_name = idx_name dnames "x";
-val P_name = idx_name dnames "P";
-val n_eqs = length eqs;
-
-(* ----- theorems concerning finite approximation and finite induction ------ *)
-
-val take_rews =
- maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
-
-local
- fun one_con p (con, args) =
- let
- val P_names = map P_name (1 upto (length dnames));
- val vns = Name.variant_list P_names (map vname args);
- val nonlazy_vns = map snd (filter_out (is_lazy o fst) (args ~~ vns));
- fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
- val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
- val t2 = lift ind_hyp (filter is_rec args, t1);
- val t3 = lift_defined (bound_arg vns) (nonlazy_vns, t2);
- in Library.foldr mk_All (vns, t3) end;
-
- fun one_eq ((p, cons), concl) =
- mk_trp (%:p $ UU) ===> Logic.list_implies (map (one_con p) cons, concl);
-
- fun ind_term concf = Library.foldr one_eq
- (mapn (fn n => fn x => (P_name n, x)) 1 conss,
- mk_trp (foldr1 mk_conj (mapn concf 1 dnames)));
- val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
- fun quant_tac ctxt i = EVERY
- (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames);
-
- fun ind_prems_tac prems = EVERY
- (maps (fn cons =>
- (resolve_tac prems 1 ::
- maps (fn (_,args) =>
- resolve_tac prems 1 ::
- map (K(atac 1)) (nonlazy args) @
- map (K(atac 1)) (filter is_rec args))
- cons))
- conss);
- local
- (* check whether every/exists constructor of the n-th part of the equation:
- it has a possibly indirectly recursive argument that isn't/is possibly
- indirectly lazy *)
- fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg =>
- is_rec arg andalso not(rec_of arg mem ns) andalso
- ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
- rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
- (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
- ) o snd) cons;
- fun all_rec_to ns = rec_to forall not all_rec_to ns;
- fun warn (n,cons) =
- if all_rec_to [] false (n,cons)
- then (warning ("domain "^List.nth(dnames,n)^" is empty!"); true)
- else false;
- fun lazy_rec_to ns = rec_to exists I lazy_rec_to ns;
-
- in
- val n__eqs = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
- val is_emptys = map warn n__eqs;
- val is_finite = forall (not o lazy_rec_to [] false) n__eqs;
- end;
-in (* local *)
- val _ = trace " Proving finite_ind...";
- val finite_ind =
- let
- fun concf n dn = %:(P_name n) $ (dc_take dn $ %:"n" `%(x_name n));
- val goal = ind_term concf;
-
- fun tacf {prems, context} =
- let
- val tacs1 = [
- quant_tac context 1,
- simp_tac HOL_ss 1,
- InductTacs.induct_tac context [[SOME "n"]] 1,
- simp_tac (take_ss addsimps prems) 1,
- TRY (safe_tac HOL_cs)];
- fun arg_tac arg =
- (* FIXME! case_UU_tac *)
- case_UU_tac context (prems @ con_rews) 1
- (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
- fun con_tacs (con, args) =
- asm_simp_tac take_ss 1 ::
- map arg_tac (filter is_nonlazy_rec args) @
- [resolve_tac prems 1] @
- map (K (atac 1)) (nonlazy args) @
- map (K (etac spec 1)) (filter is_rec args);
- fun cases_tacs (cons, cases) =
- res_inst_tac context [(("y", 0), "x")] cases 1 ::
- asm_simp_tac (take_ss addsimps prems) 1 ::
- maps con_tacs cons;
- in
- tacs1 @ maps cases_tacs (conss ~~ cases)
- end;
- in pg'' thy [] goal tacf
- handle ERROR _ => (warning "Proof of finite_ind failed."; TrueI)
- end;
-
val _ = trace " Proving take_lemmas...";
val take_lemmas =
let
fun take_lemma (ax_chain_take, ax_lub_take) =
- Drule.export_without_context
- (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
+ Drule.export_without_context
+ (@{thm lub_ID_take_lemma} OF [ax_chain_take, ax_lub_take]);
in map take_lemma (axs_chain_take ~~ axs_lub_take) end;
-
val axs_reach =
let
fun reach (ax_chain_take, ax_lub_take) =
- Drule.export_without_context
- (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
+ Drule.export_without_context
+ (@{thm lub_ID_reach} OF [ax_chain_take, ax_lub_take]);
in map reach (axs_chain_take ~~ axs_lub_take) end;
-
-(* ----- theorems concerning finiteness and induction ----------------------- *)
-
- val global_ctxt = ProofContext.init thy;
+end;
- val _ = trace " Proving finites, ind...";
- val (finites, ind) =
- (
- if is_finite
- then (* finite case *)
- let
- fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %:"x" === %:"x");
- fun dname_lemma dn =
- let
- val prem1 = mk_trp (defined (%:"x"));
- val disj1 = mk_all ("n", dc_take dn $ Bound 0 ` %:"x" === UU);
- val prem2 = mk_trp (mk_disj (disj1, take_enough dn));
- val concl = mk_trp (take_enough dn);
- val goal = prem1 ===> prem2 ===> concl;
- val tacs = [
- etac disjE 1,
- etac notE 1,
- resolve_tac take_lemmas 1,
- asm_simp_tac take_ss 1,
- atac 1];
- in pg [] goal (K tacs) end;
- val _ = trace " Proving finite_lemmas1a";
- val finite_lemmas1a = map dname_lemma dnames;
-
- val _ = trace " Proving finite_lemma1b";
- val finite_lemma1b =
- let
- fun mk_eqn n ((dn, args), _) =
- let
- val disj1 = dc_take dn $ Bound 1 ` Bound 0 === UU;
- val disj2 = dc_take dn $ Bound 1 ` Bound 0 === Bound 0;
- in
- mk_constrainall
- (x_name n, Type (dn,args), mk_disj (disj1, disj2))
- end;
- val goal =
- mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs)));
- fun arg_tacs ctxt vn = [
- eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1,
- etac disjE 1,
- asm_simp_tac (HOL_ss addsimps con_rews) 1,
- asm_simp_tac take_ss 1];
- fun con_tacs ctxt (con, args) =
- asm_simp_tac take_ss 1 ::
- maps (arg_tacs ctxt) (nonlazy_rec args);
- fun foo_tacs ctxt n (cons, cases) =
- simp_tac take_ss 1 ::
- rtac allI 1 ::
- res_inst_tac ctxt [(("y", 0), x_name n)] cases 1 ::
- asm_simp_tac take_ss 1 ::
- maps (con_tacs ctxt) cons;
- fun tacs ctxt =
- rtac allI 1 ::
- InductTacs.induct_tac ctxt [[SOME "n"]] 1 ::
- simp_tac take_ss 1 ::
- TRY (safe_tac (empty_cs addSEs [conjE] addSIs [conjI])) ::
- flat (mapn (foo_tacs ctxt) 1 (conss ~~ cases));
- in pg [] goal tacs end;
+val take_rews =
+ maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
- fun one_finite (dn, l1b) =
- let
- val goal = mk_trp (%%:(dn^"_finite") $ %:"x");
- fun tacs ctxt = [
- (* FIXME! case_UU_tac *)
- case_UU_tac ctxt take_rews 1 "x",
- eresolve_tac finite_lemmas1a 1,
- step_tac HOL_cs 1,
- step_tac HOL_cs 1,
- cut_facts_tac [l1b] 1,
- fast_tac HOL_cs 1];
- in pg axs_finite_def goal tacs end;
-
- val _ = trace " Proving finites";
- val finites = map one_finite (dnames ~~ atomize global_ctxt finite_lemma1b);
- val _ = trace " Proving ind";
- val ind =
- let
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- fun tacf {prems, context} =
- let
- fun finite_tacs (finite, fin_ind) = [
- rtac(rewrite_rule axs_finite_def finite RS exE)1,
- etac subst 1,
- rtac fin_ind 1,
- ind_prems_tac prems];
- in
- TRY (safe_tac HOL_cs) ::
- maps finite_tacs (finites ~~ atomize global_ctxt finite_ind)
- end;
- in pg'' thy [] (ind_term concf) tacf end;
- in (finites, ind) end (* let *)
-
- else (* infinite case *)
- let
- fun one_finite n dn =
- read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle;
- val finites = mapn one_finite 1 dnames;
+(* prove induction rules, unless definition is indirect recursive *)
+val thy =
+ if is_indirect then thy else
+ prove_induction (comp_dnam, eqs) take_lemmas axs_reach take_rews thy;
- val goal =
- let
- fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
- fun concf n dn = %:(P_name n) $ %:(x_name n);
- in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
- val cont_rules =
- @{thms cont_id cont_const cont2cont_Rep_CFun
- cont2cont_fst cont2cont_snd};
- val subgoal =
- let fun p n dn = %:(P_name n) $ (dc_take dn $ Bound 0 `%(x_name n));
- in mk_trp (mk_all ("n", foldr1 mk_conj (mapn p 1 dnames))) end;
- val subgoal' = legacy_infer_term thy subgoal;
- fun tacf {prems, context} =
- let
- val subtac =
- EVERY [rtac allI 1, rtac finite_ind 1, ind_prems_tac prems];
- val subthm = Goal.prove context [] [] subgoal' (K subtac);
- in
- map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [
- cut_facts_tac (subthm :: take (length dnames) prems) 1,
- REPEAT (rtac @{thm conjI} 1 ORELSE
- EVERY [etac @{thm admD [OF _ ch2ch_Rep_CFunL]} 1,
- resolve_tac axs_chain_take 1,
- asm_simp_tac HOL_basic_ss 1])
- ]
- end;
- val ind = (pg'' thy [] goal tacf
- handle ERROR _ =>
- (warning "Cannot prove infinite induction rule"; TrueI)
- );
- in (finites, ind) end
- )
- handle THM _ =>
- (warning "Induction proofs failed (THM raised)."; ([], TrueI))
- | ERROR _ =>
- (warning "Cannot prove induction rule"; ([], TrueI));
-
-end; (* local *)
-
-val (coind, thy) = prove_coinduction (comp_dnam, eqs) take_lemmas thy;
-
-val inducts = Project_Rule.projections (ProofContext.init thy) ind;
-fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
-val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
+val thy =
+ if is_indirect then thy else
+ prove_coinduction (comp_dnam, eqs) take_lemmas thy;
in thy |> Sign.add_path comp_dnam
|> snd o PureThy.add_thmss [
((Binding.name "take_lemmas", take_lemmas ), []),
- ((Binding.name "reach" , axs_reach ), []),
- ((Binding.name "finites" , finites ), []),
- ((Binding.name "finite_ind" , [finite_ind]), []),
- ((Binding.name "ind" , [ind] ), []),
- ((Binding.name "coind" , [coind] ), [])]
- |> (if induct_failed then I
- else snd o PureThy.add_thmss (map ind_rule (dnames ~~ inducts)))
+ ((Binding.name "reach" , axs_reach ), [])]
|> Sign.parent_path |> pair take_rews
end; (* let *)
end; (* struct *)
--- a/src/HOLCF/ex/Domain_ex.thy Fri Mar 05 17:55:30 2010 +0100
+++ b/src/HOLCF/ex/Domain_ex.thy Sat Mar 06 07:30:21 2010 +0100
@@ -52,18 +52,18 @@
text {*
Indirect recusion is allowed for sums, products, lifting, and the
- continuous function space. However, the domain package currently
- cannot prove the induction rules. A fix is planned for the next
- release.
+ continuous function space. However, the domain package does not
+ generate an induction rule in terms of the constructors.
*}
domain 'a d7 = d7a "'a d7 \<oplus> int lift" | d7b "'a \<otimes> 'a d7" | d7c (lazy "'a d7 \<rightarrow> 'a")
-thm d7.ind -- "currently replaced with dummy theorem"
+(* d7.ind is absent *)
text {*
Indirect recursion using previously-defined datatypes is currently
- not allowed. This restriction should go away by the next release.
+ not allowed. This restriction does not apply to the new definitional
+ domain package.
*}
(*
domain 'a slist = SNil | SCons 'a "'a slist"
@@ -167,6 +167,7 @@
thm tree.take_take
thm tree.deflation_take
thm tree.take_lemmas
+thm tree.lub_take
thm tree.reach
thm tree.finite_ind
@@ -199,15 +200,14 @@
I don't know what is going on here. The failed proof has to do with
the finiteness predicate.
*}
-(*
+
domain foo = Foo (lazy "bar") and bar = Bar
- -- "Tactic failed."
-*)
+ -- "Cannot prove induction rule"
text {* Declaring class constraints on the LHS is currently broken. *}
(*
domain ('a::cpo) box = Box (lazy 'a)
- -- "Malformed YXML encoding: multiple results"
+ -- "Proof failed"
*)
text {*
--- a/src/Pure/Thy/present.ML Fri Mar 05 17:55:30 2010 +0100
+++ b/src/Pure/Thy/present.ML Sat Mar 06 07:30:21 2010 +0100
@@ -402,6 +402,7 @@
if length path > 1 then update_index parent_html_prefix name else ();
(case readme of NONE => () | SOME path => File.copy path html_prefix);
write_graph sorted_graph (Path.append html_prefix graph_path);
+ File.isabelle_tool "browser" "-b";
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
(HTML.applet_pages name (Url.File index_path, name));