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