src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 35953 0460ff79bb52
child 36053 29e242e9e9a3
equal deleted inserted replaced
35952:5baac0d38977 35953:0460ff79bb52
       
     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