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