src/Provers/splitter.ML
 changeset 1030 1d8fa2fc4b9c parent 943 8477483f663f child 1064 5d6fb2c938e0
equal inserted replaced
1029:27808dabf4af 1030:1d8fa2fc4b9c
`     1 (*  Title:      Provers/splitter`
`     1 (*  Title:      Provers/splitter`
`     2     ID:         \$Id\$`
`     2     ID:         \$Id\$`
`     3     Author:     Tobias Nipkow`
`     3     Author:     Tobias Nipkow`
`     4     Copyright   1993  TU Munich`
`     4     Copyright   1995  TU Munich`
`     5 `
`     5 `
`     6 Generic case-splitter, suitable for most logics.`
`     6 Generic case-splitter, suitable for most logics.`
`     7 `
`     7 `
`     8 Use:`
`     8 Use:`
`     9 `
`     9 `
`    28   end;`
`    28   end;`
`    29 `
`    29 `
`    30 val trlift = lift RS transitive_thm;`
`    30 val trlift = lift RS transitive_thm;`
`    31 val _ \$ (Var(P,PT)\$_) \$ _ = concl_of trlift;`
`    31 val _ \$ (Var(P,PT)\$_) \$ _ = concl_of trlift;`
`    32 `
`    32 `
`    41 `
`    33 `
`    42 fun mk_context cmap Ts maxi t =`
`    34 fun mk_cntxt Ts t pos T maxi =`
`    43   let fun var (t,i) = Var(("X",i),type_of1(Ts,t))`
`    35   let fun var (t,i) = Var(("X",i),type_of1(Ts,t));`
`       `
`    36       fun down [] t i = Bound 0`
`       `
`    37         | down (p::ps) t i =`
`       `
`    38             let val (h,ts) = strip_comb t`
`       `
`    39                 val v1 = map var (take(p,ts) ~~ (i upto (i+p-1)))`
`       `
`    40                 val u::us = drop(p,ts)`
`       `
`    41                 val v2 = map var (us ~~ ((i+p) upto (i+length(ts)-2)))`
`       `
`    42       in list_comb(h,v1@[down ps u (i+length ts)]@v2) end;`
`       `
`    43   in Abs("", T, down (rev pos) t maxi) end;`
`    44 `
`    44 `
`    45       fun mka((None,i,ts),t) = if contains cmap t`
`    45 fun add_lbnos(is,t) = add_loose_bnos(t,0,is);`
`    46             then let val (u,T,j) = mk(t,i) in (Some(T),j,ts@[u]) end`
`       `
`    47             else (None,i+1,ts@[var(t,i)])`
`       `
`    48         | mka((some,i,ts),t) = (some,i+1,ts@[var(t,i)])`
`       `
`    49       and mk(t as Abs _, i) = (Bound 0,type_of1(Ts,t),i)`
`       `
`    50         | mk(t,i) =`
`       `
`    51             let val (f,ts) = strip_comb t`
`       `
`    52                 val (Some(T),j,us) = foldl mka ((None,i,[]),ts)`
`       `
`    53             in (list_comb(f,us),T,j) end`
`       `
`    54 `
`    46 `
`    55       val (u,T,_) = mk(t,maxi+1)`
`    47 fun typ_test _ [] = true`
`    56   in Abs("",T,u) end;`
`    48   | typ_test T ((_,U,_)::_) = (T=U);`
`       `
`    49 `
`       `
`    50 fun mk_split_pack(thm,T,n,ts,apsns) =`
`       `
`    51   if n <= length ts andalso typ_test T apsns`
`       `
`    52   then let val lev = length apsns`
`       `
`    53            val lbnos = foldl add_lbnos ([],take(n,ts))`
`       `
`    54            val flbnos = filter (fn i => i < lev) lbnos`
`       `
`    55        in [(thm, if null flbnos then [] else rev apsns)] end`
`       `
`    56   else [];`
`       `
`    57 `
`       `
`    58 fun split_posns cmap Ts t =`
`       `
`    59   let fun posns Ts pos apsns (Abs(_,T,t)) =`
`       `
`    60             let val U = fastype_of1(T::Ts,t)`
`       `
`    61             in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end`
`       `
`    62         | posns Ts pos apsns t =`
`       `
`    63             let val (h,ts) = strip_comb t`
`       `
`    64                 fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);`
`       `
`    65                 val a = case h of`
`       `
`    66                   Const(c,_) =>`
`       `
`    67                     (case assoc(cmap,c) of`
`       `
`    68                        Some(thm,T,n) => mk_split_pack(thm,T,n,ts,apsns)`
`       `
`    69                      | None => [])`
`       `
`    70                 | _ => []`
`       `
`    71              in snd(foldl iter ((0,a),ts)) end`
`       `
`    72   in posns Ts [] [] t end;`
`    57 `
`    73 `
`    58 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);`
`    74 fun nth_subgoal i thm = nth_elem(i-1,prems_of thm);`
`    59 `
`    75 `
`    60 fun goal_concl i thm = Logic.strip_assums_concl(nth_subgoal i thm);`
`    76 fun shorter((_,ps),(_,qs)) = length ps <= length qs;`
`    61 `
`    77 `
`    62 fun inst_lift cmap state lift i =`
`    78 fun select cmap state i =`
`       `
`    79   let val goali = nth_subgoal i state`
`       `
`    80       val Ts = rev(map #2 (Logic.strip_params goali))`
`       `
`    81       val _ \$ t \$ _ = Logic.strip_assums_concl goali;`
`       `
`    82   in (Ts,t,sort shorter (split_posns cmap Ts t)) end;`
`       `
`    83 `
`       `
`    84 fun inst_lift Ts t (T,U,pos) state lift i =`
`    63   let val sg = #sign(rep_thm state)`
`    85   let val sg = #sign(rep_thm state)`
`    64       val tsig = #tsig(Sign.rep_sg sg)`
`    86       val tsig = #tsig(Sign.rep_sg sg)`
`    65       val goali = nth_subgoal i state`
`    87       val cntxt = mk_cntxt Ts t pos (T-->U) (#maxidx(rep_thm lift))`
`    66       val Ts = map #2 (Logic.strip_params goali)`
`       `
`    67       val _ \$ t \$ _ = Logic.strip_assums_concl goali;`
`       `
`    68       val cntxt = mk_context cmap (rev Ts) (#maxidx(rep_thm lift)) t`
`       `
`    69       val cu = cterm_of sg cntxt`
`    88       val cu = cterm_of sg cntxt`
`    70       val uT = #T(rep_cterm cu)`
`    89       val uT = #T(rep_cterm cu)`
`    71       val cP' = cterm_of sg (Var(P,uT))`
`    90       val cP' = cterm_of sg (Var(P,uT))`
`    72       val ixnTs = Type.typ_match tsig ([],(PT,uT));`
`    91       val ixnTs = Type.typ_match tsig ([],(PT,uT));`
`    73       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;`
`    92       val ixncTs = map (fn (x,y) => (x,ctyp_of sg y)) ixnTs;`
`    74   in instantiate (ixncTs, [(cP',cu)]) lift end;`
`    93   in instantiate (ixncTs, [(cP',cu)]) lift end;`
`    75 `
`    94 `
`    99 `
`    95 `
`   100 fun split_tac [] i = no_tac`
`    96 fun split_tac [] i = no_tac`
`   101   | split_tac splits i =`
`    97   | split_tac splits i =`
`   102   let fun const(thm) = let val _\$(_\$lhs)\$_ = concl_of thm`
`    98   let fun const(thm) = let val _\$(t as _\$lhs)\$_ = concl_of thm`
`   103                            val (Const(a,_),args) = strip_comb lhs`
`    99                            val (Const(a,_),args) = strip_comb lhs`
`   104                        in (a,(length args,thm)) end`
`   100                        in (a,(thm,fastype_of t,length args)) end`
`   105       val cmap = map const splits;`
`   101       val cmap = map const splits;`
`   106       fun lift thm = rtac (inst_lift cmap thm trlift i) i`
`   102       fun lift Ts t p state = rtac (inst_lift Ts t p state trlift i) i`
`   107       fun lift_split thm =`
`   103       fun lift_split state =`
`   108             case splittable cmap i thm of`
`   104             let val (Ts,t,splits) = select cmap state i`
`   109               Some(split) => rtac split i`
`   105             in case splits of`
`   110             | None => EVERY[STATE lift, rtac reflexive_thm (i+1),`
`   106                  [] => no_tac`
`   111                             STATE lift_split]`
`   107                | (thm,apsns)::_ =>`
`       `
`   108                    (case apsns of`
`       `
`   109                       [] => rtac thm i`
`       `
`   110                     | p::_ => EVERY[STATE(lift Ts t p),`
`       `
`   111                                     rtac reflexive_thm (i+1),`
`       `
`   112                                     STATE lift_split])`
`       `
`   113             end`
`   112   in STATE(fn thm =>`
`   114   in STATE(fn thm =>`
`   113        if (i <= nprems_of thm)  andalso  contains cmap (goal_concl i thm)`
`   115        if i <= nprems_of thm then rtac iffD i THEN STATE lift_split`
`   114        then EVERY[rtac iffD i, STATE lift_split]`
`       `
`   115        else no_tac)`
`   116        else no_tac)`
`   116   end;`
`   117   end;`
`   117 `
`   118 `
`   118 in split_tac end;`
`   119 in split_tac end;`