35953

1 
theory Predicate_Compile_Alternative_Defs


2 
imports "../Predicate_Compile"


3 
begin


4 


5 
section {* Common constants *}


6 


7 
declare HOL.if_bool_eq_disj[code_pred_inline]


8 


9 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}


10 


11 
section {* Pairs *}


12 


13 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}


14 


15 
section {* Bounded quantifiers *}


16 


17 
declare Ball_def[code_pred_inline]


18 
declare Bex_def[code_pred_inline]


19 


20 
section {* Set operations *}


21 


22 
declare Collect_def[code_pred_inline]


23 
declare mem_def[code_pred_inline]


24 


25 
declare eq_reflection[OF empty_def, code_pred_inline]


26 
declare insert_code[code_pred_def]


27 


28 
declare subset_iff[code_pred_inline]


29 


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]


33 


34 
lemma Diff[code_pred_inline]:


35 
"(A  B) = (%x. A x \<and> \<not> B x)"


36 
by (auto simp add: mem_def)


37 


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)


41 


42 
section {* Setup for Numerals *}


43 


44 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}


45 
setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}


46 


47 
setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}


48 


49 
subsection {* Inductive definitions for arithmetic on natural numbers *}


50 


51 
inductive plusP


52 
where


53 
"plusP x 0 x"


54 
 "plusP x y z ==> plusP x (Suc y) (Suc z)"


55 


56 
setup {* Predicate_Compile_Fun.add_function_predicate_translation


57 
(@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}


58 


59 
inductive less_nat


60 
where


61 
"less_nat 0 (Suc y)"


62 
 "less_nat x y ==> less_nat (Suc x) (Suc y)"


63 


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


74 


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)"


79 


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


88 


89 
section {* Alternative list definitions *}


90 


91 
text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}


92 


93 
lemma [code_pred_def]:


94 
"length [] = 0"


95 
"length (x # xs) = Suc (length xs)"


96 
by auto


97 


98 
subsection {* Alternative rules for set *}


99 


100 
lemma set_ConsI1 [code_pred_intro]:


101 
"set (x # xs) x"


102 
unfolding mem_def[symmetric, of _ x]


103 
by auto


104 


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


109 


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


122 


123 
subsection {* Alternative rules for list_all2 *}


124 


125 
lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"


126 
by auto


127 


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


130 


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


144 


145 


146 


147 
end 