# HG changeset patch # User tsewell@rubicon.NSW.bigpond.net.au # Date 1253697468 -36000 # Node ID f65d74a264dd1d92c39e20776fac9c4a21a9cddb # Parent 5b65449d76692d31de744a1b3269468e0e0d8703 Initial response to feedback from Norbert, Makarius on record patch As Norbert recommended, the IsTuple.thy and istuple_support.ML files have been integrated into Record.thy and record.ML. I haven't merged the structures - record.ML now contains Record and IsTupleSupport. Some of the cosmetic changes Makarius requested have been made, including renaming variables with camel-case and run-together names and removing the tab character from the Author: line. Constants are defined with definition rather than constdefs. The split_ex_prf inner function has been cleaned up. diff -r 5b65449d7669 -r f65d74a264dd src/HOL/IsTuple.thy --- a/src/HOL/IsTuple.thy Tue Sep 22 13:52:19 2009 +1000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,389 +0,0 @@ -(* Title: HOL/IsTuple.thy - Author: Thomas Sewell, NICTA -*) - -header {* Operators on types isomorphic to tuples *} - -theory IsTuple imports Product_Type - -uses ("Tools/istuple_support.ML") - -begin - -text {* -This module provides operators and lemmas for types isomorphic to tuples. -These types are used in defining efficient records. Consider the record -access/update simplification "alpha (beta_update f rec) = alpha rec" for -distinct fields alpha and beta of some record rec with n fields. There -are n^2 such theorems, which prohibits storage of all of them for -large n. The rules can be proved on the fly by case decomposition and -simplification in O(n) time. By creating O(n) isomorphic-tuple types -while defining the record, however, we can prove the access/update -simplification in O(log(n)^2) time. - -The O(n) cost of case decomposition is not because O(n) steps are taken, -but rather because the resulting rule must contain O(n) new variables and -an O(n) size concrete record construction. To sidestep this cost, we would -like to avoid case decomposition in proving access/update theorems. - -Record types are defined as isomorphic to tuple types. For instance, a -record type with fields 'a, 'b, 'c and 'd might be introduced as -isomorphic to 'a \ ('b \ ('c \ 'd)). If we balance the tuple tree to -('a \ 'b) \ ('c \ 'd) then accessors can be defined by converting to -the underlying type then using O(log(n)) fst or snd operations. -Updators can be defined similarly, if we introduce a fst_update and -snd_update function. Furthermore, we can prove the access/update -theorem in O(log(n)) steps by using simple rewrites on fst, snd, -fst_update and snd_update. - -The catch is that, although O(log(n)) steps were taken, the underlying -type we converted to is a tuple tree of size O(n). Processing this term -type wastes performance. We avoid this for large n by taking each -subtree of size K and defining a new type isomorphic to that tuple -subtree. The record can now be defined as isomorphic to a tuple tree -of these O(n/K) new types, or, if n > K*K, we can repeat the process, -until the record can be defined in terms of a tuple tree of complexity -less than the constant K. - -If we prove the access/update theorem on this type with the analagous -steps to the tuple tree, we consume O(log(n)^2) time as the intermediate -terms are O(log(n)) in size and the types needed have size bounded by K. -To enable this analagous traversal, we define the functions seen below: -istuple_fst, istuple_snd, istuple_fst_update and istuple_snd_update. -These functions generalise tuple operations by taking a parameter that -encapsulates a tuple isomorphism. The rewrites needed on these functions -now need an additional assumption which is that the isomorphism works. - -These rewrites are typically used in a structured way. They are here -presented as the introduction rule isomorphic_tuple.intros rather than -as a rewrite rule set. The introduction form is an optimisation, as net -matching can be performed at one term location for each step rather than -the simplifier searching the term for possible pattern matches. The rule -set is used as it is viewed outside the locale, with the locale assumption -(that the isomorphism is valid) left as rule assumption. All rules are -structured to aid net matching, using either a point-free form or an -encapsulating predicate. -*} - -typedef ('a, 'b, 'c) tuple_isomorphism - = "UNIV :: (('a \ ('b \ 'c)) \ (('b \ 'c) \ 'a)) set" - by simp - -constdefs - "TupleIsomorphism repr abst \ Abs_tuple_isomorphism (repr, abst)" - -constdefs - istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'b" - "istuple_fst isom \ let (repr, abst) = Rep_tuple_isomorphism isom in fst \ repr" - istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'c" - "istuple_snd isom \ let (repr, abst) = Rep_tuple_isomorphism isom in snd \ repr" - istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \ ('b \ 'b) \ ('a \ 'a)" - "istuple_fst_update isom \ - let (repr, abst) = Rep_tuple_isomorphism isom in - (\f v. abst (f (fst (repr v)), snd (repr v)))" - istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \ ('c \ 'c) \ ('a \ 'a)" - "istuple_snd_update isom \ - let (repr, abst) = Rep_tuple_isomorphism isom in - (\f v. abst (fst (repr v), f (snd (repr v))))" - istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \ 'b \ 'c \ 'a" - "istuple_cons isom \ let (repr, abst) = Rep_tuple_isomorphism isom in curry abst" - -text {* -These predicates are used in the introduction rule set to constrain -matching appropriately. The elimination rules for them produce the -desired theorems once they are proven. The final introduction rules are -used when no further rules from the introduction rule set can apply. -*} - -constdefs - istuple_surjective_proof_assist :: "'a \ 'b \ ('a \ 'b) \ bool" - "istuple_surjective_proof_assist x y f \ f x = y" - istuple_update_accessor_cong_assist :: "(('b \ 'b) \ ('a \ 'a)) - \ ('a \ 'b) \ bool" - "istuple_update_accessor_cong_assist upd acc - \ (\f v. upd (\x. f (acc v)) v = upd f v) - \ (\v. upd id v = v)" - istuple_update_accessor_eq_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) - \ 'a \ ('b \ 'b) \ 'a \ 'b \ bool" - "istuple_update_accessor_eq_assist upd acc v f v' x - \ upd f v = v' \ acc v = x - \ istuple_update_accessor_cong_assist upd acc" - -lemma update_accessor_congruence_foldE: - assumes uac: "istuple_update_accessor_cong_assist upd acc" - and r: "r = r'" and v: "acc r' = v'" - and f: "\v. v' = v \ f v = f' v" - shows "upd f r = upd f' r'" - using uac r v[symmetric] - apply (subgoal_tac "upd (\x. f (acc r')) r' = upd (\x. f' (acc r')) r'") - apply (simp add: istuple_update_accessor_cong_assist_def) - apply (simp add: f) - done - -lemma update_accessor_congruence_unfoldE: - "\ istuple_update_accessor_cong_assist upd acc; - r = r'; acc r' = v'; \v. v = v' \ f v = f' v \ - \ upd f r = upd f' r'" - apply (erule(2) update_accessor_congruence_foldE) - apply simp - done - -lemma istuple_update_accessor_cong_assist_id: - "istuple_update_accessor_cong_assist upd acc \ upd id = id" - by (rule ext, simp add: istuple_update_accessor_cong_assist_def) - -lemma update_accessor_noopE: - assumes uac: "istuple_update_accessor_cong_assist upd acc" - and acc: "f (acc x) = acc x" - shows "upd f x = x" - using uac - by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def] - cong: update_accessor_congruence_unfoldE[OF uac]) - -lemma update_accessor_noop_compE: - assumes uac: "istuple_update_accessor_cong_assist upd acc" - assumes acc: "f (acc x) = acc x" - shows "upd (g \ f) x = upd g x" - by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac]) - -lemma update_accessor_cong_assist_idI: - "istuple_update_accessor_cong_assist id id" - by (simp add: istuple_update_accessor_cong_assist_def) - -lemma update_accessor_cong_assist_triv: - "istuple_update_accessor_cong_assist upd acc - \ istuple_update_accessor_cong_assist upd acc" - by assumption - -lemma update_accessor_accessor_eqE: - "\ istuple_update_accessor_eq_assist upd acc v f v' x \ \ acc v = x" - by (simp add: istuple_update_accessor_eq_assist_def) - -lemma update_accessor_updator_eqE: - "\ istuple_update_accessor_eq_assist upd acc v f v' x \ \ upd f v = v'" - by (simp add: istuple_update_accessor_eq_assist_def) - -lemma istuple_update_accessor_eq_assist_idI: - "v' = f v \ istuple_update_accessor_eq_assist id id v f v' v" - by (simp add: istuple_update_accessor_eq_assist_def - update_accessor_cong_assist_idI) - -lemma istuple_update_accessor_eq_assist_triv: - "istuple_update_accessor_eq_assist upd acc v f v' x - \ istuple_update_accessor_eq_assist upd acc v f v' x" - by assumption - -lemma istuple_update_accessor_cong_from_eq: - "istuple_update_accessor_eq_assist upd acc v f v' x - \ istuple_update_accessor_cong_assist upd acc" - by (simp add: istuple_update_accessor_eq_assist_def) - -lemma o_eq_dest: - "a o b = c o d \ a (b v) = c (d v)" - apply (clarsimp simp: o_def) - apply (erule fun_cong) - done - -lemma o_eq_elim: - "\ a o b = c o d; \ \v. a (b v) = c (d v) \ \ R \ \ R" - apply (erule meta_mp) - apply (erule o_eq_dest) - done - -lemma istuple_surjective_proof_assistI: - "f x = y \ - istuple_surjective_proof_assist x y f" - by (simp add: istuple_surjective_proof_assist_def) - -lemma istuple_surjective_proof_assist_idE: - "istuple_surjective_proof_assist x y id \ x = y" - by (simp add: istuple_surjective_proof_assist_def) - -locale isomorphic_tuple = - fixes isom :: "('a, 'b, 'c) tuple_isomorphism" - and repr and abst - defines "repr \ fst (Rep_tuple_isomorphism isom)" - defines "abst \ snd (Rep_tuple_isomorphism isom)" - assumes repr_inv: "\x. abst (repr x) = x" - assumes abst_inv: "\y. repr (abst y) = y" - -begin - -lemma repr_inj: - "(repr x = repr y) = (x = y)" - apply (rule iffI, simp_all) - apply (drule_tac f=abst in arg_cong, simp add: repr_inv) - done - -lemma abst_inj: - "(abst x = abst y) = (x = y)" - apply (rule iffI, simp_all) - apply (drule_tac f=repr in arg_cong, simp add: abst_inv) - done - -lemma split_Rep: - "split f (Rep_tuple_isomorphism isom) - = f repr abst" - by (simp add: split_def repr_def abst_def) - -lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj - -lemma istuple_access_update_fst_fst: - "\ f o h g = j o f \ \ - (f o istuple_fst isom) o (istuple_fst_update isom o h) g - = j o (f o istuple_fst isom)" - by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_access_update_snd_snd: - "\ f o h g = j o f \ \ - (f o istuple_snd isom) o (istuple_snd_update isom o h) g - = j o (f o istuple_snd isom)" - by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_access_update_fst_snd: - "(f o istuple_fst isom) o (istuple_snd_update isom o h) g - = id o (f o istuple_fst isom)" - by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_access_update_snd_fst: - "(f o istuple_snd isom) o (istuple_fst_update isom o h) g - = id o (f o istuple_snd isom)" - by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_update_swap_fst_fst: - "\ h f o j g = j g o h f \ \ - (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g - = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f" - by (clarsimp simp: istuple_fst_update_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_update_swap_snd_snd: - "\ h f o j g = j g o h f \ \ - (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g - = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f" - by (clarsimp simp: istuple_snd_update_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_update_swap_fst_snd: - "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g - = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f" - by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_update_swap_snd_fst: - "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g - = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f" - by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps - intro!: ext elim!: o_eq_elim) - -lemma istuple_update_compose_fst_fst: - "\ h f o j g = k (f o g) \ \ - (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g - = (istuple_fst_update isom o k) (f o g)" - by (fastsimp simp: istuple_fst_update_def simps - intro!: ext elim!: o_eq_elim dest: fun_cong) - -lemma istuple_update_compose_snd_snd: - "\ h f o j g = k (f o g) \ \ - (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g - = (istuple_snd_update isom o k) (f o g)" - by (fastsimp simp: istuple_snd_update_def simps - intro!: ext elim!: o_eq_elim dest: fun_cong) - -lemma istuple_surjective_proof_assist_step: - "\ istuple_surjective_proof_assist v a (istuple_fst isom o f); - istuple_surjective_proof_assist v b (istuple_snd isom o f) \ - \ istuple_surjective_proof_assist v (istuple_cons isom a b) f" - by (clarsimp simp: istuple_surjective_proof_assist_def simps - istuple_fst_def istuple_snd_def istuple_cons_def) - -lemma istuple_fst_update_accessor_cong_assist: - "istuple_update_accessor_cong_assist f g \ - istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)" - by (clarsimp simp: istuple_update_accessor_cong_assist_def simps - istuple_fst_update_def istuple_fst_def) - -lemma istuple_snd_update_accessor_cong_assist: - "istuple_update_accessor_cong_assist f g \ - istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)" - by (clarsimp simp: istuple_update_accessor_cong_assist_def simps - istuple_snd_update_def istuple_snd_def) - -lemma istuple_fst_update_accessor_eq_assist: - "istuple_update_accessor_eq_assist f g a u a' v \ - istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom) - (istuple_cons isom a b) u (istuple_cons isom a' b) v" - by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def - istuple_update_accessor_cong_assist_def istuple_cons_def simps) - -lemma istuple_snd_update_accessor_eq_assist: - "istuple_update_accessor_eq_assist f g b u b' v \ - istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom) - (istuple_cons isom a b) u (istuple_cons isom a b') v" - by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def - istuple_update_accessor_cong_assist_def istuple_cons_def simps) - -lemma istuple_cons_conj_eqI: - "\ (a = c \ b = d \ P) = Q \ \ - (istuple_cons isom a b = istuple_cons isom c d \ P) = Q" - by (clarsimp simp: istuple_cons_def simps) - -lemmas intros = - istuple_access_update_fst_fst - istuple_access_update_snd_snd - istuple_access_update_fst_snd - istuple_access_update_snd_fst - istuple_update_swap_fst_fst - istuple_update_swap_snd_snd - istuple_update_swap_fst_snd - istuple_update_swap_snd_fst - istuple_update_compose_fst_fst - istuple_update_compose_snd_snd - istuple_surjective_proof_assist_step - istuple_fst_update_accessor_eq_assist - istuple_snd_update_accessor_eq_assist - istuple_fst_update_accessor_cong_assist - istuple_snd_update_accessor_cong_assist - istuple_cons_conj_eqI - -end - -lemma isomorphic_tuple_intro: - assumes repr_inj: "\x y. (repr x = repr y) = (x = y)" - and abst_inv: "\z. repr (abst z) = z" - shows "v \ TupleIsomorphism repr abst \ isomorphic_tuple v" - apply (rule isomorphic_tuple.intro, - simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse - tuple_isomorphism_def abst_inv) - apply (cut_tac x="abst (repr x)" and y="x" in repr_inj) - apply (simp add: abst_inv) - done - -constdefs - "tuple_istuple \ TupleIsomorphism id id" - -lemma tuple_istuple: - "isomorphic_tuple tuple_istuple" - by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def) - -lemma refl_conj_eq: - "Q = R \ (P \ Q) = (P \ R)" - by simp - -lemma meta_all_sameI: - "(\x. PROP P x \ PROP Q x) \ (\x. PROP P x) \ (\x. PROP Q x)" - by simp - -lemma istuple_UNIV_I: "\x. x\UNIV \ True" - by simp - -lemma istuple_True_simp: "(True \ PROP P) \ PROP P" - by simp - -use "Tools/istuple_support.ML"; - -end diff -r 5b65449d7669 -r f65d74a264dd src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Sep 22 13:52:19 2009 +1000 +++ b/src/HOL/Record.thy Wed Sep 23 19:17:48 2009 +1000 @@ -1,11 +1,12 @@ (* Title: HOL/Record.thy - Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen + Authors: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen + Thomas Sewell, NICTA *) header {* Extensible records with structural subtyping *} theory Record -imports Product_Type IsTuple +imports Product_Type uses ("Tools/record.ML") begin @@ -64,6 +65,402 @@ "_record_scheme" :: "[fields, 'a] => 'a" ("(3\_,/ (2\ =/ _)\)") "_record_update" :: "['a, updates] => 'b" ("_/(3\_\)" [900,0] 900) +subsection {* Operators and lemmas for types isomorphic to tuples *} + +text {* +Records are isomorphic to compound tuple types. To implement efficient +records, we make this isomorphism explicit. Consider the record +access/update simplification "alpha (beta_update f rec) = alpha rec" for +distinct fields alpha and beta of some record rec with n fields. There +are n^2 such theorems, which prohibits storage of all of them for +large n. The rules can be proved on the fly by case decomposition and +simplification in O(n) time. By creating O(n) isomorphic-tuple types +while defining the record, however, we can prove the access/update +simplification in O(log(n)^2) time. + +The O(n) cost of case decomposition is not because O(n) steps are taken, +but rather because the resulting rule must contain O(n) new variables and +an O(n) size concrete record construction. To sidestep this cost, we would +like to avoid case decomposition in proving access/update theorems. + +Record types are defined as isomorphic to tuple types. For instance, a +record type with fields 'a, 'b, 'c and 'd might be introduced as +isomorphic to 'a \ ('b \ ('c \ 'd)). If we balance the tuple tree to +('a \ 'b) \ ('c \ 'd) then accessors can be defined by converting to +the underlying type then using O(log(n)) fst or snd operations. +Updators can be defined similarly, if we introduce a fst_update and +snd_update function. Furthermore, we can prove the access/update +theorem in O(log(n)) steps by using simple rewrites on fst, snd, +fst_update and snd_update. + +The catch is that, although O(log(n)) steps were taken, the underlying +type we converted to is a tuple tree of size O(n). Processing this term +type wastes performance. We avoid this for large n by taking each +subtree of size K and defining a new type isomorphic to that tuple +subtree. A record can now be defined as isomorphic to a tuple tree +of these O(n/K) new types, or, if n > K*K, we can repeat the process, +until the record can be defined in terms of a tuple tree of complexity +less than the constant K. + +If we prove the access/update theorem on this type with the analagous +steps to the tuple tree, we consume O(log(n)^2) time as the intermediate +terms are O(log(n)) in size and the types needed have size bounded by K. +To enable this analagous traversal, we define the functions seen below: +istuple_fst, istuple_snd, istuple_fst_update and istuple_snd_update. +These functions generalise tuple operations by taking a parameter that +encapsulates a tuple isomorphism. The rewrites needed on these functions +now need an additional assumption which is that the isomorphism works. + +These rewrites are typically used in a structured way. They are here +presented as the introduction rule isomorphic_tuple.intros rather than +as a rewrite rule set. The introduction form is an optimisation, as net +matching can be performed at one term location for each step rather than +the simplifier searching the term for possible pattern matches. The rule +set is used as it is viewed outside the locale, with the locale assumption +(that the isomorphism is valid) left as a rule assumption. All rules are +structured to aid net matching, using either a point-free form or an +encapsulating predicate. +*} + +typedef ('a, 'b, 'c) tuple_isomorphism + = "UNIV :: (('a \ ('b \ 'c)) \ (('b \ 'c) \ 'a)) set" + by simp + +definition + "TupleIsomorphism repr abst = Abs_tuple_isomorphism (repr, abst)" + +definition + istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'b" +where + "istuple_fst isom \ let (repr, abst) = Rep_tuple_isomorphism isom in fst \ repr" + +definition + istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'c" +where + "istuple_snd isom \ let (repr, abst) = Rep_tuple_isomorphism isom in snd \ repr" + +definition + istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \ ('b \ 'b) \ ('a \ 'a)" +where + "istuple_fst_update isom \ + let (repr, abst) = Rep_tuple_isomorphism isom in + (\f v. abst (f (fst (repr v)), snd (repr v)))" + +definition + istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \ ('c \ 'c) \ ('a \ 'a)" +where + "istuple_snd_update isom \ + let (repr, abst) = Rep_tuple_isomorphism isom in + (\f v. abst (fst (repr v), f (snd (repr v))))" + +definition + istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \ 'b \ 'c \ 'a" +where + "istuple_cons isom \ let (repr, abst) = Rep_tuple_isomorphism isom in curry abst" + +text {* +These predicates are used in the introduction rule set to constrain +matching appropriately. The elimination rules for them produce the +desired theorems once they are proven. The final introduction rules are +used when no further rules from the introduction rule set can apply. +*} + +definition + istuple_surjective_proof_assist :: "'a \ 'b \ ('a \ 'b) \ bool" +where + "istuple_surjective_proof_assist x y f \ (f x = y)" + +definition + istuple_update_accessor_cong_assist :: "(('b \ 'b) \ ('a \ 'a)) + \ ('a \ 'b) \ bool" +where + "istuple_update_accessor_cong_assist upd acc + \ (\f v. upd (\x. f (acc v)) v = upd f v) + \ (\v. upd id v = v)" + +definition + istuple_update_accessor_eq_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) + \ 'a \ ('b \ 'b) \ 'a \ 'b \ bool" +where + "istuple_update_accessor_eq_assist upd acc v f v' x + \ upd f v = v' \ acc v = x + \ istuple_update_accessor_cong_assist upd acc" + +lemma update_accessor_congruence_foldE: + assumes uac: "istuple_update_accessor_cong_assist upd acc" + and r: "r = r'" and v: "acc r' = v'" + and f: "\v. v' = v \ f v = f' v" + shows "upd f r = upd f' r'" + using uac r v[symmetric] + apply (subgoal_tac "upd (\x. f (acc r')) r' = upd (\x. f' (acc r')) r'") + apply (simp add: istuple_update_accessor_cong_assist_def) + apply (simp add: f) + done + +lemma update_accessor_congruence_unfoldE: + "\ istuple_update_accessor_cong_assist upd acc; + r = r'; acc r' = v'; \v. v = v' \ f v = f' v \ + \ upd f r = upd f' r'" + apply (erule(2) update_accessor_congruence_foldE) + apply simp + done + +lemma istuple_update_accessor_cong_assist_id: + "istuple_update_accessor_cong_assist upd acc \ upd id = id" + by (rule ext, simp add: istuple_update_accessor_cong_assist_def) + +lemma update_accessor_noopE: + assumes uac: "istuple_update_accessor_cong_assist upd acc" + and acc: "f (acc x) = acc x" + shows "upd f x = x" + using uac + by (simp add: acc istuple_update_accessor_cong_assist_id[OF uac, unfolded id_def] + cong: update_accessor_congruence_unfoldE[OF uac]) + +lemma update_accessor_noop_compE: + assumes uac: "istuple_update_accessor_cong_assist upd acc" + assumes acc: "f (acc x) = acc x" + shows "upd (g \ f) x = upd g x" + by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac]) + +lemma update_accessor_cong_assist_idI: + "istuple_update_accessor_cong_assist id id" + by (simp add: istuple_update_accessor_cong_assist_def) + +lemma update_accessor_cong_assist_triv: + "istuple_update_accessor_cong_assist upd acc + \ istuple_update_accessor_cong_assist upd acc" + by assumption + +lemma update_accessor_accessor_eqE: + "\ istuple_update_accessor_eq_assist upd acc v f v' x \ \ acc v = x" + by (simp add: istuple_update_accessor_eq_assist_def) + +lemma update_accessor_updator_eqE: + "\ istuple_update_accessor_eq_assist upd acc v f v' x \ \ upd f v = v'" + by (simp add: istuple_update_accessor_eq_assist_def) + +lemma istuple_update_accessor_eq_assist_idI: + "v' = f v \ istuple_update_accessor_eq_assist id id v f v' v" + by (simp add: istuple_update_accessor_eq_assist_def + update_accessor_cong_assist_idI) + +lemma istuple_update_accessor_eq_assist_triv: + "istuple_update_accessor_eq_assist upd acc v f v' x + \ istuple_update_accessor_eq_assist upd acc v f v' x" + by assumption + +lemma istuple_update_accessor_cong_from_eq: + "istuple_update_accessor_eq_assist upd acc v f v' x + \ istuple_update_accessor_cong_assist upd acc" + by (simp add: istuple_update_accessor_eq_assist_def) + +lemma o_eq_dest: + "a o b = c o d \ a (b v) = c (d v)" + apply (clarsimp simp: o_def) + apply (erule fun_cong) + done + +lemma o_eq_elim: + "\ a o b = c o d; \ \v. a (b v) = c (d v) \ \ R \ \ R" + apply (erule meta_mp) + apply (erule o_eq_dest) + done + +lemma istuple_surjective_proof_assistI: + "f x = y \ + istuple_surjective_proof_assist x y f" + by (simp add: istuple_surjective_proof_assist_def) + +lemma istuple_surjective_proof_assist_idE: + "istuple_surjective_proof_assist x y id \ x = y" + by (simp add: istuple_surjective_proof_assist_def) + +locale isomorphic_tuple = + fixes isom :: "('a, 'b, 'c) tuple_isomorphism" + and repr and abst + defines "repr \ fst (Rep_tuple_isomorphism isom)" + defines "abst \ snd (Rep_tuple_isomorphism isom)" + assumes repr_inv: "\x. abst (repr x) = x" + assumes abst_inv: "\y. repr (abst y) = y" + +begin + +lemma repr_inj: + "(repr x = repr y) = (x = y)" + apply (rule iffI, simp_all) + apply (drule_tac f=abst in arg_cong, simp add: repr_inv) + done + +lemma abst_inj: + "(abst x = abst y) = (x = y)" + apply (rule iffI, simp_all) + apply (drule_tac f=repr in arg_cong, simp add: abst_inv) + done + +lemma split_Rep: + "split f (Rep_tuple_isomorphism isom) + = f repr abst" + by (simp add: split_def repr_def abst_def) + +lemmas simps = Let_def split_Rep repr_inv abst_inv repr_inj abst_inj + +lemma istuple_access_update_fst_fst: + "\ f o h g = j o f \ \ + (f o istuple_fst isom) o (istuple_fst_update isom o h) g + = j o (f o istuple_fst isom)" + by (clarsimp simp: istuple_fst_update_def istuple_fst_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_access_update_snd_snd: + "\ f o h g = j o f \ \ + (f o istuple_snd isom) o (istuple_snd_update isom o h) g + = j o (f o istuple_snd isom)" + by (clarsimp simp: istuple_snd_update_def istuple_snd_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_access_update_fst_snd: + "(f o istuple_fst isom) o (istuple_snd_update isom o h) g + = id o (f o istuple_fst isom)" + by (clarsimp simp: istuple_snd_update_def istuple_fst_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_access_update_snd_fst: + "(f o istuple_snd isom) o (istuple_fst_update isom o h) g + = id o (f o istuple_snd isom)" + by (clarsimp simp: istuple_fst_update_def istuple_snd_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_update_swap_fst_fst: + "\ h f o j g = j g o h f \ \ + (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g + = (istuple_fst_update isom o j) g o (istuple_fst_update isom o h) f" + by (clarsimp simp: istuple_fst_update_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_update_swap_snd_snd: + "\ h f o j g = j g o h f \ \ + (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g + = (istuple_snd_update isom o j) g o (istuple_snd_update isom o h) f" + by (clarsimp simp: istuple_snd_update_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_update_swap_fst_snd: + "(istuple_snd_update isom o h) f o (istuple_fst_update isom o j) g + = (istuple_fst_update isom o j) g o (istuple_snd_update isom o h) f" + by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_update_swap_snd_fst: + "(istuple_fst_update isom o h) f o (istuple_snd_update isom o j) g + = (istuple_snd_update isom o j) g o (istuple_fst_update isom o h) f" + by (clarsimp simp: istuple_fst_update_def istuple_snd_update_def simps + intro!: ext elim!: o_eq_elim) + +lemma istuple_update_compose_fst_fst: + "\ h f o j g = k (f o g) \ \ + (istuple_fst_update isom o h) f o (istuple_fst_update isom o j) g + = (istuple_fst_update isom o k) (f o g)" + by (fastsimp simp: istuple_fst_update_def simps + intro!: ext elim!: o_eq_elim dest: fun_cong) + +lemma istuple_update_compose_snd_snd: + "\ h f o j g = k (f o g) \ \ + (istuple_snd_update isom o h) f o (istuple_snd_update isom o j) g + = (istuple_snd_update isom o k) (f o g)" + by (fastsimp simp: istuple_snd_update_def simps + intro!: ext elim!: o_eq_elim dest: fun_cong) + +lemma istuple_surjective_proof_assist_step: + "\ istuple_surjective_proof_assist v a (istuple_fst isom o f); + istuple_surjective_proof_assist v b (istuple_snd isom o f) \ + \ istuple_surjective_proof_assist v (istuple_cons isom a b) f" + by (clarsimp simp: istuple_surjective_proof_assist_def simps + istuple_fst_def istuple_snd_def istuple_cons_def) + +lemma istuple_fst_update_accessor_cong_assist: + "istuple_update_accessor_cong_assist f g \ + istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)" + by (clarsimp simp: istuple_update_accessor_cong_assist_def simps + istuple_fst_update_def istuple_fst_def) + +lemma istuple_snd_update_accessor_cong_assist: + "istuple_update_accessor_cong_assist f g \ + istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)" + by (clarsimp simp: istuple_update_accessor_cong_assist_def simps + istuple_snd_update_def istuple_snd_def) + +lemma istuple_fst_update_accessor_eq_assist: + "istuple_update_accessor_eq_assist f g a u a' v \ + istuple_update_accessor_eq_assist (istuple_fst_update isom o f) (g o istuple_fst isom) + (istuple_cons isom a b) u (istuple_cons isom a' b) v" + by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_fst_update_def istuple_fst_def + istuple_update_accessor_cong_assist_def istuple_cons_def simps) + +lemma istuple_snd_update_accessor_eq_assist: + "istuple_update_accessor_eq_assist f g b u b' v \ + istuple_update_accessor_eq_assist (istuple_snd_update isom o f) (g o istuple_snd isom) + (istuple_cons isom a b) u (istuple_cons isom a b') v" + by (clarsimp simp: istuple_update_accessor_eq_assist_def istuple_snd_update_def istuple_snd_def + istuple_update_accessor_cong_assist_def istuple_cons_def simps) + +lemma istuple_cons_conj_eqI: + "\ (a = c \ b = d \ P) = Q \ \ + (istuple_cons isom a b = istuple_cons isom c d \ P) = Q" + by (clarsimp simp: istuple_cons_def simps) + +lemmas intros = + istuple_access_update_fst_fst + istuple_access_update_snd_snd + istuple_access_update_fst_snd + istuple_access_update_snd_fst + istuple_update_swap_fst_fst + istuple_update_swap_snd_snd + istuple_update_swap_fst_snd + istuple_update_swap_snd_fst + istuple_update_compose_fst_fst + istuple_update_compose_snd_snd + istuple_surjective_proof_assist_step + istuple_fst_update_accessor_eq_assist + istuple_snd_update_accessor_eq_assist + istuple_fst_update_accessor_cong_assist + istuple_snd_update_accessor_cong_assist + istuple_cons_conj_eqI + +end + +lemma isomorphic_tuple_intro: + assumes repr_inj: "\x y. (repr x = repr y) = (x = y)" + and abst_inv: "\z. repr (abst z) = z" + shows "v \ TupleIsomorphism repr abst \ isomorphic_tuple v" + apply (rule isomorphic_tuple.intro, + simp_all add: TupleIsomorphism_def Abs_tuple_isomorphism_inverse + tuple_isomorphism_def abst_inv) + apply (cut_tac x="abst (repr x)" and y="x" in repr_inj) + apply (simp add: abst_inv) + done + +definition + "tuple_istuple \ TupleIsomorphism id id" + +lemma tuple_istuple: + "isomorphic_tuple tuple_istuple" + by (simp add: isomorphic_tuple_intro[OF _ _ reflexive] tuple_istuple_def) + +lemma refl_conj_eq: + "Q = R \ (P \ Q) = (P \ R)" + by simp + +lemma meta_all_sameI: + "(\x. PROP P x \ PROP Q x) \ (\x. PROP P x) \ (\x. PROP Q x)" + by simp + +lemma istuple_UNIV_I: "\x. x\UNIV \ True" + by simp + +lemma istuple_True_simp: "(True \ PROP P) \ PROP P" + by simp + use "Tools/record.ML" setup Record.setup diff -r 5b65449d7669 -r f65d74a264dd src/HOL/Tools/istuple_support.ML --- a/src/HOL/Tools/istuple_support.ML Tue Sep 22 13:52:19 2009 +1000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,149 +0,0 @@ -(* Title: HOL/Tools/ntuple_support.ML - Author: Thomas Sewell, NICTA - -Support for defining instances of tuple-like types and supplying -introduction rules needed by the record package. -*) - - -signature ISTUPLE_SUPPORT = -sig - val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> - (term * term * theory); - - val mk_cons_tuple: term * term -> term; - val dest_cons_tuple: term -> term * term; - - val istuple_intros_tac: theory -> int -> tactic; - - val named_cterm_instantiate: (string * cterm) list -> thm -> thm; -end; - -structure IsTupleSupport : ISTUPLE_SUPPORT = -struct - -val isomN = "_TupleIsom"; -val defN = "_def"; - -val istuple_UNIV_I = @{thm "istuple_UNIV_I"}; -val istuple_True_simp = @{thm "istuple_True_simp"}; - -val istuple_intro = @{thm "isomorphic_tuple_intro"}; -val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"}); - -val constname = fst o dest_Const; -val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple}); - -val istuple_constN = constname @{term isomorphic_tuple}; -val istuple_consN = constname @{term istuple_cons}; - -val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"}); - -fun named_cterm_instantiate values thm = let - fun match name (Var ((name', _), _)) = name = name' - | match name _ = false; - fun getvar name = case (find_first (match name) - (OldTerm.term_vars (prop_of thm))) - of SOME var => cterm_of (theory_of_thm thm) var - | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]) - in - cterm_instantiate (map (apfst getvar) values) thm - end; - -structure IsTupleThms = TheoryDataFun -( - type T = thm Symtab.table; - val empty = Symtab.make [tuple_istuple]; - val copy = I; - val extend = I; - val merge = K (Symtab.merge Thm.eq_thm_prop); -); - -fun do_typedef name repT alphas thy = - let - fun get_thms thy name = - let - val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT, - Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name; - val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp]; - in (map rewrite_rule [rep_inject, abs_inverse], - Const (absN, repT --> absT), absT) end; - in - thy - |> Typecopy.typecopy (Binding.name name, alphas) repT NONE - |-> (fn (name, _) => `(fn thy => get_thms thy name)) - end; - -fun mk_cons_tuple (left, right) = let - val (leftT, rightT) = (fastype_of left, fastype_of right); - val prodT = HOLogic.mk_prodT (leftT, rightT); - val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]); - in - Const (istuple_consN, isomT --> leftT --> rightT --> prodT) - $ Const (fst tuple_istuple, isomT) $ left $ right - end; - -fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) - = if ic = istuple_consN then (left, right) - else raise TERM ("dest_cons_tuple", [v]) - | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]); - -fun add_istuple_type (name, alphas) (leftT, rightT) thy = -let - val repT = HOLogic.mk_prodT (leftT, rightT); - - val (([rep_inject, abs_inverse], absC, absT), typ_thy) = - thy - |> do_typedef name repT alphas - ||> Sign.add_path name; - - (* construct a type and body for the isomorphism constant by - instantiating the theorem to which the definition will be applied *) - val intro_inst = rep_inject RS - (named_cterm_instantiate [("abst", cterm_of typ_thy absC)] - istuple_intro); - val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); - val isomT = fastype_of body; - val isomBind = Binding.name (name ^ isomN); - val isom = Const (Sign.full_name typ_thy isomBind, isomT); - val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body)); - - val ([isom_def], cdef_thy) = - typ_thy - |> Sign.add_consts_i [Syntax.no_syn (isomBind, isomT)] - |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; - - val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro)); - val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT) - - val thm_thy = - cdef_thy - |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop - (constname isom, istuple)) - |> Sign.parent_path; -in - (isom, cons $ isom, thm_thy) -end; - -fun istuple_intros_tac thy = let - val isthms = IsTupleThms.get thy; - fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]); - val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let - val goal' = Envir.beta_eta_contract goal; - val isom = case goal' of (Const tp $ (Const pr $ Const is)) - => if fst tp = "Trueprop" andalso fst pr = istuple_constN - then Const is - else err "unexpected goal predicate" goal' - | _ => err "unexpected goal format" goal'; - val isthm = case Symtab.lookup isthms (constname isom) of - SOME isthm => isthm - | NONE => err "no thm found for constant" isom; - in rtac isthm n end); - in - fn n => resolve_from_net_tac istuple_intros n - THEN use_istuple_thm_tac n - end; - -end; - - diff -r 5b65449d7669 -r f65d74a264dd src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Tue Sep 22 13:52:19 2009 +1000 +++ b/src/HOL/Tools/record.ML Wed Sep 23 19:17:48 2009 +1000 @@ -52,6 +52,146 @@ end; +signature ISTUPLE_SUPPORT = +sig + val add_istuple_type: bstring * string list -> (typ * typ) -> theory -> + (term * term * theory); + + val mk_cons_tuple: term * term -> term; + val dest_cons_tuple: term -> term * term; + + val istuple_intros_tac: theory -> int -> tactic; + + val named_cterm_instantiate: (string * cterm) list -> thm -> thm; +end; + +structure IsTupleSupport : ISTUPLE_SUPPORT = +struct + +val isomN = "_TupleIsom"; +val defN = "_def"; + +val istuple_UNIV_I = @{thm "istuple_UNIV_I"}; +val istuple_True_simp = @{thm "istuple_True_simp"}; + +val istuple_intro = @{thm "isomorphic_tuple_intro"}; +val istuple_intros = build_net (@{thms "isomorphic_tuple.intros"}); + +val constname = fst o dest_Const; +val tuple_istuple = (constname @{term tuple_istuple}, @{thm tuple_istuple}); + +val istuple_constN = constname @{term isomorphic_tuple}; +val istuple_consN = constname @{term istuple_cons}; + +val tup_isom_typeN = fst (dest_Type @{typ "('a, 'b, 'c) tuple_isomorphism"}); + +fun named_cterm_instantiate values thm = let + fun match name (Var ((name', _), _)) = name = name' + | match name _ = false; + fun getvar name = case (find_first (match name) + (OldTerm.term_vars (prop_of thm))) + of SOME var => cterm_of (theory_of_thm thm) var + | NONE => raise THM ("named_cterm_instantiate: " ^ name, 0, [thm]) + in + cterm_instantiate (map (apfst getvar) values) thm + end; + +structure IsTupleThms = TheoryDataFun +( + type T = thm Symtab.table; + val empty = Symtab.make [tuple_istuple]; + val copy = I; + val extend = I; + val merge = K (Symtab.merge Thm.eq_thm_prop); +); + +fun do_typedef name repT alphas thy = + let + fun get_thms thy name = + let + val SOME { Rep_inject=rep_inject, Abs_name=absN, abs_type=absT, + Abs_inverse=abs_inverse, ...} = Typedef.get_info thy name; + val rewrite_rule = MetaSimplifier.rewrite_rule [istuple_UNIV_I, istuple_True_simp]; + in (map rewrite_rule [rep_inject, abs_inverse], + Const (absN, repT --> absT), absT) end; + in + thy + |> Typecopy.typecopy (Binding.name name, alphas) repT NONE + |-> (fn (name, _) => `(fn thy => get_thms thy name)) + end; + +fun mk_cons_tuple (left, right) = let + val (leftT, rightT) = (fastype_of left, fastype_of right); + val prodT = HOLogic.mk_prodT (leftT, rightT); + val isomT = Type (tup_isom_typeN, [prodT, leftT, rightT]); + in + Const (istuple_consN, isomT --> leftT --> rightT --> prodT) + $ Const (fst tuple_istuple, isomT) $ left $ right + end; + +fun dest_cons_tuple (v as Const (ic, _) $ Const _ $ left $ right) + = if ic = istuple_consN then (left, right) + else raise TERM ("dest_cons_tuple", [v]) + | dest_cons_tuple v = raise TERM ("dest_cons_tuple", [v]); + +fun add_istuple_type (name, alphas) (leftT, rightT) thy = +let + val repT = HOLogic.mk_prodT (leftT, rightT); + + val (([rep_inject, abs_inverse], absC, absT), typ_thy) = + thy + |> do_typedef name repT alphas + ||> Sign.add_path name; + + (* construct a type and body for the isomorphism constant by + instantiating the theorem to which the definition will be applied *) + val intro_inst = rep_inject RS + (named_cterm_instantiate [("abst", cterm_of typ_thy absC)] + istuple_intro); + val (_, body) = Logic.dest_equals (List.last (prems_of intro_inst)); + val isomT = fastype_of body; + val isom_bind = Binding.name (name ^ isomN); + val isom = Const (Sign.full_name typ_thy isom_bind, isomT); + val isom_spec = (name ^ isomN ^ defN, Logic.mk_equals (isom, body)); + + val ([isom_def], cdef_thy) = + typ_thy + |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)] + |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)]; + + val istuple = isom_def RS (abs_inverse RS (rep_inject RS istuple_intro)); + val cons = Const (istuple_consN, isomT --> leftT --> rightT --> absT) + + val thm_thy = + cdef_thy + |> IsTupleThms.map (Symtab.insert Thm.eq_thm_prop + (constname isom, istuple)) + |> Sign.parent_path; +in + (isom, cons $ isom, thm_thy) +end; + +fun istuple_intros_tac thy = let + val isthms = IsTupleThms.get thy; + fun err s t = raise TERM ("istuple_intros_tac: " ^ s, [t]); + val use_istuple_thm_tac = SUBGOAL (fn (goal, n) => let + val goal' = Envir.beta_eta_contract goal; + val isom = case goal' of (Const tp $ (Const pr $ Const is)) + => if fst tp = "Trueprop" andalso fst pr = istuple_constN + then Const is + else err "unexpected goal predicate" goal' + | _ => err "unexpected goal format" goal'; + val isthm = case Symtab.lookup isthms (constname isom) of + SOME isthm => isthm + | NONE => err "no thm found for constant" isom; + in rtac isthm n end); + in + fn n => resolve_from_net_tac istuple_intros n + THEN use_istuple_thm_tac n + end; + +end; + structure Record: RECORD = struct @@ -68,6 +208,7 @@ val o_assoc = @{thm "o_assoc"}; val id_apply = @{thm id_apply}; val id_o_apps = [@{thm id_apply}, @{thm id_o}, @{thm o_id}]; +val Not_eq_iff = @{thm Not_eq_iff}; val refl_conj_eq = thm "refl_conj_eq"; val meta_all_sameI = thm "meta_all_sameI"; @@ -966,14 +1107,14 @@ val T = range_type (fastype_of f); in mk_comp (Const ("Fun.id", T --> T)) f end; -fun get_updfuns (upd $ _ $ t) = upd :: get_updfuns t - | get_updfuns _ = []; +fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t + | get_upd_funs _ = []; fun get_accupd_simps thy term defset intros_tac = let val (acc, [body]) = strip_comb term; val recT = domain_type (fastype_of acc); - val updfuns = sort_distinct TermOrd.fast_term_ord - (get_updfuns body); + val upd_funs = sort_distinct TermOrd.fast_term_ord + (get_upd_funs body); fun get_simp upd = let val T = domain_type (fastype_of upd); val lhs = mk_comp acc (upd $ Free ("f", T)); @@ -987,7 +1128,7 @@ val dest = if is_sel_upd_pair thy acc upd then o_eq_dest else o_eq_id_dest; in standard (othm RS dest) end; - in map get_simp updfuns end; + in map get_simp upd_funs end; structure SymSymTab = Table(type key = string * string val ord = prod_ord fast_string_ord fast_string_ord); @@ -1009,26 +1150,26 @@ fun get_updupd_simps thy term defset intros_tac = let val recT = fastype_of term; - val updfuns = get_updfuns term; + val upd_funs = get_upd_funs term; val cname = fst o dest_Const; fun getswap u u' = get_updupd_simp thy defset intros_tac u u' (cname u = cname u'); - fun buildswapstoeq upd [] swaps = swaps - | buildswapstoeq upd (u::us) swaps = let + fun build_swaps_to_eq upd [] swaps = swaps + | build_swaps_to_eq upd (u::us) swaps = let val key = (cname u, cname upd); val newswaps = if SymSymTab.defined swaps key then swaps else SymSymTab.insert (K true) (key, getswap u upd) swaps; in if cname u = cname upd then newswaps - else buildswapstoeq upd us newswaps end; - fun swapsneeded [] prev seen swaps = map snd (SymSymTab.dest swaps) - | swapsneeded (u::us) prev seen swaps = + else build_swaps_to_eq upd us newswaps end; + fun swaps_needed [] prev seen swaps = map snd (SymSymTab.dest swaps) + | swaps_needed (u::us) prev seen swaps = if Symtab.defined seen (cname u) - then swapsneeded us prev seen - (buildswapstoeq u prev swaps) - else swapsneeded us (u::prev) + then swaps_needed us prev seen + (build_swaps_to_eq u prev swaps) + else swaps_needed us (u::prev) (Symtab.insert (K true) (cname u, ()) seen) swaps; - in swapsneeded updfuns [] Symtab.empty SymSymTab.empty end; + in swaps_needed upd_funs [] Symtab.empty SymSymTab.empty end; val named_cterm_instantiate = IsTupleSupport.named_cterm_instantiate; @@ -2222,14 +2363,13 @@ fun split_ex_prf () = let - val ss = HOL_basic_ss addsimps [not_ex RS sym, nth simp_thms 1]; - val [Pv] = OldTerm.term_vars (prop_of split_object); - val cPv = cterm_of defs_thy Pv; - val cP = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0))); - val so3 = cterm_instantiate ([(cPv, cP)]) split_object; - val so4 = simplify ss so3; + val ss = HOL_basic_ss addsimps [not_ex RS sym, Not_eq_iff]; + val P_nm = fst (dest_Free P); + val not_P = cterm_of defs_thy (lambda r0 (HOLogic.mk_not (P $ r0))); + val so' = named_cterm_instantiate ([(P_nm, not_P)]) split_object; + val so'' = simplify ss so'; in - prove_standard [] split_ex_prop (fn prems => resolve_tac [so4] 1) + prove_standard [] split_ex_prop (fn prems => resolve_tac [so''] 1) end; val split_ex = timeit_msg "record split_ex proof:" split_ex_prf;