src/Provers/splitter.ML
author nipkow
Wed Mar 08 14:35:26 1995 +0100 (1995-03-08)
changeset 943 8477483f663f
parent 927 305e7cfda869
child 1030 1d8fa2fc4b9c
permissions -rw-r--r--
Replaced read by read_cterm.
     1 (*  Title:      Provers/splitter
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1993  TU Munich
     5 
     6 Generic case-splitter, suitable for most logics.
     7 
     8 Use:
     9 
    10 val split_tac = mk_case_split_tac iffD;
    11 
    12 by(case_split_tac splits i);
    13 
    14 where splits = [P(elim(...)) == rhs, ...]
    15       iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
    16 
    17 *)
    18 
    19 fun mk_case_split_tac iffD =
    20 let
    21 
    22 val lift =
    23   let val ct = read_cterm (#sign(rep_thm iffD))
    24            ("[| !!x::'b::logic. Q(x) == R(x) |] ==> \
    25             \P(%x.Q(x)) == P(%x.R(x))::'a::logic",propT)
    26   in prove_goalw_cterm [] ct
    27      (fn [prem] => [rewtac prem, rtac reflexive_thm 1])
    28   end;
    29 
    30 val trlift = lift RS transitive_thm;
    31 val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
    32 
    33 fun contains cmap =
    34   let fun isin i (Abs(_,_,b)) = isin 0 b
    35         | isin i (s$t) = isin (i+1) s orelse isin 0 t
    36         | isin i (Const(c,_)) = (case assoc(cmap,c) of
    37                                    Some(n,_) => n <= i
    38                                  | None => false)
    39         | isin _ _ = false
    40   in isin 0 end;
    41 
    42 fun mk_context cmap Ts maxi t =
    43   let fun var (t,i) = Var(("X",i),type_of1(Ts,t))
    44 
    45       fun mka((None,i,ts),t) = if contains cmap t
    46             then let val (u,T,j) = mk(t,i) in (Some(T),j,ts@[u]) end
    47             else (None,i+1,ts@[var(t,i)])
    48         | mka((some,i,ts),t) = (some,i+1,ts@[var(t,i)])
    49       and mk(t as Abs _, i) = (Bound 0,type_of1(Ts,t),i)
    50         | mk(t,i) =
    51             let val (f,ts) = strip_comb t
    52                 val (Some(T),j,us) = foldl mka ((None,i,[]),ts)
    53             in (list_comb(f,us),T,j) end
    54 
    55       val (u,T,_) = mk(t,maxi+1)
    56   in Abs("",T,u) end;
    57 
    58 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
    59 
    60 fun goal_concl i thm = Logic.strip_assums_concl(nth_subgoal i thm);
    61 
    62 fun inst_lift cmap state lift i =
    63   let val sg = #sign(rep_thm state)
    64       val tsig = #tsig(Sign.rep_sg sg)
    65       val goali = nth_subgoal i state
    66       val Ts = map #2 (Logic.strip_params goali)
    67       val _ $ t $ _ = Logic.strip_assums_concl goali;
    68       val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t
    69       val cu = cterm_of sg cntxt
    70       val uT = #T(rep_cterm cu)
    71       val cP' = cterm_of sg (Var(P,uT))
    72       val ixnTs = Type.typ_match tsig ([],(PT,uT));
    73       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;
    74   in instantiate (ixncTs, [(cP',cu)]) lift end;
    75 
    76 fun splittable al i thm =
    77   let val tm = goal_concl i thm
    78       fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t
    79         | nobound j k (s$t) = nobound j k s andalso nobound j k t
    80         | nobound j k (Bound n) = n < k orelse k+j <= n
    81         | nobound _ _ _ = true;
    82       fun find j (None,t) = (case t of
    83             Abs(_,_,t) => find (j+1) (None,t)
    84           | _ => let val (h,args) = strip_comb t
    85                      fun no() = foldl (find j) (None,args)
    86                  in case h of
    87                       Const(c,_) =>
    88                         (case assoc(al,c) of
    89                            Some(n,thm) =>
    90                              if length args < n then no()
    91                              else if forall (nobound j 0) (take(n,args))
    92                                   then Some(thm)
    93                                   else no()
    94                          | None => no())
    95                     | _ => no()
    96                  end)
    97         | find _ (some,_) = some
    98   in find 0 (None,tm) end;
    99 
   100 fun split_tac [] i = no_tac
   101   | split_tac splits i =
   102   let fun const(thm) = let val _$(_$lhs)$_ = concl_of thm
   103                            val (Const(a,_),args) = strip_comb lhs
   104                        in (a,(length args,thm)) end
   105       val cmap = map const splits;
   106       fun lift thm = rtac (inst_lift cmap thm trlift i) i
   107       fun lift_split thm =
   108             case splittable cmap i thm of
   109               Some(split) => rtac split i
   110             | None => EVERY[STATE lift, rtac reflexive_thm (i+1),
   111                             STATE lift_split]
   112   in STATE(fn thm =>
   113        if (i <= nprems_of thm)  andalso  contains cmap (goal_concl i thm)
   114        then EVERY[rtac iffD i, STATE lift_split]
   115        else no_tac)
   116   end;
   117 
   118 in split_tac end;