equal
deleted
inserted
replaced
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; |