move lemmas to theory file, towards textual proof reconstruction
authorblanchet
Thu Mar 13 14:48:20 2014 +0100 (2014-03-13)
changeset 561036689512f3710
parent 56102 439dda276b3f
child 56104 fd6e132ee4fb
move lemmas to theory file, towards textual proof reconstruction
src/HOL/SMT2.thy
src/HOL/Tools/SMT2/smt2_builtin.ML
src/HOL/Tools/SMT2/smt2_normalize.ML
src/HOL/Tools/SMT2/z3_new_interface.ML
     1.1 --- a/src/HOL/SMT2.thy	Thu Mar 13 14:48:05 2014 +0100
     1.2 +++ b/src/HOL/SMT2.thy	Thu Mar 13 14:48:20 2014 +0100
     1.3 @@ -85,6 +85,39 @@
     1.4  lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other  fun_upd_upd fun_app_def
     1.5  
     1.6  
     1.7 +subsection {* Normalization *}
     1.8 +
     1.9 +lemma case_bool_if[abs_def]: "case_bool x y P = (if P then x else y)"
    1.10 +  by simp
    1.11 +
    1.12 +lemma nat_int: "\<forall>n. nat (int n) = n" by simp
    1.13 +lemma int_nat_nneg: "\<forall>i. i \<ge> 0 \<longrightarrow> int (nat i) = i" by simp
    1.14 +lemma int_nat_neg: "\<forall>i. i < 0 \<longrightarrow> int (nat i) = 0" by simp
    1.15 +
    1.16 +lemma nat_zero_as_int: "0 = nat 0" by (rule transfer_nat_int_numerals(1))
    1.17 +lemma nat_one_as_int: "1 = nat 1" by (rule transfer_nat_int_numerals(2))
    1.18 +lemma nat_numeral_as_int: "numeral = (\<lambda>i. nat (numeral i))" by simp
    1.19 +lemma nat_less_as_int: "op < = (\<lambda>a b. int a < int b)" by simp
    1.20 +lemma nat_leq_as_int: "op \<le> = (\<lambda>a b. int a <= int b)" by simp
    1.21 +lemma Suc_as_int: "Suc = (\<lambda>a. nat (int a + 1))" by (rule ext) simp
    1.22 +lemma nat_plus_as_int: "op + = (\<lambda>a b. nat (int a + int b))" by (rule ext)+ simp
    1.23 +lemma nat_minus_as_int: "op - = (\<lambda>a b. nat (int a - int b))" by (rule ext)+ simp
    1.24 +lemma nat_times_as_int: "op * = (\<lambda>a b. nat (int a * int b))" by (simp add: nat_mult_distrib)
    1.25 +lemma nat_div_as_int: "op div = (\<lambda>a b. nat (int a div int b))" by (simp add: nat_div_distrib)
    1.26 +lemma nat_mod_as_int: "op mod = (\<lambda>a b. nat (int a mod int b))" by (simp add: nat_mod_distrib)
    1.27 +
    1.28 +lemma int_Suc: "int (Suc n) = int n + 1" by simp
    1.29 +lemma int_plus: "int (n + m) = int n + int m" by (rule of_nat_add)
    1.30 +lemma int_minus: "int (n - m) = int (nat (int n - int m))" by auto
    1.31 +
    1.32 +lemmas Ex1_def_raw = Ex1_def[abs_def]
    1.33 +lemmas Ball_def_raw = Ball_def[abs_def]
    1.34 +lemmas Bex_def_raw = Bex_def[abs_def]
    1.35 +lemmas abs_if_raw = abs_if[abs_def]
    1.36 +lemmas min_def_raw = min_def[abs_def]
    1.37 +lemmas max_def_raw = max_def[abs_def]
    1.38 +
    1.39 +
    1.40  subsection {* Integer division and modulo for Z3 *}
    1.41  
    1.42  text {*
     2.1 --- a/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Mar 13 14:48:05 2014 +0100
     2.2 +++ b/src/HOL/Tools/SMT2/smt2_builtin.ML	Thu Mar 13 14:48:20 2014 +0100
     2.3 @@ -29,20 +29,15 @@
     2.4    val add_builtin_fun: SMT2_Util.class -> (string * typ) * bfunr option bfun -> Context.generic ->
     2.5      Context.generic
     2.6    val add_builtin_fun': SMT2_Util.class -> term * string -> Context.generic -> Context.generic
     2.7 -  val add_builtin_fun_ext: (string * typ) * term list bfun ->
     2.8 -    Context.generic -> Context.generic
     2.9 +  val add_builtin_fun_ext: (string * typ) * term list bfun -> Context.generic -> Context.generic
    2.10    val add_builtin_fun_ext': string * typ -> Context.generic -> Context.generic
    2.11    val add_builtin_fun_ext'': string -> Context.generic -> Context.generic
    2.12 -  val dest_builtin_fun: Proof.context -> string * typ -> term list ->
    2.13 -    bfunr option
    2.14 +  val dest_builtin_fun: Proof.context -> string * typ -> term list -> bfunr option
    2.15    val dest_builtin_eq: Proof.context -> term -> term -> bfunr option
    2.16 -  val dest_builtin_pred: Proof.context -> string * typ -> term list ->
    2.17 -    bfunr option
    2.18 -  val dest_builtin_conn: Proof.context -> string * typ -> term list ->
    2.19 -    bfunr option
    2.20 +  val dest_builtin_pred: Proof.context -> string * typ -> term list -> bfunr option
    2.21 +  val dest_builtin_conn: Proof.context -> string * typ -> term list -> bfunr option
    2.22    val dest_builtin: Proof.context -> string * typ -> term list -> bfunr option
    2.23 -  val dest_builtin_ext: Proof.context -> string * typ -> term list ->
    2.24 -    term list option
    2.25 +  val dest_builtin_ext: Proof.context -> string * typ -> term list -> term list option
    2.26    val is_builtin_fun: Proof.context -> string * typ -> term list -> bool
    2.27    val is_builtin_fun_ext: Proof.context -> string * typ -> term list -> bool
    2.28  end
     3.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:05 2014 +0100
     3.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Mar 13 14:48:20 2014 +0100
     3.3 @@ -58,36 +58,25 @@
     3.4  fun atomize_conv ctxt ct =
     3.5    (case Thm.term_of ct of
     3.6      @{const "==>"} $ _ $ _ =>
     3.7 -      Conv.binop_conv (atomize_conv ctxt) then_conv
     3.8 -      Conv.rewr_conv @{thm atomize_imp}
     3.9 +      Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_imp}
    3.10    | Const (@{const_name "=="}, _) $ _ $ _ =>
    3.11 -      Conv.binop_conv (atomize_conv ctxt) then_conv
    3.12 -      Conv.rewr_conv @{thm atomize_eq}
    3.13 +      Conv.binop_conv (atomize_conv ctxt) then_conv Conv.rewr_conv @{thm atomize_eq}
    3.14    | Const (@{const_name all}, _) $ Abs _ =>
    3.15 -      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
    3.16 -      Conv.rewr_conv @{thm atomize_all}
    3.17 +      Conv.binder_conv (atomize_conv o snd) ctxt then_conv Conv.rewr_conv @{thm atomize_all}
    3.18    | _ => Conv.all_conv) ct
    3.19  
    3.20  val setup_atomize =
    3.21 -  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"},
    3.22 -    @{const_name "=="}, @{const_name all}, @{const_name Trueprop}]
    3.23 +  fold SMT2_Builtin.add_builtin_fun_ext'' [@{const_name "==>"}, @{const_name "=="},
    3.24 +    @{const_name all}, @{const_name Trueprop}]
    3.25  
    3.26  
    3.27  (** unfold special quantifiers **)
    3.28  
    3.29  local
    3.30 -  val ex1_def = mk_meta_eq @{lemma
    3.31 -    "Ex1 = (%P. EX x. P x & (ALL y. P y --> y = x))"
    3.32 -    by (rule ext) (simp only: Ex1_def)}
    3.33 -
    3.34 -  val ball_def = mk_meta_eq @{lemma "Ball = (%A P. ALL x. x : A --> P x)"
    3.35 -    by (rule ext)+ (rule Ball_def)}
    3.36 -
    3.37 -  val bex_def = mk_meta_eq @{lemma "Bex = (%A P. EX x. x : A & P x)"
    3.38 -    by (rule ext)+ (rule Bex_def)}
    3.39 -
    3.40 -  val special_quants = [(@{const_name Ex1}, ex1_def),
    3.41 -    (@{const_name Ball}, ball_def), (@{const_name Bex}, bex_def)]
    3.42 +  val special_quants = [
    3.43 +    (@{const_name Ex1}, @{thm Ex1_def_raw}),
    3.44 +    (@{const_name Ball}, @{thm Ball_def_raw}),
    3.45 +    (@{const_name Bex}, @{thm Bex_def_raw})]
    3.46    
    3.47    fun special_quant (Const (n, _)) = AList.lookup (op =) special_quants n
    3.48      | special_quant _ = NONE
    3.49 @@ -101,8 +90,7 @@
    3.50  fun unfold_special_quants_conv ctxt =
    3.51    SMT2_Util.if_exists_conv (is_some o special_quant) (Conv.top_conv special_quant_conv ctxt)
    3.52  
    3.53 -val setup_unfolded_quants =
    3.54 -  fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
    3.55 +val setup_unfolded_quants = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) special_quants
    3.56  
    3.57  end
    3.58  
    3.59 @@ -202,8 +190,7 @@
    3.60    val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})  
    3.61    fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
    3.62  
    3.63 -  val trigger_eq =
    3.64 -    mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)}
    3.65 +  val trigger_eq = mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)}
    3.66  
    3.67    fun insert_trigger_conv [] ct = Conv.all_conv ct
    3.68      | insert_trigger_conv ctss ct =
    3.69 @@ -282,13 +269,10 @@
    3.70        @{const SMT2.trigger} $ _ $ _ => Conv.arg_conv cv
    3.71      | _ => cv) ct
    3.72  
    3.73 -  val weight_eq =
    3.74 -    mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)}
    3.75 +  val weight_eq = mk_meta_eq @{lemma "p = SMT2.weight i p" by (simp add: weight_def)}
    3.76    fun mk_weight_eq w =
    3.77      let val cv = Thm.dest_arg1 (Thm.rhs_of weight_eq)
    3.78 -    in
    3.79 -      Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq
    3.80 -    end
    3.81 +    in Thm.instantiate ([], [(cv, Numeral.mk_cnumber @{ctyp int} w)]) weight_eq end
    3.82  
    3.83    fun add_weight_conv NONE _ = Conv.all_conv
    3.84      | add_weight_conv (SOME weight) ctxt =
    3.85 @@ -348,18 +332,15 @@
    3.86    fun is_case_bool (Const (@{const_name "bool.case_bool"}, _)) = true
    3.87      | is_case_bool _ = false
    3.88  
    3.89 -  val thm = mk_meta_eq @{lemma
    3.90 -    "case_bool = (%x y P. if P then x else y)" by (rule ext)+ simp}
    3.91 -
    3.92    fun unfold_conv _ =
    3.93 -    SMT2_Util.if_true_conv (is_case_bool o Term.head_of) (expand_head_conv (Conv.rewr_conv thm))
    3.94 +    SMT2_Util.if_true_conv (is_case_bool o Term.head_of)
    3.95 +      (expand_head_conv (Conv.rewr_conv @{thm case_bool_if}))
    3.96  in
    3.97  
    3.98  fun rewrite_case_bool_conv ctxt =
    3.99    SMT2_Util.if_exists_conv is_case_bool (Conv.top_conv unfold_conv ctxt)
   3.100  
   3.101 -val setup_case_bool =
   3.102 -  SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   3.103 +val setup_case_bool = SMT2_Builtin.add_builtin_fun_ext'' @{const_name "bool.case_bool"}
   3.104  
   3.105  end
   3.106  
   3.107 @@ -367,17 +348,10 @@
   3.108  (** unfold abs, min and max **)
   3.109  
   3.110  local
   3.111 -  val abs_def = mk_meta_eq @{lemma "abs = (%a::'a::abs_if. if a < 0 then - a else a)"
   3.112 -    by (rule ext) (rule abs_if)}
   3.113 -
   3.114 -  val min_def = mk_meta_eq @{lemma "min = (%a b. if a <= b then a else b)"
   3.115 -    by (rule ext)+ (rule min_def)}
   3.116 -
   3.117 -  val max_def = mk_meta_eq  @{lemma "max = (%a b. if a <= b then b else a)"
   3.118 -    by (rule ext)+ (rule max_def)}
   3.119 -
   3.120 -  val defs = [(@{const_name min}, min_def), (@{const_name max}, max_def),
   3.121 -    (@{const_name abs}, abs_def)]
   3.122 +  val defs = [
   3.123 +    (@{const_name min}, @{thm min_def_raw}),
   3.124 +    (@{const_name max}, @{thm max_def_raw}),
   3.125 +    (@{const_name abs}, @{thm abs_if_raw})]
   3.126  
   3.127    fun abs_min_max ctxt (Const (n, Type (@{type_name fun}, [T, _]))) =
   3.128          (case AList.lookup (op =) defs n of
   3.129 @@ -402,11 +376,7 @@
   3.130  (** embedding of standard natural number operations into integer operations **)
   3.131  
   3.132  local
   3.133 -  val nat_embedding = @{lemma
   3.134 -    "ALL n. nat (int n) = n"
   3.135 -    "ALL i. i >= 0 --> int (nat i) = i"
   3.136 -    "ALL i. i < 0 --> int (nat i) = 0"
   3.137 -    by simp_all}
   3.138 +  val nat_embedding = @{thms nat_int int_nat_nneg int_nat_neg}
   3.139  
   3.140    val simple_nat_ops = [
   3.141      @{const less (nat)}, @{const less_eq (nat)},
   3.142 @@ -429,34 +399,13 @@
   3.143    fun is_nat_const' @{const of_nat (int)} = true
   3.144      | is_nat_const' t = is_nat_const t
   3.145  
   3.146 -  val expands = map mk_meta_eq @{lemma
   3.147 -    "0 = nat 0"
   3.148 -    "1 = nat 1"
   3.149 -    "(numeral :: num => nat) = (%i. nat (numeral i))"
   3.150 -    "op < = (%a b. int a < int b)"
   3.151 -    "op <= = (%a b. int a <= int b)"
   3.152 -    "Suc = (%a. nat (int a + 1))"
   3.153 -    "op + = (%a b. nat (int a + int b))"
   3.154 -    "op - = (%a b. nat (int a - int b))"
   3.155 -    "op * = (%a b. nat (int a * int b))"
   3.156 -    "op div = (%a b. nat (int a div int b))"
   3.157 -    "op mod = (%a b. nat (int a mod int b))"
   3.158 -    by (fastforce simp add: nat_mult_distrib nat_div_distrib nat_mod_distrib)+}
   3.159 +  val expands = map mk_meta_eq @{thms nat_zero_as_int nat_one_as_int nat_numeral_as_int
   3.160 +    nat_less_as_int nat_leq_as_int Suc_as_int nat_plus_as_int nat_minus_as_int nat_times_as_int
   3.161 +    nat_div_as_int nat_mod_as_int}
   3.162  
   3.163 -  val ints = map mk_meta_eq @{lemma
   3.164 -    "int 0 = 0"
   3.165 -    "int 1 = 1"
   3.166 -    "int (Suc n) = int n + 1"
   3.167 -    "int (n + m) = int n + int m"
   3.168 -    "int (n - m) = int (nat (int n - int m))"
   3.169 -    "int (n * m) = int n * int m"
   3.170 -    "int (n div m) = int n div int m"
   3.171 -    "int (n mod m) = int n mod int m"
   3.172 -    by (auto simp add: int_mult zdiv_int zmod_int)}
   3.173 -
   3.174 -  val int_if = mk_meta_eq @{lemma
   3.175 -    "int (if P then n else m) = (if P then int n else int m)"
   3.176 -    by simp}
   3.177 +  val ints = map mk_meta_eq @{thms int_0 int_1 int_Suc int_plus int_minus int_mult zdiv_int
   3.178 +    zmod_int}
   3.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}
   3.180  
   3.181    fun mk_number_eq ctxt i lhs =
   3.182      let
     4.1 --- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 14:48:05 2014 +0100
     4.2 +++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 14:48:20 2014 +0100
     4.3 @@ -42,8 +42,7 @@
     4.4      | is_div_mod @{const mod (int)} = true
     4.5      | is_div_mod _ = false
     4.6  
     4.7 -  val have_int_div_mod =
     4.8 -    exists (Term.exists_subterm is_div_mod o Thm.prop_of)
     4.9 +  val have_int_div_mod = exists (Term.exists_subterm is_div_mod o Thm.prop_of)
    4.10  
    4.11    fun add_div_mod _ (thms, extra_thms) =
    4.12      if have_int_div_mod thms orelse have_int_div_mod extra_thms then
    4.13 @@ -101,8 +100,7 @@
    4.14    fun merge data = Ord_List.merge fst_int_ord data
    4.15  )
    4.16  
    4.17 -fun add_mk_builtins mk =
    4.18 -  Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
    4.19 +fun add_mk_builtins mk = Mk_Builtins.map (Ord_List.insert fst_int_ord (serial (), mk))
    4.20  
    4.21  fun get_mk_builtins ctxt = map snd (Mk_Builtins.get (Context.Proof ctxt))
    4.22