diff -r 357f74e0090c -r 7264824baf66 src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Nov 10 16:11:39 2009 +0100 +++ b/src/HOL/Record.thy Tue Nov 10 16:11:43 2009 +0100 @@ -3,15 +3,386 @@ Author: Markus Wenzel, TU Muenchen Author: Norbert Schirmer, TU Muenchen Author: Thomas Sewell, NICTA + Author: Florian Haftmann, TU Muenchen *) header {* Extensible records with structural subtyping *} theory Record -imports Product_Type +imports Datatype uses ("Tools/record.ML") begin +subsection {* Introduction *} + +text {* + Records are isomorphic to compound tuple types. To implement + efficient records, we make this isomorphism explicit. Consider the + record access/update simplification @{text "alpha (beta_update f + rec) = alpha rec"} for distinct fields alpha and beta of some record + rec with n fields. There are @{text "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 + @{text "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 @{text "'a"}, @{text "'b"}, @{text "'c"} + and @{text "'d"} might be introduced as isomorphic to @{text "'a \ + ('b \ ('c \ 'd))"}. If we balance the tuple tree to @{text "('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 @{text + "fst_update"} and @{text "snd_update"} function. Furthermore, we can + prove the access/update theorem in O(log(n)) steps by using simple + rewrites on fst, snd, @{text "fst_update"} and @{text "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 @{text + "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 @{text "O(log(n)^2)"} + time as the intermediate terms are @{text "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: @{text + "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"} + and @{text "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 @{text "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. +*} + +subsection {* Operators and lemmas for types isomorphic to tuples *} + +datatype ('a, 'b, 'c) tuple_isomorphism = TupleIsomorphism "'a \ 'b \ 'c" "'b \ 'c \ 'a" + +primrec repr :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'b \ 'c" where + "repr (TupleIsomorphism r a) = r" + +primrec abst :: "('a, 'b, 'c) tuple_isomorphism \ 'b \ 'c \ 'a" where + "abst (TupleIsomorphism r a) = a" + +definition istuple_fst :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'b" where + "istuple_fst isom = fst \ repr isom" + +definition istuple_snd :: "('a, 'b, 'c) tuple_isomorphism \ 'a \ 'c" where + "istuple_snd isom = snd \ repr isom" + +definition istuple_fst_update :: "('a, 'b, 'c) tuple_isomorphism \ ('b \ 'b) \ ('a \ 'a)" where + "istuple_fst_update isom f = abst isom \ apfst f \ repr isom" + +definition istuple_snd_update :: "('a, 'b, 'c) tuple_isomorphism \ ('c \ 'c) \ ('a \ 'a)" where + "istuple_snd_update isom f = abst isom \ apsnd f \ repr isom" + +definition istuple_cons :: "('a, 'b, 'c) tuple_isomorphism \ 'b \ 'c \ 'a" where + "istuple_cons isom = curry (abst isom)" + + +subsection {* Logical infrastructure for records *} + +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 (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 \ Record.repr isom" + defines "abst \ Record.abst 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 + +lemmas simps = Let_def repr_inv abst_inv repr_inj abst_inj repr_def [symmetric] abst_def [symmetric] + +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 apfst_compose intro!: ext) + +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 apsnd_compose intro!: ext) + +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) + +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) + +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 (clarsimp simp: istuple_fst_update_def simps apfst_compose intro!: ext) + +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 (clarsimp simp: istuple_snd_update_def simps apsnd_compose intro!: ext) + +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: + assumes "istuple_update_accessor_cong_assist f g" + shows "istuple_update_accessor_cong_assist (istuple_fst_update isom o f) (g o istuple_fst isom)" +proof - + from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id) + with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps + istuple_fst_update_def istuple_fst_def) +qed + +lemma istuple_snd_update_accessor_cong_assist: + assumes "istuple_update_accessor_cong_assist f g" + shows "istuple_update_accessor_cong_assist (istuple_snd_update isom o f) (g o istuple_snd isom)" +proof - + from assms have "f id = id" by (rule istuple_update_accessor_cong_assist_id) + with assms show ?thesis by (clarsimp simp: istuple_update_accessor_cong_assist_def simps + istuple_snd_update_def istuple_snd_def) +qed + +lemma istuple_fst_update_accessor_eq_assist: + assumes "istuple_update_accessor_eq_assist f g a u a' v" + shows "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" +proof - + from assms have "f id = id" + by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id) + with assms show ?thesis 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) +qed + +lemma istuple_snd_update_accessor_eq_assist: + assumes "istuple_update_accessor_eq_assist f g b u b' v" + shows "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" +proof - + from assms have "f id = id" + by (auto simp add: istuple_update_accessor_eq_assist_def intro: istuple_update_accessor_cong_assist_id) + with assms show ?thesis 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) +qed + +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: + fixes repr abst + assumes repr_inj: "\x y. repr x = repr y \ x = y" + and abst_inv: "\z. repr (abst z) = z" + assumes v: "v \ TupleIsomorphism repr abst" + shows "isomorphic_tuple v" + apply (rule isomorphic_tuple.intro) + apply (simp_all add: abst_inv v) + 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 istuple_UNIV_I: "x \ UNIV \ True" + by simp + +lemma istuple_True_simp: "(True \ PROP P) \ PROP P" + by simp + lemma prop_subst: "s = t \ PROP P t \ PROP P s" by simp @@ -22,14 +393,11 @@ "a o b = c \ a (b v) = c v" by clarsimp -lemma id_o_refl: - "id o f = f o id" - by simp - lemma o_eq_id_dest: "a o b = id o c \ a (b v) = c v" by clarsimp + subsection {* Concrete record syntax *} nonterminals @@ -63,400 +431,15 @@ "_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 @{text "alpha (beta_update f rec) = alpha rec"} for -distinct fields alpha and beta of some record rec with n fields. There -are @{text "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 @{text "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 @{text "'a \ ('b \ ('c \ 'd))"}. If we balance the tuple tree to -@{text "('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 @{text "fst_update"} and -@{text "snd_update"} function. Furthermore, we can prove the access/update -theorem in O(log(n)) steps by using simple rewrites on fst, snd, -@{text "fst_update"} and @{text "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 @{text "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 @{text "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: -@{text "istuple_fst"}, @{text "istuple_snd"}, @{text "istuple_fst_update"} -and @{text "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 @{text "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 istuple_UNIV_I: "\x. x\UNIV \ True" - by simp - -lemma istuple_True_simp: "(True \ PROP P) \ PROP P" - by simp +subsection {* Record package *} use "Tools/record.ML" setup Record.setup +hide (open) const TupleIsomorphism repr abst istuple_fst istuple_snd + istuple_fst_update istuple_snd_update istuple_cons + istuple_surjective_proof_assist istuple_update_accessor_cong_assist + istuple_update_accessor_eq_assist tuple_istuple + end