src/HOL/Tools/record_package.ML
changeset 16822 7fa91e6176ed
parent 16783 26fccaaf9cb4
child 16872 a51699621d22
equal deleted inserted replaced
16821:ba1f6aba44ed 16822:7fa91e6176ed
   853   in (quick_and_dirty_prove true sg [] prop (fn _ => (simp_tac (simpset addsimps thms) 1)))
   853   in (quick_and_dirty_prove true sg [] prop (fn _ => (simp_tac (simpset addsimps thms) 1)))
   854   end;
   854   end;
   855 
   855 
   856 
   856 
   857 local
   857 local
   858 
   858 fun eq (s1:string) (s2:string) = (s1 = s2);
   859 fun get_fields extfields T = 
   859 fun has_field extfields f T =
   860      Library.foldl (fn (xs,(eN,_))=>xs@(Symtab.lookup_multi (extfields,eN)))
   860      exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi (extfields,eN))) 
   861              ([],(dest_recTs T));
   861        (dest_recTs T);
   862 fun eq s1 s2 = (String.compare (s1, s2) = EQUAL);
       
   863 in
   862 in
   864 (* record_simproc *)
   863 (* record_simproc *)
   865 (* Simplifies selections of an record update:
   864 (* Simplifies selections of an record update:
   866  *  (1)  S (r(|S:=k|)) = k respectively
   865  *  (1)  S (r(|S:=k|)) = k respectively
   867  *  (2)  S (r(|X:=k|)) = S r
   866  *  (2)  S (r(|X:=k|)) = S r
   892                                val rv = mk_abs_var "r" r
   891                                val rv = mk_abs_var "r" r
   893                                val rb = Bound 0
   892                                val rb = Bound 0
   894                                val kv = mk_abs_var "k" k
   893                                val kv = mk_abs_var "k" k
   895                                val kb = Bound 1 
   894                                val kb = Bound 1 
   896                              in SOME (upd$kb$rb,kb,[kv,rv],true) end
   895                              in SOME (upd$kb$rb,kb,[kv,rv],true) end
   897                         else if exists (eq u_name o fst) (get_fields extfields rangeS)
   896                         else if has_field extfields u_name rangeS
   898                              orelse exists (eq s o fst) (get_fields extfields updT)
   897                              orelse has_field extfields s updT
   899                              then NONE
   898                              then NONE
   900 			     else (case mk_eq_terms r of 
   899 			     else (case mk_eq_terms r of 
   901                                      SOME (trm,trm',vars,update_s) 
   900                                      SOME (trm,trm',vars,update_s) 
   902                                      => let   
   901                                      => let   
   903 					  val kv = mk_abs_var "k" k
   902 					  val kv = mk_abs_var "k" k
   943              
   942              
   944 	     fun mk_abs_var x t = (x, fastype_of t);
   943 	     fun mk_abs_var x t = (x, fastype_of t);
   945              fun sel_name u = NameSpace.base (unsuffix updateN u);
   944              fun sel_name u = NameSpace.base (unsuffix updateN u);
   946 
   945 
   947              fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
   946              fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
   948                   if exists (eq s o fst) (get_fields extfields mT) then upd else seed s r
   947                   if has_field extfields s mT then upd else seed s r
   949                | seed _ r = r;
   948                | seed _ r = r;
   950 
   949 
   951              fun grow u uT k vars (sprout,skeleton) = 
   950              fun grow u uT k vars (sprout,skeleton) = 
   952 		   if sel_name u = moreN
   951 		   if sel_name u = moreN
   953                    then let val kv = mk_abs_var "k" k;
   952                    then let val kv = mk_abs_var "k" k;