src/HOL/Tools/Function/termination.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35408 b48ab741683b
child 37387 3581483cca6c
permissions -rw-r--r--
modernized structure Object_Logic;
     1 (*  Title:       HOL/Tools/Function/termination.ML
     2     Author:      Alexander Krauss, TU Muenchen
     3 
     4 Context data for termination proofs
     5 *)
     6 
     7 
     8 signature TERMINATION =
     9 sig
    10 
    11   type data
    12   datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
    13 
    14   val mk_sumcases : data -> typ -> term list -> term
    15 
    16   val get_num_points : data -> int
    17   val get_types      : data -> int -> typ
    18   val get_measures   : data -> int -> term list
    19 
    20   (* read from cache *)
    21   val get_chain      : data -> term -> term -> thm option option
    22   val get_descent    : data -> term -> term -> term -> cell option
    23 
    24   val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term)
    25 
    26   val CALLS : (term list * int -> tactic) -> int -> tactic
    27 
    28   (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
    29   type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
    30 
    31   val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
    32 
    33   val REPEAT : ttac -> ttac
    34 
    35   val wf_union_tac : Proof.context -> tactic
    36 
    37   val decompose_tac : Proof.context -> tactic -> ttac
    38 
    39   val derive_diag : Proof.context -> tactic -> 
    40     (data -> int -> tactic) -> data -> int -> tactic
    41 
    42   val derive_all  : Proof.context -> tactic ->
    43     (data -> int -> tactic) -> data -> int -> tactic
    44 
    45 end
    46 
    47 
    48 
    49 structure Termination : TERMINATION =
    50 struct
    51 
    52 open Function_Lib
    53 
    54 val term2_ord = prod_ord Term_Ord.fast_term_ord Term_Ord.fast_term_ord
    55 structure Term2tab = Table(type key = term * term val ord = term2_ord);
    56 structure Term3tab =
    57   Table(type key = term * (term * term) val ord = prod_ord Term_Ord.fast_term_ord term2_ord);
    58 
    59 (** Analyzing binary trees **)
    60 
    61 (* Skeleton of a tree structure *)
    62 
    63 datatype skel =
    64   SLeaf of int (* index *)
    65 | SBranch of (skel * skel)
    66 
    67 
    68 (* abstract make and dest functions *)
    69 fun mk_tree leaf branch =
    70   let fun mk (SLeaf i) = leaf i
    71         | mk (SBranch (s, t)) = branch (mk s, mk t)
    72   in mk end
    73 
    74 
    75 fun dest_tree split =
    76   let fun dest (SLeaf i) x = [(i, x)]
    77         | dest (SBranch (s, t)) x =
    78           let val (l, r) = split x
    79           in dest s l @ dest t r end
    80   in dest end
    81 
    82 
    83 (* concrete versions for sum types *)
    84 fun is_inj (Const (@{const_name Sum_Type.Inl}, _) $ _) = true
    85   | is_inj (Const (@{const_name Sum_Type.Inr}, _) $ _) = true
    86   | is_inj _ = false
    87 
    88 fun dest_inl (Const (@{const_name Sum_Type.Inl}, _) $ t) = SOME t
    89   | dest_inl _ = NONE
    90 
    91 fun dest_inr (Const (@{const_name Sum_Type.Inr}, _) $ t) = SOME t
    92   | dest_inr _ = NONE
    93 
    94 
    95 fun mk_skel ps =
    96   let
    97     fun skel i ps =
    98       if forall is_inj ps andalso not (null ps)
    99       then let
   100           val (j, s) = skel i (map_filter dest_inl ps)
   101           val (k, t) = skel j (map_filter dest_inr ps)
   102         in (k, SBranch (s, t)) end
   103       else (i + 1, SLeaf i)
   104   in
   105     snd (skel 0 ps)
   106   end
   107 
   108 (* compute list of types for nodes *)
   109 fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
   110 
   111 (* find index and raw term *)
   112 fun dest_inj (SLeaf i) trm = (i, trm)
   113   | dest_inj (SBranch (s, t)) trm =
   114     case dest_inl trm of
   115       SOME trm' => dest_inj s trm'
   116     | _ => dest_inj t (the (dest_inr trm))
   117 
   118 
   119 
   120 (** Matrix cell datatype **)
   121 
   122 datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
   123 
   124 
   125 type data =
   126   skel                            (* structure of the sum type encoding "program points" *)
   127   * (int -> typ)                  (* types of program points *)
   128   * (term list Inttab.table)      (* measures for program points *)
   129   * (thm option Term2tab.table)   (* which calls form chains? *)
   130   * (cell Term3tab.table)         (* local descents *)
   131 
   132 
   133 fun map_chains f (p, T, M, C, D) = (p, T, M, f C, D)
   134 fun map_descent f (p, T, M, C, D) = (p, T, M, C, f D)
   135 
   136 fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
   137 fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
   138 
   139 (* Build case expression *)
   140 fun mk_sumcases (sk, _, _, _, _) T fs =
   141   mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
   142           (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
   143           sk
   144   |> fst
   145 
   146 fun mk_sum_skel rel =
   147   let
   148     val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
   149     fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   150       let
   151         val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
   152           = Term.strip_qnt_body "Ex" c
   153       in cons r o cons l end
   154   in
   155     mk_skel (fold collect_pats cs [])
   156   end
   157 
   158 fun create ctxt T rel =
   159   let
   160     val sk = mk_sum_skel rel
   161     val Ts = node_types sk T
   162     val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
   163   in
   164     (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
   165   end
   166 
   167 fun get_num_points (sk, _, _, _, _) =
   168   let
   169     fun num (SLeaf i) = i + 1
   170       | num (SBranch (s, t)) = num t
   171   in num sk end
   172 
   173 fun get_types (_, T, _, _, _) = T
   174 fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
   175 
   176 fun get_chain (_, _, _, C, _) c1 c2 =
   177   Term2tab.lookup C (c1, c2)
   178 
   179 fun get_descent (_, _, _, _, D) c m1 m2 =
   180   Term3tab.lookup D (c, (m1, m2))
   181 
   182 fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
   183   let
   184     val (sk, _, _, _, _) = D
   185     val vs = Term.strip_qnt_vars "Ex" c
   186 
   187     (* FIXME: throw error "dest_call" for malformed terms *)
   188     val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   189       = Term.strip_qnt_body "Ex" c
   190     val (p, l') = dest_inj sk l
   191     val (q, r') = dest_inj sk r
   192   in
   193     (vs, p, l', q, r', Gam)
   194   end
   195   | dest_call D t = error "dest_call"
   196 
   197 
   198 fun mk_desc thy tac vs Gam l r m1 m2 =
   199   let
   200     fun try rel =
   201       try_proof (cterm_of thy
   202         (Term.list_all (vs,
   203            Logic.mk_implies (HOLogic.mk_Trueprop Gam,
   204              HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
   205                $ (m2 $ r) $ (m1 $ l)))))) tac
   206   in
   207     case try @{const_name Orderings.less} of
   208        Solved thm => Less thm
   209      | Stuck thm =>
   210        (case try @{const_name Orderings.less_eq} of
   211           Solved thm2 => LessEq (thm2, thm)
   212         | Stuck thm2 =>
   213           if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
   214           then False thm2 else None (thm2, thm)
   215         | _ => raise Match) (* FIXME *)
   216      | _ => raise Match
   217 end
   218 
   219 fun derive_descent thy tac c m1 m2 D =
   220   case get_descent D c m1 m2 of
   221     SOME _ => D
   222   | NONE => 
   223     let
   224       val (vs, _, l, _, r, Gam) = dest_call D c
   225     in 
   226       note_descent c m1 m2 (mk_desc thy tac vs Gam l r m1 m2) D
   227     end
   228 
   229 fun CALLS tac i st =
   230   if Thm.no_prems st then all_tac st
   231   else case Thm.term_of (Thm.cprem_of st i) of
   232     (_ $ (_ $ rel)) => tac (Function_Lib.dest_binop_list @{const_name Lattices.sup} rel, i) st
   233   |_ => no_tac st
   234 
   235 type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
   236 
   237 fun TERMINATION ctxt tac =
   238   SUBGOAL (fn (_ $ (Const (@{const_name wf}, wfT) $ rel), i) =>
   239   let
   240     val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
   241   in
   242     tac (create ctxt T rel) i
   243   end)
   244 
   245 
   246 (* A tactic to convert open to closed termination goals *)
   247 local
   248 fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
   249   let
   250     val (vars, prop) = Function_Lib.dest_all_all t
   251     val (prems, concl) = Logic.strip_horn prop
   252     val (lhs, rhs) = concl
   253       |> HOLogic.dest_Trueprop
   254       |> HOLogic.dest_mem |> fst
   255       |> HOLogic.dest_prod
   256   in
   257     (vars, prems, lhs, rhs)
   258   end
   259 
   260 fun mk_pair_compr (T, qs, l, r, conds) =
   261   let
   262     val pT = HOLogic.mk_prodT (T, T)
   263     val n = length qs
   264     val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
   265     val conds' = if null conds then [HOLogic.true_const] else conds
   266   in
   267     HOLogic.Collect_const pT $
   268     Abs ("uu_", pT,
   269       (foldr1 HOLogic.mk_conj (peq :: conds')
   270       |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
   271   end
   272 
   273 in
   274 
   275 fun wf_union_tac ctxt st =
   276   let
   277     val thy = ProofContext.theory_of ctxt
   278     val cert = cterm_of (theory_of_thm st)
   279     val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
   280 
   281     fun mk_compr ineq =
   282       let
   283         val (vars, prems, lhs, rhs) = dest_term ineq
   284       in
   285         mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
   286       end
   287 
   288     val relation =
   289       if null ineqs
   290       then Const (@{const_abbrev Set.empty}, fastype_of rel)
   291       else map mk_compr ineqs
   292         |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
   293 
   294     fun solve_membership_tac i =
   295       (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
   296       THEN' (fn j => TRY (rtac @{thm UnI1} j))
   297       THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
   298       THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
   299       THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
   300         ORELSE' ((rtac @{thm conjI})
   301           THEN' (rtac @{thm refl})
   302           THEN' (blast_tac (claset_of ctxt))))  (* Solve rest of context... not very elegant *)
   303       ) i
   304   in
   305     ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
   306      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
   307   end
   308 
   309 end
   310 
   311 
   312 (* continuation passing repeat combinator *)
   313 fun REPEAT ttac cont err_cont =
   314     ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
   315 
   316 (*** DEPENDENCY GRAPHS ***)
   317 
   318 fun prove_chain thy chain_tac c1 c2 =
   319   let
   320     val goal =
   321       HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
   322         Const (@{const_abbrev Set.empty}, fastype_of c1))
   323       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
   324   in
   325     case Function_Lib.try_proof (cterm_of thy goal) chain_tac of
   326       Function_Lib.Solved thm => SOME thm
   327     | _ => NONE
   328   end
   329 
   330 fun derive_chains ctxt chain_tac cont D = CALLS (fn (cs, i) =>
   331   let
   332     val thy = ProofContext.theory_of ctxt
   333 
   334     fun derive_chain c1 c2 D =
   335       if is_some (get_chain D c1 c2) then D else
   336       note_chain c1 c2 (prove_chain thy chain_tac c1 c2) D
   337   in
   338     cont (fold_product derive_chain cs cs D) i
   339   end)
   340 
   341 
   342 fun mk_dgraph D cs =
   343   Term_Graph.empty
   344   |> fold (fn c => Term_Graph.new_node (c, ())) cs
   345   |> fold_product (fn c1 => fn c2 =>
   346      if is_none (get_chain D c1 c2 |> the_default NONE)
   347      then Term_Graph.add_edge (c1, c2) else I)
   348      cs cs
   349 
   350 fun ucomp_empty_tac T =
   351   REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
   352     ORELSE' rtac @{thm union_comp_emptyL}
   353     ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
   354 
   355 fun regroup_calls_tac cs = CALLS (fn (cs', i) =>
   356  let
   357    val is = map (fn c => find_index (curry op aconv c) cs') cs
   358  in
   359    CONVERSION (Conv.arg_conv (Conv.arg_conv
   360      (Function_Lib.regroup_union_conv is))) i
   361  end)
   362 
   363 
   364 fun solve_trivial_tac D = CALLS (fn ([c], i) =>
   365   (case get_chain D c c of
   366      SOME (SOME thm) => rtac @{thm wf_no_loop} i
   367                         THEN rtac thm i
   368    | _ => no_tac)
   369   | _ => no_tac)
   370 
   371 fun decompose_tac' cont err_cont D = CALLS (fn (cs, i) =>
   372   let
   373     val G = mk_dgraph D cs
   374     val sccs = Term_Graph.strong_conn G
   375 
   376     fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
   377       | split (SCC::rest) i =
   378         regroup_calls_tac SCC i
   379         THEN rtac @{thm wf_union_compatible} i
   380         THEN rtac @{thm less_by_empty} (i + 2)
   381         THEN ucomp_empty_tac (the o the oo get_chain D) (i + 2)
   382         THEN split rest (i + 1)
   383         THEN (solve_trivial_tac D i ORELSE cont D i)
   384   in
   385     if length sccs > 1 then split sccs i
   386     else solve_trivial_tac D i ORELSE err_cont D i
   387   end)
   388 
   389 fun decompose_tac ctxt chain_tac cont err_cont =
   390   derive_chains ctxt chain_tac (decompose_tac' cont err_cont)
   391 
   392 
   393 (*** Local Descent Proofs ***)
   394 
   395 fun gen_descent diag ctxt tac cont D = CALLS (fn (cs, i) =>
   396   let
   397     val thy = ProofContext.theory_of ctxt
   398     val measures_of = get_measures D
   399 
   400     fun derive c D =
   401       let
   402         val (_, p, _, q, _, _) = dest_call D c
   403       in
   404         if diag andalso p = q
   405         then fold (fn m => derive_descent thy tac c m m) (measures_of p) D
   406         else fold_product (derive_descent thy tac c)
   407                (measures_of p) (measures_of q) D
   408       end
   409   in
   410     cont (Function_Common.PROFILE "deriving descents" (fold derive cs) D) i
   411   end)
   412 
   413 fun derive_diag ctxt = gen_descent true ctxt
   414 fun derive_all ctxt = gen_descent false ctxt
   415 
   416 
   417 end