--- a/CONTRIBUTORS Mon Oct 25 12:24:38 2010 +0200
+++ b/CONTRIBUTORS Mon Oct 25 13:36:20 2010 +0200
@@ -7,6 +7,9 @@
--------------------------------------
* September 2010: Florian Haftmann, TUM
+ Refined concepts for evaluation, i.e. normalisation of terms using different techniques.
+
+* September 2010: Florian Haftmann, TUM
Code generation for Scala.
* August 2010: Johannes Hoelzl, Armin Heller, and Robert Himmelmann, TUM
--- a/src/HOL/ATP.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/ATP.thy Mon Oct 25 13:36:20 2010 +0200
@@ -6,10 +6,11 @@
header {* Automatic Theorem Provers (ATPs) *}
theory ATP
-imports Plain
-uses "Tools/ATP/atp_problem.ML"
- "Tools/ATP/atp_proof.ML"
- "Tools/ATP/atp_systems.ML"
+imports HOL
+uses
+ "Tools/ATP/atp_problem.ML"
+ "Tools/ATP/atp_proof.ML"
+ "Tools/ATP/atp_systems.ML"
begin
setup ATP_Systems.setup
--- a/src/HOL/IsaMakefile Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/IsaMakefile Mon Oct 25 13:36:20 2010 +0200
@@ -144,6 +144,7 @@
@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
PLAIN_DEPENDENCIES = $(BASE_DEPENDENCIES) \
+ ATP.thy \
Complete_Lattice.thy \
Complete_Partial_Order.thy \
Datatype.thy \
@@ -169,6 +170,7 @@
Rings.thy \
SAT.thy \
Set.thy \
+ Sledgehammer.thy \
Sum_Type.thy \
Tools/abel_cancel.ML \
Tools/arith_data.ML \
@@ -237,7 +239,6 @@
@$(ISABELLE_TOOL) usedir -b -f plain.ML -g true $(OUT)/Pure HOL-Plain
MAIN_DEPENDENCIES = $(PLAIN_DEPENDENCIES) \
- ATP.thy \
Big_Operators.thy \
Code_Evaluation.thy \
Code_Numeral.thy \
@@ -268,7 +269,6 @@
Refute.thy \
Semiring_Normalization.thy \
SetInterval.thy \
- Sledgehammer.thy \
SMT.thy \
String.thy \
Typerep.thy \
--- a/src/HOL/Library/Dlist.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Oct 25 13:36:20 2010 +0200
@@ -143,11 +143,11 @@
proof (induct xs)
case Nil from empty show ?case by (simp add: empty_def)
next
- case (insert x xs)
+ case (Cons x xs)
then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
by (simp_all add: member_def List.member_def)
with insrt have "P (insert x (Dlist xs))" .
- with insert show ?case by (simp add: insert_def distinct_remdups_id)
+ with Cons show ?case by (simp add: insert_def distinct_remdups_id)
qed
with dxs show "P dxs" by simp
qed
--- a/src/HOL/Library/Permutation.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/Library/Permutation.thy Mon Oct 25 13:36:20 2010 +0200
@@ -168,7 +168,7 @@
apply simp
apply (subgoal_tac "a#list <~~> a#ysa@zs")
apply (metis Cons_eq_appendI perm_append_Cons trans)
- apply (metis Cons Cons_eq_appendI distinct_simps(2)
+ apply (metis Cons Cons_eq_appendI distinct.simps(2)
distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
apply (fastsimp simp add: insert_ident)
--- a/src/HOL/List.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/List.thy Mon Oct 25 13:36:20 2010 +0200
@@ -5,7 +5,7 @@
header {* The datatype of finite lists *}
theory List
-imports Plain Quotient Presburger Code_Numeral Recdef
+imports Plain Presburger Recdef Code_Numeral Quotient
uses ("Tools/list_code.ML")
begin
@@ -174,15 +174,10 @@
"removeAll x [] = []"
| "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
-inductive
+primrec
distinct :: "'a list \<Rightarrow> bool" where
- Nil: "distinct []"
- | insert: "x \<notin> set xs \<Longrightarrow> distinct xs \<Longrightarrow> distinct (x # xs)"
-
-lemma distinct_simps [simp, code]:
- "distinct [] \<longleftrightarrow> True"
- "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
- by (auto intro: distinct.intros elim: distinct.cases)
+ "distinct [] \<longleftrightarrow> True"
+ | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
primrec
remdups :: "'a list \<Rightarrow> 'a list" where
@@ -786,9 +781,8 @@
by (induct xs) auto
lemma map_cong [fundef_cong, recdef_cong]:
-"xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
--- {* a congruence rule for @{text map} *}
-by simp
+ "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
+ by simp
lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
by (cases xs) auto
@@ -990,14 +984,14 @@
"(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
by (auto dest!: split_list_first)
-lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
-proof (induct xs rule:rev_induct)
+lemma split_list_last: "x \<in> set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
+proof (induct xs rule: rev_induct)
case Nil thus ?case by simp
next
case (snoc a xs)
show ?case
proof cases
- assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
+ assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE)
next
assume "x \<noteq> a" thus ?case using snoc by fastsimp
qed
@@ -1030,8 +1024,7 @@
show ?case
proof cases
assume "P x"
- thus ?thesis by simp
- (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
+ thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
next
assume "\<not> P x"
hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
--- a/src/HOL/Main.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/Main.thy Mon Oct 25 13:36:20 2010 +0200
@@ -1,7 +1,7 @@
header {* Main HOL *}
theory Main
-imports Plain Record Predicate_Compile Nitpick SMT
+imports Plain Record Predicate_Compile Nitpick SMT Quotient
begin
text {*
--- a/src/HOL/Plain.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/Plain.thy Mon Oct 25 13:36:20 2010 +0200
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Extraction Metis
+imports Datatype FunDef Extraction Sledgehammer
begin
text {*
--- a/src/HOL/Refute.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/Refute.thy Mon Oct 25 13:36:20 2010 +0200
@@ -8,7 +8,7 @@
header {* Refute *}
theory Refute
-imports Hilbert_Choice List Sledgehammer
+imports Hilbert_Choice List
uses "Tools/refute.ML"
begin
--- a/src/HOL/Sledgehammer.thy Mon Oct 25 12:24:38 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Mon Oct 25 13:36:20 2010 +0200
@@ -7,7 +7,7 @@
header {* Sledgehammer: Isabelle--ATP Linkup *}
theory Sledgehammer
-imports ATP
+imports ATP Metis
uses "Tools/Sledgehammer/sledgehammer_util.ML"
"Tools/Sledgehammer/sledgehammer_filter.ML"
"Tools/Sledgehammer/sledgehammer_atp_translate.ML"