tuned whitespace;
authorwenzelm
Wed Dec 14 15:48:18 2016 +0100 (2016-12-14)
changeset 64566679710d324f1
parent 64565 5069ddebc937
child 64567 7141a3a4dc83
tuned whitespace;
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/proofterm.ML	Wed Dec 14 11:53:45 2016 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Wed Dec 14 15:48:18 2016 +0100
     1.3 @@ -533,11 +533,13 @@
     1.4        prf_add_loose_bnos plev tlev prf2
     1.5          (prf_add_loose_bnos plev tlev prf1 p)
     1.6    | prf_add_loose_bnos plev tlev (prf % opt) (is, js) =
     1.7 -      prf_add_loose_bnos plev tlev prf (case opt of
     1.8 +      prf_add_loose_bnos plev tlev prf
     1.9 +        (case opt of
    1.10            NONE => (is, insert (op =) ~1 js)
    1.11          | SOME t => (is, add_loose_bnos (t, tlev, js)))
    1.12    | prf_add_loose_bnos plev tlev (AbsP (_, opt, prf)) (is, js) =
    1.13 -      prf_add_loose_bnos (plev+1) tlev prf (case opt of
    1.14 +      prf_add_loose_bnos (plev+1) tlev prf
    1.15 +        (case opt of
    1.16            NONE => (is, insert (op =) ~1 js)
    1.17          | SOME t => (is, add_loose_bnos (t, tlev, js)))
    1.18    | prf_add_loose_bnos plev tlev (Abst (_, _, prf)) p =
    1.19 @@ -635,7 +637,7 @@
    1.20            handle Same.SAME => prf % Same.map_option (subst' lev) t)
    1.21        | subst _ _ = raise Same.SAME
    1.22      and substh lev prf = (subst lev prf handle Same.SAME => prf);
    1.23 -  in case args of [] => prf | _ => substh 0 prf end;
    1.24 +  in (case args of [] => prf | _ => substh 0 prf) end;
    1.25  
    1.26  fun prf_subst_pbounds args prf =
    1.27    let
    1.28 @@ -651,7 +653,7 @@
    1.29        | subst (prf % t) Plev tlev = subst prf Plev tlev % t
    1.30        | subst  _ _ _ = raise Same.SAME
    1.31      and substh prf Plev tlev = (subst prf Plev tlev handle Same.SAME => prf)
    1.32 -  in case args of [] => prf | _ => substh prf 0 0 end;
    1.33 +  in (case args of [] => prf | _ => substh prf 0 0) end;
    1.34  
    1.35  
    1.36  (**** Freezing and thawing of variables in proof terms ****)
    1.37 @@ -992,7 +994,7 @@
    1.38          | Var _ => SOME (remove_types t)
    1.39          | _ => NONE) %
    1.40          (case head_of g of
    1.41 -           Abs _ => SOME (remove_types u)
    1.42 +          Abs _ => SOME (remove_types u)
    1.43          | Var _ => SOME (remove_types u)
    1.44          | _ => NONE) %% prf1 %% prf2
    1.45       | _ => prf % NONE % NONE %% prf1 %% prf2)
    1.46 @@ -1105,7 +1107,8 @@
    1.47        add_npvars q p Ts (vs, if p andalso q then betapply (t, Var (("",0), T)) else t)
    1.48    | add_npvars q p Ts (vs, Abs (_, T, t)) = add_npvars q p (T::Ts) (vs, t)
    1.49    | add_npvars _ _ Ts (vs, t) = add_npvars' Ts (vs, t)
    1.50 -and add_npvars' Ts (vs, t) = (case strip_comb t of
    1.51 +and add_npvars' Ts (vs, t) =
    1.52 +  (case strip_comb t of
    1.53      (Var (ixn, _), ts) => if test_args [] ts then vs
    1.54        else Library.foldl (add_npvars' Ts)
    1.55          (AList.update (op =) (ixn,
    1.56 @@ -1115,19 +1118,20 @@
    1.57  
    1.58  fun prop_vars (Const ("Pure.imp", _) $ P $ Q) = union (op =) (prop_vars P) (prop_vars Q)
    1.59    | prop_vars (Const ("Pure.all", _) $ Abs (_, _, t)) = prop_vars t
    1.60 -  | prop_vars t = (case strip_comb t of
    1.61 -      (Var (ixn, _), _) => [ixn] | _ => []);
    1.62 +  | prop_vars t = (case strip_comb t of (Var (ixn, _), _) => [ixn] | _ => []);
    1.63  
    1.64  fun is_proj t =
    1.65    let
    1.66 -    fun is_p i t = (case strip_comb t of
    1.67 +    fun is_p i t =
    1.68 +      (case strip_comb t of
    1.69          (Bound _, []) => false
    1.70        | (Bound j, ts) => j >= i orelse exists (is_p i) ts
    1.71        | (Abs (_, _, u), _) => is_p (i+1) u
    1.72        | (_, ts) => exists (is_p i) ts)
    1.73 -  in (case strip_abs_body t of
    1.74 -        Bound _ => true
    1.75 -      | t' => is_p 0 t')
    1.76 +  in
    1.77 +    (case strip_abs_body t of
    1.78 +      Bound _ => true
    1.79 +    | t' => is_p 0 t')
    1.80    end;
    1.81  
    1.82  fun needed_vars prop =
    1.83 @@ -1196,7 +1200,8 @@
    1.84              val (ts', ts'') = chop (length vs) ts;
    1.85              val insts = take (length ts') (map (fst o dest_Var) vs) ~~ ts';
    1.86              val nvs = Library.foldl (fn (ixns', (ixn, ixns)) =>
    1.87 -              insert (op =) ixn (case AList.lookup (op =) insts ixn of
    1.88 +              insert (op =) ixn
    1.89 +                (case AList.lookup (op =) insts ixn of
    1.90                    SOME (SOME t) => if is_proj t then union (op =) ixns ixns' else ixns'
    1.91                  | _ => union (op =) ixns ixns'))
    1.92                    (needed prop ts'' prfs, add_npvars false true [] ([], prop));
    1.93 @@ -1250,12 +1255,12 @@
    1.94  
    1.95      fun mtch Ts i j (pinst, tinst) (Hyp (Var (ixn, _)), prf) =
    1.96            if i = 0 andalso j = 0 then ((ixn, prf) :: pinst, tinst)
    1.97 -          else (case apfst (flt i) (apsnd (flt j)
    1.98 -                  (prf_add_loose_bnos 0 0 prf ([], []))) of
    1.99 +          else
   1.100 +            (case apfst (flt i) (apsnd (flt j) (prf_add_loose_bnos 0 0 prf ([], []))) of
   1.101                ([], []) => ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
   1.102 -            | ([], _) => if j = 0 then
   1.103 -                   ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
   1.104 -                 else raise PMatch
   1.105 +            | ([], _) =>
   1.106 +                if j = 0 then ((ixn, incr_pboundvars (~i) (~j) prf) :: pinst, tinst)
   1.107 +                else raise PMatch
   1.108              | _ => raise PMatch)
   1.109        | mtch Ts i j inst (prf1 % opt1, prf2 % opt2) =
   1.110            optmatch (matcht Ts j) (mtch Ts i j inst (prf1, prf2)) (opt1, opt2)
   1.111 @@ -1389,45 +1394,57 @@
   1.112        | rew0 Ts hs prf = rew Ts hs prf;
   1.113  
   1.114      fun rew1 _ _ (Hyp (Var _)) _ = NONE
   1.115 -      | rew1 Ts hs skel prf = (case rew2 Ts hs skel prf of
   1.116 -          SOME prf1 => (case rew0 Ts hs prf1 of
   1.117 -              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
   1.118 -            | NONE => SOME prf1)
   1.119 -        | NONE => (case rew0 Ts hs prf of
   1.120 -              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
   1.121 -            | NONE => NONE))
   1.122 +      | rew1 Ts hs skel prf =
   1.123 +          (case rew2 Ts hs skel prf of
   1.124 +            SOME prf1 =>
   1.125 +              (case rew0 Ts hs prf1 of
   1.126 +                SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts hs skel' prf2))
   1.127 +              | NONE => SOME prf1)
   1.128 +          | NONE =>
   1.129 +              (case rew0 Ts hs prf of
   1.130 +                SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts hs skel' prf1))
   1.131 +              | NONE => NONE))
   1.132  
   1.133 -    and rew2 Ts hs skel (prf % SOME t) = (case prf of
   1.134 +    and rew2 Ts hs skel (prf % SOME t) =
   1.135 +          (case prf of
   1.136              Abst (_, _, body) =>
   1.137                let val prf' = prf_subst_bounds [t] body
   1.138                in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
   1.139 -          | _ => (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
   1.140 -              SOME prf' => SOME (prf' % SOME t)
   1.141 -            | NONE => NONE))
   1.142 +          | _ =>
   1.143 +              (case rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf of
   1.144 +                SOME prf' => SOME (prf' % SOME t)
   1.145 +              | NONE => NONE))
   1.146        | rew2 Ts hs skel (prf % NONE) = Option.map (fn prf' => prf' % NONE)
   1.147            (rew1 Ts hs (case skel of skel' % _ => skel' | _ => no_skel) prf)
   1.148 -      | rew2 Ts hs skel (prf1 %% prf2) = (case prf1 of
   1.149 +      | rew2 Ts hs skel (prf1 %% prf2) =
   1.150 +          (case prf1 of
   1.151              AbsP (_, _, body) =>
   1.152                let val prf' = prf_subst_pbounds [prf2] body
   1.153                in SOME (the_default prf' (rew2 Ts hs no_skel prf')) end
   1.154            | _ =>
   1.155 -            let val (skel1, skel2) = (case skel of
   1.156 -                skel1 %% skel2 => (skel1, skel2)
   1.157 -              | _ => (no_skel, no_skel))
   1.158 -            in case rew1 Ts hs skel1 prf1 of
   1.159 -                SOME prf1' => (case rew1 Ts hs skel2 prf2 of
   1.160 +            let
   1.161 +              val (skel1, skel2) =
   1.162 +                (case skel of
   1.163 +                  skel1 %% skel2 => (skel1, skel2)
   1.164 +                | _ => (no_skel, no_skel))
   1.165 +            in
   1.166 +              (case rew1 Ts hs skel1 prf1 of
   1.167 +                SOME prf1' =>
   1.168 +                  (case rew1 Ts hs skel2 prf2 of
   1.169                      SOME prf2' => SOME (prf1' %% prf2')
   1.170                    | NONE => SOME (prf1' %% prf2))
   1.171 -              | NONE => (case rew1 Ts hs skel2 prf2 of
   1.172 +              | NONE =>
   1.173 +                  (case rew1 Ts hs skel2 prf2 of
   1.174                      SOME prf2' => SOME (prf1 %% prf2')
   1.175 -                  | NONE => NONE)
   1.176 +                  | NONE => NONE))
   1.177              end)
   1.178 -      | rew2 Ts hs skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts) hs
   1.179 +      | rew2 Ts hs skel (Abst (s, T, prf)) =
   1.180 +          (case rew1 (the_default dummyT T :: Ts) hs
   1.181                (case skel of Abst (_, _, skel') => skel' | _ => no_skel) prf of
   1.182              SOME prf' => SOME (Abst (s, T, prf'))
   1.183            | NONE => NONE)
   1.184 -      | rew2 Ts hs skel (AbsP (s, t, prf)) = (case rew1 Ts (t :: hs)
   1.185 -              (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
   1.186 +      | rew2 Ts hs skel (AbsP (s, t, prf)) =
   1.187 +          (case rew1 Ts (t :: hs) (case skel of AbsP (_, _, skel') => skel' | _ => no_skel) prf of
   1.188              SOME prf' => SOME (AbsP (s, t, prf'))
   1.189            | NONE => NONE)
   1.190        | rew2 _ _ _ _ = NONE;
   1.191 @@ -1580,8 +1597,7 @@
   1.192    in (pthm, proof_combP (proof_combt' (head, args), argsP)) end;
   1.193  
   1.194  fun unconstrain_thm_proof thy shyps concl promises body =
   1.195 -  let
   1.196 -    val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
   1.197 +  let val (pthm, head, _, _, args) = prepare_thm_proof thy "" shyps [] concl promises body
   1.198    in (pthm, proof_combt' (head, args)) end;
   1.199  
   1.200