src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
changeset 35953 0460ff79bb52
child 36053 29e242e9e9a3
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Mar 24 17:40:43 2010 +0100
     1.3 @@ -0,0 +1,147 @@
     1.4 +theory Predicate_Compile_Alternative_Defs
     1.5 +imports "../Predicate_Compile"
     1.6 +begin
     1.7 +
     1.8 +section {* Common constants *}
     1.9 +
    1.10 +declare HOL.if_bool_eq_disj[code_pred_inline]
    1.11 +
    1.12 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name Let}] *}
    1.13 +
    1.14 +section {* Pairs *}
    1.15 +
    1.16 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
    1.17 +
    1.18 +section {* Bounded quantifiers *}
    1.19 +
    1.20 +declare Ball_def[code_pred_inline]
    1.21 +declare Bex_def[code_pred_inline]
    1.22 +
    1.23 +section {* Set operations *}
    1.24 +
    1.25 +declare Collect_def[code_pred_inline]
    1.26 +declare mem_def[code_pred_inline]
    1.27 +
    1.28 +declare eq_reflection[OF empty_def, code_pred_inline]
    1.29 +declare insert_code[code_pred_def]
    1.30 +
    1.31 +declare subset_iff[code_pred_inline]
    1.32 +
    1.33 +declare Int_def[code_pred_inline]
    1.34 +declare eq_reflection[OF Un_def, code_pred_inline]
    1.35 +declare eq_reflection[OF UNION_def, code_pred_inline]
    1.36 +
    1.37 +lemma Diff[code_pred_inline]:
    1.38 +  "(A - B) = (%x. A x \<and> \<not> B x)"
    1.39 +by (auto simp add: mem_def)
    1.40 +
    1.41 +lemma set_equality[code_pred_inline]:
    1.42 +  "(A = B) = ((\<forall>x. A x \<longrightarrow> B x) \<and> (\<forall>x. B x \<longrightarrow> A x))"
    1.43 +by (fastsimp simp add: mem_def)
    1.44 +
    1.45 +section {* Setup for Numerals *}
    1.46 +
    1.47 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name number_of}] *}
    1.48 +setup {* Predicate_Compile_Data.keep_functions [@{const_name number_of}] *}
    1.49 +
    1.50 +setup {* Predicate_Compile_Data.ignore_consts [@{const_name div}, @{const_name mod}, @{const_name times}] *}
    1.51 +
    1.52 +subsection {* Inductive definitions for arithmetic on natural numbers *}
    1.53 +
    1.54 +inductive plusP
    1.55 +where
    1.56 +  "plusP x 0 x"
    1.57 +|  "plusP x y z ==> plusP x (Suc y) (Suc z)"
    1.58 +
    1.59 +setup {* Predicate_Compile_Fun.add_function_predicate_translation
    1.60 +  (@{term "op + :: nat => nat => nat"}, @{term "plusP"}) *}
    1.61 +
    1.62 +inductive less_nat
    1.63 +where
    1.64 +  "less_nat 0 (Suc y)"
    1.65 +| "less_nat x y ==> less_nat (Suc x) (Suc y)"
    1.66 +
    1.67 +lemma [code_pred_inline]:
    1.68 +  "x < y = less_nat x y"
    1.69 +apply (rule iffI)
    1.70 +apply (induct x arbitrary: y)
    1.71 +apply (case_tac y) apply (auto intro: less_nat.intros)
    1.72 +apply (case_tac y)
    1.73 +apply (auto intro: less_nat.intros)
    1.74 +apply (induct rule: less_nat.induct)
    1.75 +apply auto
    1.76 +done
    1.77 +
    1.78 +inductive less_eq_nat
    1.79 +where
    1.80 +  "less_eq_nat 0 y"
    1.81 +| "less_eq_nat x y ==> less_eq_nat (Suc x) (Suc y)"
    1.82 +
    1.83 +lemma [code_pred_inline]:
    1.84 +"x <= y = less_eq_nat x y"
    1.85 +apply (rule iffI)
    1.86 +apply (induct x arbitrary: y)
    1.87 +apply (auto intro: less_eq_nat.intros)
    1.88 +apply (case_tac y) apply (auto intro: less_eq_nat.intros)
    1.89 +apply (induct rule: less_eq_nat.induct)
    1.90 +apply auto done
    1.91 +
    1.92 +section {* Alternative list definitions *}
    1.93 +
    1.94 +text {* size simps are not yet added to the Spec_Rules interface. So they are just added manually here! *}
    1.95 + 
    1.96 +lemma [code_pred_def]:
    1.97 +  "length [] = 0"
    1.98 +  "length (x # xs) = Suc (length xs)"
    1.99 +by auto
   1.100 +
   1.101 +subsection {* Alternative rules for set *}
   1.102 +
   1.103 +lemma set_ConsI1 [code_pred_intro]:
   1.104 +  "set (x # xs) x"
   1.105 +unfolding mem_def[symmetric, of _ x]
   1.106 +by auto
   1.107 +
   1.108 +lemma set_ConsI2 [code_pred_intro]:
   1.109 +  "set xs x ==> set (x' # xs) x" 
   1.110 +unfolding mem_def[symmetric, of _ x]
   1.111 +by auto
   1.112 +
   1.113 +code_pred [skip_proof] set
   1.114 +proof -
   1.115 +  case set
   1.116 +  from this show thesis
   1.117 +    apply (case_tac xb)
   1.118 +    apply auto
   1.119 +    unfolding mem_def[symmetric, of _ xc]
   1.120 +    apply auto
   1.121 +    unfolding mem_def
   1.122 +    apply fastsimp
   1.123 +    done
   1.124 +qed
   1.125 +
   1.126 +subsection {* Alternative rules for list_all2 *}
   1.127 +
   1.128 +lemma list_all2_NilI [code_pred_intro]: "list_all2 P [] []"
   1.129 +by auto
   1.130 +
   1.131 +lemma list_all2_ConsI [code_pred_intro]: "list_all2 P xs ys ==> P x y ==> list_all2 P (x#xs) (y#ys)"
   1.132 +by auto
   1.133 +
   1.134 +code_pred [skip_proof] list_all2
   1.135 +proof -
   1.136 +  case list_all2
   1.137 +  from this show thesis
   1.138 +    apply -
   1.139 +    apply (case_tac xb)
   1.140 +    apply (case_tac xc)
   1.141 +    apply auto
   1.142 +    apply (case_tac xc)
   1.143 +    apply auto
   1.144 +    apply fastsimp
   1.145 +    done
   1.146 +qed
   1.147 +
   1.148 +
   1.149 +
   1.150 +end
   1.151 \ No newline at end of file