# HG changeset patch # User huffman # Date 1315959919 25200 # Node ID 14f7da460ce87cd04ba53e3f73c456012ba58ecd # Parent 58eef4843641234fb6b36b22a53590f5ca3cd627 tuned proofs diff -r 58eef4843641 -r 14f7da460ce8 src/HOL/Record.thy --- a/src/HOL/Record.thy Tue Sep 13 17:07:33 2011 -0700 +++ b/src/HOL/Record.thy Tue Sep 13 17:25:19 2011 -0700 @@ -55,9 +55,9 @@ 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)"} + analogous 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 + the types needed have size bounded by K. To enable this analogous traversal, we define the functions seen below: @{text "iso_tuple_fst"}, @{text "iso_tuple_snd"}, @{text "iso_tuple_fst_update"} and @{text "iso_tuple_snd_update"}. These functions generalise tuple @@ -229,61 +229,62 @@ (f o iso_tuple_fst isom) o (iso_tuple_fst_update isom o h) g = j o (f o iso_tuple_fst isom)" by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_fst_def simps - intro!: ext elim!: o_eq_elim) + fun_eq_iff) lemma iso_tuple_access_update_snd_snd: "f o h g = j o f \ (f o iso_tuple_snd isom) o (iso_tuple_snd_update isom o h) g = j o (f o iso_tuple_snd isom)" by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_snd_def simps - intro!: ext elim!: o_eq_elim) + fun_eq_iff) lemma iso_tuple_access_update_fst_snd: "(f o iso_tuple_fst isom) o (iso_tuple_snd_update isom o h) g = id o (f o iso_tuple_fst isom)" by (clarsimp simp: iso_tuple_snd_update_def iso_tuple_fst_def simps - intro!: ext elim!: o_eq_elim) + fun_eq_iff) lemma iso_tuple_access_update_snd_fst: "(f o iso_tuple_snd isom) o (iso_tuple_fst_update isom o h) g = id o (f o iso_tuple_snd isom)" by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_def simps - intro!: ext elim!: o_eq_elim) + fun_eq_iff) lemma iso_tuple_update_swap_fst_fst: "h f o j g = j g o h f \ (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g = (iso_tuple_fst_update isom o j) g o (iso_tuple_fst_update isom o h) f" - by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext) + by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff) lemma iso_tuple_update_swap_snd_snd: "h f o j g = j g o h f \ (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g = (iso_tuple_snd_update isom o j) g o (iso_tuple_snd_update isom o h) f" - by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext) + by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff) lemma iso_tuple_update_swap_fst_snd: "(iso_tuple_snd_update isom o h) f o (iso_tuple_fst_update isom o j) g = (iso_tuple_fst_update isom o j) g o (iso_tuple_snd_update isom o h) f" by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def - simps intro!: ext) + simps fun_eq_iff) lemma iso_tuple_update_swap_snd_fst: "(iso_tuple_fst_update isom o h) f o (iso_tuple_snd_update isom o j) g = (iso_tuple_snd_update isom o j) g o (iso_tuple_fst_update isom o h) f" - by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps intro!: ext) + by (clarsimp simp: iso_tuple_fst_update_def iso_tuple_snd_update_def simps + fun_eq_iff) lemma iso_tuple_update_compose_fst_fst: "h f o j g = k (f o g) \ (iso_tuple_fst_update isom o h) f o (iso_tuple_fst_update isom o j) g = (iso_tuple_fst_update isom o k) (f o g)" - by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose intro!: ext) + by (clarsimp simp: iso_tuple_fst_update_def simps apfst_compose fun_eq_iff) lemma iso_tuple_update_compose_snd_snd: "h f o j g = k (f o g) \ (iso_tuple_snd_update isom o h) f o (iso_tuple_snd_update isom o j) g = (iso_tuple_snd_update isom o k) (f o g)" - by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose intro!: ext) + by (clarsimp simp: iso_tuple_snd_update_def simps apsnd_compose fun_eq_iff) lemma iso_tuple_surjective_proof_assist_step: "iso_tuple_surjective_proof_assist v a (iso_tuple_fst isom o f) \