src/Provers/splitter.ML
changeset 0 a5a9c433f639
child 4 2695ba9b40f7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Provers/splitter.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,112 @@
     1.4 +(*** case splitting ***)
     1.5 +(*
     1.6 +Use:
     1.7 +
     1.8 +val split_tac = mk_case_split_tac iffD;
     1.9 +
    1.10 +by(case_split_tac splits i);
    1.11 +
    1.12 +where splits = [P(elim(...)) == rhs, ...]
    1.13 +      iffD  = [| P <-> Q; Q |] ==> P (* is called iffD2 in HOL *)
    1.14 +
    1.15 +*)
    1.16 +
    1.17 +fun mk_case_split_tac iffD =
    1.18 +let
    1.19 +
    1.20 +val lift = prove_goal Pure.thy
    1.21 +  "[| !!x::'b::logic. Q(x) == R(x) |] ==> P(%x.Q(x)) == P(%x.R(x))::'a::logic"
    1.22 +  (fn [prem] => [rewtac prem, rtac reflexive_thm 1]);
    1.23 +(*
    1.24 +val iffD = prove_goal Pure.thy "[| PROP P == PROP Q; PROP Q |] ==> PROP P"
    1.25 +  (fn [p1,p2] => [rtac (equal_elim (symmetric p1) p2) 1]);
    1.26 +*)
    1.27 +val trlift = lift RS transitive_thm;
    1.28 +val _ $ (Var(P,PT)$_) $ _ = concl_of trlift;
    1.29 +
    1.30 +fun contains cmap =
    1.31 +  let fun isin i (Abs(_,_,b)) = isin 0 b
    1.32 +        | isin i (s$t) = isin (i+1) s orelse isin 0 t
    1.33 +        | isin i (Const(c,_)) = (case assoc(cmap,c) of
    1.34 +                                   Some(n,_) => n <= i
    1.35 +                                 | None => false)
    1.36 +        | isin _ _ = false
    1.37 +  in isin 0 end;
    1.38 +
    1.39 +fun mk_context cmap Ts maxi t =
    1.40 +  let fun var (t,i) = Var(("X",i),type_of1(Ts,t))
    1.41 +
    1.42 +      fun mka((None,i,ts),t) = if contains cmap t
    1.43 +            then let val (u,T,j) = mk(t,i) in (Some(T),j,ts@[u]) end
    1.44 +            else (None,i+1,ts@[var(t,i)])
    1.45 +        | mka((some,i,ts),t) = (some,i+1,ts@[var(t,i)])
    1.46 +      and mk(t as Abs _, i) = (Bound 0,type_of1(Ts,t),i)
    1.47 +        | mk(t,i) =
    1.48 +            let val (f,ts) = strip_comb t
    1.49 +                val (Some(T),j,us) = foldl mka ((None,i,[]),ts)
    1.50 +            in (list_comb(f,us),T,j) end
    1.51 +
    1.52 +      val (u,T,_) = mk(t,maxi+1)
    1.53 +  in Abs("",T,u) end;
    1.54 +
    1.55 +fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);
    1.56 +
    1.57 +fun goal_concl i thm = Logic.strip_assums_concl(nth_subgoal i thm);
    1.58 +
    1.59 +fun inst_lift cmap state lift i =
    1.60 +  let val sg = #sign(rep_thm state)
    1.61 +      val tsig = #tsig(Sign.rep_sg sg)
    1.62 +      val goali = nth_subgoal i state
    1.63 +      val Ts = map #2 (Logic.strip_params goali)
    1.64 +      val _ $ t $ _ = Logic.strip_assums_concl goali;
    1.65 +      val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t
    1.66 +      val cu = Sign.cterm_of sg cntxt
    1.67 +      val uT = #T(Sign.rep_cterm cu)
    1.68 +      val cP' = Sign.cterm_of sg (Var(P,uT))
    1.69 +      val ixnTs = Type.typ_match tsig ([],(PT,uT));
    1.70 +      val ixncTs = map (fn (x,y) => (x,Sign.ctyp_of sg y)) ixnTs;
    1.71 +  in instantiate (ixncTs, [(cP',cu)]) lift end;
    1.72 +
    1.73 +fun splittable al i thm =
    1.74 +  let val tm = goal_concl i thm
    1.75 +      fun nobound j k (Abs(_,_,t)) = nobound j (k+1) t
    1.76 +        | nobound j k (s$t) = nobound j k s andalso nobound j k t
    1.77 +        | nobound j k (Bound n) = n < k orelse k+j <= n
    1.78 +        | nobound _ _ _ = true;
    1.79 +      fun find j (None,t) = (case t of
    1.80 +            Abs(_,_,t) => find (j+1) (None,t)
    1.81 +          | _ => let val (h,args) = strip_comb t
    1.82 +                     fun no() = foldl (find j) (None,args)
    1.83 +                 in case h of
    1.84 +                      Const(c,_) =>
    1.85 +                        (case assoc(al,c) of
    1.86 +                           Some(n,thm) =>
    1.87 +                             if length args < n then no()
    1.88 +                             else if forall (nobound j 0) (take(n,args))
    1.89 +                                  then Some(thm)
    1.90 +                                  else no()
    1.91 +                         | None => no())
    1.92 +                    | _ => no()
    1.93 +                 end)
    1.94 +        | find _ (some,_) = some
    1.95 +  in find 0 (None,tm) end;
    1.96 +
    1.97 +fun split_tac [] i = no_tac
    1.98 +  | split_tac splits i =
    1.99 +  let fun const(thm) = let val _$(_$lhs)$_ = concl_of thm
   1.100 +                           val (Const(a,_),args) = strip_comb lhs
   1.101 +                       in (a,(length args,thm)) end
   1.102 +      val cmap = map const splits;
   1.103 +      fun lift thm = rtac (inst_lift cmap thm trlift i) i
   1.104 +      fun lift_split thm =
   1.105 +            case splittable cmap i thm of
   1.106 +              Some(split) => rtac split i
   1.107 +            | None => EVERY[STATE lift, rtac reflexive_thm (i+1),
   1.108 +                            STATE lift_split]
   1.109 +  in STATE(fn thm =>
   1.110 +       if (i <= nprems_of thm)  andalso  contains cmap (goal_concl i thm)
   1.111 +       then EVERY[rtac iffD i, STATE lift_split]
   1.112 +       else no_tac)
   1.113 +  end;
   1.114 +
   1.115 +in split_tac end;