src/HOLCF/cont_proc.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17876 b9c92f384109
child 19594 a1e630503c57
permissions -rw-r--r--
setup: theory -> theory;
huffman@16386
     1
(*  Title:      HOLCF/cont_proc.ML
huffman@16386
     2
    ID:         $Id$
huffman@16386
     3
    Author:     Brian Huffman
huffman@16386
     4
*)
huffman@16386
     5
huffman@16386
     6
signature CONT_PROC =
huffman@16386
     7
sig
huffman@16386
     8
  val is_lcf_term: term -> bool
huffman@16386
     9
  val cont_thms: term -> thm list
huffman@16403
    10
  val all_cont_thms: term -> thm list
huffman@16629
    11
  val cont_tac: int -> tactic
huffman@16386
    12
  val cont_proc: theory -> simproc
wenzelm@18708
    13
  val setup: theory -> theory
huffman@16386
    14
end;
huffman@16386
    15
huffman@16386
    16
structure ContProc: CONT_PROC =
huffman@16386
    17
struct
huffman@16386
    18
huffman@16386
    19
(** theory context references **)
huffman@16386
    20
huffman@16386
    21
val cont_K = thm "cont_const";
huffman@16386
    22
val cont_I = thm "cont_id";
huffman@16386
    23
val cont_A = thm "cont2cont_Rep_CFun";
huffman@16386
    24
val cont_L = thm "cont2cont_LAM";
huffman@16386
    25
val cont_R = thm "cont_Rep_CFun2";
huffman@16386
    26
huffman@16386
    27
(* checks whether a term is written entirely in the LCF sublanguage *)
huffman@16386
    28
fun is_lcf_term (Const("Cfun.Rep_CFun",_) $ t $ u) = is_lcf_term t andalso is_lcf_term u
huffman@16386
    29
  | is_lcf_term (Const("Cfun.Abs_CFun",_) $ Abs (_,_,t)) = is_lcf_term t
huffman@16386
    30
  | is_lcf_term (_ $ _) = false
huffman@16386
    31
  | is_lcf_term (Abs _) = false
huffman@16386
    32
  | is_lcf_term _ = true; (* Const, Free, Var, and Bound are OK *)
huffman@16386
    33
huffman@16386
    34
(*
huffman@16386
    35
  efficiently generates a cont thm for every LAM abstraction in a term,
huffman@16386
    36
  using forward proof and reusing common subgoals
huffman@16386
    37
*)
huffman@16386
    38
local
huffman@16386
    39
  fun var 0 = [SOME cont_I]
huffman@16386
    40
    | var n = NONE :: var (n-1);
huffman@16386
    41
huffman@16386
    42
  fun k NONE     = cont_K
huffman@16386
    43
    | k (SOME x) = x;
huffman@16386
    44
huffman@16386
    45
  fun ap NONE NONE = NONE
huffman@16386
    46
    | ap x    y    = SOME (k y RS (k x RS cont_A));
huffman@16386
    47
huffman@16386
    48
  fun zip []      []      = []
huffman@16386
    49
    | zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
huffman@16386
    50
    | zip (x::xs) []      = (ap x    NONE) :: zip xs []
huffman@16386
    51
    | zip (x::xs) (y::ys) = (ap x    y   ) :: zip xs ys
huffman@16386
    52
huffman@16386
    53
  fun lam [] = ([], cont_K)
huffman@16386
    54
    | lam (x::ys) = let
huffman@16386
    55
        (* should use "standard" for thms that are used multiple times *)
huffman@16386
    56
        (* it seems to allow for sharing in explicit proof objects *)
huffman@16386
    57
        val x' = standard (k x);
huffman@16386
    58
        val Lx = x' RS cont_L;
huffman@16386
    59
        in (map (fn y => SOME (k y RS Lx)) ys, x') end;
huffman@16386
    60
huffman@16386
    61
  (* first list: cont thm for each dangling bound variable *)
huffman@16403
    62
  (* second list: cont thm for each LAM in t *)
huffman@16403
    63
  (* if b = false, only return cont thm for outermost LAMs *)
huffman@16403
    64
  fun cont_thms1 b (Const _ $ f $ t) = let
huffman@16403
    65
        val (cs1,ls1) = cont_thms1 b f;
huffman@16403
    66
        val (cs2,ls2) = cont_thms1 b t;
huffman@16403
    67
        in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
huffman@16403
    68
    | cont_thms1 b (Const _ $ Abs (_,_,t)) = let
huffman@16403
    69
        val (cs,ls) = cont_thms1 b t;
huffman@16386
    70
        val (cs',l) = lam cs;
huffman@16386
    71
        in (cs',l::ls) end
huffman@16403
    72
    | cont_thms1 _ (Bound n) = (var n, [])
huffman@16403
    73
    | cont_thms1 _ _ = ([],[]);
huffman@16386
    74
in
huffman@16386
    75
  (* precondition: is_lcf_term t = true *)
huffman@16403
    76
  fun cont_thms t = snd (cont_thms1 false t);
huffman@16403
    77
  fun all_cont_thms t = snd (cont_thms1 true t);
huffman@16386
    78
end;
huffman@16386
    79
huffman@16386
    80
(*
huffman@16386
    81
  Given the term "cont f", the procedure tries to construct the
huffman@16386
    82
  theorem "cont f == True". If this theorem cannot be completely
huffman@16386
    83
  solved by the introduction rules, then the procedure returns a
huffman@16386
    84
  conditional rewrite rule with the unsolved subgoals as premises.
huffman@16386
    85
*)
huffman@16386
    86
huffman@16386
    87
local
huffman@16629
    88
  val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
huffman@16629
    89
  
huffman@16629
    90
  fun cont_tac_of_term (Const("Cont.cont",_) $ f) =
huffman@16386
    91
    let
huffman@16386
    92
      val f' = Const("Cfun.Abs_CFun",dummyT) $ f;
huffman@16629
    93
    in
huffman@16629
    94
      if is_lcf_term f'
huffman@16629
    95
        then rtac (hd (cont_thms f'))
huffman@16629
    96
        else REPEAT_ALL_NEW (resolve_tac rules)
huffman@16629
    97
    end
huffman@16629
    98
    | cont_tac_of_term _ = K no_tac;
huffman@16386
    99
in
huffman@16629
   100
  val cont_tac = SUBGOAL (fn (t,i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
huffman@16629
   101
end;
huffman@16629
   102
huffman@16629
   103
local
huffman@16629
   104
  fun solve_cont thy _ t =
huffman@16629
   105
    let
huffman@16629
   106
      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
huffman@16629
   107
    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
huffman@16629
   108
in
huffman@16629
   109
  fun cont_proc thy = Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
huffman@16386
   110
end;
huffman@16386
   111
huffman@16386
   112
val setup =
wenzelm@18708
   113
  (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [cont_proc thy]); thy));
huffman@16386
   114
huffman@16386
   115
end;