src/HOL/HOLCF/Tools/cont_proc.ML
changeset 40832 4352ca878c41
parent 40774 0437dbc127b3
child 41296 6aaf80ea9715
     1.1 --- a/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Nov 30 14:01:49 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML	Tue Nov 30 14:21:57 2010 -0800
     1.3 @@ -10,21 +10,21 @@
     1.4    val cont_tac: int -> tactic
     1.5    val cont_proc: theory -> simproc
     1.6    val setup: theory -> theory
     1.7 -end;
     1.8 +end
     1.9  
    1.10  structure ContProc :> CONT_PROC =
    1.11  struct
    1.12  
    1.13  (** theory context references **)
    1.14  
    1.15 -val cont_K = @{thm cont_const};
    1.16 -val cont_I = @{thm cont_id};
    1.17 -val cont_A = @{thm cont2cont_APP};
    1.18 -val cont_L = @{thm cont2cont_LAM};
    1.19 -val cont_R = @{thm cont_Rep_cfun2};
    1.20 +val cont_K = @{thm cont_const}
    1.21 +val cont_I = @{thm cont_id}
    1.22 +val cont_A = @{thm cont2cont_APP}
    1.23 +val cont_L = @{thm cont2cont_LAM}
    1.24 +val cont_R = @{thm cont_Rep_cfun2}
    1.25  
    1.26  (* checks whether a term contains no dangling bound variables *)
    1.27 -fun is_closed_term t = not (Term.loose_bvar (t, 0));
    1.28 +fun is_closed_term t = not (Term.loose_bvar (t, 0))
    1.29  
    1.30  (* checks whether a term is written entirely in the LCF sublanguage *)
    1.31  fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
    1.32 @@ -34,7 +34,7 @@
    1.33    | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
    1.34        is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
    1.35    | is_lcf_term (Bound _) = true
    1.36 -  | is_lcf_term t = is_closed_term t;
    1.37 +  | is_lcf_term t = is_closed_term t
    1.38  
    1.39  (*
    1.40    efficiently generates a cont thm for every LAM abstraction in a term,
    1.41 @@ -42,13 +42,13 @@
    1.42  *)
    1.43  local
    1.44    fun var 0 = [SOME cont_I]
    1.45 -    | var n = NONE :: var (n-1);
    1.46 +    | var n = NONE :: var (n-1)
    1.47  
    1.48    fun k NONE     = cont_K
    1.49 -    | k (SOME x) = x;
    1.50 +    | k (SOME x) = x
    1.51  
    1.52    fun ap NONE NONE = NONE
    1.53 -    | ap x    y    = SOME (k y RS (k x RS cont_A));
    1.54 +    | ap x    y    = SOME (k y RS (k x RS cont_A))
    1.55  
    1.56    fun zip []      []      = []
    1.57      | zip []      (y::ys) = (ap NONE y   ) :: zip [] ys
    1.58 @@ -60,36 +60,36 @@
    1.59      let
    1.60        (* should use "close_derivation" for thms that are used multiple times *)
    1.61        (* it seems to allow for sharing in explicit proof objects *)
    1.62 -      val x' = Thm.close_derivation (k x);
    1.63 -      val Lx = x' RS cont_L;
    1.64 -    in (map (fn y => SOME (k y RS Lx)) ys, x') end;
    1.65 +      val x' = Thm.close_derivation (k x)
    1.66 +      val Lx = x' RS cont_L
    1.67 +    in (map (fn y => SOME (k y RS Lx)) ys, x') end
    1.68  
    1.69    (* first list: cont thm for each dangling bound variable *)
    1.70    (* second list: cont thm for each LAM in t *)
    1.71    (* if b = false, only return cont thm for outermost LAMs *)
    1.72    fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) =
    1.73      let
    1.74 -      val (cs1,ls1) = cont_thms1 b f;
    1.75 -      val (cs2,ls2) = cont_thms1 b t;
    1.76 +      val (cs1,ls1) = cont_thms1 b f
    1.77 +      val (cs2,ls2) = cont_thms1 b t
    1.78      in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
    1.79      | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
    1.80      let
    1.81 -      val (cs, ls) = cont_thms1 b t;
    1.82 -      val (cs', l) = lam cs;
    1.83 +      val (cs, ls) = cont_thms1 b t
    1.84 +      val (cs', l) = lam cs
    1.85      in (cs', l::ls) end
    1.86      | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) =
    1.87      let
    1.88 -      val t' = Term.incr_boundvars 1 t $ Bound 0;
    1.89 -      val (cs, ls) = cont_thms1 b t';
    1.90 -      val (cs', l) = lam cs;
    1.91 +      val t' = Term.incr_boundvars 1 t $ Bound 0
    1.92 +      val (cs, ls) = cont_thms1 b t'
    1.93 +      val (cs', l) = lam cs
    1.94      in (cs', l::ls) end
    1.95      | cont_thms1 _ (Bound n) = (var n, [])
    1.96 -    | cont_thms1 _ _ = ([], []);
    1.97 +    | cont_thms1 _ _ = ([], [])
    1.98  in
    1.99    (* precondition: is_lcf_term t = true *)
   1.100 -  fun cont_thms t = snd (cont_thms1 false t);
   1.101 -  fun all_cont_thms t = snd (cont_thms1 true t);
   1.102 -end;
   1.103 +  fun cont_thms t = snd (cont_thms1 false t)
   1.104 +  fun all_cont_thms t = snd (cont_thms1 true t)
   1.105 +end
   1.106  
   1.107  (*
   1.108    Given the term "cont f", the procedure tries to construct the
   1.109 @@ -100,37 +100,37 @@
   1.110  
   1.111  val cont_tac =
   1.112    let
   1.113 -    val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
   1.114 +    val rules = [cont_K, cont_I, cont_R, cont_A, cont_L]
   1.115    
   1.116      fun new_cont_tac f' i =
   1.117        case all_cont_thms f' of
   1.118          [] => no_tac
   1.119 -      | (c::cs) => rtac c i;
   1.120 +      | (c::cs) => rtac c i
   1.121  
   1.122      fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
   1.123        let
   1.124 -        val f' = Const (@{const_name Abs_cfun}, dummyT) $ f;
   1.125 +        val f' = Const (@{const_name Abs_cfun}, dummyT) $ f
   1.126        in
   1.127          if is_lcf_term f'
   1.128          then new_cont_tac f'
   1.129          else REPEAT_ALL_NEW (resolve_tac rules)
   1.130        end
   1.131 -      | cont_tac_of_term _ = K no_tac;
   1.132 +      | cont_tac_of_term _ = K no_tac
   1.133    in
   1.134      SUBGOAL (fn (t, i) =>
   1.135        cont_tac_of_term (HOLogic.dest_Trueprop t) i)
   1.136 -  end;
   1.137 +  end
   1.138  
   1.139  local
   1.140    fun solve_cont thy _ t =
   1.141      let
   1.142 -      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI;
   1.143 +      val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI
   1.144      in Option.map fst (Seq.pull (cont_tac 1 tr)) end
   1.145  in
   1.146    fun cont_proc thy =
   1.147 -    Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont;
   1.148 -end;
   1.149 +    Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont
   1.150 +end
   1.151  
   1.152 -fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy;
   1.153 +fun setup thy = Simplifier.map_simpset (fn ss => ss addsimprocs [cont_proc thy]) thy
   1.154  
   1.155 -end;
   1.156 +end