src/Provers/splitter.ML
 changeset 0 a5a9c433f639 child 4 2695ba9b40f7
equal 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;`