src/HOLCF/Tools/cont_proc.ML
author paulson
Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854 0ebcd575d3c6
parent 24043 9b156986a4e9
child 26496 49ae9456eba9
permissions -rw-r--r--
filtering out some package theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOLCF/Tools/cont_proc.ML
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     3
    Author:     Brian Huffman
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     5
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
signature CONT_PROC =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
sig
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     8
  val is_lcf_term: term -> bool
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     9
  val cont_thms: term -> thm list
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    10
  val all_cont_thms: term -> thm list
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    11
  val cont_tac: int -> tactic
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    12
  val cont_proc: theory -> simproc
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    13
  val setup: theory -> theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    14
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    15
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    16
structure ContProc: CONT_PROC =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    17
struct
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    18
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    19
(** theory context references **)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    20
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    21
val cont_K = thm "cont_const";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    22
val cont_I = thm "cont_id";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    23
val cont_A = thm "cont2cont_Rep_CFun";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    24
val cont_L = thm "cont2cont_LAM";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    25
val cont_R = thm "cont_Rep_CFun2";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    26
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    27
(* checks whether a term contains no dangling bound variables *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    28
val is_closed_term =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    29
  let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    30
    fun bound_less i (t $ u) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    31
          bound_less i t andalso bound_less i u
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    32
      | bound_less i (Abs (_, _, t)) = bound_less (i+1) t
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    33
      | bound_less i (Bound n) = n < i
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    34
      | bound_less i _ = true; (* Const, Free, and Var are OK *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    35
  in bound_less 0 end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    36
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    37
(* checks whether a term is written entirely in the LCF sublanguage *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    38
fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    39
      is_lcf_term t andalso is_lcf_term u
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
  | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    41
  | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    42
  | is_lcf_term (Bound _) = true
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
  | is_lcf_term t = is_closed_term t;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    44
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    45
(*
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    46
  efficiently generates a cont thm for every LAM abstraction in a term,
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    47
  using forward proof and reusing common subgoals
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    48
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    49
local
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    50
  fun var 0 = [SOME cont_I]
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    51
    | var n = NONE :: var (n-1);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    52
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    53
  fun k NONE     = cont_K
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    54
    | k (SOME x) = x;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    55
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    56
  fun ap NONE NONE = NONE
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    57
    | ap x    y    = SOME (k y RS (k x RS cont_A));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    58
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    59
  fun zip []      []      = []
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    60
    | zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    61
    | zip (x::xs) []      = (ap x    NONE) :: zip xs []
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    62
    | zip (x::xs) (y::ys) = (ap x    y   ) :: zip xs ys
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    63
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    64
  fun lam [] = ([], cont_K)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    65
    | lam (x::ys) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    66
    let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    67
      (* should use "standard" for thms that are used multiple times *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    68
      (* it seems to allow for sharing in explicit proof objects *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    69
      val x' = standard (k x);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    70
      val Lx = x' RS cont_L;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    71
    in (map (fn y => SOME (k y RS Lx)) ys, x') end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    72
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    73
  (* first list: cont thm for each dangling bound variable *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    74
  (* second list: cont thm for each LAM in t *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    75
  (* if b = false, only return cont thm for outermost LAMs *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    76
  fun cont_thms1 b (Const ("Cfun.Rep_CFun", _) $ f $ t) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    77
    let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    78
      val (cs1,ls1) = cont_thms1 b f;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    79
      val (cs2,ls2) = cont_thms1 b t;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    80
    in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    81
    | cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    82
    let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    83
      val (cs, ls) = cont_thms1 b t;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    84
      val (cs', l) = lam cs;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    85
    in (cs', l::ls) end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    86
    | cont_thms1 _ (Bound n) = (var n, [])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    87
    | cont_thms1 _ _ = ([], []);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    88
in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    89
  (* precondition: is_lcf_term t = true *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    90
  fun cont_thms t = snd (cont_thms1 false t);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    91
  fun all_cont_thms t = snd (cont_thms1 true t);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    92
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    93
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    94
(*
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    95
  Given the term "cont f", the procedure tries to construct the
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    96
  theorem "cont f == True". If this theorem cannot be completely
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    97
  solved by the introduction rules, then the procedure returns a
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    98
  conditional rewrite rule with the unsolved subgoals as premises.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    99
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   100
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   101
local
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   102
  val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   103
  
24043
9b156986a4e9 marked some CRITICAL sections;
wenzelm
parents: 23152
diff changeset
   104
  (* FIXME proper cache as theory data!? *)
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   105
  val prev_cont_thms : thm list ref = ref [];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   106
24043
9b156986a4e9 marked some CRITICAL sections;
wenzelm
parents: 23152
diff changeset
   107
  fun old_cont_tac i thm = CRITICAL (fn () =>
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   108
    case !prev_cont_thms of
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   109
      [] => no_tac thm
24043
9b156986a4e9 marked some CRITICAL sections;
wenzelm
parents: 23152
diff changeset
   110
    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   111
24043
9b156986a4e9 marked some CRITICAL sections;
wenzelm
parents: 23152
diff changeset
   112
  fun new_cont_tac f' i thm = CRITICAL (fn () =>
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   113
    case all_cont_thms f' of
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   114
      [] => no_tac thm
24043
9b156986a4e9 marked some CRITICAL sections;
wenzelm
parents: 23152
diff changeset
   115
    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   116
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   117
  fun cont_tac_of_term (Const ("Cont.cont", _) $ f) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   118
    let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   119
      val f' = Const ("Cfun.Abs_CFun", dummyT) $ f;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   120
    in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   121
      if is_lcf_term f'
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   122
      then old_cont_tac ORELSE' new_cont_tac f'
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   123
      else REPEAT_ALL_NEW (resolve_tac rules)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   124
    end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   125
    | cont_tac_of_term _ = K no_tac;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   126
in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   127
  val cont_tac =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   128
    SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   129
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   130
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   131
local
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   132
  fun solve_cont thy _ t =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   133
    let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   134
      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   135
    in Option.map fst (Seq.pull (cont_tac 1 tr)) end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   136
in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   137
  fun cont_proc thy =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   138
    Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   139
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   140
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   141
val setup =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   142
  (fn thy =>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   143
    (Simplifier.change_simpset_of thy
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   144
      (fn ss => ss addsimprocs [cont_proc thy]); thy));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   145
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   146
end;