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