moved further predicate compile files to HOL-Library
authorbulwahn
Wed Mar 24 17:40:43 2010 +0100 (2010-03-24)
changeset 359530460ff79bb52
parent 35952 5baac0d38977
child 35954 d87d85a5d9ab
moved further predicate compile files to HOL-Library
src/HOL/IsaMakefile
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Predicate_Compile_Quickcheck.thy
src/HOL/ex/Predicate_Compile_Alternative_Defs.thy
src/HOL/ex/Predicate_Compile_Quickcheck.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 24 17:40:43 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 24 17:40:43 2010 +0100
     1.3 @@ -419,7 +419,8 @@
     1.4    Library/Nat_Bijection.thy $(SRC)/Tools/float.ML			\
     1.5    $(SRC)/HOL/Tools/float_arith.ML Library/positivstellensatz.ML		\
     1.6    Library/reify_data.ML Library/reflection.ML Library/LaTeXsugar.thy	\
     1.7 -  Library/OptionalSugar.thy Library/SML_Quickcheck.thy
     1.8 +  Library/OptionalSugar.thy \
     1.9 +  Library/Predicate_Compile_Quickcheck.thy Library/SML_Quickcheck.thy
    1.10  	@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
    1.11  
    1.12  
    1.13 @@ -965,7 +966,6 @@
    1.14    ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy				\
    1.15    ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
    1.16    ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
    1.17 -  ex/Predicate_Compile_Quickcheck.thy 					\
    1.18    ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
    1.19    ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
    1.20    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Mar 24 17:40:43 2010 +0100
     2.3 @@ -0,0 +1,147 @@
     2.4 +theory Predicate_Compile_Alternative_Defs
     2.5 +imports "../Predicate_Compile"
     2.6 +begin
     2.7 +
     2.8 +section {* Common constants *}
     2.9 +
    2.10 +declare HOL.if_bool_eq_disj[code_pred_inline]
    2.11 +
    2.12 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
    2.13 +
    2.14 +section {* Pairs *}
    2.15 +
    2.16 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
    2.17 +
    2.18 +section {* Bounded quantifiers *}
    2.19 +
    2.20 +declare Ball_def[code_pred_inline]
    2.21 +declare Bex_def[code_pred_inline]
    2.22 +
    2.23 +section {* Set operations *}
    2.24 +
    2.25 +declare Collect_def[code_pred_inline]
    2.26 +declare mem_def[code_pred_inline]
    2.27 +
    2.28 +declare eq_reflection[OF empty_def, code_pred_inline]
    2.29 +declare insert_code[code_pred_def]
    2.30 +
    2.31 +declare subset_iff[code_pred_inline]
    2.32 +
    2.33 +declare Int_def[code_pred_inline]
    2.34 +declare eq_reflection[OF Un_def, code_pred_inline]
    2.35 +declare eq_reflection[OF UNION_def, code_pred_inline]
    2.36 +
    2.37 +lemma Diff[code_pred_inline]:
    2.38 +  "(A - B) = (%x. A x \<and> \<not> B x)"
    2.39 +by (auto simp add: mem_def)
    2.40 +
    2.41 +lemma set_equality[code_pred_inline]:
    2.42 +  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
    2.43 +by (fastsimp simp add: mem_def)
    2.44 +
    2.45 +section {* Setup for Numerals *}
    2.46 +
    2.47 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
    2.48 +setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
    2.49 +
    2.50 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
    2.51 +
    2.52 +subsection {* Inductive definitions for arithmetic on natural numbers *}
    2.53 +
    2.54 +inductive plusP
    2.55 +where
    2.56 +  "plusP x 0 x"
    2.57 +|  "plusP x y z ==> plusP x (Suc y) (Suc z)"
    2.58 +
    2.59 +setup {* Predicate_Compile_Fun.add_function_predicate_translation
    2.60 +  (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
    2.61 +
    2.62 +inductive less_nat
    2.63 +where
    2.64 +  "less_nat 0 (Suc y)"
    2.65 +| "less_nat x y ==> less_nat (Suc x) (Suc y)"
    2.66 +
    2.67 +lemma [code_pred_inline]:
    2.68 +  "x < y = less_nat x y"
    2.69 +apply (rule iffI)
    2.70 +apply (induct x arbitrary: y)
    2.71 +apply (case_tac y) apply (auto intro: less_nat.intros)
    2.72 +apply (case_tac y)
    2.73 +apply (auto intro: less_nat.intros)
    2.74 +apply (induct rule: less_nat.induct)
    2.75 +apply auto
    2.76 +done
    2.77 +
    2.78 +inductive less_eq_nat
    2.79 +where
    2.80 +  "less_eq_nat 0 y"
    2.81 +| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
    2.82 +
    2.83 +lemma [code_pred_inline]:
    2.84 +"x <= y = less_eq_nat x y"
    2.85 +apply (rule iffI)
    2.86 +apply (induct x arbitrary: y)
    2.87 +apply (auto intro: less_eq_nat.intros)
    2.88 +apply (case_tac y) apply (auto intro: less_eq_nat.intros)
    2.89 +apply (induct rule: less_eq_nat.induct)
    2.90 +apply auto done
    2.91 +
    2.92 +section {* Alternative list definitions *}
    2.93 +
    2.94 +text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
    2.95 + 
    2.96 +lemma [code_pred_def]:
    2.97 +  "length [] = 0"
    2.98 +  "length (x # xs) = Suc (length xs)"
    2.99 +by auto
   2.100 +
   2.101 +subsection {* Alternative rules for set *}
   2.102 +
   2.103 +lemma set_ConsI1 [code_pred_intro]:
   2.104 +  "set (x # xs) x"
   2.105 +unfolding mem_def[symmetric, of _ x]
   2.106 +by auto
   2.107 +
   2.108 +lemma set_ConsI2 [code_pred_intro]:
   2.109 +  "set xs x ==> set (x' # xs) x" 
   2.110 +unfolding mem_def[symmetric, of _ x]
   2.111 +by auto
   2.112 +
   2.113 +code_pred [skip_proof] set
   2.114 +proof -
   2.115 +  case set
   2.116 +  from this show thesis
   2.117 +    apply (case_tac xb)
   2.118 +    apply auto
   2.119 +    unfolding mem_def[symmetric, of _ xc]
   2.120 +    apply auto
   2.121 +    unfolding mem_def
   2.122 +    apply fastsimp
   2.123 +    done
   2.124 +qed
   2.125 +
   2.126 +subsection {* Alternative rules for list_all2 *}
   2.127 +
   2.128 +lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
   2.129 +by auto
   2.130 +
   2.131 +lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
   2.132 +by auto
   2.133 +
   2.134 +code_pred [skip_proof] list_all2
   2.135 +proof -
   2.136 +  case list_all2
   2.137 +  from this show thesis
   2.138 +    apply -
   2.139 +    apply (case_tac xb)
   2.140 +    apply (case_tac xc)
   2.141 +    apply auto
   2.142 +    apply (case_tac xc)
   2.143 +    apply auto
   2.144 +    apply fastsimp
   2.145 +    done
   2.146 +qed
   2.147 +
   2.148 +
   2.149 +
   2.150 +end
   2.151 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Wed Mar 24 17:40:43 2010 +0100
     3.3 @@ -0,0 +1,14 @@
     3.4 +(* Author: Lukas Bulwahn, TU Muenchen *)
     3.5 +
     3.6 +header {* A Prototype of Quickcheck based on the Predicate Compiler *}
     3.7 +
     3.8 +theory Predicate_Compile_Quickcheck
     3.9 +imports Main Predicate_Compile_Alternative_Defs
    3.10 +uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
    3.11 +begin
    3.12 +
    3.13 +setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 4) *}
    3.14 +setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 4) *}
    3.15 +setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 4) *}
    3.16 +
    3.17 +end
    3.18 \ No newline at end of file
     4.1 --- a/src/HOL/ex/Predicate_Compile_Alternative_Defs.thy	Wed Mar 24 17:40:43 2010 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,147 +0,0 @@
     4.4 -theory Predicate_Compile_Alternative_Defs
     4.5 -imports "../Predicate_Compile"
     4.6 -begin
     4.7 -
     4.8 -section {* Common constants *}
     4.9 -
    4.10 -declare HOL.if_bool_eq_disj[code_pred_inline]
    4.11 -
    4.12 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
    4.13 -
    4.14 -section {* Pairs *}
    4.15 -
    4.16 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
    4.17 -
    4.18 -section {* Bounded quantifiers *}
    4.19 -
    4.20 -declare Ball_def[code_pred_inline]
    4.21 -declare Bex_def[code_pred_inline]
    4.22 -
    4.23 -section {* Set operations *}
    4.24 -
    4.25 -declare Collect_def[code_pred_inline]
    4.26 -declare mem_def[code_pred_inline]
    4.27 -
    4.28 -declare eq_reflection[OF empty_def, code_pred_inline]
    4.29 -declare insert_code[code_pred_def]
    4.30 -
    4.31 -declare subset_iff[code_pred_inline]
    4.32 -
    4.33 -declare Int_def[code_pred_inline]
    4.34 -declare eq_reflection[OF Un_def, code_pred_inline]
    4.35 -declare eq_reflection[OF UNION_def, code_pred_inline]
    4.36 -
    4.37 -lemma Diff[code_pred_inline]:
    4.38 -  "(A - B) = (%x. A x \<and> \<not> B x)"
    4.39 -by (auto simp add: mem_def)
    4.40 -
    4.41 -lemma set_equality[code_pred_inline]:
    4.42 -  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
    4.43 -by (fastsimp simp add: mem_def)
    4.44 -
    4.45 -section {* Setup for Numerals *}
    4.46 -
    4.47 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
    4.48 -setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
    4.49 -
    4.50 -setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
    4.51 -
    4.52 -subsection {* Inductive definitions for arithmetic on natural numbers *}
    4.53 -
    4.54 -inductive plusP
    4.55 -where
    4.56 -  "plusP x 0 x"
    4.57 -|  "plusP x y z ==> plusP x (Suc y) (Suc z)"
    4.58 -
    4.59 -setup {* Predicate_Compile_Fun.add_function_predicate_translation
    4.60 -  (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
    4.61 -
    4.62 -inductive less_nat
    4.63 -where
    4.64 -  "less_nat 0 (Suc y)"
    4.65 -| "less_nat x y ==> less_nat (Suc x) (Suc y)"
    4.66 -
    4.67 -lemma [code_pred_inline]:
    4.68 -  "x < y = less_nat x y"
    4.69 -apply (rule iffI)
    4.70 -apply (induct x arbitrary: y)
    4.71 -apply (case_tac y) apply (auto intro: less_nat.intros)
    4.72 -apply (case_tac y)
    4.73 -apply (auto intro: less_nat.intros)
    4.74 -apply (induct rule: less_nat.induct)
    4.75 -apply auto
    4.76 -done
    4.77 -
    4.78 -inductive less_eq_nat
    4.79 -where
    4.80 -  "less_eq_nat 0 y"
    4.81 -| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
    4.82 -
    4.83 -lemma [code_pred_inline]:
    4.84 -"x <= y = less_eq_nat x y"
    4.85 -apply (rule iffI)
    4.86 -apply (induct x arbitrary: y)
    4.87 -apply (auto intro: less_eq_nat.intros)
    4.88 -apply (case_tac y) apply (auto intro: less_eq_nat.intros)
    4.89 -apply (induct rule: less_eq_nat.induct)
    4.90 -apply auto done
    4.91 -
    4.92 -section {* Alternative list definitions *}
    4.93 -
    4.94 -text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
    4.95 - 
    4.96 -lemma [code_pred_def]:
    4.97 -  "length [] = 0"
    4.98 -  "length (x # xs) = Suc (length xs)"
    4.99 -by auto
   4.100 -
   4.101 -subsection {* Alternative rules for set *}
   4.102 -
   4.103 -lemma set_ConsI1 [code_pred_intro]:
   4.104 -  "set (x # xs) x"
   4.105 -unfolding mem_def[symmetric, of _ x]
   4.106 -by auto
   4.107 -
   4.108 -lemma set_ConsI2 [code_pred_intro]:
   4.109 -  "set xs x ==> set (x' # xs) x" 
   4.110 -unfolding mem_def[symmetric, of _ x]
   4.111 -by auto
   4.112 -
   4.113 -code_pred [skip_proof] set
   4.114 -proof -
   4.115 -  case set
   4.116 -  from this show thesis
   4.117 -    apply (case_tac xb)
   4.118 -    apply auto
   4.119 -    unfolding mem_def[symmetric, of _ xc]
   4.120 -    apply auto
   4.121 -    unfolding mem_def
   4.122 -    apply fastsimp
   4.123 -    done
   4.124 -qed
   4.125 -
   4.126 -subsection {* Alternative rules for list_all2 *}
   4.127 -
   4.128 -lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
   4.129 -by auto
   4.130 -
   4.131 -lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
   4.132 -by auto
   4.133 -
   4.134 -code_pred [skip_proof] list_all2
   4.135 -proof -
   4.136 -  case list_all2
   4.137 -  from this show thesis
   4.138 -    apply -
   4.139 -    apply (case_tac xb)
   4.140 -    apply (case_tac xc)
   4.141 -    apply auto
   4.142 -    apply (case_tac xc)
   4.143 -    apply auto
   4.144 -    apply fastsimp
   4.145 -    done
   4.146 -qed
   4.147 -
   4.148 -
   4.149 -
   4.150 -end
   4.151 \ No newline at end of file
     5.1 --- a/src/HOL/ex/Predicate_Compile_Quickcheck.thy	Wed Mar 24 17:40:43 2010 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,14 +0,0 @@
     5.4 -(* Author: Lukas Bulwahn, TU Muenchen *)
     5.5 -
     5.6 -header {* A Prototype of Quickcheck based on the Predicate Compiler *}
     5.7 -
     5.8 -theory Predicate_Compile_Quickcheck
     5.9 -imports Main Predicate_Compile_Alternative_Defs
    5.10 -uses "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
    5.11 -begin
    5.12 -
    5.13 -setup {* Quickcheck.add_generator ("predicate_compile_wo_ff", Predicate_Compile_Quickcheck.quickcheck_compile_term false true 4) *}
    5.14 -setup {* Quickcheck.add_generator ("predicate_compile_ff_fs", Predicate_Compile_Quickcheck.quickcheck_compile_term true true 4) *}
    5.15 -setup {* Quickcheck.add_generator ("predicate_compile_ff_nofs", Predicate_Compile_Quickcheck.quickcheck_compile_term true false 4) *}
    5.16 -
    5.17 -end
    5.18 \ No newline at end of file
     6.1 --- a/src/HOL/ex/ROOT.ML	Wed Mar 24 17:40:43 2010 +0100
     6.2 +++ b/src/HOL/ex/ROOT.ML	Wed Mar 24 17:40:43 2010 +0100
     6.3 @@ -11,8 +11,7 @@
     6.4    "Eval_Examples",
     6.5    "Codegenerator_Test",
     6.6    "Codegenerator_Pretty_Test",
     6.7 -  "NormalForm",
     6.8 -  "Predicate_Compile_Quickcheck"
     6.9 +  "NormalForm"
    6.10  ];
    6.11  
    6.12  use_thys [