# HG changeset patch
# User haftmann
# Date 1288006580 -7200
# Node ID cfed65476db7e36f7466c2bd219b3e481214ecf8
# Parent  06191c5f36867a56b935ef10d0e67b99e8c29d89# Parent  1d8ad2ff3e011bde4d52d7ae65743899912d847b
merged

diff -r 06191c5f3686 -r cfed65476db7 CONTRIBUTORS
--- 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
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/ATP.thy
--- 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
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/IsaMakefile
--- 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 \
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/Library/Dlist.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
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/Library/Permutation.thy
--- 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)
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/List.thy
--- 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
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/Main.thy
--- 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 {*
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/Plain.thy
--- 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 {*
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/Refute.thy
--- 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
 
diff -r 06191c5f3686 -r cfed65476db7 src/HOL/Sledgehammer.thy
--- 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"