# HG changeset patch # User hoelzl # Date 1267782133 -3600 # Node ID c7ddb7105dded178662496efdc6a310f46138f61 # Parent b16d99a72dc9eed6bb398288af1ed6074aeae7c4# Parent 374c638a796e9729aefa99c31d332c5b1aa19183 merged diff -r b16d99a72dc9 -r c7ddb7105dde Admin/isatest/settings/at-poly-test --- 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" diff -r b16d99a72dc9 -r c7ddb7105dde README_REPOSITORY --- 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 ----------------------- diff -r b16d99a72dc9 -r c7ddb7105dde src/HOL/Auth/Message.thy --- 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 \ parts H) = (G \ 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\ parts G; G \ parts H |] ==> X\ parts H" by (drule parts_mono, blast) @@ -611,7 +611,7 @@ by blast lemma synth_subset_iff [simp]: "(synth G \ synth H) = (G \ 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\ synth G; G \ synth H |] ==> X\ synth H" by (drule synth_mono, blast) @@ -674,8 +674,7 @@ lemma parts_insert_subset_Un: "X\ G ==> parts(insert X H) \ parts G \ 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} \ synth (analz H) \ parts H"} *} +text{*More specifically for Fake. See also @{text Fake_parts_sing} below *} lemma Fake_parts_insert: "X \ synth (analz H) ==> parts (insert X H) \ synth (analz H) \ parts H" @@ -884,17 +883,17 @@ lemma Fake_analz_eq [simp]: "X \ 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 \ analz H ==> ALL G. H \ G --> analz (insert X G) = analz G"; + "X \ analz H ==> ALL G. H \ 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 \ synth (analz H) - ==> ALL G. H \ G --> (Key K \ analz (insert X G)) = (Key K \ analz G)"; + ==> ALL G. H \ G --> (Key K \ analz (insert X G)) = (Key K \ analz G)" apply (erule synth.induct) apply (simp_all add: gen_analz_insert_eq subset_trans [OF _ subset_insertI]) done diff -r b16d99a72dc9 -r c7ddb7105dde src/HOL/Tools/ATP_Manager/atp_manager.ML --- 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); diff -r b16d99a72dc9 -r c7ddb7105dde src/HOL/Tools/ATP_Manager/atp_wrapper.ML --- 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)); diff -r b16d99a72dc9 -r c7ddb7105dde src/HOL/Tools/metis_tools.ML --- 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"; diff -r b16d99a72dc9 -r c7ddb7105dde src/HOL/Tools/res_axioms.ML --- 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 = diff -r b16d99a72dc9 -r c7ddb7105dde src/HOLCF/FOCUS/Fstreams.thy --- 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 = ooo t) & (EX X. chain X & (ALL i. EX j. 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, ooo t)) & (EX X. chain X & (ALL i. EX j. (a, 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) diff -r b16d99a72dc9 -r c7ddb7105dde src/HOLCF/Tools/Domain/domain_take_proofs.ML --- 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 diff -r b16d99a72dc9 -r c7ddb7105dde src/HOLCF/Tools/Domain/domain_theorems.ML --- 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]);