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