src/HOL/SizeChange/sct.ML
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 30450 7655e6533209
child 30607 c3d1590debd8
permissions -rw-r--r--
simplified method setup;
     1 (*  Title:      HOL/SizeChange/sct.ML
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 
     5 Tactics for size change termination.
     6 *)
     7 signature SCT =
     8 sig
     9   val abs_rel_tac : tactic
    10   val mk_call_graph : Proof.context -> tactic
    11 end
    12 
    13 structure Sct : SCT =
    14 struct
    15 
    16 fun matrix [] ys = []
    17   | matrix (x::xs) ys = map (pair x) ys :: matrix xs ys
    18 
    19 fun map_matrix f xss = map (map f) xss
    20 
    21 val scgT = @{typ "nat scg"}
    22 val acgT = @{typ "nat acg"}
    23 
    24 fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT))
    25 fun graphT nT eT = Type ("Graphs.graph", [nT, eT])
    26 
    27 fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT)
    28 
    29 val stepP_const = "Interpretation.stepP"
    30 val stepP_def = thm "Interpretation.stepP.simps"
    31 
    32 fun mk_stepP RD1 RD2 M1 M2 Rel =
    33     let val RDT = fastype_of RD1
    34       val MT = fastype_of M1
    35     in
    36       Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT)
    37             $ RD1 $ RD2 $ M1 $ M2 $ Rel
    38     end
    39 
    40 val no_stepI = thm "Interpretation.no_stepI"
    41 
    42 val approx_const = "Interpretation.approx"
    43 val approx_empty = thm "Interpretation.approx_empty"
    44 val approx_less = thm "Interpretation.approx_less"
    45 val approx_leq = thm "Interpretation.approx_leq"
    46 
    47 fun mk_approx G RD1 RD2 Ms1 Ms2 =
    48     let val RDT = fastype_of RD1
    49       val MsT = fastype_of Ms1
    50     in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end
    51 
    52 val sound_int_const = "Interpretation.sound_int"
    53 val sound_int_def = thm "Interpretation.sound_int_def"
    54 fun mk_sound_int A RDs M =
    55     let val RDsT = fastype_of RDs
    56       val MT = fastype_of M
    57     in Const (sound_int_const, acgT --> RDsT --> MT --> HOLogic.boolT) $ A $ RDs $ M end
    58 
    59 
    60 val nth_const = "List.nth"
    61 fun mk_nth xs =
    62     let val lT as Type (_, [T]) = fastype_of xs
    63     in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
    64 
    65 
    66 val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
    67 
    68 val all_less_zero = thm "Interpretation.all_less_zero"
    69 val all_less_Suc = thm "Interpretation.all_less_Suc"
    70 
    71 (* --> Library? *)
    72 fun del_index n [] = []
    73   | del_index n (x :: xs) =
    74     if n>0 then x :: del_index (n - 1) xs else xs
    75 
    76 (* Lists as finite multisets *)
    77 
    78 fun remove1 eq x [] = []
    79   | remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys
    80 
    81 fun multi_union eq [] ys = ys
    82   | multi_union eq (x::xs) ys = x :: multi_union eq xs (remove1 eq x ys)
    83 
    84 fun dest_ex (Const ("Ex", _) $ Abs (a as (_,T,_))) =
    85     let
    86       val (n, body) = Term.dest_abs a
    87     in
    88       (Free (n, T), body)
    89     end
    90   | dest_ex _ = raise Match
    91 
    92 fun dest_all_ex (t as (Const ("Ex",_) $ _)) =
    93     let
    94       val (v,b) = dest_ex t
    95       val (vs, b') = dest_all_ex b
    96     in
    97       (v :: vs, b')
    98     end
    99   | dest_all_ex t = ([],t)
   100 
   101 fun dist_vars [] vs = (null vs orelse error "dist_vars"; [])
   102   | dist_vars (T::Ts) vs =
   103     case find_index (fn v => fastype_of v = T) vs of
   104       ~1 => Free ("", T) :: dist_vars Ts vs
   105     |  i => (nth vs i) :: dist_vars Ts (del_index i vs)
   106 
   107 fun dest_case rebind t =
   108     let
   109       val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t
   110       val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs
   111     in
   112       foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match]
   113     end
   114 
   115 fun bind_many [] = I
   116   | bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs)
   117 
   118 (* Builds relation descriptions from a relation definition *)
   119 fun mk_reldescs (Abs a) =
   120     let
   121       val (_, Abs a') = Term.dest_abs a
   122       val (_, b) = Term.dest_abs a'
   123       val cases = HOLogic.dest_disj b
   124       val (vss, bs) = split_list (map dest_all_ex cases)
   125       val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) []
   126       val rebind = map (bind_many o dist_vars unionTs) vss
   127 
   128       val RDs = map2 dest_case rebind bs
   129     in
   130       HOLogic.mk_list (fastype_of (hd RDs)) RDs
   131     end
   132 
   133 fun abs_rel_tac (st : thm) =
   134     let
   135       val thy = theory_of_thm st
   136       val (def, rd) = HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (prems_of st)))
   137       val RDs = cterm_of thy (mk_reldescs def)
   138       val rdvar = Var (the_single (Term.add_vars rd [])) |> cterm_of thy
   139     in
   140       Seq.single (cterm_instantiate [(rdvar, RDs)] st)
   141     end
   142 
   143 
   144 
   145 
   146 
   147 
   148 (* very primitive *)
   149 fun measures_of ctxt RD =
   150     let
   151       val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD)))))
   152       val measures = MeasureFunctions.get_measure_functions ctxt domT
   153     in
   154       measures
   155     end
   156 
   157 val mk_number = HOLogic.mk_nat
   158 val dest_number = HOLogic.dest_nat
   159 
   160 fun nums_to i = map mk_number (0 upto (i - 1))
   161 
   162 val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"]
   163 val nth_ss = (HOL_basic_ss addsimps nth_simps)
   164 val simp_nth_tac = simp_tac nth_ss
   165 
   166 
   167 fun tabulate_tlist thy l =
   168     let
   169       val n = length (HOLogic.dest_list l)
   170       val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1))
   171     in
   172       the o Inttab.lookup table
   173     end
   174 
   175 val get_elem = snd o Logic.dest_equals o prop_of
   176 
   177 fun inst_nums thy i j (t:thm) =
   178   instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t
   179 
   180 datatype call_fact =
   181    NoStep of thm
   182  | Graph of (term * thm)
   183 
   184 fun rand (_ $ t) = t
   185 
   186 fun setup_probe_goal thy domT Dtab Mtab (i, j) =
   187     let
   188       val RD1 = get_elem (Dtab i)
   189       val RD2 = get_elem (Dtab j)
   190       val Ms1 = get_elem (Mtab i)
   191       val Ms2 = get_elem (Mtab j)
   192 
   193       val Mst1 = HOLogic.dest_list (rand Ms1)
   194       val Mst2 = HOLogic.dest_list (rand Ms2)
   195 
   196       val mvar1 = Free ("sctmfv1", domT --> HOLogic.natT)
   197       val mvar2 = Free ("sctmfv2", domT --> HOLogic.natT)
   198       val relvar = Free ("sctmfrel", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
   199       val N = length Mst1 and M = length Mst2
   200       val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar)
   201                          |> cterm_of thy
   202                          |> Goal.init
   203                          |> CLASIMPSET auto_tac |> Seq.hd
   204 
   205       val no_step = saved_state
   206                       |> forall_intr (cterm_of thy relvar)
   207                       |> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const))))
   208                       |> CLASIMPSET auto_tac |> Seq.hd
   209 
   210     in
   211       if Thm.no_prems no_step
   212       then NoStep (Goal.finish no_step RS no_stepI)
   213       else
   214         let
   215           fun set_m1 i =
   216               let
   217                 val M1 = nth Mst1 i
   218                 val with_m1 = saved_state
   219                                 |> forall_intr (cterm_of thy mvar1)
   220                                 |> forall_elim (cterm_of thy M1)
   221                                 |> CLASIMPSET auto_tac |> Seq.hd
   222 
   223                 fun set_m2 j =
   224                     let
   225                       val M2 = nth Mst2 j
   226                       val with_m2 = with_m1
   227                                       |> forall_intr (cterm_of thy mvar2)
   228                                       |> forall_elim (cterm_of thy M2)
   229                                       |> CLASIMPSET auto_tac |> Seq.hd
   230 
   231                       val decr = forall_intr (cterm_of thy relvar)
   232                                    #> forall_elim (cterm_of thy @{const HOL.less(nat)})
   233                                    #> CLASIMPSET auto_tac #> Seq.hd
   234 
   235                       val decreq = forall_intr (cterm_of thy relvar)
   236                                      #> forall_elim (cterm_of thy @{const HOL.less_eq(nat)})
   237                                      #> CLASIMPSET auto_tac #> Seq.hd
   238 
   239                       val thm1 = decr with_m2
   240                     in
   241                       if Thm.no_prems thm1
   242                       then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1))
   243                       else let val thm2 = decreq with_m2 in
   244                              if Thm.no_prems thm2
   245                              then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1))
   246                              else all_tac end
   247                     end
   248               in set_m2 end
   249 
   250           val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2)
   251 
   252           val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1)))
   253                       THEN (rtac approx_empty 1)
   254 
   255           val approx_thm = goal
   256                     |> cterm_of thy
   257                     |> Goal.init
   258                     |> tac |> Seq.hd
   259                     |> Goal.finish
   260 
   261           val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm
   262         in
   263           Graph (G, approx_thm)
   264         end
   265     end
   266 
   267 fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n))
   268 
   269 val in_graph_tac =
   270     simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
   271     THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *)
   272 
   273 fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
   274   | approx_tac (Graph (G, thm)) =
   275     rtac disjI2 1
   276     THEN rtac exI 1
   277     THEN rtac conjI 1
   278     THEN rtac thm 2
   279     THEN in_graph_tac
   280 
   281 fun all_less_tac [] = rtac all_less_zero 1
   282   | all_less_tac (t :: ts) = rtac all_less_Suc 1
   283                                   THEN simp_nth_tac 1
   284                                   THEN t
   285                                   THEN all_less_tac ts
   286 
   287 
   288 fun mk_length l = HOLogic.size_const (fastype_of l) $ l;
   289 val length_simps = thms "Interpretation.length_simps"
   290 
   291 
   292 
   293 fun mk_call_graph ctxt (st : thm) =
   294     let
   295       val thy = theory_of_thm st
   296       val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st))
   297 
   298       val RDs = HOLogic.dest_list RDlist
   299       val n = length RDs
   300 
   301       val Mss = map (measures_of ctxt) RDs
   302 
   303       val domT = domain_type (fastype_of (hd (hd Mss)))
   304 
   305       val mfuns = map (fn Ms => mk_nth (HOLogic.mk_list (fastype_of (hd Ms)) Ms)) Mss
   306                       |> (fn l => HOLogic.mk_list (fastype_of (hd l)) l)
   307 
   308       val Dtab = tabulate_tlist thy RDlist
   309       val Mtab = tabulate_tlist thy mfuns
   310 
   311       val len_simp = Simplifier.rewrite (HOL_basic_ss addsimps length_simps) (cterm_of thy (mk_length RDlist))
   312 
   313       val mlens = map length Mss
   314 
   315       val indices = (n - 1 downto 0)
   316       val pairs = matrix indices indices
   317       val parts = map_matrix (fn (n,m) =>
   318                                  (timeap_msg (string_of_int n ^ "," ^ string_of_int m)
   319                                              (setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs
   320 
   321 
   322       val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^
   323                                                                             Syntax.string_of_term ctxt G ^ ",\n")
   324                                                      | _ => I) cs) parts ""
   325       val _ = warning s
   326 
   327 
   328       val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs)
   329                     |> HOLogic.mk_set (edgeT HOLogic.natT scgT)
   330                     |> curry op $ (graph_const HOLogic.natT scgT)
   331 
   332 
   333       val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
   334 
   335       val tac =
   336           (SIMPSET (unfold_tac [sound_int_def, len_simp]))
   337             THEN all_less_tac (map (all_less_tac o map approx_tac) parts)
   338     in
   339       tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
   340     end
   341 
   342 
   343 end
   344 
   345 
   346 
   347 
   348 
   349 
   350