--- a/Admin/isatest/settings/at-poly-test Thu Mar 04 21:52:26 2010 +0100
+++ b/Admin/isatest/settings/at-poly-test Fri Mar 05 10:42:13 2010 +0100
@@ -1,6 +1,6 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.3.0"
+ POLYML_HOME="/home/polyml/polyml-svn"
ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
--- a/README_REPOSITORY Thu Mar 04 21:52:26 2010 +0100
+++ b/README_REPOSITORY Fri Mar 05 10:42:13 2010 +0100
@@ -83,6 +83,8 @@
See also the fine documentation for further details, especially the
book http://hgbook.red-bean.com/
+There is also a nice tutorial at http://hginit.com/
+
Shared pull/push access
-----------------------
--- a/src/HOL/Auth/Message.thy Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOL/Auth/Message.thy Fri Mar 05 10:42:13 2010 +0100
@@ -236,7 +236,7 @@
by blast
lemma parts_subset_iff [simp]: "(parts G \<subseteq> parts H) = (G \<subseteq> parts H)"
-by (metis equalityE parts_idem parts_increasing parts_mono subset_trans)
+by (metis parts_idem parts_increasing parts_mono subset_trans)
lemma parts_trans: "[| X\<in> parts G; G \<subseteq> parts H |] ==> X\<in> parts H"
by (drule parts_mono, blast)
@@ -611,7 +611,7 @@
by blast
lemma synth_subset_iff [simp]: "(synth G \<subseteq> synth H) = (G \<subseteq> synth H)"
-by (metis equalityE subset_trans synth_idem synth_increasing synth_mono)
+by (metis subset_trans synth_idem synth_increasing synth_mono)
lemma synth_trans: "[| X\<in> synth G; G \<subseteq> synth H |] ==> X\<in> synth H"
by (drule synth_mono, blast)
@@ -674,8 +674,7 @@
lemma parts_insert_subset_Un: "X\<in> G ==> parts(insert X H) \<subseteq> parts G \<union> parts H"
by (metis UnCI Un_upper2 insert_subset parts_Un parts_mono)
-text{*More specifically for Fake. Very occasionally we could do with a version
- of the form @{term"parts{X} \<subseteq> synth (analz H) \<union> parts H"} *}
+text{*More specifically for Fake. See also @{text Fake_parts_sing} below *}
lemma Fake_parts_insert:
"X \<in> synth (analz H) ==>
parts (insert X H) \<subseteq> synth (analz H) \<union> parts H"
@@ -884,17 +883,17 @@
lemma Fake_analz_eq [simp]:
"X \<in> synth(analz H) ==> synth (analz (insert X H)) = synth (analz H)"
-by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute equalityI
+by (metis Fake_analz_insert Un_absorb Un_absorb1 Un_commute
subset_insertI synth_analz_mono synth_increasing synth_subset_iff)
text{*Two generalizations of @{text analz_insert_eq}*}
lemma gen_analz_insert_eq [rule_format]:
- "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G";
+ "X \<in> analz H ==> ALL G. H \<subseteq> G --> analz (insert X G) = analz G"
by (blast intro: analz_cut analz_insertI analz_mono [THEN [2] rev_subsetD])
lemma synth_analz_insert_eq [rule_format]:
"X \<in> synth (analz H)
- ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)";
+ ==> ALL G. H \<subseteq> G --> (Key K \<in> analz (insert X G)) = (Key K \<in> analz G)"
apply (erule synth.induct)
apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI])
done
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 10:42:13 2010 +0100
@@ -89,7 +89,7 @@
fun unregister message thread = Synchronized.change global_state
(fn state as {manager, timeout_heap, active, cancelling, messages, store} =>
(case lookup_thread active thread of
- SOME (birth_time, _, description) =>
+ SOME (_, _, description) =>
let
val active' = delete_thread thread active;
val cancelling' = (thread, (Time.now (), description)) :: cancelling;
@@ -267,7 +267,7 @@
"Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
| ERROR msg => ("Error: " ^ msg);
val _ = unregister message (Thread.self ());
- in () end)
+ in () end);
in () end);
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Fri Mar 05 10:42:13 2010 +0100
@@ -111,14 +111,14 @@
|> Exn.release
|> tap (after path);
-fun external_prover relevance_filter prepare write cmd args find_failure produce_answer
- axiom_clauses filtered_clauses name subgoalno goal =
+fun external_prover relevance_filter prepare write cmd args produce_answer name
+ ({with_full_types, subgoal, goal, axiom_clauses, filtered_clauses}: problem) =
let
(* get clauses and prepare them for writing *)
val (ctxt, (chain_ths, th)) = goal;
val thy = ProofContext.theory_of ctxt;
val chain_ths = map (Thm.put_name_hint Res_Reconstruct.chained_hint) chain_ths;
- val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoalno);
+ val goal_cls = #1 (Res_Axioms.neg_conjecture_clauses ctxt th subgoal);
val the_filtered_clauses =
(case filtered_clauses of
NONE => relevance_filter goal goal_cls
@@ -138,8 +138,8 @@
Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr)
in
if destdir' = "" then File.tmp_path probfile
- else if File.exists (Path.explode (destdir'))
- then Path.append (Path.explode (destdir')) probfile
+ else if File.exists (Path.explode destdir')
+ then Path.append (Path.explode destdir') probfile
else error ("No such directory: " ^ destdir')
end;
@@ -167,7 +167,7 @@
if Config.get ctxt measure_runtime then split_time s else (s, 0)
fun run_on probfile =
if File.exists cmd then
- write probfile clauses
+ write with_full_types probfile clauses
|> pair (apfst split_time' (bash_output (cmd_line probfile)))
else error ("Bad executable: " ^ Path.implode cmd);
@@ -178,16 +178,16 @@
else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
val (((proof, time), rc), conj_pos) =
- with_path cleanup export run_on (prob_pathname subgoalno);
+ with_path cleanup export run_on (prob_pathname subgoal);
(* check for success and print out some information on failure *)
- val failure = find_failure proof;
+ val failure = Res_Reconstruct.find_failure proof;
val success = rc = 0 andalso is_none failure;
val (message, real_thm_names) =
if is_some failure then ("External prover failed.", [])
else if rc <> 0 then ("External prover failed: " ^ proof, [])
else apfst (fn s => "Try this command: " ^ s)
- (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno));
+ (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal));
in
{success = success, message = message,
theorem_names = real_thm_names, runtime = time, proof = proof,
@@ -201,22 +201,17 @@
let
val {max_new_clauses, insert_theory_const, emit_structured_proof, command, arguments} =
prover_config;
- val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem;
in
external_prover
(Res_ATP.get_relevant max_new_clauses insert_theory_const)
(Res_ATP.prepare_clauses false)
- (Res_HOL_Clause.tptp_write_file with_full_types)
+ Res_HOL_Clause.tptp_write_file
command
(arguments timeout)
- Res_Reconstruct.find_failure
(if emit_structured_proof then Res_Reconstruct.structured_proof
else Res_Reconstruct.lemma_list false)
- axiom_clauses
- filtered_clauses
name
- subgoal
- goal
+ problem
end;
fun tptp_prover (name, config) = (name, gen_tptp_prover (name, config));
@@ -276,22 +271,17 @@
fun gen_dfg_prover (name, prover_config: prover_config) timeout problem =
let
- val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config
- val {with_full_types, subgoal, goal, axiom_clauses, filtered_clauses} = problem
+ val {max_new_clauses, insert_theory_const, command, arguments, ...} = prover_config;
in
external_prover
(Res_ATP.get_relevant max_new_clauses insert_theory_const)
(Res_ATP.prepare_clauses true)
- (Res_HOL_Clause.dfg_write_file with_full_types)
+ Res_HOL_Clause.dfg_write_file
command
(arguments timeout)
- Res_Reconstruct.find_failure
(Res_Reconstruct.lemma_list true)
- axiom_clauses
- filtered_clauses
name
- subgoal
- goal
+ problem
end;
fun dfg_prover (name, config) = (name, gen_dfg_prover (name, config));
--- a/src/HOL/Tools/metis_tools.ML Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOL/Tools/metis_tools.ML Fri Mar 05 10:42:13 2010 +0100
@@ -714,12 +714,12 @@
let val _ = trace_msg (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type Res_Axioms.type_has_empty_sort (prop_of st0)
- then (error "metis: Proof state contains the empty sort"; Seq.empty)
- else
- (Meson.MESON Res_Axioms.neg_clausify
- (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
- THEN Res_Axioms.expand_defs_tac st0) st0
+ if exists_type Res_Axioms.type_has_topsort (prop_of st0)
+ then raise METIS "Metis: Proof state contains the universal sort {}"
+ else
+ (Meson.MESON Res_Axioms.neg_clausify
+ (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
+ THEN Res_Axioms.expand_defs_tac st0) st0
end
handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
@@ -734,7 +734,7 @@
type_lits_setup #>
method @{binding metis} HO "METIS for FOL & HOL problems" #>
method @{binding metisF} FO "METIS for FOL problems" #>
- method @{binding metisFT} FT "METIS With-fully typed translation" #>
+ method @{binding metisFT} FT "METIS with fully-typed translation" #>
Method.setup @{binding finish_clausify}
(Scan.succeed (K (SIMPLE_METHOD (Res_Axioms.expand_defs_tac refl))))
"cleanup after conversion to clauses";
--- a/src/HOL/Tools/res_axioms.ML Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOL/Tools/res_axioms.ML Fri Mar 05 10:42:13 2010 +0100
@@ -12,7 +12,7 @@
val pairname: thm -> string * thm
val multi_base_blacklist: string list
val bad_for_atp: thm -> bool
- val type_has_empty_sort: typ -> bool
+ val type_has_topsort: typ -> bool
val cnf_rules_pairs: theory -> (string * thm) list -> (thm * (string * int)) list
val neg_clausify: thm list -> thm list
val expand_defs_tac: thm -> tactic
@@ -31,10 +31,10 @@
fun freeze_thm th = #1 (Drule.legacy_freeze_thaw th);
-fun type_has_empty_sort (TFree (_, [])) = true
- | type_has_empty_sort (TVar (_, [])) = true
- | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts
- | type_has_empty_sort _ = false;
+val type_has_topsort = Term.exists_subtype
+ (fn TFree (_, []) => true
+ | TVar (_, []) => true
+ | _ => false);
(**** Transformation of Elimination Rules into First-Order Formulas****)
@@ -321,7 +321,7 @@
fun bad_for_atp th =
too_complex (prop_of th)
- orelse exists_type type_has_empty_sort (prop_of th)
+ orelse exists_type type_has_topsort (prop_of th)
orelse is_strange_thm th;
val multi_base_blacklist =
--- a/src/HOLCF/FOCUS/Fstreams.thy Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOLCF/FOCUS/Fstreams.thy Fri Mar 05 10:42:13 2010 +0100
@@ -240,7 +240,6 @@
==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & (LUB i. X i) = s)"
apply (auto simp add: fstreams_lub_lemma1)
apply (rule_tac x="%n. stream_take n$s" in exI, auto)
-apply (simp add: chain_stream_take)
apply (induct_tac i, auto)
apply (drule fstreams_lub_lemma1, auto)
apply (rule_tac x="j" in exI, auto)
@@ -293,7 +292,6 @@
==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & (LUB i. X i) = ms)"
apply (auto simp add: fstreams_lub_lemma2)
apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
-apply (simp add: chain_stream_take)
apply (induct_tac i, auto)
apply (drule fstreams_lub_lemma2, auto)
apply (rule_tac x="j" in exI, auto)
--- a/src/HOLCF/Tools/Domain/domain_take_proofs.ML Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_take_proofs.ML Fri Mar 05 10:42:13 2010 +0100
@@ -188,6 +188,13 @@
(Thm.no_attributes (Binding.name name, thm))
||> Sign.parent_path;
+fun add_qualified_simp_thm name (path, thm) thy =
+ thy
+ |> Sign.add_path path
+ |> yield_singleton PureThy.add_thms
+ ((Binding.name name, thm), [Simplifier.simp_add])
+ ||> Sign.parent_path;
+
(******************************************************************************)
(************************** defining take functions ***************************)
(******************************************************************************)
@@ -262,9 +269,9 @@
val goal = mk_trp (mk_chain take_const);
val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
- val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
+ val thm = Goal.prove_global thy [] [] goal (K tac);
in
- add_qualified_thm "chain_take" (dname, chain_take_thm) thy
+ add_qualified_simp_thm "chain_take" (dname, thm) thy
end;
val (chain_take_thms, thy) =
fold_map prove_chain_take (take_consts ~~ dnames) thy;
@@ -342,17 +349,17 @@
(conjuncts dnames deflation_take_thm)) thy;
(* prove strictness of take functions *)
- fun prove_take_strict (take_const, dname) thy =
+ fun prove_take_strict (deflation_take, dname) thy =
let
- val goal = mk_trp (mk_strict (take_const $ Free ("n", natT)));
- val tac = rtac @{thm deflation_strict} 1
- THEN resolve_tac deflation_take_thms 1;
- val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
+ val take_strict_thm =
+ Drule.export_without_context
+ (@{thm deflation_strict} OF [deflation_take]);
in
add_qualified_thm "take_strict" (dname, take_strict_thm) thy
end;
val (take_strict_thms, thy) =
- fold_map prove_take_strict (take_consts ~~ dnames) thy;
+ fold_map prove_take_strict
+ (deflation_take_thms ~~ dnames) thy;
(* prove take/take rules *)
fun prove_take_take ((chain_take, deflation_take), dname) thy =
@@ -367,6 +374,19 @@
fold_map prove_take_take
(chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
+ (* prove take_below rules *)
+ fun prove_take_below (deflation_take, dname) thy =
+ let
+ val take_below_thm =
+ Drule.export_without_context
+ (@{thm deflation.below} OF [deflation_take]);
+ in
+ add_qualified_thm "take_below" (dname, take_below_thm) thy
+ end;
+ val (take_below_thms, thy) =
+ fold_map prove_take_below
+ (deflation_take_thms ~~ dnames) thy;
+
(* define finiteness predicates *)
fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
let
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Mar 04 21:52:26 2010 +0100
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Fri Mar 05 10:42:13 2010 +0100
@@ -196,15 +196,20 @@
pat_rews @ dist_les @ dist_eqs)
end; (* let *)
-fun comp_theorems (comp_dnam, eqs: eq list) thy =
+fun prove_coinduction
+ (comp_dnam, eqs : eq list)
+ (take_lemmas : thm list)
+ (thy : theory) : thm * theory =
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;
+fun dc_take dn = %%:(dn^"_take");
+val x_name = idx_name dnames "x";
+val n_eqs = length eqs;
-val _ = message ("Proving induction properties of domain "^comp_dname^" ...");
+val take_rews =
+ maps (fn dn => PureThy.get_thms thy (dn ^ ".take_rews")) dnames;
(* ----- define bisimulation predicate -------------------------------------- *)
@@ -280,6 +285,74 @@
||> Sign.parent_path;
end; (* local *)
+(* ----- theorem concerning coinduction ------------------------------------- *)
+
+local
+ val pg = pg' thy;
+ val xs = mapn (fn n => K (x_name n)) 1 dnames;
+ fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
+ val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
+ val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
+ val _ = trace " Proving coind_lemma...";
+ val coind_lemma =
+ let
+ fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
+ fun mk_eqn n dn =
+ (dc_take dn $ %:"n" ` bnd_arg n 0) ===
+ (dc_take dn $ %:"n" ` bnd_arg n 1);
+ fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
+ val goal =
+ mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
+ Library.foldr mk_all2 (xs,
+ Library.foldr mk_imp (mapn mk_prj 0 dnames,
+ foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
+ fun x_tacs ctxt n x = [
+ rotate_tac (n+1) 1,
+ etac all2E 1,
+ eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
+ TRY (safe_tac HOL_cs),
+ REPEAT (CHANGED (asm_simp_tac take_ss 1))];
+ fun tacs ctxt = [
+ rtac impI 1,
+ InductTacs.induct_tac ctxt [[SOME "n"]] 1,
+ simp_tac take_ss 1,
+ safe_tac HOL_cs] @
+ flat (mapn (x_tacs ctxt) 0 xs);
+ in pg [ax_bisim_def] goal tacs end;
+in
+ val _ = trace " Proving coind...";
+ val coind =
+ let
+ fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
+ fun mk_eqn x = %:x === %:(x^"'");
+ val goal =
+ mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
+ Logic.list_implies (mapn mk_prj 0 xs,
+ mk_trp (foldr1 mk_conj (map mk_eqn xs)));
+ val tacs =
+ TRY (safe_tac HOL_cs) ::
+ maps (fn take_lemma => [
+ rtac take_lemma 1,
+ cut_facts_tac [coind_lemma] 1,
+ fast_tac HOL_cs 1])
+ take_lemmas;
+ in pg [] goal (K tacs) end;
+end; (* local *)
+
+in
+ (coind, thy)
+end;
+
+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^" ...");
+
val pg = pg' thy;
(* ----- getting the composite axiom and definitions ------------------------ *)
@@ -556,58 +629,7 @@
end; (* local *)
-(* ----- theorem concerning coinduction ------------------------------------- *)
-
-local
- val xs = mapn (fn n => K (x_name n)) 1 dnames;
- fun bnd_arg n i = Bound(2*(n_eqs - n)-i-1);
- val take_ss = HOL_ss addsimps (@{thm Rep_CFun_strict1} :: take_rews);
- val sproj = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
- val _ = trace " Proving coind_lemma...";
- val coind_lemma =
- let
- fun mk_prj n _ = proj (%:"R") eqs n $ bnd_arg n 0 $ bnd_arg n 1;
- fun mk_eqn n dn =
- (dc_take dn $ %:"n" ` bnd_arg n 0) ===
- (dc_take dn $ %:"n" ` bnd_arg n 1);
- fun mk_all2 (x,t) = mk_all (x, mk_all (x^"'", t));
- val goal =
- mk_trp (mk_imp (%%:(comp_dname^"_bisim") $ %:"R",
- Library.foldr mk_all2 (xs,
- Library.foldr mk_imp (mapn mk_prj 0 dnames,
- foldr1 mk_conj (mapn mk_eqn 0 dnames)))));
- fun x_tacs ctxt n x = [
- rotate_tac (n+1) 1,
- etac all2E 1,
- eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1,
- TRY (safe_tac HOL_cs),
- REPEAT (CHANGED (asm_simp_tac take_ss 1))];
- fun tacs ctxt = [
- rtac impI 1,
- InductTacs.induct_tac ctxt [[SOME "n"]] 1,
- simp_tac take_ss 1,
- safe_tac HOL_cs] @
- flat (mapn (x_tacs ctxt) 0 xs);
- in pg [ax_bisim_def] goal tacs end;
-in
- val _ = trace " Proving coind...";
- val coind =
- let
- fun mk_prj n x = mk_trp (proj (%:"R") eqs n $ %:x $ %:(x^"'"));
- fun mk_eqn x = %:x === %:(x^"'");
- val goal =
- mk_trp (%%:(comp_dname^"_bisim") $ %:"R") ===>
- Logic.list_implies (mapn mk_prj 0 xs,
- mk_trp (foldr1 mk_conj (map mk_eqn xs)));
- val tacs =
- TRY (safe_tac HOL_cs) ::
- maps (fn take_lemma => [
- rtac take_lemma 1,
- cut_facts_tac [coind_lemma] 1,
- fast_tac HOL_cs 1])
- take_lemmas;
- in pg [] goal (K tacs) end;
-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]);