# HG changeset patch # User wenzelm # Date 1693407448 -7200 # Node ID 8d7394e533f853c7c5043abc2e547069c493ee90 # Parent b96b73a79da3a40dbe228cdd06be68dcde21c73a tuned whitespace; diff -r b96b73a79da3 -r 8d7394e533f8 src/HOL/Examples/Records.thy --- a/src/HOL/Examples/Records.thy Mon Aug 28 13:00:24 2023 +0200 +++ b/src/HOL/Examples/Records.thy Wed Aug 30 16:57:28 2023 +0200 @@ -299,24 +299,26 @@ apply (simp) done + subsection \Simprocs for update and equality\ record alph1 = -a::nat -b::nat + a :: nat + b :: nat record alph2 = alph1 + -c::nat -d::nat + c :: nat + d :: nat -record alph3 = alph2 + - e::nat - f::nat +record alph3 = alph2 + + e :: nat + f :: nat -text \The simprocs that are activated by default are: -\<^item> @{ML [source] Record.simproc}: field selection of (nested) record updates. -\<^item> @{ML [source] Record.upd_simproc}: nested record updates. -\<^item> @{ML [source] Record.eq_simproc}: (componentwise) equality of records. +text \ + The simprocs that are activated by default are: + \<^item> @{ML [source] Record.simproc}: field selection of (nested) record updates. + \<^item> @{ML [source] Record.upd_simproc}: nested record updates. + \<^item> @{ML [source] Record.eq_simproc}: (componentwise) equality of records. \ @@ -325,15 +327,15 @@ by simp text \Normalisation towards an update ordering (string ordering of update function names) can -be configured as follows.\ + be configured as follows.\ schematic_goal "r\b := y, a := x\ = ?X" supply [[record_sort_updates]] by simp text \Note the interplay between update ordering and record equality. Without update ordering -the following equality is handled by @{ML [source] Record.eq_simproc}. Record equality is thus -solved by componentwise comparison of all the fields of the records which can be expensive -in the presence of many fields.\ + the following equality is handled by @{ML [source] Record.eq_simproc}. Record equality is thus + solved by componentwise comparison of all the fields of the records which can be expensive + in the presence of many fields.\ lemma "r\f := x1, a:= x2\ = r\a := x2, f:= x1\" by simp @@ -344,7 +346,7 @@ oops text \With update ordering the equality is already established after update normalisation. There -is no need for componentwise comparison.\ + is no need for componentwise comparison.\ lemma "r\f := x1, a:= x2\ = r\a := x2, f:= x1\" supply [[record_sort_updates, simproc del: Record.eq]] @@ -391,13 +393,13 @@ setup \ -let - val N = 300 -in - Record.add_record {overloaded=false} ([], \<^binding>\large_record\) NONE - (map (fn i => (Binding.make ("fld_" ^ string_of_int i, \<^here>), @{typ nat}, Mixfix.NoSyn)) - (1 upto N)) -end + let + val N = 300 + in + Record.add_record {overloaded = false} ([], \<^binding>\large_record\) NONE + (map (fn i => (Binding.make ("fld_" ^ string_of_int i, \<^here>), @{typ nat}, Mixfix.NoSyn)) + (1 upto N)) + end \ declare [[record_codegen]]