--- 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;
--- 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;
--- 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\<lparr>A255:=x\<rparr>) = A155 r"
-by simp
-
-lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
-by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
-by simp
-
-lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
-apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_upd_simproc]) 1*})
-done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
- apply simp
- done
-
-lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply simp
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* simp_tac
- (HOL_basic_ss addsimprocs [Record.record_split_simproc (K ~1)]) 1*})
- apply auto
- done
-
-lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply auto
- done
-
-lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>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 "\<exists>x. P x"
- using pre
- apply -
- apply (tactic {* Record.record_split_simp_tac [] (K ~1) 1*})
- apply auto
- done
- }
- show ?thesis ..
-qed
-
-
-lemma "\<exists>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
--- /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\<lparr>A255:=x\<rparr>) = A155 r"
+ by simp
+
+lemma "A155 (r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = A155 r"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ by simp
+
+lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.upd_simproc]) 1*})
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply simp
+ done
+
+lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply simp
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*})
+ apply auto
+ done
+
+lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+
+lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>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 "\<exists>x. P x"
+ using pre
+ apply -
+ apply (tactic {* Record.split_simp_tac [] (K ~1) 1*})
+ apply auto
+ done
+ }
+ show ?thesis ..
+qed
+
+
+lemma "\<exists>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
--- 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
--- 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" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
- 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:
--- 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:
"\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
shows "monoid_cancel G"
- proof qed fact+
+ by default fact+
lemma (in monoid_cancel) is_monoid_cancel:
"monoid_cancel G"
..
sublocale group \<subseteq> 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 \<subseteq> 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 \<subseteq> 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)"
--- 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 \<in> carrier G; y \<in> carrier G |] ==>
x \<otimes> y = y \<otimes> 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 \<subseteq> |)"
- proof qed simp_all
+ by default simp_all
lemma (in group) subgroup_self:
"subgroup (carrier G) G"
--- 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 \<Z> x n = x^n"
proof -
-- "Specification"
- show "monoid \<Z>" proof qed auto
+ show "monoid \<Z>" by default auto
then interpret int: monoid \<Z> .
-- "Carrier"
@@ -79,7 +79,7 @@
where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
proof -
-- "Specification"
- show "comm_monoid \<Z>" proof qed auto
+ show "comm_monoid \<Z>" by default auto
then interpret int: comm_monoid \<Z> .
-- "Operations"
@@ -105,7 +105,7 @@
and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
proof -
-- "Specification"
- show "abelian_monoid \<Z>" proof qed auto
+ show "abelian_monoid \<Z>" by default auto
then interpret int: abelian_monoid \<Z> .
-- "Carrier"
@@ -189,7 +189,7 @@
and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
proof -
show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
- proof qed simp_all
+ by default simp_all
show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
by simp
show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
@@ -226,7 +226,7 @@
interpretation int (* [unfolded UNIV] *) :
total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
- proof qed clarsimp
+ by default clarsimp
subsection {* Generated Ideals of @{text "\<Z>"} *}
--- 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 \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> 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 \<subseteq> 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" ("\<top>\<index>")
@@ -1133,14 +1133,14 @@
"[| x \<in> carrier L; y \<in> 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 \<in> carrier L; y \<in> 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 \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> 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 \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> 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 \<subseteq> 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 \<subseteq> 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)"
--- 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 \<subseteq> ring: ring_hom_ring
- proof qed (rule homh)
+ by default (rule homh)
sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
apply (rule abelian_group_homI)
--- 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 \<in> 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 \<oplus>\<^bsub>R\<^esub> eval R R id a r"
--- 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 \
--- 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
--- 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
--- 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)
--- 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
--- 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
--- 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
--- 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
--- /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;
--- 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;
--- 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
--- 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
--- 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. *)
--- 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;
--- 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
--- 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
--- 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 =
--- 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;
--- 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);
--- 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]
--- 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"
--- 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 */
--- 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 {
--- 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))
}
}