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