src/HOL/Tools/SMT/smt_normalize.ML
changeset 40161 539d07b00e5f
parent 39483 9f0e5684f04b
child 40162 7f58a9a843c2
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:31:03 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Tue Oct 26 11:39:26 2010 +0200
     1.3 @@ -17,9 +17,10 @@
     1.4  
     1.5  signature SMT_NORMALIZE =
     1.6  sig
     1.7 -  type extra_norm = thm list -> Proof.context -> thm list * Proof.context
     1.8 -  val normalize: extra_norm -> bool -> thm list -> Proof.context ->
     1.9 -    thm list * Proof.context
    1.10 +  type extra_norm = (int * thm) list -> Proof.context ->
    1.11 +    (int * thm) list * Proof.context
    1.12 +  val normalize: extra_norm -> bool -> (int * thm) list -> Proof.context ->
    1.13 +    (int * thm) list * Proof.context
    1.14    val atomize_conv: Proof.context -> conv
    1.15    val eta_expand_conv: (Proof.context -> conv) -> Proof.context -> conv
    1.16  end
    1.17 @@ -52,8 +53,8 @@
    1.18      if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
    1.19  in
    1.20  fun trivial_distinct ctxt =
    1.21 -  map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    1.22 -    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))
    1.23 +  map (apsnd ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    1.24 +    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt)))
    1.25  end
    1.26  
    1.27  
    1.28 @@ -72,8 +73,8 @@
    1.29    val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
    1.30  in
    1.31  fun rewrite_bool_cases ctxt =
    1.32 -  map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    1.33 -    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))
    1.34 +  map (apsnd ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    1.35 +    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt)))
    1.36  end
    1.37  
    1.38  
    1.39 @@ -108,8 +109,8 @@
    1.40      Conv.no_conv
    1.41  in
    1.42  fun normalize_numerals ctxt =
    1.43 -  map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
    1.44 -    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))
    1.45 +  map (apsnd ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
    1.46 +    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt)))
    1.47  end
    1.48  
    1.49  
    1.50 @@ -117,7 +118,7 @@
    1.51  (* embedding of standard natural number operations into integer operations *)
    1.52  
    1.53  local
    1.54 -  val nat_embedding = @{lemma
    1.55 +  val nat_embedding = map (pair ~1) @{lemma
    1.56      "nat (int n) = n"
    1.57      "i >= 0 --> int (nat i) = i"
    1.58      "i < 0 --> int (nat i) = 0"
    1.59 @@ -179,8 +180,8 @@
    1.60      Term.exists_subterm (member (op aconv) [@{term int}, @{term nat}])
    1.61  in
    1.62  fun nat_as_int ctxt =
    1.63 -  map ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt)) #>
    1.64 -  exists (uses_nat_int o Thm.prop_of) ?? append nat_embedding
    1.65 +  map (apsnd ((uses_nat_type o Thm.prop_of) ?? Conv.fconv_rule (conv ctxt))) #>
    1.66 +  exists (uses_nat_int o Thm.prop_of o snd) ?? append nat_embedding
    1.67  end
    1.68  
    1.69  
    1.70 @@ -362,12 +363,13 @@
    1.71      if not (has_free_lambdas (Thm.prop_of thm)) then (thm, cx)
    1.72      else cx |> f (Thm.cprop_of thm) |>> (fn thm' => Thm.equal_elim thm' thm)
    1.73  in
    1.74 -fun lift_lambdas thms ctxt =
    1.75 +fun lift_lambdas irules ctxt =
    1.76    let
    1.77      val cx = (ctxt, Termtab.empty)
    1.78 +    val (idxs, thms) = split_list irules
    1.79      val (thms', (ctxt', defs)) = fold_map (lift_lm (traverse [])) thms cx
    1.80      val eqs = Termtab.fold (cons o normalize_rule ctxt' o snd) defs []
    1.81 -  in (eqs @ thms', ctxt') end
    1.82 +  in (map (pair ~1) eqs @ (idxs ~~ thms'), ctxt') end
    1.83  end
    1.84  
    1.85  
    1.86 @@ -384,8 +386,8 @@
    1.87      | (Free (n, _), ts) => add (free n) (length ts) #> fold traverse ts
    1.88      | (Abs (_, _, u), ts) => fold traverse (u :: ts)
    1.89      | (_, ts) => fold traverse ts)
    1.90 -  val prune = (fn (n, (true, i)) => Symtab.update (n, i) | _ => I)
    1.91 -  fun prune_tab tab = Symtab.fold prune tab Symtab.empty
    1.92 +  fun prune tab = Symtab.fold (fn (n, (true, i)) =>
    1.93 +    Symtab.update (n, i) | _ => I) tab Symtab.empty
    1.94  
    1.95    fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
    1.96    fun nary_conv conv1 conv2 ct =
    1.97 @@ -395,7 +397,7 @@
    1.98      in conv (Symtab.update (free n, 0) tb) cx end)
    1.99    val fun_app_rule = @{lemma "f x == fun_app f x" by (simp add: fun_app_def)}
   1.100  in
   1.101 -fun explicit_application ctxt thms =
   1.102 +fun explicit_application ctxt irules =
   1.103    let
   1.104      fun sub_conv tb ctxt ct =
   1.105        (case Term.strip_comb (Thm.term_of ct) of
   1.106 @@ -423,8 +425,8 @@
   1.107        if not (needs_exp_app tab (Thm.prop_of thm)) then thm
   1.108        else Conv.fconv_rule (sub_conv tab ctxt) thm
   1.109  
   1.110 -    val tab = prune_tab (fold (traverse o Thm.prop_of) thms Symtab.empty)
   1.111 -  in map (rewrite tab ctxt) thms end
   1.112 +    val tab = prune (fold (traverse o Thm.prop_of o snd) irules Symtab.empty)
   1.113 +  in map (apsnd (rewrite tab ctxt)) irules end
   1.114  end
   1.115  
   1.116  
   1.117 @@ -465,11 +467,11 @@
   1.118          end)
   1.119  in
   1.120  
   1.121 -fun datatype_selectors thms ctxt =
   1.122 +fun datatype_selectors irules ctxt =
   1.123    let
   1.124 -    val ns = Symtab.keys (fold (collect o Thm.prop_of) thms Symtab.empty)
   1.125 +    val ns = Symtab.keys (fold (collect o Thm.prop_of o snd) irules Symtab.empty)
   1.126      val cs = fold (add_constructors (ProofContext.theory_of ctxt)) ns []
   1.127 -  in (thms, fold add_selector cs ctxt) end
   1.128 +  in (irules, fold add_selector cs ctxt) end
   1.129      (* FIXME: also generate hypothetical definitions for the selectors *)
   1.130  
   1.131  end
   1.132 @@ -478,19 +480,20 @@
   1.133  
   1.134  (* combined normalization *)
   1.135  
   1.136 -type extra_norm = thm list -> Proof.context -> thm list * Proof.context
   1.137 +type extra_norm = (int * thm) list -> Proof.context ->
   1.138 +  (int * thm) list * Proof.context
   1.139  
   1.140 -fun with_context f thms ctxt = (f ctxt thms, ctxt)
   1.141 +fun with_context f irules ctxt = (f ctxt irules, ctxt)
   1.142  
   1.143 -fun normalize extra_norm with_datatypes thms ctxt =
   1.144 -  thms
   1.145 +fun normalize extra_norm with_datatypes irules ctxt =
   1.146 +  irules
   1.147    |> trivial_distinct ctxt
   1.148    |> rewrite_bool_cases ctxt
   1.149    |> normalize_numerals ctxt
   1.150    |> nat_as_int ctxt
   1.151    |> rpair ctxt
   1.152    |-> extra_norm
   1.153 -  |-> with_context (fn cx => map (normalize_rule cx))
   1.154 +  |-> with_context (fn cx => map (apsnd (normalize_rule cx)))
   1.155    |-> SMT_Monomorph.monomorph
   1.156    |-> lift_lambdas
   1.157    |-> with_context explicit_application