# HG changeset patch # User nipkow # Date 1314984344 -7200 # Node ID 17dbd9d9db380a47fe94a108036fac7ce1216a3e # Parent fe03653315667519fd9f54b81451a6e81a307e53# Parent 22bbd0d1b943422ac0653dba14a0aef5b7dc9c21 merged diff -r 22bbd0d1b943 -r 17dbd9d9db38 Admin/Benchmarks/HOL-datatype/ROOT.ML --- a/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/Admin/Benchmarks/HOL-datatype/ROOT.ML Fri Sep 02 19:25:44 2011 +0200 @@ -5,7 +5,7 @@ val tests = ["Brackin", "Instructions", "SML", "Verilog"]; -timing := true; +Toplevel.timing := true; warning "\nset quick_and_dirty\n"; quick_and_dirty := true; use_thys tests; diff -r 22bbd0d1b943 -r 17dbd9d9db38 Admin/Benchmarks/HOL-record/ROOT.ML --- a/Admin/Benchmarks/HOL-record/ROOT.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/Admin/Benchmarks/HOL-record/ROOT.ML Fri Sep 02 19:25:44 2011 +0200 @@ -3,9 +3,9 @@ Some benchmark on large record. *) -val tests = ["RecordBenchmark"]; +val tests = ["Record_Benchmark"]; -timing := true; +Toplevel.timing := true; warning "\nset quick_and_dirty\n"; quick_and_dirty := true; use_thys tests; diff -r 22bbd0d1b943 -r 17dbd9d9db38 Admin/Benchmarks/HOL-record/RecordBenchmark.thy --- a/Admin/Benchmarks/HOL-record/RecordBenchmark.thy Fri Sep 02 19:25:18 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,395 +0,0 @@ -(* Title: Admin/Benchmarks/HOL-record/RecordBenchmark.thy - Author: Norbert Schirmer, DFKI -*) - -header {* Benchmark for large record *} - -theory RecordBenchmark -imports Main -begin - -ML {* Record.timing := true *} - -record many_A = -A000::nat -A001::nat -A002::nat -A003::nat -A004::nat -A005::nat -A006::nat -A007::nat -A008::nat -A009::nat -A010::nat -A011::nat -A012::nat -A013::nat -A014::nat -A015::nat -A016::nat -A017::nat -A018::nat -A019::nat -A020::nat -A021::nat -A022::nat -A023::nat -A024::nat -A025::nat -A026::nat -A027::nat -A028::nat -A029::nat -A030::nat -A031::nat -A032::nat -A033::nat -A034::nat -A035::nat -A036::nat -A037::nat -A038::nat -A039::nat -A040::nat -A041::nat -A042::nat -A043::nat -A044::nat -A045::nat -A046::nat -A047::nat -A048::nat -A049::nat -A050::nat -A051::nat -A052::nat -A053::nat -A054::nat -A055::nat -A056::nat -A057::nat -A058::nat -A059::nat -A060::nat -A061::nat -A062::nat -A063::nat -A064::nat -A065::nat -A066::nat -A067::nat -A068::nat -A069::nat -A070::nat -A071::nat -A072::nat -A073::nat -A074::nat -A075::nat -A076::nat -A077::nat -A078::nat -A079::nat -A080::nat -A081::nat -A082::nat -A083::nat -A084::nat -A085::nat -A086::nat -A087::nat -A088::nat -A089::nat -A090::nat -A091::nat -A092::nat -A093::nat -A094::nat -A095::nat -A096::nat -A097::nat -A098::nat -A099::nat -A100::nat -A101::nat -A102::nat -A103::nat -A104::nat -A105::nat -A106::nat -A107::nat -A108::nat -A109::nat -A110::nat -A111::nat -A112::nat -A113::nat -A114::nat -A115::nat -A116::nat -A117::nat -A118::nat -A119::nat -A120::nat -A121::nat -A122::nat -A123::nat -A124::nat -A125::nat -A126::nat -A127::nat -A128::nat -A129::nat -A130::nat -A131::nat -A132::nat -A133::nat -A134::nat -A135::nat -A136::nat -A137::nat -A138::nat -A139::nat -A140::nat -A141::nat -A142::nat -A143::nat -A144::nat -A145::nat -A146::nat -A147::nat -A148::nat -A149::nat -A150::nat -A151::nat -A152::nat -A153::nat -A154::nat -A155::nat -A156::nat -A157::nat -A158::nat -A159::nat -A160::nat -A161::nat -A162::nat -A163::nat -A164::nat -A165::nat -A166::nat -A167::nat -A168::nat -A169::nat -A170::nat -A171::nat -A172::nat -A173::nat -A174::nat -A175::nat -A176::nat -A177::nat -A178::nat -A179::nat -A180::nat -A181::nat -A182::nat -A183::nat -A184::nat -A185::nat -A186::nat -A187::nat -A188::nat -A189::nat -A190::nat -A191::nat -A192::nat -A193::nat -A194::nat -A195::nat -A196::nat -A197::nat -A198::nat -A199::nat -A200::nat -A201::nat -A202::nat -A203::nat -A204::nat -A205::nat -A206::nat -A207::nat -A208::nat -A209::nat -A210::nat -A211::nat -A212::nat -A213::nat -A214::nat -A215::nat -A216::nat -A217::nat -A218::nat -A219::nat -A220::nat -A221::nat -A222::nat -A223::nat -A224::nat -A225::nat -A226::nat -A227::nat -A228::nat -A229::nat -A230::nat -A231::nat -A232::nat -A233::nat -A234::nat -A235::nat -A236::nat -A237::nat -A238::nat -A239::nat -A240::nat -A241::nat -A242::nat -A243::nat -A244::nat -A245::nat -A246::nat -A247::nat -A248::nat -A249::nat -A250::nat -A251::nat -A252::nat -A253::nat -A254::nat -A255::nat -A256::nat -A257::nat -A258::nat -A259::nat -A260::nat -A261::nat -A262::nat -A263::nat -A264::nat -A265::nat -A266::nat -A267::nat -A268::nat -A269::nat -A270::nat -A271::nat -A272::nat -A273::nat -A274::nat -A275::nat -A276::nat -A277::nat -A278::nat -A279::nat -A280::nat -A281::nat -A282::nat -A283::nat -A284::nat -A285::nat -A286::nat -A287::nat -A288::nat -A289::nat -A290::nat -A291::nat -A292::nat -A293::nat -A294::nat -A295::nat -A296::nat -A297::nat -A298::nat -A299::nat - -lemma "A155 (r\A255:=x\) = A155 r" -by simp - -lemma "A155 (r\A255:=x,A253:=y,A255:=z \) = A155 r" -by simp - -lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" -by simp - -lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" -apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.record_upd_simproc]) 1*}) -done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) - apply simp - done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) - apply simp - done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) - apply simp - done - -lemma "(\r. P (A155 r)) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) - apply simp - done - -lemma "\r. P (A155 r) \ (\x. P x)" - apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*}) - apply auto - done - -lemma "\r. P (A155 r) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) - apply auto - done - -lemma "P (A155 r) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) - apply auto - done - -lemma fixes r shows "P (A155 r) \ (\x. P x)" - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) - apply auto - done - - -lemma True -proof - - { - fix P r - assume pre: "P (A155 r)" - have "\x. P x" - using pre - apply - - apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*}) - apply auto - done - } - show ?thesis .. -qed - - -lemma "\r. A155 r = x" - apply (tactic {*simp_tac - (HOL_basic_ss addsimprocs [Record.record_ex_sel_eq_simproc]) 1*}) - done - - -end \ No newline at end of file diff -r 22bbd0d1b943 -r 17dbd9d9db38 Admin/Benchmarks/HOL-record/Record_Benchmark.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/Benchmarks/HOL-record/Record_Benchmark.thy Fri Sep 02 19:25:44 2011 +0200 @@ -0,0 +1,390 @@ +(* Title: Admin/Benchmarks/HOL-record/Record_Benchmark.thy + Author: Norbert Schirmer, DFKI +*) + +header {* Benchmark for large record *} + +theory Record_Benchmark +imports Main +begin + +declare [[record_timing]] + +record many_A = +A000::nat +A001::nat +A002::nat +A003::nat +A004::nat +A005::nat +A006::nat +A007::nat +A008::nat +A009::nat +A010::nat +A011::nat +A012::nat +A013::nat +A014::nat +A015::nat +A016::nat +A017::nat +A018::nat +A019::nat +A020::nat +A021::nat +A022::nat +A023::nat +A024::nat +A025::nat +A026::nat +A027::nat +A028::nat +A029::nat +A030::nat +A031::nat +A032::nat +A033::nat +A034::nat +A035::nat +A036::nat +A037::nat +A038::nat +A039::nat +A040::nat +A041::nat +A042::nat +A043::nat +A044::nat +A045::nat +A046::nat +A047::nat +A048::nat +A049::nat +A050::nat +A051::nat +A052::nat +A053::nat +A054::nat +A055::nat +A056::nat +A057::nat +A058::nat +A059::nat +A060::nat +A061::nat +A062::nat +A063::nat +A064::nat +A065::nat +A066::nat +A067::nat +A068::nat +A069::nat +A070::nat +A071::nat +A072::nat +A073::nat +A074::nat +A075::nat +A076::nat +A077::nat +A078::nat +A079::nat +A080::nat +A081::nat +A082::nat +A083::nat +A084::nat +A085::nat +A086::nat +A087::nat +A088::nat +A089::nat +A090::nat +A091::nat +A092::nat +A093::nat +A094::nat +A095::nat +A096::nat +A097::nat +A098::nat +A099::nat +A100::nat +A101::nat +A102::nat +A103::nat +A104::nat +A105::nat +A106::nat +A107::nat +A108::nat +A109::nat +A110::nat +A111::nat +A112::nat +A113::nat +A114::nat +A115::nat +A116::nat +A117::nat +A118::nat +A119::nat +A120::nat +A121::nat +A122::nat +A123::nat +A124::nat +A125::nat +A126::nat +A127::nat +A128::nat +A129::nat +A130::nat +A131::nat +A132::nat +A133::nat +A134::nat +A135::nat +A136::nat +A137::nat +A138::nat +A139::nat +A140::nat +A141::nat +A142::nat +A143::nat +A144::nat +A145::nat +A146::nat +A147::nat +A148::nat +A149::nat +A150::nat +A151::nat +A152::nat +A153::nat +A154::nat +A155::nat +A156::nat +A157::nat +A158::nat +A159::nat +A160::nat +A161::nat +A162::nat +A163::nat +A164::nat +A165::nat +A166::nat +A167::nat +A168::nat +A169::nat +A170::nat +A171::nat +A172::nat +A173::nat +A174::nat +A175::nat +A176::nat +A177::nat +A178::nat +A179::nat +A180::nat +A181::nat +A182::nat +A183::nat +A184::nat +A185::nat +A186::nat +A187::nat +A188::nat +A189::nat +A190::nat +A191::nat +A192::nat +A193::nat +A194::nat +A195::nat +A196::nat +A197::nat +A198::nat +A199::nat +A200::nat +A201::nat +A202::nat +A203::nat +A204::nat +A205::nat +A206::nat +A207::nat +A208::nat +A209::nat +A210::nat +A211::nat +A212::nat +A213::nat +A214::nat +A215::nat +A216::nat +A217::nat +A218::nat +A219::nat +A220::nat +A221::nat +A222::nat +A223::nat +A224::nat +A225::nat +A226::nat +A227::nat +A228::nat +A229::nat +A230::nat +A231::nat +A232::nat +A233::nat +A234::nat +A235::nat +A236::nat +A237::nat +A238::nat +A239::nat +A240::nat +A241::nat +A242::nat +A243::nat +A244::nat +A245::nat +A246::nat +A247::nat +A248::nat +A249::nat +A250::nat +A251::nat +A252::nat +A253::nat +A254::nat +A255::nat +A256::nat +A257::nat +A258::nat +A259::nat +A260::nat +A261::nat +A262::nat +A263::nat +A264::nat +A265::nat +A266::nat +A267::nat +A268::nat +A269::nat +A270::nat +A271::nat +A272::nat +A273::nat +A274::nat +A275::nat +A276::nat +A277::nat +A278::nat +A279::nat +A280::nat +A281::nat +A282::nat +A283::nat +A284::nat +A285::nat +A286::nat +A287::nat +A288::nat +A289::nat +A290::nat +A291::nat +A292::nat +A293::nat +A294::nat +A295::nat +A296::nat +A297::nat +A298::nat +A299::nat + +lemma "A155 (r\A255:=x\) = A155 r" + by simp + +lemma "A155 (r\A255:=x,A253:=y,A255:=z \) = A155 r" + by simp + +lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" + by simp + +lemma "(r\A255:=x,A253:=y,A255:=z \) = r\A253:=y,A255:=z\" + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*}) + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply simp + done + +lemma "(\r. P (A155 r)) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) + apply simp + done + +lemma "\r. P (A155 r) \ (\x. P x)" + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply auto + done + +lemma "\r. P (A155 r) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) + apply auto + done + +lemma "P (A155 r) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) + apply auto + done + +lemma fixes r shows "P (A155 r) \ (\x. P x)" + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) + apply auto + done + + +lemma True +proof - + { + fix P r + assume pre: "P (A155 r)" + have "\x. P x" + using pre + apply - + apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) + apply auto + done + } + show ?thesis .. +qed + + +lemma "\r. A155 r = x" + apply (tactic {*simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*}) + done + + +end \ No newline at end of file diff -r 22bbd0d1b943 -r 17dbd9d9db38 Admin/Benchmarks/IsaMakefile --- a/Admin/Benchmarks/IsaMakefile Fri Sep 02 19:25:18 2011 +0200 +++ b/Admin/Benchmarks/IsaMakefile Fri Sep 02 19:25:44 2011 +0200 @@ -33,7 +33,7 @@ HOL-record: HOL $(LOG)/HOL-record.gz $(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML \ - HOL-record/RecordBenchmark.thy + HOL-record/Record_Benchmark.thy @$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Algebra/AbelCoset.thy Fri Sep 02 19:25:44 2011 +0200 @@ -233,10 +233,10 @@ shows "abelian_subgroup H G" proof - interpret normal "H" "\carrier = carrier G, mult = add G, one = zero G\" - by (rule a_normal) + by (rule a_normal) show "abelian_subgroup H G" - proof qed (simp add: a_comm) + by default (simp add: a_comm) qed lemma abelian_subgroupI2: diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Fri Sep 02 19:25:44 2011 +0200 @@ -25,14 +25,14 @@ and r_cancel: "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" shows "monoid_cancel G" - proof qed fact+ + by default fact+ lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" .. sublocale group \ monoid_cancel - proof qed simp+ + by default simp_all locale comm_monoid_cancel = monoid_cancel + comm_monoid @@ -3655,7 +3655,7 @@ done sublocale factorial_monoid \ primeness_condition_monoid - proof qed (rule irreducible_is_prime) + by default (rule irreducible_is_prime) lemma (in factorial_monoid) primeness_condition: @@ -3664,10 +3664,10 @@ lemma (in factorial_monoid) gcd_condition [simp]: shows "gcd_condition_monoid G" - proof qed (rule gcdof_exists) + by default (rule gcdof_exists) sublocale factorial_monoid \ gcd_condition_monoid - proof qed (rule gcdof_exists) + by default (rule gcdof_exists) lemma (in factorial_monoid) division_weak_lattice [simp]: shows "weak_lattice (division_rel G)" diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Algebra/Group.thy Fri Sep 02 19:25:44 2011 +0200 @@ -286,7 +286,7 @@ qed then have carrier_subset_Units: "carrier G <= Units G" by (unfold Units_def) fast - show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units) + show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units) qed lemma (in monoid) group_l_invI: @@ -694,7 +694,7 @@ assumes m_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x" shows "comm_group G" - proof qed (simp_all add: m_comm) + by default (simp_all add: m_comm) lemma comm_groupI: fixes G (structure) @@ -722,7 +722,7 @@ theorem (in group) subgroups_partial_order: "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \ |)" - proof qed simp_all + by default simp_all lemma (in group) subgroup_self: "subgroup (carrier G) G" diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Algebra/IntRing.thy Fri Sep 02 19:25:44 2011 +0200 @@ -62,7 +62,7 @@ and "pow \ x n = x^n" proof - -- "Specification" - show "monoid \" proof qed auto + show "monoid \" by default auto then interpret int: monoid \ . -- "Carrier" @@ -79,7 +79,7 @@ where "finprod \ f A = (if finite A then setprod f A else undefined)" proof - -- "Specification" - show "comm_monoid \" proof qed auto + show "comm_monoid \" by default auto then interpret int: comm_monoid \ . -- "Operations" @@ -105,7 +105,7 @@ and int_finsum_eq: "finsum \ f A = (if finite A then setsum f A else undefined)" proof - -- "Specification" - show "abelian_monoid \" proof qed auto + show "abelian_monoid \" by default auto then interpret int: abelian_monoid \ . -- "Carrier" @@ -189,7 +189,7 @@ and "lless (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x < y)" proof - show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \ |)" - proof qed simp_all + by default simp_all show "carrier (| carrier = UNIV::int set, eq = op =, le = op \ |) = UNIV" by simp show "le (| carrier = UNIV::int set, eq = op =, le = op \ |) x y = (x \ y)" @@ -226,7 +226,7 @@ interpretation int (* [unfolded UNIV] *) : total_order "(| carrier = UNIV::int set, eq = op =, le = op \ |)" - proof qed clarsimp + by default clarsimp subsection {* Generated Ideals of @{text "\"} *} diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Algebra/Lattice.thy Fri Sep 02 19:25:44 2011 +0200 @@ -921,7 +921,7 @@ lemma (in weak_partial_order) weak_total_orderI: assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" shows "weak_total_order L" - proof qed (rule total) + by default (rule total) text {* Total orders are lattices. *} @@ -985,7 +985,7 @@ and inf_exists: "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" shows "weak_complete_lattice L" - proof qed (auto intro: sup_exists inf_exists) + by default (auto intro: sup_exists inf_exists) definition top :: "_ => 'a" ("\\") @@ -1133,14 +1133,14 @@ "[| x \ carrier L; y \ carrier L |] ==> EX s. least L s (Upper L {x, y})" sublocale upper_semilattice < weak: weak_upper_semilattice - proof qed (rule sup_of_two_exists) + by default (rule sup_of_two_exists) locale lower_semilattice = partial_order + assumes inf_of_two_exists: "[| x \ carrier L; y \ carrier L |] ==> EX s. greatest L s (Lower L {x, y})" sublocale lower_semilattice < weak: weak_lower_semilattice - proof qed (rule inf_of_two_exists) + by default (rule inf_of_two_exists) locale lattice = upper_semilattice + lower_semilattice @@ -1191,19 +1191,19 @@ assumes total_order_total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" sublocale total_order < weak: weak_total_order - proof qed (rule total_order_total) + by default (rule total_order_total) text {* Introduction rule: the usual definition of total order *} lemma (in partial_order) total_orderI: assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" shows "total_order L" - proof qed (rule total) + by default (rule total) text {* Total orders are lattices. *} sublocale total_order < weak: lattice - proof qed (auto intro: sup_of_two_exists inf_of_two_exists) + by default (auto intro: sup_of_two_exists inf_of_two_exists) text {* Complete lattices *} @@ -1215,7 +1215,7 @@ "[| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" sublocale complete_lattice < weak: weak_complete_lattice - proof qed (auto intro: sup_exists inf_exists) + by default (auto intro: sup_exists inf_exists) text {* Introduction rule: the usual definition of complete lattice *} @@ -1225,7 +1225,7 @@ and inf_exists: "!!A. [| A \ carrier L |] ==> EX i. greatest L i (Lower L A)" shows "complete_lattice L" - proof qed (auto intro: sup_exists inf_exists) + by default (auto intro: sup_exists inf_exists) theorem (in partial_order) complete_lattice_criterion1: assumes top_exists: "EX g. greatest L g (carrier L)" diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Algebra/RingHom.thy --- a/src/HOL/Algebra/RingHom.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Algebra/RingHom.thy Fri Sep 02 19:25:44 2011 +0200 @@ -17,7 +17,7 @@ and hom_one [simp] = ring_hom_one [OF homh] sublocale ring_hom_cring \ ring: ring_hom_ring - proof qed (rule homh) + by default (rule homh) sublocale ring_hom_ring \ abelian_group: abelian_group_hom R S apply (rule abelian_group_homI) diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Fri Sep 02 19:25:44 2011 +0200 @@ -1764,7 +1764,7 @@ and deg_r_0: "deg R r = 0" shows "r = monom P (eval R R id a f) 0" proof - - interpret UP_pre_univ_prop R R id P proof qed simp + interpret UP_pre_univ_prop R R id P by default simp have eval_ring_hom: "eval R R id a \ ring_hom P R" using eval_ring_hom [OF a] by simp have "eval R R id a f = eval R R id a ?gq \\<^bsub>R\<^esub> eval R R id a r" diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/IsaMakefile Fri Sep 02 19:25:44 2011 +0200 @@ -234,7 +234,7 @@ Tools/Meson/meson_clausify.ML \ Tools/Meson/meson_tactic.ML \ Tools/Metis/metis_reconstruct.ML \ - Tools/Metis/metis_tactics.ML \ + Tools/Metis/metis_tactic.ML \ Tools/Metis/metis_translate.ML \ Tools/abel_cancel.ML \ Tools/arith_data.ML \ diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Metis.thy --- a/src/HOL/Metis.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Metis.thy Fri Sep 02 19:25:44 2011 +0200 @@ -11,7 +11,7 @@ uses "~~/src/Tools/Metis/metis.ML" ("Tools/Metis/metis_translate.ML") ("Tools/Metis/metis_reconstruct.ML") - ("Tools/Metis/metis_tactics.ML") + ("Tools/Metis/metis_tactic.ML") ("Tools/try_methods.ML") begin @@ -36,9 +36,9 @@ use "Tools/Metis/metis_translate.ML" use "Tools/Metis/metis_reconstruct.ML" -use "Tools/Metis/metis_tactics.ML" +use "Tools/Metis/metis_tactic.ML" -setup {* Metis_Tactics.setup *} +setup {* Metis_Tactic.setup *} hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Fri Sep 02 19:25:44 2011 +0200 @@ -70,7 +70,7 @@ | tac (type_enc :: type_encs) st = st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *) |> ((if null type_encs then all_tac else rtac @{thm fork} 1) - THEN Metis_Tactics.metis_tac [type_enc] ctxt ths 1 + THEN Metis_Tactic.metis_tac [type_enc] ctxt ths 1 THEN COND (has_fewer_prems 2) all_tac no_tac THEN tac type_encs) in tac end diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Mirabelle/Tools/mirabelle_metis.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Fri Sep 02 19:25:44 2011 +0200 @@ -18,7 +18,7 @@ val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre)) - fun metis ctxt = Metis_Tactics.metis_tac [] ctxt (thms @ facts) + fun metis ctxt = Metis_Tactic.metis_tac [] ctxt (thms @ facts) in (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed") |> prefix (metis_tag id) diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Sep 02 19:25:44 2011 +0200 @@ -577,15 +577,15 @@ sledge_tac 0.25 ATP_Systems.z3_tptpN "mono_simple" ORELSE' sledge_tac 0.25 ATP_Systems.eN "mono_guards?" ORELSE' sledge_tac 0.25 ATP_Systems.spassN "poly_tags_uniform" - ORELSE' Metis_Tactics.metis_tac [] ctxt thms + ORELSE' Metis_Tactic.metis_tac [] ctxt thms else if !reconstructor = "smt" then SMT_Solver.smt_tac ctxt thms else if full orelse !reconstructor = "metis (full_types)" then - Metis_Tactics.metis_tac [Metis_Tactics.full_type_enc] ctxt thms + Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms else if !reconstructor = "metis (no_types)" then - Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] ctxt thms + Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms else if !reconstructor = "metis" then - Metis_Tactics.metis_tac [] ctxt thms + Metis_Tactic.metis_tac [] ctxt thms else K all_tac end diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri Sep 02 19:25:44 2011 +0200 @@ -349,7 +349,7 @@ map (rpair (mk_type thy prfx ty)) flds) fldtys in case get_type thy prfx s of NONE => - Record.add_record true ([], Binding.name s) NONE + Record.add_record ([], Binding.name s) NONE (map (fn (fld, T) => (Binding.name fld, T, NoSyn)) fldTs) thy | SOME rT => (case get_record_info thy rT of diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/TPTP/CASC_Setup.thy --- a/src/HOL/TPTP/CASC_Setup.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/TPTP/CASC_Setup.thy Fri Sep 02 19:25:44 2011 +0200 @@ -131,7 +131,7 @@ Sledgehammer_Filter.no_relevance_override)) ORELSE SOLVE_TIMEOUT (max_secs div 10) "metis" - (ALLGOALS (Metis_Tactics.metis_tac [] ctxt [])) + (ALLGOALS (Metis_Tactic.metis_tac [] ctxt [])) ORELSE SOLVE_TIMEOUT (max_secs div 10) "fast" (ALLGOALS (fast_tac ctxt)) ORELSE diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Fri Sep 02 19:25:44 2011 +0200 @@ -53,6 +53,7 @@ val tptp_product_type : string val tptp_forall : string val tptp_ho_forall : string + val tptp_pi_binder : string val tptp_exists : string val tptp_ho_exists : string val tptp_choice : string @@ -160,6 +161,7 @@ val tptp_product_type = "*" val tptp_forall = "!" val tptp_ho_forall = "!!" +val tptp_pi_binder = "!>" val tptp_exists = "?" val tptp_ho_exists = "??" val tptp_choice = "@+" @@ -259,7 +261,7 @@ str false ty1 ^ " " ^ tptp_fun_type ^ " " ^ str true ty2 |> not rhs ? enclose "(" ")" | str _ (ATyAbs (ss, ty)) = - tptp_forall ^ "[" ^ + tptp_pi_binder ^ "[" ^ commas (map (suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)) ss) ^ "] : " ^ str false ty in str true ty end diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/Metis/metis_tactic.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Fri Sep 02 19:25:44 2011 +0200 @@ -0,0 +1,268 @@ +(* Title: HOL/Tools/Metis/metis_tactic.ML + Author: Kong W. Susanto, Cambridge University Computer Laboratory + Author: Lawrence C. Paulson, Cambridge University Computer Laboratory + Author: Jasmin Blanchette, TU Muenchen + Copyright Cambridge University 2007 + +HOL setup for the Metis prover. +*) + +signature METIS_TACTIC = +sig + val metisN : string + val full_typesN : string + val partial_typesN : string + val no_typesN : string + val really_full_type_enc : string + val full_type_enc : string + val partial_type_enc : string + val no_type_enc : string + val full_type_syss : string list + val partial_type_syss : string list + val trace : bool Config.T + val verbose : bool Config.T + val new_skolemizer : bool Config.T + val metis_tac : string list -> Proof.context -> thm list -> int -> tactic + val setup : theory -> theory +end + +structure Metis_Tactic : METIS_TACTIC = +struct + +open ATP_Translate +open Metis_Translate +open Metis_Reconstruct + +val metisN = "metis" + +val full_typesN = "full_types" +val partial_typesN = "partial_types" +val no_typesN = "no_types" + +val really_full_type_enc = "mono_tags_uniform" +val full_type_enc = "poly_guards_uniform_query" +val partial_type_enc = "poly_args" +val no_type_enc = "erased" + +val full_type_syss = [full_type_enc, really_full_type_enc] +val partial_type_syss = partial_type_enc :: full_type_syss + +val type_enc_aliases = + [(full_typesN, full_type_syss), + (partial_typesN, partial_type_syss), + (no_typesN, [no_type_enc])] + +fun method_call_for_type_enc type_syss = + metisN ^ " (" ^ + (case AList.find (op =) type_enc_aliases type_syss of + [alias] => alias + | _ => hd type_syss) ^ ")" + +val new_skolemizer = + Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) + +(* Designed to work also with monomorphic instances of polymorphic theorems. *) +fun have_common_thm ths1 ths2 = + exists (member (Term.aconv_untyped o pairself prop_of) ths1) + (map Meson.make_meta_clause ths2) + +(*Determining which axiom clauses are actually used*) +fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) + | used_axioms _ _ = NONE + +(* Lightweight predicate type information comes in two flavors, "t = t'" and + "t => t'", where "t" and "t'" are the same term modulo type tags. + In Isabelle, type tags are stripped away, so we are left with "t = t" or + "t => t". Type tag idempotence is also handled this way. *) +fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth = + let val thy = Proof_Context.theory_of ctxt in + case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of + Const (@{const_name HOL.eq}, _) $ _ $ t => + let + val ct = cterm_of thy t + val cT = ctyp_of_term ct + in refl |> Drule.instantiate' [SOME cT] [SOME ct] end + | Const (@{const_name disj}, _) $ t1 $ t2 => + (if can HOLogic.dest_not t1 then t2 else t1) + |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial + | _ => raise Fail "unexpected tags sym clause" + end + |> Meson.make_meta_clause + +val clause_params = + {ordering = Metis_KnuthBendixOrder.default, + orderLiterals = Metis_Clause.UnsignedLiteralOrder, + orderTerms = true} +val active_params = + {clause = clause_params, + prefactor = #prefactor Metis_Active.default, + postfactor = #postfactor Metis_Active.default} +val waiting_params = + {symbolsWeight = 1.0, + variablesWeight = 0.0, + literalsWeight = 0.0, + models = []} +val resolution_params = {active = active_params, waiting = waiting_params} + +(* Main function to start Metis proof and reconstruction *) +fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 = + let val thy = Proof_Context.theory_of ctxt + val new_skolemizer = + Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) + val th_cls_pairs = + map2 (fn j => fn th => + (Thm.get_name_hint th, + Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) + (0 upto length ths0 - 1) ths0 + val ths = maps (snd o snd) th_cls_pairs + val dischargers = map (fst o snd) th_cls_pairs + val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls + val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths + val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) + val type_enc = type_enc_from_string Sound type_enc + val (sym_tab, axioms, old_skolems) = + prepare_metis_problem ctxt type_enc cls ths + fun get_isa_thm mth Isa_Reflexive_or_Trivial = + reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth + | get_isa_thm _ (Isa_Raw ith) = ith + val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) + val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") + val thms = axioms |> map fst + val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms + val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") + in + case filter (fn t => prop_of t aconv @{prop False}) cls of + false_th :: _ => [false_th RS @{thm FalseE}] + | [] => + case Metis_Resolution.new resolution_params + {axioms = thms, conjecture = []} + |> Metis_Resolution.loop of + Metis_Resolution.Contradiction mth => + let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ + Metis_Thm.toString mth) + val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt + (*add constraints arising from converting goal to clause form*) + val proof = Metis_Proof.proof mth + val result = + axioms + |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof + val used = map_filter (used_axioms axioms) proof + val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") + val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used + val names = th_cls_pairs |> map fst + val used_names = + th_cls_pairs + |> map_filter (fn (name, (_, cls)) => + if have_common_thm used cls then SOME name + else NONE) + val unused_names = names |> subtract (op =) used_names + in + if not (null cls) andalso not (have_common_thm used cls) then + verbose_warning ctxt "The assumptions are inconsistent" + else + (); + if not (null unused_names) then + "Unused theorems: " ^ commas_quote unused_names + |> verbose_warning ctxt + else + (); + case result of + (_,ith)::_ => + (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); + [discharge_skolem_premises ctxt dischargers ith]) + | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) + end + | Metis_Resolution.Satisfiable _ => + (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); + if null fallback_type_syss then + () + else + raise METIS ("FOL_SOLVE", + "No first-order proof with the lemmas supplied"); + []) + end + handle METIS (loc, msg) => + case fallback_type_syss of + [] => error ("Failed to replay Metis proof in Isabelle." ^ + (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg + else "")) + | _ => + (verbose_warning ctxt + ("Falling back on " ^ + quote (method_call_for_type_enc fallback_type_syss) ^ "..."); + FOL_SOLVE fallback_type_syss ctxt cls ths0) + +fun neg_clausify ctxt = + single + #> Meson.make_clauses_unsorted ctxt + #> map Meson_Clausify.introduce_combinators_in_theorem + #> Meson.finish_cnf + +fun preskolem_tac ctxt st0 = + (if exists (Meson.has_too_many_clauses ctxt) + (Logic.prems_of_goal (prop_of st0) 1) then + Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1 + THEN cnf.cnfx_rewrite_tac ctxt 1 + else + all_tac) st0 + +val type_has_top_sort = + exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) + +fun generic_metis_tac type_syss ctxt ths i st0 = + let + val _ = trace_msg ctxt (fn () => + "Metis called with theorems\n" ^ + cat_lines (map (Display.string_of_thm ctxt) ths)) + fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 + in + if exists_type type_has_top_sort (prop_of st0) then + verbose_warning ctxt "Proof state contains the universal sort {}" + else + (); + Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0 + end + +fun metis_tac [] = generic_metis_tac partial_type_syss + | metis_tac type_syss = generic_metis_tac type_syss + +(* Whenever "X" has schematic type variables, we treat "using X by metis" as + "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. + We don't do it for nonschematic facts "X" because this breaks a few proofs + (in the rare and subtle case where a proof relied on extensionality not being + applied) and brings few benefits. *) +val has_tvar = + exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of + +fun method default_type_syss (override_type_syss, ths) ctxt facts = + let + val _ = + if default_type_syss = full_type_syss then + legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead" + else + () + val (schem_facts, nonschem_facts) = List.partition has_tvar facts + val type_syss = override_type_syss |> the_default default_type_syss + in + HEADGOAL (Method.insert_tac nonschem_facts THEN' + CHANGED_PROP + o generic_metis_tac type_syss ctxt (schem_facts @ ths)) + end + +fun setup_method (binding, type_syss) = + ((Args.parens (Scan.repeat Parse.short_ident) + >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s])) + |> Scan.option |> Scan.lift) + -- Attrib.thms >> (METHOD oo method type_syss) + |> Method.setup binding + +val setup = + [((@{binding metis}, partial_type_syss), + "Metis for FOL and HOL problems"), + ((@{binding metisFT}, full_type_syss), + "Metis for FOL/HOL problems with fully-typed translation")] + |> fold (uncurry setup_method) + +end; diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Fri Sep 02 19:25:18 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,268 +0,0 @@ -(* Title: HOL/Tools/Metis/metis_tactics.ML - Author: Kong W. Susanto, Cambridge University Computer Laboratory - Author: Lawrence C. Paulson, Cambridge University Computer Laboratory - Author: Jasmin Blanchette, TU Muenchen - Copyright Cambridge University 2007 - -HOL setup for the Metis prover. -*) - -signature METIS_TACTICS = -sig - val metisN : string - val full_typesN : string - val partial_typesN : string - val no_typesN : string - val really_full_type_enc : string - val full_type_enc : string - val partial_type_enc : string - val no_type_enc : string - val full_type_syss : string list - val partial_type_syss : string list - val trace : bool Config.T - val verbose : bool Config.T - val new_skolemizer : bool Config.T - val metis_tac : string list -> Proof.context -> thm list -> int -> tactic - val setup : theory -> theory -end - -structure Metis_Tactics : METIS_TACTICS = -struct - -open ATP_Translate -open Metis_Translate -open Metis_Reconstruct - -val metisN = "metis" - -val full_typesN = "full_types" -val partial_typesN = "partial_types" -val no_typesN = "no_types" - -val really_full_type_enc = "mono_tags_uniform" -val full_type_enc = "poly_guards_uniform_query" -val partial_type_enc = "poly_args" -val no_type_enc = "erased" - -val full_type_syss = [full_type_enc, really_full_type_enc] -val partial_type_syss = partial_type_enc :: full_type_syss - -val type_enc_aliases = - [(full_typesN, full_type_syss), - (partial_typesN, partial_type_syss), - (no_typesN, [no_type_enc])] - -fun method_call_for_type_enc type_syss = - metisN ^ " (" ^ - (case AList.find (op =) type_enc_aliases type_syss of - [alias] => alias - | _ => hd type_syss) ^ ")" - -val new_skolemizer = - Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) - -(* Designed to work also with monomorphic instances of polymorphic theorems. *) -fun have_common_thm ths1 ths2 = - exists (member (Term.aconv_untyped o pairself prop_of) ths1) - (map Meson.make_meta_clause ths2) - -(*Determining which axiom clauses are actually used*) -fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) - | used_axioms _ _ = NONE - -(* Lightweight predicate type information comes in two flavors, "t = t'" and - "t => t'", where "t" and "t'" are the same term modulo type tags. - In Isabelle, type tags are stripped away, so we are left with "t = t" or - "t => t". Type tag idempotence is also handled this way. *) -fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth = - let val thy = Proof_Context.theory_of ctxt in - case hol_clause_from_metis ctxt type_enc sym_tab old_skolems mth of - Const (@{const_name HOL.eq}, _) $ _ $ t => - let - val ct = cterm_of thy t - val cT = ctyp_of_term ct - in refl |> Drule.instantiate' [SOME cT] [SOME ct] end - | Const (@{const_name disj}, _) $ t1 $ t2 => - (if can HOLogic.dest_not t1 then t2 else t1) - |> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial - | _ => raise Fail "unexpected tags sym clause" - end - |> Meson.make_meta_clause - -val clause_params = - {ordering = Metis_KnuthBendixOrder.default, - orderLiterals = Metis_Clause.UnsignedLiteralOrder, - orderTerms = true} -val active_params = - {clause = clause_params, - prefactor = #prefactor Metis_Active.default, - postfactor = #postfactor Metis_Active.default} -val waiting_params = - {symbolsWeight = 1.0, - variablesWeight = 0.0, - literalsWeight = 0.0, - models = []} -val resolution_params = {active = active_params, waiting = waiting_params} - -(* Main function to start Metis proof and reconstruction *) -fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 = - let val thy = Proof_Context.theory_of ctxt - val new_skolemizer = - Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) - val th_cls_pairs = - map2 (fn j => fn th => - (Thm.get_name_hint th, - Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) - (0 upto length ths0 - 1) ths0 - val ths = maps (snd o snd) th_cls_pairs - val dischargers = map (fst o snd) th_cls_pairs - val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls - val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths - val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) - val type_enc = type_enc_from_string Sound type_enc - val (sym_tab, axioms, old_skolems) = - prepare_metis_problem ctxt type_enc cls ths - fun get_isa_thm mth Isa_Reflexive_or_Trivial = - reflexive_or_trivial_from_metis ctxt type_enc sym_tab old_skolems mth - | get_isa_thm _ (Isa_Raw ith) = ith - val axioms = axioms |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) - val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") - val thms = axioms |> map fst - val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms - val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") - in - case filter (fn t => prop_of t aconv @{prop False}) cls of - false_th :: _ => [false_th RS @{thm FalseE}] - | [] => - case Metis_Resolution.new resolution_params - {axioms = thms, conjecture = []} - |> Metis_Resolution.loop of - Metis_Resolution.Contradiction mth => - let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ - Metis_Thm.toString mth) - val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt - (*add constraints arising from converting goal to clause form*) - val proof = Metis_Proof.proof mth - val result = - axioms - |> fold (replay_one_inference ctxt' type_enc old_skolems sym_tab) proof - val used = map_filter (used_axioms axioms) proof - val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") - val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used - val names = th_cls_pairs |> map fst - val used_names = - th_cls_pairs - |> map_filter (fn (name, (_, cls)) => - if have_common_thm used cls then SOME name - else NONE) - val unused_names = names |> subtract (op =) used_names - in - if not (null cls) andalso not (have_common_thm used cls) then - verbose_warning ctxt "The assumptions are inconsistent" - else - (); - if not (null unused_names) then - "Unused theorems: " ^ commas_quote unused_names - |> verbose_warning ctxt - else - (); - case result of - (_,ith)::_ => - (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); - [discharge_skolem_premises ctxt dischargers ith]) - | _ => (trace_msg ctxt (fn () => "Metis: No result"); []) - end - | Metis_Resolution.Satisfiable _ => - (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); - if null fallback_type_syss then - () - else - raise METIS ("FOL_SOLVE", - "No first-order proof with the lemmas supplied"); - []) - end - handle METIS (loc, msg) => - case fallback_type_syss of - [] => error ("Failed to replay Metis proof in Isabelle." ^ - (if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg - else "")) - | _ => - (verbose_warning ctxt - ("Falling back on " ^ - quote (method_call_for_type_enc fallback_type_syss) ^ "..."); - FOL_SOLVE fallback_type_syss ctxt cls ths0) - -fun neg_clausify ctxt = - single - #> Meson.make_clauses_unsorted ctxt - #> map Meson_Clausify.introduce_combinators_in_theorem - #> Meson.finish_cnf - -fun preskolem_tac ctxt st0 = - (if exists (Meson.has_too_many_clauses ctxt) - (Logic.prems_of_goal (prop_of st0) 1) then - Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1 - THEN cnf.cnfx_rewrite_tac ctxt 1 - else - all_tac) st0 - -val type_has_top_sort = - exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) - -fun generic_metis_tac type_syss ctxt ths i st0 = - let - val _ = trace_msg ctxt (fn () => - "Metis called with theorems\n" ^ - cat_lines (map (Display.string_of_thm ctxt) ths)) - fun tac clause = resolve_tac (FOL_SOLVE type_syss ctxt clause ths) 1 - in - if exists_type type_has_top_sort (prop_of st0) then - verbose_warning ctxt "Proof state contains the universal sort {}" - else - (); - Meson.MESON (preskolem_tac ctxt) (maps (neg_clausify ctxt)) tac ctxt i st0 - end - -fun metis_tac [] = generic_metis_tac partial_type_syss - | metis_tac type_syss = generic_metis_tac type_syss - -(* Whenever "X" has schematic type variables, we treat "using X by metis" as - "by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. - We don't do it for nonschematic facts "X" because this breaks a few proofs - (in the rare and subtle case where a proof relied on extensionality not being - applied) and brings few benefits. *) -val has_tvar = - exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of - -fun method default_type_syss (override_type_syss, ths) ctxt facts = - let - val _ = - if default_type_syss = full_type_syss then - legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead" - else - () - val (schem_facts, nonschem_facts) = List.partition has_tvar facts - val type_syss = override_type_syss |> the_default default_type_syss - in - HEADGOAL (Method.insert_tac nonschem_facts THEN' - CHANGED_PROP - o generic_metis_tac type_syss ctxt (schem_facts @ ths)) - end - -fun setup_method (binding, type_syss) = - ((Args.parens (Scan.repeat Parse.short_ident) - >> maps (fn s => AList.lookup (op =) type_enc_aliases s |> the_default [s])) - |> Scan.option |> Scan.lift) - -- Attrib.thms >> (METHOD oo method type_syss) - |> Method.setup binding - -val setup = - [((@{binding metis}, partial_type_syss), - "Metis for FOL and HOL problems"), - ((@{binding metisFT}, full_type_syss), - "Metis for FOL/HOL problems with fully-typed translation")] - |> fold (uncurry setup_method) - -end; diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Sep 02 19:25:44 2011 +0200 @@ -299,7 +299,7 @@ (* Sledgehammer the given subgoal *) -val default_minimize_prover = Metis_Tactics.metisN +val default_minimize_prover = Metis_Tactic.metisN val is_raw_param_relevant_for_minimize = member (op =) params_for_minimize o fst o unalias_raw_param diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 02 19:25:44 2011 +0200 @@ -128,9 +128,9 @@ "Async_Manager". *) val das_tool = "Sledgehammer" -val metisN = Metis_Tactics.metisN -val metis_full_typesN = metisN ^ "_" ^ Metis_Tactics.full_typesN -val metis_no_typesN = metisN ^ "_" ^ Metis_Tactics.no_typesN +val metisN = Metis_Tactic.metisN +val metis_full_typesN = metisN ^ "_" ^ Metis_Tactic.full_typesN +val metis_no_typesN = metisN ^ "_" ^ Metis_Tactic.no_typesN val metis_prover_infos = [(metisN, Metis), @@ -413,15 +413,15 @@ in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end fun tac_for_reconstructor Metis = - Metis_Tactics.metis_tac [Metis_Tactics.partial_type_enc] + Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc] | tac_for_reconstructor Metis_Full_Types = - Metis_Tactics.metis_tac Metis_Tactics.full_type_syss + Metis_Tactic.metis_tac Metis_Tactic.full_type_syss | tac_for_reconstructor Metis_No_Types = - Metis_Tactics.metis_tac [Metis_Tactics.no_type_enc] + Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] | tac_for_reconstructor _ = raise Fail "unexpected reconstructor" fun timed_reconstructor reconstructor debug timeout ths = - (Config.put Metis_Tactics.verbose debug + (Config.put Metis_Tactic.verbose debug #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths)) |> timed_apply timeout @@ -505,7 +505,7 @@ (* Important messages are important but not so important that users want to see them each time. *) -val atp_important_message_keep_quotient = 10 +val atp_important_message_keep_quotient = 25 fun choose_type_enc soundness best_type_enc format = the_default best_type_enc diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/lin_arith.ML --- a/src/HOL/Tools/lin_arith.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Tools/lin_arith.ML Fri Sep 02 19:25:44 2011 +0200 @@ -22,7 +22,7 @@ val split_limit: int Config.T val neq_limit: int Config.T val verbose: bool Config.T - val trace: bool Unsynchronized.ref + val trace: bool Config.T end; structure Lin_Arith: LIN_ARITH = @@ -102,14 +102,16 @@ val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9); val neq_limit = Attrib.setup_config_int @{binding linarith_neq_limit} (K 9); -val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true); +val verbose = Attrib.setup_config_bool @{binding linarith_verbose} (K true); +val trace = Attrib.setup_config_bool @{binding linarith_trace} (K false); structure LA_Data = struct -val fast_arith_neq_limit = neq_limit; -val fast_arith_verbose = verbose; +val neq_limit = neq_limit; +val verbose = verbose; +val trace = trace; (* Decomposition of terms *) @@ -779,7 +781,6 @@ fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false; val lin_arith_tac = Fast_Arith.lin_arith_tac; -val trace = Fast_Arith.trace; (* reduce contradictory <= to False. Most of the work is done by the cancel tactics. *) diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Tools/record.ML Fri Sep 02 19:25:44 2011 +0200 @@ -26,7 +26,7 @@ val get_info: theory -> string -> info option val the_info: theory -> string -> info val get_hierarchy: theory -> (string * typ list) -> (string * ((string * sort) * typ) list) list - val add_record: bool -> (string * sort) list * binding -> (typ list * string) option -> + val add_record: (string * sort) list * binding -> (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory val last_extT: typ -> (string * typ list) option @@ -2438,12 +2438,9 @@ in -fun add_record quiet_mode (params, binding) raw_parent raw_fields thy = +fun add_record (params, binding) raw_parent raw_fields thy = let val _ = Theory.requires thy "Record" "record definitions"; - val _ = - if quiet_mode then () - else writeln ("Defining record " ^ Binding.print binding ^ " ..."); val ctxt = Proof_Context.init_global thy; fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T) @@ -2493,7 +2490,7 @@ end handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding); -fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy = +fun add_record_cmd (raw_params, binding) raw_parent raw_fields thy = let val ctxt = Proof_Context.init_global thy; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; @@ -2501,7 +2498,7 @@ val (parent, ctxt2) = read_parent raw_parent ctxt1; val (fields, ctxt3) = fold_map read_field raw_fields ctxt2; val params' = map (Proof_Context.check_tfree ctxt3) params; - in thy |> add_record quiet_mode (params', binding) parent fields end; + in thy |> add_record (params', binding) parent fields end; end; @@ -2521,6 +2518,6 @@ (Parse.type_args_constrained -- Parse.binding -- (Parse.$$$ "=" |-- Scan.option (Parse.typ --| Parse.$$$ "+") -- Scan.repeat1 Parse.const_binding) - >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z))); + >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd x y z))); end; diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/Tools/try_methods.ML --- a/src/HOL/Tools/try_methods.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/Tools/try_methods.ML Fri Sep 02 19:25:44 2011 +0200 @@ -113,7 +113,7 @@ fun do_try_methods mode timeout_opt quad st = let - val st = st |> Proof.map_context (Config.put Metis_Tactics.verbose false #> + val st = st |> Proof.map_context (Config.put Metis_Tactic.verbose false #> Config.put Lin_Arith.verbose false) in if mode = Normal then diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/ex/Arith_Examples.thy --- a/src/HOL/ex/Arith_Examples.thy Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/ex/Arith_Examples.thy Fri Sep 02 19:25:44 2011 +0200 @@ -28,9 +28,6 @@ does not do.) *} -(* -ML {* set Lin_Arith.trace; *} -*) subsection {* Splitting of Operators: @{term max}, @{term min}, @{term abs}, @{term minus}, @{term nat}, @{term Divides.mod}, @@ -243,8 +240,4 @@ a + b <= nat (max (abs i) (abs j))" by linarith -(* -ML {* reset Lin_Arith.trace; *} -*) - end diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Fri Sep 02 19:25:44 2011 +0200 @@ -71,7 +71,7 @@ fun sledgehammer_with_metis_tac ctxt override_params relevance_override i th = case run_atp override_params relevance_override i i ctxt th of SOME facts => - Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th + Metis_Tactic.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th | NONE => Seq.empty fun sledgehammer_as_oracle_tac ctxt override_params relevance_override i th = diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/Provers/Arith/fast_lin_arith.ML --- a/src/Provers/Arith/fast_lin_arith.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/Provers/Arith/fast_lin_arith.ML Fri Sep 02 19:25:44 2011 +0200 @@ -59,10 +59,10 @@ (*the limit on the number of ~= allowed; because each ~= is split into two cases, this can lead to an explosion*) - val fast_arith_neq_limit: int Config.T + val neq_limit: int Config.T - (*configures whether (potentially spurious) counterexamples are printed*) - val fast_arith_verbose: bool Config.T + val verbose: bool Config.T + val trace: bool Config.T end; (* decomp(`x Rel y') should yield (p,i,Rel,q,j,d) @@ -104,7 +104,6 @@ val add_simps: thm list -> Context.generic -> Context.generic val add_simprocs: simproc list -> Context.generic -> Context.generic val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic - val trace: bool Unsynchronized.ref end; functor Fast_Lin_Arith @@ -183,8 +182,6 @@ treat non-negative atoms separately rather than adding 0 <= atom *) -val trace = Unsynchronized.ref false; - datatype lineq_type = Eq | Le | Lt; datatype injust = Asm of int @@ -392,8 +389,8 @@ | extract xs [] = raise Empty in extract [] end; -fun print_ineqs ineqs = - if !trace then +fun print_ineqs ctxt ineqs = + if Config.get ctxt LA_Data.trace then tracing(cat_lines(""::map (fn Lineq(c,t,l,_) => string_of_int c ^ (case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ @@ -403,12 +400,12 @@ type history = (int * lineq list) list; datatype result = Success of injust | Failure of history; -fun elim (ineqs, hist) = - let val _ = print_ineqs ineqs +fun elim ctxt (ineqs, hist) = + let val _ = print_ineqs ctxt ineqs val (triv, nontriv) = List.partition is_trivial ineqs in if not (null triv) then case Library.find_first is_contradictory triv of - NONE => elim (nontriv, hist) + NONE => elim ctxt (nontriv, hist) | SOME(Lineq(_,_,_,j)) => Success j else if null nontriv then Failure hist @@ -426,7 +423,7 @@ val (ioth,roth) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) (othereqs @ noneqs) val others = map (elim_var v eq) roth @ ioth - in elim(others,(v,nontriv)::hist) end + in elim ctxt (others,(v,nontriv)::hist) end else let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs val numlist = 0 upto (length (hd lists) - 1) @@ -439,7 +436,7 @@ let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) val (no,yes) = List.partition (fn (Lineq(_,_,l,_)) => nth l v = 0) ineqs val (pos,neg) = List.partition(fn (Lineq(_,_,l,_)) => nth l v > 0) yes - in elim(no @ map_product (elim_var v) pos neg, (v,nontriv)::hist) end + in elim ctxt (no @ map_product (elim_var v) pos neg, (v,nontriv)::hist) end end end end; @@ -448,14 +445,18 @@ (* Translate back a proof. *) (* ------------------------------------------------------------------------- *) -fun trace_thm ctxt msg th = - (if !trace then (tracing msg; tracing (Display.string_of_thm ctxt th)) else (); th); +fun trace_thm ctxt msgs th = + (if Config.get ctxt LA_Data.trace + then tracing (cat_lines (msgs @ [Display.string_of_thm ctxt th])) + else (); th); -fun trace_term ctxt msg t = - (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t) +fun trace_term ctxt msgs t = + (if Config.get ctxt LA_Data.trace + then tracing (cat_lines (msgs @ [Syntax.string_of_term ctxt t])) + else (); t); -fun trace_msg msg = - if !trace then tracing msg else (); +fun trace_msg ctxt msg = + if Config.get ctxt LA_Data.trace then tracing msg else (); val union_term = union Pattern.aeconv; val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t')); @@ -499,7 +500,7 @@ NONE => (the (try_add ([thm2] RL inj_thms) thm1) handle Option => - (trace_thm ctxt "" thm1; trace_thm ctxt "" thm2; + (trace_thm ctxt [] thm1; trace_thm ctxt [] thm2; raise Fail "Linear arithmetic: failed to add thms")) | SOME thm => thm) | SOME thm => thm); @@ -538,25 +539,25 @@ else mult n thm; fun simp thm = - let val thm' = trace_thm ctxt "Simplified:" (full_simplify simpset' thm) + let val thm' = trace_thm ctxt ["Simplified:"] (full_simplify simpset' thm) in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end; - fun mk (Asm i) = trace_thm ctxt ("Asm " ^ string_of_int i) (nth asms i) - | mk (Nat i) = trace_thm ctxt ("Nat " ^ string_of_int i) (LA_Logic.mk_nat_thm thy (nth atoms i)) - | mk (LessD j) = trace_thm ctxt "L" (hd ([mk j] RL lessD)) - | mk (NotLeD j) = trace_thm ctxt "NLe" (mk j RS LA_Logic.not_leD) - | mk (NotLeDD j) = trace_thm ctxt "NLeD" (hd ([mk j RS LA_Logic.not_leD] RL lessD)) - | mk (NotLessD j) = trace_thm ctxt "NL" (mk j RS LA_Logic.not_lessD) - | mk (Added (j1, j2)) = simp (trace_thm ctxt "+" (add_thms (mk j1) (mk j2))) + fun mk (Asm i) = trace_thm ctxt ["Asm " ^ string_of_int i] (nth asms i) + | mk (Nat i) = trace_thm ctxt ["Nat " ^ string_of_int i] (LA_Logic.mk_nat_thm thy (nth atoms i)) + | mk (LessD j) = trace_thm ctxt ["L"] (hd ([mk j] RL lessD)) + | mk (NotLeD j) = trace_thm ctxt ["NLe"] (mk j RS LA_Logic.not_leD) + | mk (NotLeDD j) = trace_thm ctxt ["NLeD"] (hd ([mk j RS LA_Logic.not_leD] RL lessD)) + | mk (NotLessD j) = trace_thm ctxt ["NL"] (mk j RS LA_Logic.not_lessD) + | mk (Added (j1, j2)) = simp (trace_thm ctxt ["+"] (add_thms (mk j1) (mk j2))) | mk (Multiplied (n, j)) = - (trace_msg ("*" ^ string_of_int n); trace_thm ctxt "*" (mult_thm (n, mk j))) + (trace_msg ctxt ("*" ^ string_of_int n); trace_thm ctxt ["*"] (mult_thm (n, mk j))) in let - val _ = trace_msg "mkthm"; - val thm = trace_thm ctxt "Final thm:" (mk just); + val _ = trace_msg ctxt "mkthm"; + val thm = trace_thm ctxt ["Final thm:"] (mk just); val fls = simplify simpset' thm; - val _ = trace_thm ctxt "After simplification:" fls; + val _ = trace_thm ctxt ["After simplification:"] fls; val _ = if LA_Logic.is_False fls then () else @@ -566,7 +567,7 @@ warning "Linear arithmetic should have refuted the assumptions.\n\ \Please inform Tobias Nipkow.") in fls end - handle FalseE thm => trace_thm ctxt "False reached early:" thm + handle FalseE thm => trace_thm ctxt ["False reached early:"] thm end; end; @@ -642,7 +643,9 @@ handle NoEx => NONE in case ex of - SOME s => (warning "Linear arithmetic failed - see trace for a (potentially spurious) counterexample."; tracing s) + SOME s => + (warning "Linear arithmetic failed -- see trace for a (potentially spurious) counterexample."; + tracing s) | NONE => warning "Linear arithmetic failed" end; @@ -714,7 +717,7 @@ val result = (Ts, terms) |> (* user-defined preprocessing of the subgoal *) (if do_pre then LA_Data.pre_decomp ctxt else Library.single) - |> tap (fn subgoals => trace_msg ("Preprocessing yields " ^ + |> tap (fn subgoals => trace_msg ctxt ("Preprocessing yields " ^ string_of_int (length subgoals) ^ " subgoal(s) total.")) |> (* produce the internal encoding of (in-)equalities *) map (apsnd (map (fn t => (LA_Data.decomp ctxt t, LA_Data.domain_is_nat t)))) @@ -725,7 +728,7 @@ |> (* numbering of hypotheses, ignoring irrelevant ones *) map (apsnd (number_hyps 0)) in - trace_msg ("Splitting of inequalities yields " ^ + trace_msg ctxt ("Splitting of inequalities yields " ^ string_of_int (length result) ^ " subgoal(s) total."); result end; @@ -748,12 +751,12 @@ val iatoms = atoms ~~ ixs val natlineqs = map_filter (mknat Ts ixs) iatoms val ineqs = map mkleq initems @ natlineqs - in case elim (ineqs, []) of + in case elim ctxt (ineqs, []) of Success j => - (trace_msg ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); + (trace_msg ctxt ("Contradiction! (" ^ string_of_int (length js + 1) ^ ")"); refute initemss (js @ [j])) | Failure hist => - (if not show_ex orelse not (Config.get ctxt LA_Data.fast_arith_verbose) then () + (if not show_ex orelse not (Config.get ctxt LA_Data.verbose) then () else let val (param_names, ctxt') = ctxt |> Variable.variant_fixes (map fst params) @@ -775,19 +778,19 @@ fun prove ctxt params show_ex do_pre Hs concl : bool * injust list option = let - val _ = trace_msg "prove:" + val _ = trace_msg ctxt "prove:" (* append the negated conclusion to 'Hs' -- this corresponds to *) (* 'DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i)' at the *) (* theorem/tactic level *) val Hs' = Hs @ [LA_Logic.neg_prop concl] fun is_neq NONE = false | is_neq (SOME (_,_,r,_,_,_)) = (r = "~=") - val neq_limit = Config.get ctxt LA_Data.fast_arith_neq_limit + val neq_limit = Config.get ctxt LA_Data.neq_limit val split_neq = count is_neq (map (LA_Data.decomp ctxt) Hs') <= neq_limit in if split_neq then () else - trace_msg ("fast_arith_neq_limit exceeded (current value is " ^ + trace_msg ctxt ("neq_limit exceeded (current value is " ^ string_of_int neq_limit ^ "), ignoring all inequalities"); (split_neq, refute ctxt params show_ex do_pre split_neq Hs') end handle TERM ("neg_prop", _) => @@ -795,7 +798,7 @@ (* the conclusion is not of the form 'Trueprop $ _' (simply *) (* dropping the conclusion doesn't work either, because even *) (* 'False' does not imply arbitrary 'concl::prop') *) - (trace_msg "prove failed (cannot negate conclusion)."; + (trace_msg ctxt "prove failed (cannot negate conclusion)."; (false, NONE)); fun refute_tac ss (i, split_neq, justs) = @@ -803,8 +806,8 @@ let val ctxt = Simplifier.the_context ss; val _ = trace_thm ctxt - ("refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ - string_of_int (length justs) ^ " justification(s)):") state + ["refute_tac (on subgoal " ^ string_of_int i ^ ", with " ^ + string_of_int (length justs) ^ " justification(s)):"] state val {neqE, ...} = get_data ctxt; fun just1 j = (* eliminate inequalities *) @@ -812,7 +815,7 @@ REPEAT_DETERM (eresolve_tac neqE i) else all_tac) THEN - PRIMITIVE (trace_thm ctxt "State after neqE:") THEN + PRIMITIVE (trace_thm ctxt ["State after neqE:"]) THEN (* use theorems generated from the actual justifications *) Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ss prems j) 1) ctxt i in @@ -820,7 +823,7 @@ DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN (* user-defined preprocessing of the subgoal *) DETERM (LA_Data.pre_tac ss i) THEN - PRIMITIVE (trace_thm ctxt "State after pre_tac:") THEN + PRIMITIVE (trace_thm ctxt ["State after pre_tac:"]) THEN (* prove every resulting subgoal, using its justification *) EVERY (map just1 justs) end state; @@ -835,11 +838,11 @@ val params = rev (Logic.strip_params A) val Hs = Logic.strip_assums_hyp A val concl = Logic.strip_assums_concl A - val _ = trace_term ctxt ("Trying to refute subgoal " ^ string_of_int i) A + val _ = trace_term ctxt ["Trying to refute subgoal " ^ string_of_int i] A in case prove ctxt params show_ex true Hs concl of - (_, NONE) => (trace_msg "Refutation failed."; no_tac) - | (split_neq, SOME js) => (trace_msg "Refutation succeeded."; + (_, NONE) => (trace_msg ctxt "Refutation failed."; no_tac) + | (split_neq, SOME js) => (trace_msg ctxt "Refutation succeeded."; refute_tac ss (i, split_neq, js)) end); @@ -912,7 +915,7 @@ val (Falsethm, _) = fwdproof ss tree js val contr = if pos then LA_Logic.ccontr else LA_Logic.notI val concl = Thm.implies_intr cnTconcl Falsethm COMP contr - in SOME (trace_thm ctxt "Proved by lin. arith. prover:" (LA_Logic.mk_Eq concl)) end + in SOME (trace_thm ctxt ["Proved by lin. arith. prover:"] (LA_Logic.mk_Eq concl)) end (*in case concl contains ?-var, which makes assume fail:*) (* FIXME Variable.import_terms *) handle THM _ => NONE; diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/Pure/PIDE/document.ML Fri Sep 02 19:25:44 2011 +0200 @@ -24,7 +24,7 @@ type edit = string * node_edit type state val init_state: state - val define_command: command_id -> string -> state -> state + val define_command: command_id -> string -> string -> state -> state val join_commands: state -> state val cancel_execution: state -> Future.task list val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state @@ -112,7 +112,13 @@ fun map_entries f = map_node (fn (touched, header, perspective, entries, last_exec, result) => (touched, header, perspective, f entries, last_exec, result)); -fun iterate_entries start f (Node {entries, ...}) = Entries.iterate start f entries; +fun get_entries (Node {entries, ...}) = entries; + +fun iterate_entries f = Entries.iterate NONE f o get_entries; +fun iterate_entries_after start f (Node {entries, ...}) = + (case Entries.get_after entries start of + NONE => I + | SOME id => Entries.iterate (SOME id) f entries); fun get_last_exec (Node {last_exec, ...}) = last_exec; fun set_last_exec last_exec = @@ -183,8 +189,9 @@ fun touch_node name nodes = fold (fn desc => - update_node desc (set_touched true) #> - desc <> name ? update_node desc (map_entries (reset_after NONE))) + update_node desc + (set_touched true #> + desc <> name ? (map_entries (reset_after NONE) #> set_result no_result))) (Graph.all_succs nodes [name]) nodes; in @@ -231,7 +238,7 @@ abstype state = State of {versions: version Inttab.table, (*version_id -> document content*) commands: - Toplevel.transition future Inttab.table * (*command_id -> transition (future parsing)*) + (string * Toplevel.transition future) Inttab.table * (*command_id -> name * transition*) Toplevel.transition future list, (*recent commands to be joined*) execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table, (*exec_id -> command_id with eval/print process*) @@ -246,7 +253,7 @@ val init_state = make_state (Inttab.make [(no_id, empty_version)], - (Inttab.make [(no_id, Future.value Toplevel.empty)], []), + (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []), Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))], Future.new_group NONE); @@ -267,7 +274,7 @@ (* commands *) -fun define_command (id: command_id) text = +fun define_command (id: command_id) name text = map_state (fn (versions, (commands, recent), execs, execution) => let val id_string = print_id id; @@ -276,14 +283,14 @@ Position.setmp_thread_data (Position.id_only id_string) (fn () => Outer_Syntax.read_command (Position.id id_string) text) ()); val commands' = - Inttab.update_new (id, tr) commands + Inttab.update_new (id, (name, tr)) commands handle Inttab.DUP dup => err_dup "command" dup; in (versions, (commands', tr :: recent), execs, execution) end); fun the_command (State {commands, ...}) (id: command_id) = (case Inttab.lookup (#1 commands) id of NONE => err_undef "command" id - | SOME tr => tr); + | SOME command => command); val join_commands = map_state (fn (versions, (commands, recent), execs, execution) => @@ -345,9 +352,7 @@ val _ = Multithreading.interrupted (); val _ = Toplevel.status tr Markup.forked; val start = Timing.start (); - val (errs, result) = - if Toplevel.is_toplevel st andalso not is_init then ([], SOME st) - else run (is_init orelse is_proof) (Toplevel.set_print false tr) st; + val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; val _ = timing tr (Timing.result start); val _ = Toplevel.status tr Markup.joined; val _ = List.app (Toplevel.error_msg tr) errs; @@ -384,28 +389,51 @@ local -fun last_common last_visible node0 node = +fun last_common state last_visible node0 node = let - fun get_common ((prev, id), exec) (found, (_, visible)) = + fun update_flags prev (visible, initial) = + let + val visible' = visible andalso prev <> last_visible; + val initial' = initial andalso + (case prev of + NONE => true + | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id)))); + in (visible', initial') end; + fun get_common ((prev, id), exec) (found, (_, flags)) = if found then NONE else let val found' = is_none exec orelse exec <> lookup_entry node0 id - in SOME (found', (prev, visible andalso prev <> last_visible)) end; - in #2 (iterate_entries NONE get_common node (false, (NONE, true))) end; + in SOME (found', (prev, update_flags prev flags)) end; + val (found, (common, flags)) = + iterate_entries get_common node (false, (NONE, (true, true))); + in + if found then (common, flags) + else + let val last = Entries.get_after (get_entries node) common + in (last, update_flags last flags) end + end; + +fun illegal_init () = error "Illegal theory header after end of theory"; -fun new_exec state init command_id' (execs, exec) = - let - val command' = the_command state command_id'; - val exec_id' = new_id (); - val exec' = - snd exec |> Lazy.map (fn (st, _) => - let val tr = - Future.join command' - |> Toplevel.modify_init init - |> Toplevel.put_id (print_id exec_id'); - in run_command tr st end) - |> pair command_id'; - in ((exec_id', exec') :: execs, exec') end; +fun new_exec state bad_init command_id' (execs, exec, init) = + if bad_init andalso is_none init then NONE + else + let + val (name, tr0) = the_command state command_id'; + val (modify_init, init') = + if Keyword.is_theory_begin name then + (Toplevel.modify_init (the_default illegal_init init), NONE) + else (I, init); + val exec_id' = new_id (); + val exec' = + snd exec |> Lazy.map (fn (st, _) => + let val tr = + Future.join tr0 + |> modify_init + |> Toplevel.put_id (print_id exec_id'); + in run_command tr st end) + |> pair command_id'; + in SOME ((exec_id', exec') :: execs, exec', init') end; fun make_required nodes = let @@ -417,6 +445,10 @@ all_visible Symtab.empty; in Symtab.defined required end; +fun check_theory nodes name = + is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *) + is_some (Exn.get_res (get_header (get_node nodes name))); + fun init_theory deps name node = let val (thy_name, imports, uses) = Exn.release (get_header node); @@ -454,6 +486,8 @@ let val node0 = node_of old_version name; fun init () = init_theory deps name node; + val bad_init = + not (check_theory nodes name andalso forall (check_theory nodes o #1) deps); in (singleton o Future.forks) {name = "Document.update", group = NONE, @@ -462,18 +496,19 @@ let val required = is_required name; val last_visible = #2 (get_perspective node); - val (common, visible) = last_common last_visible node0 node; + val (common, (visible, initial)) = last_common state last_visible node0 node; val common_exec = the_exec state (the_default_entry node common); - val (execs, exec) = ([], common_exec) |> + val (execs, exec, _) = + ([], common_exec, if initial then SOME init else NONE) |> (visible orelse required) ? - iterate_entries (after_entry node common) + iterate_entries_after common (fn ((prev, id), _) => fn res => if not required andalso prev = last_visible then NONE - else SOME (new_exec state init id res)) node; + else new_exec state bad_init id res) node; val no_execs = - iterate_entries (after_entry node0 common) + iterate_entries_after common (fn ((_, id0), exec0) => fn res => if is_none exec0 then NONE else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res @@ -533,7 +568,7 @@ (singleton o Future.forks) {name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)), deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} - (iterate_entries NONE (fn (_, exec) => fn () => SOME (force_exec node exec)) node)); + (iterate_entries (fn (_, exec) => fn () => SOME (force_exec node exec)) node)); in (versions, commands, execs, execution) end); diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Sep 02 19:25:18 2011 +0200 +++ b/src/Pure/PIDE/document.scala Fri Sep 02 19:25:44 2011 +0200 @@ -47,6 +47,7 @@ case other: Name => node == other.node case _ => false } + override def toString: String = theory } sealed abstract class Edit[A, B] diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Fri Sep 02 19:25:18 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Fri Sep 02 19:25:44 2011 +0200 @@ -9,7 +9,8 @@ val _ = Isabelle_Process.add_command "Isar_Document.define_command" - (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text)); + (fn [id, name, text] => + Document.change_state (Document.define_command (Document.parse_id id) name text)); val _ = Isabelle_Process.add_command "Isar_Document.cancel_execution" diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Fri Sep 02 19:25:18 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Fri Sep 02 19:25:44 2011 +0200 @@ -148,8 +148,9 @@ { /* commands */ - def define_command(id: Document.Command_ID, text: String): Unit = - input("Isar_Document.define_command", Document.ID(id), text) + def define_command(command: Command): Unit = + input("Isar_Document.define_command", + Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source)) /* document versions */ diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Sep 02 19:25:18 2011 +0200 +++ b/src/Pure/System/session.scala Fri Sep 02 19:25:44 2011 +0200 @@ -253,7 +253,7 @@ { if (!global_state().defined_command(command.id)) { global_state.change(_.define_command(command)) - prover.get.define_command(command.id, Symbol.encode(command.source)) + prover.get.define_command(command) } } doc_edits foreach { diff -r 22bbd0d1b943 -r 17dbd9d9db38 src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Fri Sep 02 19:25:18 2011 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Fri Sep 02 19:25:44 2011 +0200 @@ -93,7 +93,8 @@ if (nodes_status != nodes_status1) { nodes_status = nodes_status1 val order = - Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList) + Library.sort_wrt((name: Document.Node.Name) => name.theory, + nodes_status.keySet.toList) status.listData = order.map(name => name.theory + " " + nodes_status(name)) } }