src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
 author bulwahn Wed Mar 24 17:40:43 2010 +0100 (2010-03-24) changeset 35953 0460ff79bb52 child 36053 29e242e9e9a3 permissions -rw-r--r--
moved further predicate compile files to HOL-Library
1 theory Predicate_Compile_Alternative_Defs
2 imports "../Predicate_Compile"
3 begin
5 section {* Common constants *}
7 declare HOL.if_bool_eq_disj[code_pred_inline]
9 setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
11 section {* Pairs *}
13 setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
15 section {* Bounded quantifiers *}
17 declare Ball_def[code_pred_inline]
18 declare Bex_def[code_pred_inline]
20 section {* Set operations *}
22 declare Collect_def[code_pred_inline]
23 declare mem_def[code_pred_inline]
25 declare eq_reflection[OF empty_def, code_pred_inline]
26 declare insert_code[code_pred_def]
28 declare subset_iff[code_pred_inline]
30 declare Int_def[code_pred_inline]
31 declare eq_reflection[OF Un_def, code_pred_inline]
32 declare eq_reflection[OF UNION_def, code_pred_inline]
34 lemma Diff[code_pred_inline]:
35   "(A - B) = (%x. A x \<and> \<not> B x)"
36 by (auto simp add: mem_def)
38 lemma set_equality[code_pred_inline]:
39   "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
40 by (fastsimp simp add: mem_def)
42 section {* Setup for Numerals *}
44 setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
45 setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
47 setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
49 subsection {* Inductive definitions for arithmetic on natural numbers *}
51 inductive plusP
52 where
53   "plusP x 0 x"
54 |  "plusP x y z ==> plusP x (Suc y) (Suc z)"
56 setup {* Predicate_Compile_Fun.add_function_predicate_translation
57   (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
59 inductive less_nat
60 where
61   "less_nat 0 (Suc y)"
62 | "less_nat x y ==> less_nat (Suc x) (Suc y)"
64 lemma [code_pred_inline]:
65   "x < y = less_nat x y"
66 apply (rule iffI)
67 apply (induct x arbitrary: y)
68 apply (case_tac y) apply (auto intro: less_nat.intros)
69 apply (case_tac y)
70 apply (auto intro: less_nat.intros)
71 apply (induct rule: less_nat.induct)
72 apply auto
73 done
75 inductive less_eq_nat
76 where
77   "less_eq_nat 0 y"
78 | "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
80 lemma [code_pred_inline]:
81 "x <= y = less_eq_nat x y"
82 apply (rule iffI)
83 apply (induct x arbitrary: y)
84 apply (auto intro: less_eq_nat.intros)
85 apply (case_tac y) apply (auto intro: less_eq_nat.intros)
86 apply (induct rule: less_eq_nat.induct)
87 apply auto done
89 section {* Alternative list definitions *}
91 text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
93 lemma [code_pred_def]:
94   "length [] = 0"
95   "length (x # xs) = Suc (length xs)"
96 by auto
98 subsection {* Alternative rules for set *}
100 lemma set_ConsI1 [code_pred_intro]:
101   "set (x # xs) x"
102 unfolding mem_def[symmetric, of _ x]
103 by auto
105 lemma set_ConsI2 [code_pred_intro]:
106   "set xs x ==> set (x' # xs) x"
107 unfolding mem_def[symmetric, of _ x]
108 by auto
110 code_pred [skip_proof] set
111 proof -
112   case set
113   from this show thesis
114     apply (case_tac xb)
115     apply auto
116     unfolding mem_def[symmetric, of _ xc]
117     apply auto
118     unfolding mem_def
119     apply fastsimp
120     done
121 qed
123 subsection {* Alternative rules for list_all2 *}
125 lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
126 by auto
128 lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
129 by auto
131 code_pred [skip_proof] list_all2
132 proof -
133   case list_all2
134   from this show thesis
135     apply -
136     apply (case_tac xb)
137     apply (case_tac xc)
138     apply auto
139     apply (case_tac xc)
140     apply auto
141     apply fastsimp
142     done
143 qed
147 end