# HG changeset patch # User haftmann # Date 1281628603 -7200 # Node ID 3142c1e21a0e25fe46a3bfc718ee593df0612cf6 # Parent 7c045c03598f6eb3e175e8c83b068eb918cb9f5b moved Record.thy from session Plain to Main; avoid variable name acc diff -r 7c045c03598f -r 3142c1e21a0e src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 12 17:56:41 2010 +0200 +++ b/src/HOL/IsaMakefile Thu Aug 12 17:56:43 2010 +0200 @@ -207,14 +207,12 @@ Tools/old_primrec.ML \ Tools/primrec.ML \ Tools/prop_logic.ML \ - Tools/record.ML \ Tools/refute.ML \ Tools/refute_isar.ML \ Tools/rewrite_hol_proof.ML \ Tools/sat_funcs.ML \ Tools/sat_solver.ML \ Tools/split_rule.ML \ - Tools/typecopy.ML \ Tools/typedef_codegen.ML \ Tools/typedef.ML \ Transitive_Closure.thy \ @@ -305,6 +303,7 @@ Tools/Predicate_Compile/predicate_compile_specialisation.ML \ Tools/Predicate_Compile/predicate_compile_pred.ML \ Tools/quickcheck_generators.ML \ + Tools/quickcheck_record.ML \ Tools/Qelim/cooper.ML \ Tools/Qelim/cooper_procedure.ML \ Tools/Qelim/qelim.ML \ @@ -314,6 +313,7 @@ Tools/Quotient/quotient_term.ML \ Tools/Quotient/quotient_typ.ML \ Tools/recdef.ML \ + Tools/record.ML \ Tools/semiring_normalizer.ML \ Tools/Sledgehammer/clausifier.ML \ Tools/Sledgehammer/meson_tactic.ML \ @@ -343,6 +343,7 @@ Tools/string_code.ML \ Tools/string_syntax.ML \ Tools/transfer.ML \ + Tools/typecopy.ML \ Tools/TFL/casesplit.ML \ Tools/TFL/dcterm.ML \ Tools/TFL/post.ML \ diff -r 7c045c03598f -r 3142c1e21a0e src/HOL/Record.thy --- a/src/HOL/Record.thy Thu Aug 12 17:56:41 2010 +0200 +++ b/src/HOL/Record.thy Thu Aug 12 17:56:43 2010 +0200 @@ -9,8 +9,8 @@ header {* Extensible records with structural subtyping *} theory Record -imports Datatype -uses ("Tools/record.ML") +imports Plain Quickcheck +uses ("Tools/typecopy.ML") ("Tools/record.ML") ("Tools/quickcheck_record.ML") begin subsection {* Introduction *} @@ -123,67 +123,67 @@ definition iso_tuple_update_accessor_cong_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) \ bool" where - "iso_tuple_update_accessor_cong_assist upd acc \ - (\f v. upd (\x. f (acc v)) v = upd f v) \ (\v. upd id v = v)" + "iso_tuple_update_accessor_cong_assist upd ac \ + (\f v. upd (\x. f (ac v)) v = upd f v) \ (\v. upd id v = v)" definition iso_tuple_update_accessor_eq_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) \ 'a \ ('b \ 'b) \ 'a \ 'b \ bool" where - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - upd f v = v' \ acc v = x \ iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + upd f v = v' \ ac v = x \ iso_tuple_update_accessor_cong_assist upd ac" lemma update_accessor_congruence_foldE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and r: "r = r'" and v: "acc r' = v'" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and r: "r = r'" and v: "ac 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 (subgoal_tac "upd (\x. f (ac r')) r' = upd (\x. f' (ac r')) r'") apply (simp add: iso_tuple_update_accessor_cong_assist_def) apply (simp add: f) done lemma update_accessor_congruence_unfoldE: - "iso_tuple_update_accessor_cong_assist upd acc \ - r = r' \ acc r' = v' \ (\v. v = v' \ f v = f' v) \ + "iso_tuple_update_accessor_cong_assist upd ac \ + r = r' \ ac 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 iso_tuple_update_accessor_cong_assist_id: - "iso_tuple_update_accessor_cong_assist upd acc \ upd id = id" + "iso_tuple_update_accessor_cong_assist upd ac \ upd id = id" by rule (simp add: iso_tuple_update_accessor_cong_assist_def) lemma update_accessor_noopE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and acc: "f (acc x) = acc x" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and ac: "f (ac x) = ac x" shows "upd f x = x" using uac - by (simp add: acc iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] + by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] cong: update_accessor_congruence_unfoldE [OF uac]) lemma update_accessor_noop_compE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and acc: "f (acc x) = acc x" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and ac: "f (ac x) = ac x" shows "upd (g \ f) x = upd g x" - by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac]) + by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac]) lemma update_accessor_cong_assist_idI: "iso_tuple_update_accessor_cong_assist id id" by (simp add: iso_tuple_update_accessor_cong_assist_def) lemma update_accessor_cong_assist_triv: - "iso_tuple_update_accessor_cong_assist upd acc \ - iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_cong_assist upd ac \ + iso_tuple_update_accessor_cong_assist upd ac" by assumption lemma update_accessor_accessor_eqE: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ acc v = x" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ ac v = x" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma update_accessor_updator_eqE: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ upd f v = v'" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ upd f v = v'" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma iso_tuple_update_accessor_eq_assist_idI: @@ -191,13 +191,13 @@ by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI) lemma iso_tuple_update_accessor_eq_assist_triv: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - iso_tuple_update_accessor_eq_assist upd acc v f v' x" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + iso_tuple_update_accessor_eq_assist upd ac v f v' x" by assumption lemma iso_tuple_update_accessor_cong_from_eq: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + iso_tuple_update_accessor_cong_assist upd ac" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma iso_tuple_surjective_proof_assistI: @@ -452,8 +452,9 @@ subsection {* Record package *} -use "Tools/record.ML" -setup Record.setup +use "Tools/typecopy.ML" setup Typecopy.setup +use "Tools/record.ML" setup Record.setup +use "Tools/quickcheck_record.ML" setup Quickcheck_Record.setup hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons