# HG changeset patch
# User bulwahn
# Date 1269448843 -3600
# Node ID 0460ff79bb52f943b3ff5bd185a5ac3d8a4f77fe
# Parent  5baac0d3897766c6d2685629e288ed2d8584fab2
moved further predicate compile files to HOL-Library

diff -r 5baac0d38977 -r 0460ff79bb52 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Mar 24 17:40:43 2010 +0100
+++ b/src/HOL/IsaMakefile	Wed Mar 24 17:40:43 2010 +0100
@@ -419,7 +419,8 @@
   Library/Nat_Bijection.thy $(SRC)/Tools/float.ML			\
   $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
   Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
-  Library/OptionalSugar.thy Library/SML_Quickcheck.thy
+  Library/OptionalSugar.thy \
+  Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
 	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
 
 
@@ -965,7 +966,6 @@
   ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy				\
   ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
   ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
-  ex/Predicate_Compile_Quickcheck.thy 					\
   ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
   ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
diff -r 5baac0d38977 -r 0460ff79bb52 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Mar 24 17:40:43 2010 +0100
@@ -0,0 +1,147 @@
+theory Predicate_Compile_Alternative_Defs
+imports "../Predicate_Compile"
+begin
+
+section {* Common constants *}
+
+declare HOL.if_bool_eq_disj[code_pred_inline]
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
+
+section {* Pairs *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
+
+section {* Bounded quantifiers *}
+
+declare Ball_def[code_pred_inline]
+declare Bex_def[code_pred_inline]
+
+section {* Set operations *}
+
+declare Collect_def[code_pred_inline]
+declare mem_def[code_pred_inline]
+
+declare eq_reflection[OF empty_def, code_pred_inline]
+declare insert_code[code_pred_def]
+
+declare subset_iff[code_pred_inline]
+
+declare Int_def[code_pred_inline]
+declare eq_reflection[OF Un_def, code_pred_inline]
+declare eq_reflection[OF UNION_def, code_pred_inline]
+
+lemma Diff[code_pred_inline]:
+  "(A - B) = (%x. A x \<and> \<not> B x)"
+by (auto simp add: mem_def)
+
+lemma set_equality[code_pred_inline]:
+  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
+by (fastsimp simp add: mem_def)
+
+section {* Setup for Numerals *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
+setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
+
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
+
+subsection {* Inductive definitions for arithmetic on natural numbers *}
+
+inductive plusP
+where
+  "plusP x 0 x"
+|  "plusP x y z ==> plusP x (Suc y) (Suc z)"
+
+setup {* Predicate_Compile_Fun.add_function_predicate_translation
+  (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
+
+inductive less_nat
+where
+  "less_nat 0 (Suc y)"
+| "less_nat x y ==> less_nat (Suc x) (Suc y)"
+
+lemma [code_pred_inline]:
+  "x < y = less_nat x y"
+apply (rule iffI)
+apply (induct x arbitrary: y)
+apply (case_tac y) apply (auto intro: less_nat.intros)
+apply (case_tac y)
+apply (auto intro: less_nat.intros)
+apply (induct rule: less_nat.induct)
+apply auto
+done
+
+inductive less_eq_nat
+where
+  "less_eq_nat 0 y"
+| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
+
+lemma [code_pred_inline]:
+"x <= y = less_eq_nat x y"
+apply (rule iffI)
+apply (induct x arbitrary: y)
+apply (auto intro: less_eq_nat.intros)
+apply (case_tac y) apply (auto intro: less_eq_nat.intros)
+apply (induct rule: less_eq_nat.induct)
+apply auto done
+
+section {* Alternative list definitions *}
+
+text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
+ 
+lemma [code_pred_def]:
+  "length [] = 0"
+  "length (x # xs) = Suc (length xs)"
+by auto
+
+subsection {* Alternative rules for set *}
+
+lemma set_ConsI1 [code_pred_intro]:
+  "set (x # xs) x"
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+lemma set_ConsI2 [code_pred_intro]:
+  "set xs x ==> set (x' # xs) x" 
+unfolding mem_def[symmetric, of _ x]
+by auto
+
+code_pred [skip_proof] set
+proof -
+  case set
+  from this show thesis
+    apply (case_tac xb)
+    apply auto
+    unfolding mem_def[symmetric, of _ xc]
+    apply auto
+    unfolding mem_def
+    apply fastsimp
+    done
+qed
+
+subsection {* Alternative rules for list_all2 *}
+
+lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
+by auto
+
+lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
+by auto
+
+code_pred [skip_proof] list_all2
+proof -
+  case list_all2
+  from this show thesis
+    apply -
+    apply (case_tac xb)
+    apply (case_tac xc)
+    apply auto
+    apply (case_tac xc)
+    apply auto
+    apply fastsimp
+    done
+qed
+
+
+
+end
\ No newline at end of file
diff -r 5baac0d38977 -r 0460ff79bb52 src/HOL/Library/Predicate_Compile_Quickcheck.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Wed Mar 24 17:40:43 2010 +0100
@@ -0,0 +1,14 @@
+(* Author: Lukas Bulwahn, TU Muenchen *)
+
+header {* A Prototype of Quickcheck based on the Predicate Compiler *}
+
+theory Predicate_Compile_Quickcheck
+imports Main Predicate_Compile_Alternative_Defs
+uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
+begin
+
+setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 4) *}
+setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 4) *}
+
+end
\ No newline at end of file
diff -r 5baac0d38977 -r 0460ff79bb52 src/HOL/ex/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy	Wed Mar 24 17:40:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-theory Predicate_Compile_Alternative_Defs
-imports "../Predicate_Compile"
-begin
-
-section {* Common constants *}
-
-declare HOL.if_bool_eq_disj[code_pred_inline]
-
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
-
-section {* Pairs *}
-
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
-
-section {* Bounded quantifiers *}
-
-declare Ball_def[code_pred_inline]
-declare Bex_def[code_pred_inline]
-
-section {* Set operations *}
-
-declare Collect_def[code_pred_inline]
-declare mem_def[code_pred_inline]
-
-declare eq_reflection[OF empty_def, code_pred_inline]
-declare insert_code[code_pred_def]
-
-declare subset_iff[code_pred_inline]
-
-declare Int_def[code_pred_inline]
-declare eq_reflection[OF Un_def, code_pred_inline]
-declare eq_reflection[OF UNION_def, code_pred_inline]
-
-lemma Diff[code_pred_inline]:
-  "(A - B) = (%x. A x \<and> \<not> B x)"
-by (auto simp add: mem_def)
-
-lemma set_equality[code_pred_inline]:
-  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
-by (fastsimp simp add: mem_def)
-
-section {* Setup for Numerals *}
-
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
-setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
-
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
-
-subsection {* Inductive definitions for arithmetic on natural numbers *}
-
-inductive plusP
-where
-  "plusP x 0 x"
-|  "plusP x y z ==> plusP x (Suc y) (Suc z)"
-
-setup {* Predicate_Compile_Fun.add_function_predicate_translation
-  (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
-
-inductive less_nat
-where
-  "less_nat 0 (Suc y)"
-| "less_nat x y ==> less_nat (Suc x) (Suc y)"
-
-lemma [code_pred_inline]:
-  "x < y = less_nat x y"
-apply (rule iffI)
-apply (induct x arbitrary: y)
-apply (case_tac y) apply (auto intro: less_nat.intros)
-apply (case_tac y)
-apply (auto intro: less_nat.intros)
-apply (induct rule: less_nat.induct)
-apply auto
-done
-
-inductive less_eq_nat
-where
-  "less_eq_nat 0 y"
-| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
-
-lemma [code_pred_inline]:
-"x <= y = less_eq_nat x y"
-apply (rule iffI)
-apply (induct x arbitrary: y)
-apply (auto intro: less_eq_nat.intros)
-apply (case_tac y) apply (auto intro: less_eq_nat.intros)
-apply (induct rule: less_eq_nat.induct)
-apply auto done
-
-section {* Alternative list definitions *}
-
-text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
- 
-lemma [code_pred_def]:
-  "length [] = 0"
-  "length (x # xs) = Suc (length xs)"
-by auto
-
-subsection {* Alternative rules for set *}
-
-lemma set_ConsI1 [code_pred_intro]:
-  "set (x # xs) x"
-unfolding mem_def[symmetric, of _ x]
-by auto
-
-lemma set_ConsI2 [code_pred_intro]:
-  "set xs x ==> set (x' # xs) x" 
-unfolding mem_def[symmetric, of _ x]
-by auto
-
-code_pred [skip_proof] set
-proof -
-  case set
-  from this show thesis
-    apply (case_tac xb)
-    apply auto
-    unfolding mem_def[symmetric, of _ xc]
-    apply auto
-    unfolding mem_def
-    apply fastsimp
-    done
-qed
-
-subsection {* Alternative rules for list_all2 *}
-
-lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
-by auto
-
-lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
-by auto
-
-code_pred [skip_proof] list_all2
-proof -
-  case list_all2
-  from this show thesis
-    apply -
-    apply (case_tac xb)
-    apply (case_tac xc)
-    apply auto
-    apply (case_tac xc)
-    apply auto
-    apply fastsimp
-    done
-qed
-
-
-
-end
\ No newline at end of file
diff -r 5baac0d38977 -r 0460ff79bb52 src/HOL/ex/Predicate_Compile_Quickcheck.thy
--- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Wed Mar 24 17:40:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Author: Lukas Bulwahn, TU Muenchen *)
-
-header {* A Prototype of Quickcheck based on the Predicate Compiler *}
-
-theory Predicate_Compile_Quickcheck
-imports Main Predicate_Compile_Alternative_Defs
-uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
-begin
-
-setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 4) *}
-setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 4) *}
-
-end
\ No newline at end of file
diff -r 5baac0d38977 -r 0460ff79bb52 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Wed Mar 24 17:40:43 2010 +0100
+++ b/src/HOL/ex/ROOT.ML	Wed Mar 24 17:40:43 2010 +0100
@@ -11,8 +11,7 @@
   "Eval_Examples",
   "Codegenerator_Test",
   "Codegenerator_Pretty_Test",
-  "NormalForm",
-  "Predicate_Compile_Quickcheck"
+  "NormalForm"
 ];
 
 use_thys [