src/HOL/HOLCF/Tools/cont_proc.ML
author huffman
Tue Nov 30 14:21:57 2010 -0800 (2010-11-30)
changeset 40832 4352ca878c41
parent 40774 0437dbc127b3
child 41296 6aaf80ea9715
permissions -rw-r--r--
remove gratuitous semicolons from ML code
wenzelm@23152
     1
(*  Title:      HOLCF/Tools/cont_proc.ML
wenzelm@23152
     2
    Author:     Brian Huffman
wenzelm@23152
     3
*)
wenzelm@23152
     4
wenzelm@23152
     5
signature CONT_PROC =
wenzelm@23152
     6
sig
wenzelm@23152
     7
  val is_lcf_term: term -> bool
wenzelm@23152
     8
  val cont_thms: term -> thm list
wenzelm@23152
     9
  val all_cont_thms: term -> thm list
huffman@29662
    10
  val cont_tac: int -> tactic
wenzelm@23152
    11
  val cont_proc: theory -> simproc
wenzelm@23152
    12
  val setup: theory -> theory
huffman@40832
    13
end
wenzelm@23152
    14
huffman@31023
    15
structure ContProc :> CONT_PROC =
wenzelm@23152
    16
struct
wenzelm@23152
    17
wenzelm@23152
    18
(** theory context references **)
wenzelm@23152
    19
huffman@40832
    20
val cont_K = @{thm cont_const}
huffman@40832
    21
val cont_I = @{thm cont_id}
huffman@40832
    22
val cont_A = @{thm cont2cont_APP}
huffman@40832
    23
val cont_L = @{thm cont2cont_LAM}
huffman@40832
    24
val cont_R = @{thm cont_Rep_cfun2}
wenzelm@23152
    25
wenzelm@23152
    26
(* checks whether a term contains no dangling bound variables *)
huffman@40832
    27
fun is_closed_term t = not (Term.loose_bvar (t, 0))
wenzelm@23152
    28
wenzelm@23152
    29
(* checks whether a term is written entirely in the LCF sublanguage *)
huffman@40327
    30
fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
wenzelm@23152
    31
      is_lcf_term t andalso is_lcf_term u
huffman@40327
    32
  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
huffman@29047
    33
      is_lcf_term t
huffman@40327
    34
  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
huffman@29373
    35
      is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
wenzelm@23152
    36
  | is_lcf_term (Bound _) = true
huffman@40832
    37
  | is_lcf_term t = is_closed_term t
wenzelm@23152
    38
wenzelm@23152
    39
(*
wenzelm@23152
    40
  efficiently generates a cont thm for every LAM abstraction in a term,
wenzelm@23152
    41
  using forward proof and reusing common subgoals
wenzelm@23152
    42
*)
wenzelm@23152
    43
local
wenzelm@23152
    44
  fun var 0 = [SOME cont_I]
huffman@40832
    45
    | var n = NONE :: var (n-1)
wenzelm@23152
    46
wenzelm@23152
    47
  fun k NONE     = cont_K
huffman@40832
    48
    | k (SOME x) = x
wenzelm@23152
    49
wenzelm@23152
    50
  fun ap NONE NONE = NONE
huffman@40832
    51
    | ap x    y    = SOME (k y RS (k x RS cont_A))
wenzelm@23152
    52
wenzelm@23152
    53
  fun zip []      []      = []
wenzelm@23152
    54
    | zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
wenzelm@23152
    55
    | zip (x::xs) []      = (ap x    NONE) :: zip xs []
wenzelm@23152
    56
    | zip (x::xs) (y::ys) = (ap x    y   ) :: zip xs ys
wenzelm@23152
    57
wenzelm@23152
    58
  fun lam [] = ([], cont_K)
wenzelm@23152
    59
    | lam (x::ys) =
wenzelm@23152
    60
    let
huffman@29371
    61
      (* should use "close_derivation" for thms that are used multiple times *)
wenzelm@23152
    62
      (* it seems to allow for sharing in explicit proof objects *)
huffman@40832
    63
      val x' = Thm.close_derivation (k x)
huffman@40832
    64
      val Lx = x' RS cont_L
huffman@40832
    65
    in (map (fn y => SOME (k y RS Lx)) ys, x') end
wenzelm@23152
    66
wenzelm@23152
    67
  (* first list: cont thm for each dangling bound variable *)
wenzelm@23152
    68
  (* second list: cont thm for each LAM in t *)
wenzelm@23152
    69
  (* if b = false, only return cont thm for outermost LAMs *)
huffman@40327
    70
  fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) =
wenzelm@23152
    71
    let
huffman@40832
    72
      val (cs1,ls1) = cont_thms1 b f
huffman@40832
    73
      val (cs2,ls2) = cont_thms1 b t
wenzelm@23152
    74
    in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
huffman@40327
    75
    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
wenzelm@23152
    76
    let
huffman@40832
    77
      val (cs, ls) = cont_thms1 b t
huffman@40832
    78
      val (cs', l) = lam cs
wenzelm@23152
    79
    in (cs', l::ls) end
huffman@40327
    80
    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) =
huffman@29373
    81
    let
huffman@40832
    82
      val t' = Term.incr_boundvars 1 t $ Bound 0
huffman@40832
    83
      val (cs, ls) = cont_thms1 b t'
huffman@40832
    84
      val (cs', l) = lam cs
huffman@29373
    85
    in (cs', l::ls) end
wenzelm@23152
    86
    | cont_thms1 _ (Bound n) = (var n, [])
huffman@40832
    87
    | cont_thms1 _ _ = ([], [])
wenzelm@23152
    88
in
wenzelm@23152
    89
  (* precondition: is_lcf_term t = true *)
huffman@40832
    90
  fun cont_thms t = snd (cont_thms1 false t)
huffman@40832
    91
  fun all_cont_thms t = snd (cont_thms1 true t)
huffman@40832
    92
end
wenzelm@23152
    93
wenzelm@23152
    94
(*
wenzelm@23152
    95
  Given the term "cont f", the procedure tries to construct the
wenzelm@23152
    96
  theorem "cont f == True". If this theorem cannot be completely
wenzelm@23152
    97
  solved by the introduction rules, then the procedure returns a
wenzelm@23152
    98
  conditional rewrite rule with the unsolved subgoals as premises.
wenzelm@23152
    99
*)
wenzelm@23152
   100
huffman@29662
   101
val cont_tac =
huffman@29048
   102
  let
huffman@40832
   103
    val rules = [cont_K, cont_I, cont_R, cont_A, cont_L]
wenzelm@23152
   104
  
huffman@29662
   105
    fun new_cont_tac f' i =
huffman@29048
   106
      case all_cont_thms f' of
huffman@29662
   107
        [] => no_tac
huffman@40832
   108
      | (c::cs) => rtac c i
wenzelm@23152
   109
huffman@29048
   110
    fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
huffman@29048
   111
      let
huffman@40832
   112
        val f' = Const (@{const_name Abs_cfun}, dummyT) $ f
huffman@29048
   113
      in
huffman@29048
   114
        if is_lcf_term f'
huffman@29662
   115
        then new_cont_tac f'
huffman@29048
   116
        else REPEAT_ALL_NEW (resolve_tac rules)
huffman@29048
   117
      end
huffman@40832
   118
      | cont_tac_of_term _ = K no_tac
huffman@29048
   119
  in
huffman@29048
   120
    SUBGOAL (fn (t, i) =>
huffman@29048
   121
      cont_tac_of_term (HOLogic.dest_Trueprop t) i)
huffman@40832
   122
  end
wenzelm@23152
   123
wenzelm@23152
   124
local
wenzelm@23152
   125
  fun solve_cont thy _ t =
wenzelm@23152
   126
    let
huffman@40832
   127
      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI
huffman@29662
   128
    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
wenzelm@23152
   129
in
wenzelm@23152
   130
  fun cont_proc thy =
huffman@40832
   131
    Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont
huffman@40832
   132
end
wenzelm@23152
   133
huffman@40832
   134
fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy
wenzelm@23152
   135
huffman@40832
   136
end