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