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