src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 56103 6689512f3710
parent 56100 0dc5f68a7802
child 56104 fd6e132ee4fb
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:05 2014 +0100
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     1.3 @@ -58,36 +58,25 @@
     1.4  fun atomize_conv ctxt ct =
     1.5    (case Thm.term_of ct of
     1.6      @{const "==>"} $ _ $ _ =>
     1.7 -      Conv.binop_conv (atomize_conv ctxt) then_conv
     1.8 -      Conv.rewr_conv @{thm atomize_imp}
     1.9 +      Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
    1.10    | Const (@{const_name "=="}, _) $ _ $ _ =>
    1.11 -      Conv.binop_conv (atomize_conv ctxt) then_conv
    1.12 -      Conv.rewr_conv @{thm atomize_eq}
    1.13 +      Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
    1.14    | Const (@{const_name all}, _) $ Abs _ =>
    1.15 -      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
    1.16 -      Conv.rewr_conv @{thm atomize_all}
    1.17 +      Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
    1.18    | _ => Conv.all_conv) ct
    1.19  
    1.20  val setup_atomize =
    1.21 -  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
    1.22 -    @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
    1.23 +  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    1.24 +    @{const_name all}, @{const_name Trueprop}]
    1.25  
    1.26  
    1.27  (** unfold special quantifiers **)
    1.28  
    1.29  local
    1.30 -  val ex1_def = mk_meta_eq @{lemma
    1.31 -    "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))"
    1.32 -    by (rule ext) (simp only: Ex1_def)}
    1.33 -
    1.34 -  val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)"
    1.35 -    by (rule ext)+ (rule Ball_def)}
    1.36 -
    1.37 -  val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)"
    1.38 -    by (rule ext)+ (rule Bex_def)}
    1.39 -
    1.40 -  val special_quants = [(@{const_name Ex1}, ex1_def),
    1.41 -    (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)]
    1.42 +  val special_quants = [
    1.43 +    (@{const_name Ex1}, @{thm Ex1_def_raw}),
    1.44 +    (@{const_name Ball}, @{thm Ball_def_raw}),
    1.45 +    (@{const_name Bex}, @{thm Bex_def_raw})]
    1.46    
    1.47    fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n
    1.48      | special_quant _ = NONE
    1.49 @@ -101,8 +90,7 @@
    1.50  fun unfold_special_quants_conv ctxt =
    1.51    SMT2_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
    1.52  
    1.53 -val setup_unfolded_quants =
    1.54 -  fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
    1.55 +val setup_unfolded_quants = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
    1.56  
    1.57  end
    1.58  
    1.59 @@ -202,8 +190,7 @@
    1.60    val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})  
    1.61    fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
    1.62  
    1.63 -  val trigger_eq =
    1.64 -    mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)}
    1.65 +  val trigger_eq = mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)}
    1.66  
    1.67    fun insert_trigger_conv [] ct = Conv.all_conv ct
    1.68      | insert_trigger_conv ctss ct =
    1.69 @@ -282,13 +269,10 @@
    1.70        @{const SMT2.trigger} $ _ $ _ => Conv.arg_conv cv
    1.71      | _ => cv) ct
    1.72  
    1.73 -  val weight_eq =
    1.74 -    mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)}
    1.75 +  val weight_eq = mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)}
    1.76    fun mk_weight_eq w =
    1.77      let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
    1.78 -    in
    1.79 -      Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq
    1.80 -    end
    1.81 +    in Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq end
    1.82  
    1.83    fun add_weight_conv NONE _ = Conv.all_conv
    1.84      | add_weight_conv (SOME weight) ctxt =
    1.85 @@ -348,18 +332,15 @@
    1.86    fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
    1.87      | is_case_bool _ = false
    1.88  
    1.89 -  val thm = mk_meta_eq @{lemma
    1.90 -    "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
    1.91 -
    1.92    fun unfold_conv _ =
    1.93 -    SMT2_Util.if_true_conv (is_case_bool o Term.head_of) (expand_head_conv (Conv.rewr_conv thm))
    1.94 +    SMT2_Util.if_true_conv (is_case_bool o Term.head_of)
    1.95 +      (expand_head_conv (Conv.rewr_conv @{thm case_bool_if}))
    1.96  in
    1.97  
    1.98  fun rewrite_case_bool_conv ctxt =
    1.99    SMT2_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
   1.100  
   1.101 -val setup_case_bool =
   1.102 -  SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   1.103 +val setup_case_bool = SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   1.104  
   1.105  end
   1.106  
   1.107 @@ -367,17 +348,10 @@
   1.108  (** unfold abs, min and max **)
   1.109  
   1.110  local
   1.111 -  val abs_def = mk_meta_eq @{lemma "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
   1.112 -    by (rule ext) (rule abs_if)}
   1.113 -
   1.114 -  val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)"
   1.115 -    by (rule ext)+ (rule min_def)}
   1.116 -
   1.117 -  val max_def = mk_meta_eq  @{lemma "max = (%a b. if a <= b then b else a)"
   1.118 -    by (rule ext)+ (rule max_def)}
   1.119 -
   1.120 -  val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
   1.121 -    (@{const_name abs}, abs_def)]
   1.122 +  val defs = [
   1.123 +    (@{const_name min}, @{thm min_def_raw}),
   1.124 +    (@{const_name max}, @{thm max_def_raw}),
   1.125 +    (@{const_name abs}, @{thm abs_if_raw})]
   1.126  
   1.127    fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
   1.128          (case AList.lookup (op =) defs n of
   1.129 @@ -402,11 +376,7 @@
   1.130  (** embedding of standard natural number operations into integer operations **)
   1.131  
   1.132  local
   1.133 -  val nat_embedding = @{lemma
   1.134 -    "ALL n. nat (int n) = n"
   1.135 -    "ALL i. i >= 0 --> int (nat i) = i"
   1.136 -    "ALL i. i < 0 --> int (nat i) = 0"
   1.137 -    by simp_all}
   1.138 +  val nat_embedding = @{thms nat_int int_nat_nneg int_nat_neg}
   1.139  
   1.140    val simple_nat_ops = [
   1.141      @{const less (nat)}, @{const less_eq (nat)},
   1.142 @@ -429,34 +399,13 @@
   1.143    fun is_nat_const' @{const of_nat (int)} = true
   1.144      | is_nat_const' t = is_nat_const t
   1.145  
   1.146 -  val expands = map mk_meta_eq @{lemma
   1.147 -    "0 = nat 0"
   1.148 -    "1 = nat 1"
   1.149 -    "(numeral :: num => nat) = (%i. nat (numeral i))"
   1.150 -    "op < = (%a b. int a < int b)"
   1.151 -    "op <= = (%a b. int a <= int b)"
   1.152 -    "Suc = (%a. nat (int a + 1))"
   1.153 -    "op + = (%a b. nat (int a + int b))"
   1.154 -    "op - = (%a b. nat (int a - int b))"
   1.155 -    "op * = (%a b. nat (int a * int b))"
   1.156 -    "op div = (%a b. nat (int a div int b))"
   1.157 -    "op mod = (%a b. nat (int a mod int b))"
   1.158 -    by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
   1.159 +  val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int
   1.160 +    nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int
   1.161 +    nat_div_as_int nat_mod_as_int}
   1.162  
   1.163 -  val ints = map mk_meta_eq @{lemma
   1.164 -    "int 0 = 0"
   1.165 -    "int 1 = 1"
   1.166 -    "int (Suc n) = int n + 1"
   1.167 -    "int (n + m) = int n + int m"
   1.168 -    "int (n - m) = int (nat (int n - int m))"
   1.169 -    "int (n * m) = int n * int m"
   1.170 -    "int (n div m) = int n div int m"
   1.171 -    "int (n mod m) = int n mod int m"
   1.172 -    by (auto simp add: int_mult zdiv_int zmod_int)}
   1.173 -
   1.174 -  val int_if = mk_meta_eq @{lemma
   1.175 -    "int (if P then n else m) = (if P then int n else int m)"
   1.176 -    by simp}
   1.177 +  val ints = map mk_meta_eq @{thms int_0 int_1 int_Suc int_plus int_minus int_mult zdiv_int
   1.178 +    zmod_int}
   1.179 +  val int_if = mk_meta_eq @{lemma "int (if P then n else m) = (if P then int n else int m)" by simp}
   1.180  
   1.181    fun mk_number_eq ctxt i lhs =
   1.182      let