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