src/Pure/meta_simplifier.ML
 changeset 10767 8fa4aafa7314 parent 10413 0e015d9bea4e child 11291 02db0084a695
equal inserted replaced
10766:ace2ba2d4fd1 10767:8fa4aafa7314
`   694     and subc skel`
`   694     and subc skel`
`   695           (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =`
`   695           (mss as Mss{rules,congs,procs,bounds,prems,mk_rews,termless}) t0 =`
`   696        (case term_of t0 of`
`   696        (case term_of t0 of`
`   697            Abs (a, T, t) =>`
`   697            Abs (a, T, t) =>`
`   698              let val b = variant bounds a`
`   698              let val b = variant bounds a`
`   699                  val (v, t') = dest_abs (Some ("." ^ b)) t0`
`   699                  val (v, t') = Thm.dest_abs (Some ("." ^ b)) t0`
`   700                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)`
`   700                  val mss' = mk_mss (rules, congs, procs, b :: bounds, prems, mk_rews, termless)`
`   701                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0`
`   701                  val skel' = case skel of Abs (_, _, sk) => sk | _ => skel0`
`   702              in case botc skel' mss' t' of`
`   702              in case botc skel' mss' t' of`
`   703                   Some thm => Some (abstract_rule a v thm)`
`   703                   Some thm => Some (abstract_rule a v thm)`
`   704                 | None => None`
`   704                 | None => None`
`   717                let fun appc () =`
`   717                let fun appc () =`
`   718                      let`
`   718                      let`
`   719                        val (tskel, uskel) = case skel of`
`   719                        val (tskel, uskel) = case skel of`
`   720                            tskel \$ uskel => (tskel, uskel)`
`   720                            tskel \$ uskel => (tskel, uskel)`
`   721                          | _ => (skel0, skel0);`
`   721                          | _ => (skel0, skel0);`
`   722                        val (ct, cu) = dest_comb t0`
`   722                        val (ct, cu) = Thm.dest_comb t0`
`   723                      in`
`   723                      in`
`   724                      (case botc tskel mss ct of`
`   724                      (case botc tskel mss ct of`
`   725                         Some thm1 =>`
`   725                         Some thm1 =>`
`   726                           (case botc uskel mss cu of`
`   726                           (case botc uskel mss cu of`
`   727                              Some thm2 => Some (combination thm1 thm2)`
`   727                              Some thm2 => Some (combination thm1 thm2)`
`   740 (* post processing: some partial applications h t1 ... tj, j <= length ts,`
`   740 (* post processing: some partial applications h t1 ... tj, j <= length ts,`
`   741    may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)`
`   741    may be a redex. Example: map (%x.x) = (%xs.xs) wrt map_cong *)`
`   742                           (let`
`   742                           (let`
`   743                              val thm = congc (prover mss, sign, maxidx) cong t0;`
`   743                              val thm = congc (prover mss, sign, maxidx) cong t0;`
`   744                              val t = rhs_of thm;`
`   744                              val t = rhs_of thm;`
`   745                              val (cl, cr) = dest_comb t`
`   745                              val (cl, cr) = Thm.dest_comb t`
`   746                              val dVar = Var(("", 0), dummyT)`
`   746                              val dVar = Var(("", 0), dummyT)`
`   747                              val skel =`
`   747                              val skel =`
`   748                                list_comb (h, replicate (length ts) dVar)`
`   748                                list_comb (h, replicate (length ts) dVar)`
`   749                            in case botc skel mss cl of`
`   749                            in case botc skel mss cl of`
`   750                                 None => Some thm`
`   750                                 None => Some thm`