src/HOL/Tools/Function/function_context_tree.ML
author wenzelm
Sat Jul 25 23:41:53 2015 +0200 (2015-07-25)
changeset 60781 2da59cdf531c
parent 60695 757549b4bbe6
child 60801 7664e0916eec
permissions -rw-r--r--
updated to infer_instantiate;
tuned;
wenzelm@58816
     1
(*  Title:      HOL/Tools/Function/function_context_tree.ML
krauss@19564
     2
    Author:     Alexander Krauss, TU Muenchen
krauss@19564
     3
krauss@41114
     4
Construction and traversal of trees of nested contexts along a term.
krauss@19564
     5
*)
krauss@19564
     6
wenzelm@58816
     7
signature FUNCTION_CONTEXT_TREE =
krauss@19564
     8
sig
krauss@34232
     9
  (* poor man's contexts: fixes + assumes *)
krauss@34232
    10
  type ctxt = (string * typ) list * thm list
krauss@34232
    11
  type ctx_tree
krauss@19564
    12
krauss@34232
    13
  (* FIXME: This interface is a mess and needs to be cleaned up! *)
krauss@34232
    14
  val get_function_congs : Proof.context -> thm list
krauss@34232
    15
  val add_function_cong : thm -> Context.generic -> Context.generic
krauss@34232
    16
  val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
krauss@19564
    17
krauss@34232
    18
  val cong_add: attribute
krauss@34232
    19
  val cong_del: attribute
krauss@24168
    20
krauss@34232
    21
  val mk_tree: (string * typ) -> term -> Proof.context -> term -> ctx_tree
krauss@20523
    22
wenzelm@59618
    23
  val inst_tree: Proof.context -> term -> term -> ctx_tree -> ctx_tree
krauss@19564
    24
krauss@34232
    25
  val export_term : ctxt -> term -> term
wenzelm@59618
    26
  val export_thm : Proof.context -> ctxt -> thm -> thm
wenzelm@59618
    27
  val import_thm : Proof.context -> ctxt -> thm -> thm
krauss@19564
    28
krauss@34232
    29
  val traverse_tree :
krauss@26115
    30
   (ctxt -> term ->
krauss@26115
    31
   (ctxt * thm) list ->
krauss@26115
    32
   (ctxt * thm) list * 'b ->
krauss@26115
    33
   (ctxt * thm) list * 'b)
krauss@23819
    34
   -> ctx_tree -> 'b -> 'b
krauss@19564
    35
wenzelm@51717
    36
  val rewrite_by_tree : Proof.context -> term -> thm -> (thm * thm) list ->
krauss@34232
    37
    ctx_tree -> thm * (thm * thm) list
krauss@19564
    38
end
krauss@19564
    39
wenzelm@58816
    40
structure Function_Context_Tree : FUNCTION_CONTEXT_TREE =
krauss@19564
    41
struct
krauss@19564
    42
krauss@26115
    43
type ctxt = (string * typ) list * thm list
krauss@26115
    44
krauss@33099
    45
open Function_Common
krauss@33099
    46
open Function_Lib
krauss@19564
    47
wenzelm@33519
    48
structure FunctionCongs = Generic_Data
krauss@24168
    49
(
krauss@24168
    50
  type T = thm list
krauss@24168
    51
  val empty = []
krauss@24168
    52
  val extend = I
wenzelm@33519
    53
  val merge = Thm.merge_thms
krauss@24168
    54
);
krauss@24168
    55
krauss@33099
    56
val get_function_congs = FunctionCongs.get o Context.Proof
krauss@33099
    57
val map_function_congs = FunctionCongs.map
krauss@33099
    58
val add_function_cong = FunctionCongs.map o Thm.add_thm
krauss@24168
    59
krauss@24168
    60
(* congruence rules *)
krauss@24168
    61
krauss@33099
    62
val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
krauss@33099
    63
val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
krauss@24168
    64
krauss@24168
    65
wenzelm@35403
    66
type depgraph = int Int_Graph.T
krauss@23819
    67
krauss@34232
    68
datatype ctx_tree =
krauss@34232
    69
  Leaf of term
krauss@26115
    70
  | Cong of (thm * depgraph * (ctxt * ctx_tree) list)
krauss@23819
    71
  | RCall of (term * ctx_tree)
krauss@23819
    72
krauss@19564
    73
krauss@19564
    74
(* Maps "Trueprop A = B" to "A" *)
krauss@19564
    75
val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
krauss@19564
    76
krauss@19564
    77
krauss@19564
    78
(*** Dependency analysis for congruence rules ***)
krauss@19564
    79
krauss@34232
    80
fun branch_vars t =
krauss@34232
    81
  let
krauss@34232
    82
    val t' = snd (dest_all_all t)
krauss@34232
    83
    val (assumes, concl) = Logic.strip_horn t'
krauss@34232
    84
  in
krauss@34232
    85
    (fold Term.add_vars assumes [], Term.add_vars concl [])
krauss@34232
    86
  end
krauss@19564
    87
krauss@19564
    88
fun cong_deps crule =
krauss@34232
    89
  let
wenzelm@59582
    90
    val num_branches = map_index (apsnd branch_vars) (Thm.prems_of crule)
krauss@34232
    91
  in
wenzelm@35403
    92
    Int_Graph.empty
wenzelm@35403
    93
    |> fold (fn (i,_)=> Int_Graph.new_node (i,i)) num_branches
krauss@34232
    94
    |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) =>
krauss@34232
    95
         if i = j orelse null (inter (op =) c1 t2)
wenzelm@35403
    96
         then I else Int_Graph.add_edge_acyclic (i,j))
krauss@34232
    97
       num_branches num_branches
krauss@19564
    98
    end
krauss@19564
    99
krauss@34232
   100
val default_congs =
krauss@34232
   101
  map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}]
krauss@19564
   102
krauss@19564
   103
(* Called on the INSTANTIATED branches of the congruence rule *)
wenzelm@42362
   104
fun mk_branch ctxt t =
krauss@34232
   105
  let
wenzelm@60695
   106
    val ((params, impl), ctxt') = Variable.focus NONE t ctxt
krauss@34232
   107
    val (assms, concl) = Logic.strip_horn impl
krauss@34232
   108
  in
wenzelm@42495
   109
    (ctxt', map #2 params, assms, rhs_of concl)
krauss@34232
   110
  end
krauss@34232
   111
wenzelm@42362
   112
fun find_cong_rule ctxt fvar h ((r,dep)::rs) t =
wenzelm@42362
   113
     (let
wenzelm@42362
   114
        val thy = Proof_Context.theory_of ctxt
krauss@19564
   115
wenzelm@42362
   116
        val tt' = Logic.mk_equals (Pattern.rewrite_term thy [(Free fvar, h)] [] t, t)
wenzelm@59582
   117
        val (c, subs) = (Thm.concl_of r, Thm.prems_of r)
krauss@19564
   118
wenzelm@59618
   119
        val subst = Pattern.match thy (c, tt') (Vartab.empty, Vartab.empty)
wenzelm@42362
   120
        val branches = map (mk_branch ctxt o Envir.beta_norm o Envir.subst_term subst) subs
wenzelm@59618
   121
        val inst =
wenzelm@60781
   122
          map (fn v => (#1 v, Thm.cterm_of ctxt (Envir.subst_term subst (Var v))))
wenzelm@59618
   123
            (Term.add_vars c [])
wenzelm@42362
   124
      in
wenzelm@60781
   125
        (infer_instantiate ctxt inst r, dep, branches)
wenzelm@59618
   126
      end handle Pattern.MATCH => find_cong_rule ctxt fvar h rs t)
wenzelm@40317
   127
  | find_cong_rule _ _ _ [] _ = raise General.Fail "No cong rule found!"
krauss@19564
   128
krauss@19564
   129
krauss@24168
   130
fun mk_tree fvar h ctxt t =
krauss@34232
   131
  let
krauss@34232
   132
    val congs = get_function_congs ctxt
krauss@26115
   133
krauss@34232
   134
    (* FIXME: Save in theory: *)
krauss@34232
   135
    val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs)
krauss@34232
   136
krauss@34232
   137
    fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
krauss@34232
   138
      | matchcall _ = NONE
krauss@24168
   139
wenzelm@42362
   140
    fun mk_tree' ctxt t =
krauss@34232
   141
      case matchcall t of
wenzelm@42362
   142
        SOME arg => RCall (t, mk_tree' ctxt arg)
krauss@34232
   143
      | NONE =>
krauss@34232
   144
        if not (exists_subterm (fn Free v => v = fvar | _ => false) t) then Leaf t
krauss@34232
   145
        else
krauss@34232
   146
          let
wenzelm@42362
   147
            val (r, dep, branches) = find_cong_rule ctxt fvar h congs_deps t
wenzelm@42362
   148
            fun subtree (ctxt', fixes, assumes, st) =
krauss@34232
   149
              ((fixes,
wenzelm@59621
   150
                map (Thm.assume o Thm.cterm_of ctxt) assumes),
wenzelm@42362
   151
               mk_tree' ctxt' st)
krauss@34232
   152
          in
krauss@34232
   153
            Cong (r, dep, map subtree branches)
krauss@34232
   154
          end
krauss@34232
   155
  in
krauss@34232
   156
    mk_tree' ctxt t
krauss@34232
   157
  end
krauss@19564
   158
wenzelm@59618
   159
fun inst_tree ctxt fvar f tr =
krauss@34232
   160
  let
wenzelm@59621
   161
    val cfvar = Thm.cterm_of ctxt fvar
wenzelm@59621
   162
    val cf = Thm.cterm_of ctxt f
krauss@20523
   163
krauss@34232
   164
    fun inst_term t =
krauss@34232
   165
      subst_bound(f, abstract_over (fvar, t))
krauss@34232
   166
wenzelm@36945
   167
    val inst_thm = Thm.forall_elim cf o Thm.forall_intr cfvar
krauss@20523
   168
krauss@34232
   169
    fun inst_tree_aux (Leaf t) = Leaf t
krauss@34232
   170
      | inst_tree_aux (Cong (crule, deps, branches)) =
krauss@34232
   171
        Cong (inst_thm crule, deps, map inst_branch branches)
krauss@34232
   172
      | inst_tree_aux (RCall (t, str)) =
krauss@34232
   173
        RCall (inst_term t, inst_tree_aux str)
krauss@34232
   174
    and inst_branch ((fxs, assms), str) =
wenzelm@59621
   175
      ((fxs, map (Thm.assume o Thm.cterm_of ctxt o inst_term o Thm.prop_of) assms),
krauss@34232
   176
       inst_tree_aux str)
krauss@34232
   177
  in
krauss@34232
   178
    inst_tree_aux tr
krauss@34232
   179
  end
krauss@20523
   180
krauss@20523
   181
krauss@19564
   182
(* Poor man's contexts: Only fixes and assumes *)
krauss@19564
   183
fun compose (fs1, as1) (fs2, as2) = (fs1 @ fs2, as1 @ as2)
krauss@19564
   184
krauss@19564
   185
fun export_term (fixes, assumes) =
wenzelm@59582
   186
 fold_rev (curry Logic.mk_implies o Thm.prop_of) assumes
wenzelm@27330
   187
 #> fold_rev (Logic.all o Free) fixes
krauss@19564
   188
wenzelm@59618
   189
fun export_thm ctxt (fixes, assumes) =
wenzelm@59582
   190
 fold_rev (Thm.implies_intr o Thm.cprop_of) assumes
wenzelm@59621
   191
 #> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt o Free) fixes
krauss@19564
   192
wenzelm@59618
   193
fun import_thm ctxt (fixes, athms) =
wenzelm@59621
   194
 fold (Thm.forall_elim o Thm.cterm_of ctxt o Free) fixes
wenzelm@24977
   195
 #> fold Thm.elim_implies athms
krauss@19564
   196
krauss@19564
   197
krauss@19564
   198
(* folds in the order of the dependencies of a graph. *)
krauss@19564
   199
fun fold_deps G f x =
krauss@34232
   200
  let
krauss@34232
   201
    fun fill_table i (T, x) =
krauss@34232
   202
      case Inttab.lookup T i of
krauss@34232
   203
        SOME _ => (T, x)
krauss@34232
   204
      | NONE =>
krauss@34232
   205
        let
wenzelm@44338
   206
          val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x)
krauss@34232
   207
          val (v, x'') = f (the o Inttab.lookup T') i x'
krauss@34232
   208
        in
krauss@34232
   209
          (Inttab.update (i, v) T', x'')
krauss@34232
   210
        end
krauss@34232
   211
wenzelm@35403
   212
    val (T, x) = fold fill_table (Int_Graph.keys G) (Inttab.empty, x)
krauss@34232
   213
  in
krauss@34232
   214
    (Inttab.fold (cons o snd) T [], x)
krauss@34232
   215
  end
krauss@34232
   216
krauss@26115
   217
fun traverse_tree rcOp tr =
krauss@34232
   218
  let
wenzelm@42362
   219
    fun traverse_help ctxt (Leaf _) _ x = ([], x)
wenzelm@42362
   220
      | traverse_help ctxt (RCall (t, st)) u x =
wenzelm@42362
   221
          rcOp ctxt t u (traverse_help ctxt st u x)
wenzelm@42362
   222
      | traverse_help ctxt (Cong (_, deps, branches)) u x =
krauss@34232
   223
          let
wenzelm@42362
   224
            fun sub_step lu i x =
wenzelm@42362
   225
              let
wenzelm@42362
   226
                val (ctxt', subtree) = nth branches i
wenzelm@44338
   227
                val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
wenzelm@42362
   228
                val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
wenzelm@42362
   229
                val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
wenzelm@42362
   230
              in
wenzelm@42362
   231
                (exported_subs, x')
wenzelm@42362
   232
              end
krauss@34232
   233
          in
wenzelm@42362
   234
            fold_deps deps sub_step x
wenzelm@42362
   235
            |> apfst flat
krauss@34232
   236
          end
krauss@34232
   237
  in
krauss@34232
   238
    snd o traverse_help ([], []) tr []
krauss@34232
   239
  end
krauss@19564
   240
wenzelm@51717
   241
fun rewrite_by_tree ctxt h ih x tr =
krauss@34232
   242
  let
wenzelm@59621
   243
    fun rewrite_help _ _ x (Leaf t) = (Thm.reflexive (Thm.cterm_of ctxt t), x)
krauss@34232
   244
      | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
krauss@34232
   245
        let
krauss@34232
   246
          val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
krauss@34232
   247
wenzelm@59618
   248
          val iha = import_thm ctxt (fix, h_as) ha (* (a', h a') : G *)
krauss@34232
   249
            |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
krauss@26196
   250
                                                    (* (a, h a) : G   *)
wenzelm@59621
   251
          val inst_ih = instantiate' [] [SOME (Thm.cterm_of ctxt arg)] ih
wenzelm@36945
   252
          val eq = Thm.implies_elim (Thm.implies_elim inst_ih lRi) iha (* h a = f a *)
krauss@34232
   253
wenzelm@59621
   254
          val h_a'_eq_h_a = Thm.combination (Thm.reflexive (Thm.cterm_of ctxt h)) inner
krauss@34232
   255
          val h_a_eq_f_a = eq RS eq_reflection
wenzelm@36945
   256
          val result = Thm.transitive h_a'_eq_h_a h_a_eq_f_a
krauss@34232
   257
        in
krauss@34232
   258
          (result, x')
krauss@34232
   259
        end
krauss@34232
   260
      | rewrite_help fix h_as x (Cong (crule, deps, branches)) =
krauss@34232
   261
        let
krauss@34232
   262
          fun sub_step lu i x =
krauss@34232
   263
            let
krauss@34232
   264
              val ((fixes, assumes), st) = nth branches i
wenzelm@44338
   265
              val used = map lu (Int_Graph.immediate_succs deps i)
krauss@34232
   266
                |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
krauss@34232
   267
                |> filter_out Thm.is_reflexive
krauss@26196
   268
wenzelm@59618
   269
              val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes
krauss@34232
   270
krauss@34232
   271
              val (subeq, x') =
krauss@34232
   272
                rewrite_help (fix @ fixes) (h_as @ assumes') x st
krauss@34232
   273
              val subeq_exp =
wenzelm@59618
   274
                export_thm ctxt (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
krauss@34232
   275
            in
krauss@34232
   276
              (subeq_exp, x')
krauss@34232
   277
            end
krauss@34232
   278
          val (subthms, x') = fold_deps deps sub_step x
krauss@34232
   279
        in
krauss@34232
   280
          (fold_rev (curry op COMP) subthms crule, x')
krauss@34232
   281
        end
krauss@34232
   282
  in
krauss@34232
   283
    rewrite_help [] [] x tr
krauss@34232
   284
  end
krauss@34232
   285
wenzelm@19612
   286
end