src/HOL/Tools/Function/decompose.ML
author wenzelm
Thu Jul 09 22:01:41 2009 +0200 (2009-07-09)
changeset 31971 8c1b845ed105
parent 31775 2b04504fcb69
child 32149 ef59550a55d3
permissions -rw-r--r--
renamed functor TableFun to Table, and GraphFun to Graph;
haftmann@31775
     1
(*  Title:       HOL/Tools/Function/decompose.ML
krauss@29125
     2
    Author:      Alexander Krauss, TU Muenchen
krauss@29125
     3
krauss@29125
     4
Graph decomposition using "Shallow Dependency Pairs".
krauss@29125
     5
*)
krauss@29125
     6
krauss@29125
     7
signature DECOMPOSE =
krauss@29125
     8
sig
krauss@29125
     9
krauss@29125
    10
  val derive_chains : Proof.context -> tactic
krauss@29125
    11
                      -> (Termination.data -> int -> tactic)
krauss@29125
    12
                      -> Termination.data -> int -> tactic
krauss@29125
    13
krauss@29125
    14
  val decompose_tac : Proof.context -> tactic
krauss@29125
    15
                      -> Termination.ttac
krauss@29125
    16
krauss@29125
    17
end
krauss@29125
    18
krauss@29125
    19
structure Decompose : DECOMPOSE =
krauss@29125
    20
struct
krauss@29125
    21
wenzelm@31971
    22
structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
krauss@29125
    23
krauss@29125
    24
krauss@29125
    25
fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
krauss@29125
    26
  let
krauss@29125
    27
      val thy = ProofContext.theory_of ctxt
krauss@29125
    28
krauss@29125
    29
      fun prove_chain c1 c2 D =
krauss@29125
    30
          if is_some (Termination.get_chain D c1 c2) then D else
krauss@29125
    31
          let
krauss@29125
    32
            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
haftmann@30304
    33
                                      Const (@{const_name Set.empty}, fastype_of c1))
krauss@29125
    34
                       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
krauss@29125
    35
krauss@29125
    36
            val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
krauss@29125
    37
                          FundefLib.Solved thm => SOME thm
krauss@29125
    38
                        | _ => NONE
krauss@29125
    39
          in
krauss@29125
    40
            Termination.note_chain c1 c2 chain D
krauss@29125
    41
          end
krauss@29125
    42
  in
krauss@29125
    43
    cont (fold_product prove_chain cs cs D) i
krauss@29125
    44
  end)
krauss@29125
    45
krauss@29125
    46
krauss@29125
    47
fun mk_dgraph D cs =
krauss@29125
    48
    TermGraph.empty
krauss@29125
    49
    |> fold (fn c => TermGraph.new_node (c,())) cs
krauss@29125
    50
    |> fold_product (fn c1 => fn c2 =>
krauss@29125
    51
         if is_none (Termination.get_chain D c1 c2 |> the_default NONE)
krauss@29125
    52
         then TermGraph.add_edge (c1, c2) else I)
krauss@29125
    53
       cs cs
krauss@29125
    54
krauss@29125
    55
krauss@29125
    56
fun ucomp_empty_tac T =
krauss@29125
    57
    REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
krauss@29125
    58
                    ORELSE' rtac @{thm union_comp_emptyL}
krauss@29125
    59
                    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
krauss@29125
    60
krauss@29125
    61
fun regroup_calls_tac cs = Termination.CALLS (fn (cs', i) =>
krauss@29125
    62
   let
krauss@29125
    63
     val is = map (fn c => find_index (curry op aconv c) cs') cs
krauss@29125
    64
   in
krauss@29125
    65
     CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
krauss@29125
    66
   end)
krauss@29125
    67
krauss@29125
    68
krauss@29125
    69
fun solve_trivial_tac D = Termination.CALLS
krauss@29125
    70
(fn ([c], i) =>
krauss@29125
    71
    (case Termination.get_chain D c c of
krauss@29125
    72
       SOME (SOME thm) => rtac @{thm wf_no_loop} i
krauss@29125
    73
                          THEN rtac thm i
krauss@29125
    74
     | _ => no_tac)
krauss@29125
    75
  | _ => no_tac)
krauss@29125
    76
krauss@29125
    77
fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
krauss@29125
    78
    let
krauss@29125
    79
      val G = mk_dgraph D cs
krauss@29125
    80
      val sccs = TermGraph.strong_conn G
krauss@29125
    81
krauss@29125
    82
      fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
krauss@29125
    83
        | split (SCC::rest) i =
krauss@29125
    84
            regroup_calls_tac SCC i
krauss@29125
    85
            THEN rtac @{thm wf_union_compatible} i
krauss@29125
    86
            THEN rtac @{thm less_by_empty} (i + 2)
krauss@29125
    87
            THEN ucomp_empty_tac (the o the oo Termination.get_chain D) (i + 2)
krauss@29125
    88
            THEN split rest (i + 1)
krauss@29125
    89
            THEN (solve_trivial_tac D i ORELSE cont D i)
krauss@29125
    90
    in
krauss@29125
    91
      if length sccs > 1 then split sccs i
krauss@29125
    92
      else solve_trivial_tac D i ORELSE err_cont D i
krauss@29125
    93
    end)
krauss@29125
    94
krauss@29125
    95
fun decompose_tac ctxt chain_tac cont err_cont =
krauss@29125
    96
    derive_chains ctxt chain_tac
krauss@29125
    97
    (decompose_tac' ctxt cont err_cont)
krauss@29125
    98
krauss@29125
    99
fun auto_decompose_tac ctxt =
krauss@29125
   100
    Termination.TERMINATION ctxt
krauss@29125
   101
      (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
krauss@29125
   102
                     (K (K all_tac)) (K (K no_tac)))
krauss@29125
   103
krauss@29125
   104
krauss@29125
   105
end