TFL/rules.new.sml
changeset 3332 3921ebbd9cf0
parent 3302 404fe31fd8d2
child 3353 9112a2efb9a3
equal deleted inserted replaced
3331:c81c7f8ad333 3332:3921ebbd9cf0
   502         of ([],_) => get (rst, n+1,L)
   502         of ([],_) => get (rst, n+1,L)
   503          | (vlist,body) =>
   503          | (vlist,body) =>
   504             let val eq = Logic.strip_imp_concl body
   504             let val eq = Logic.strip_imp_concl body
   505                 val (f,args) = S.strip_comb (get_lhs eq)
   505                 val (f,args) = S.strip_comb (get_lhs eq)
   506                 val (vstrl,_) = S.strip_abs f
   506                 val (vstrl,_) = S.strip_abs f
   507                 val names  = map (#Name o S.dest_var)
   507                 val names  = map (#1 o dest_Free)
   508                                  (variants (S.free_vars body) vstrl)
   508                                  (variants (S.free_vars body) vstrl)
   509             in get (rst, n+1, (names,n)::L)
   509             in get (rst, n+1, (names,n)::L)
   510             end handle _ => get (rst, n+1, L);
   510             end handle _ => get (rst, n+1, L);
   511 
   511 
   512 (* Note: rename_params_rule counts from 1, not 0 *)
   512 (* Note: rename_params_rule counts from 1, not 0 *)
   592           let val ty as Type("*", [fty,sty]) = type_of tm
   592           let val ty as Type("*", [fty,sty]) = type_of tm
   593           in  Const ("snd", ty --> sty) $ tm  end
   593           in  Const ("snd", ty --> sty) $ tm  end
   594 in
   594 in
   595 fun XFILL tych x vstruct = 
   595 fun XFILL tych x vstruct = 
   596   let fun traverse p xocc L =
   596   let fun traverse p xocc L =
   597         if (S.is_var p)
   597         if (is_Free p)
   598         then tych xocc::L
   598         then tych xocc::L
   599         else let val (p1,p2) = dest_pair p
   599         else let val (p1,p2) = dest_pair p
   600              in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
   600              in traverse p1 (mk_fst xocc) (traverse p2  (mk_snd xocc) L)
   601              end
   601              end
   602   in 
   602   in 
   624 fun PGEN tych a vstr th = 
   624 fun PGEN tych a vstr th = 
   625   let val a1 = tych a
   625   let val a1 = tych a
   626       val vstr1 = tych vstr
   626       val vstr1 = tych vstr
   627   in
   627   in
   628   forall_intr a1 
   628   forall_intr a1 
   629      (if (S.is_var vstr) 
   629      (if (is_Free vstr) 
   630       then cterm_instantiate [(vstr1,a1)] th
   630       then cterm_instantiate [(vstr1,a1)] th
   631       else VSTRUCT_ELIM tych a vstr th)
   631       else VSTRUCT_ELIM tych a vstr th)
   632   end;
   632   end;
   633 
   633 
   634 
   634 
   764                * not-fully applied occs. of "f" in the context mean that the
   764                * not-fully applied occs. of "f" in the context mean that the
   765                * current call is nested. The real solution is to pass in a
   765                * current call is nested. The real solution is to pass in a
   766                * term "f v1..vn" which is a pattern that any full application
   766                * term "f v1..vn" which is a pattern that any full application
   767                * of "f" will match.
   767                * of "f" will match.
   768                *-------------------------------------------------------------*)
   768                *-------------------------------------------------------------*)
   769               val func_name = #Name(S.dest_const func handle _ => 
   769               val func_name = #1(dest_Const func handle _ => dest_Free func)
   770                                     S.dest_var func)
   770               fun is_func tm = (#1(dest_Const tm handle _ => dest_Free tm) 
   771               fun is_func tm = (#Name(S.dest_const tm handle _ =>
   771 				= func_name)
   772                                       S.dest_var tm) = func_name)
       
   773                                handle _ => false
   772                                handle _ => false
   774               val nested = U.can(S.find_term is_func)
   773               val nested = U.can(S.find_term is_func)
   775               val rcontext = rev cntxt
   774               val rcontext = rev cntxt
   776               val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
   775               val cncl = HOLogic.dest_Trueprop o #prop o rep_thm
   777               val antl = case rcontext of [] => [] 
   776               val antl = case rcontext of [] => []