# HG changeset patch # User wenzelm # Date 1326655817 -3600 # Node ID 76e32c39dd43ba4e840567d3891f72245f81325e # Parent bed0a3584faf064a1db8813de0179ee7a186a9ac tuned example; diff -r bed0a3584faf -r 76e32c39dd43 src/HOL/ex/Records.thy --- a/src/HOL/ex/Records.thy Sun Jan 15 20:03:59 2012 +0100 +++ b/src/HOL/ex/Records.thy Sun Jan 15 20:30:17 2012 +0100 @@ -1,12 +1,12 @@ (* Title: HOL/ex/Records.thy - Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, + Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen *) header {* Using extensible records in HOL -- points and coloured points *} theory Records -imports Main Record +imports Main begin subsection {* Points *} @@ -21,9 +21,9 @@ *} -thm "point.simps" -thm "point.iffs" -thm "point.defs" +thm point.simps +thm point.iffs +thm point.defs text {* The set of theorems @{thm [source] point.simps} is added @@ -42,26 +42,20 @@ subsubsection {* Introducing concrete records and record schemes *} -definition - foo1 :: point -where - foo1_def: "foo1 = (| xpos = 1, ypos = 0 |)" +definition foo1 :: point + where "foo1 = (| xpos = 1, ypos = 0 |)" -definition - foo3 :: "'a => 'a point_scheme" -where - foo3_def: "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)" +definition foo3 :: "'a => 'a point_scheme" + where "foo3 ext = (| xpos = 1, ypos = 0, ... = ext |)" subsubsection {* Record selection and record update *} -definition - getX :: "'a point_scheme => nat" where - "getX r = xpos r" +definition getX :: "'a point_scheme => nat" + where "getX r = xpos r" -definition - setX :: "'a point_scheme => nat => 'a point_scheme" where - "setX r n = r (| xpos := n |)" +definition setX :: "'a point_scheme => nat => 'a point_scheme" + where "setX r n = r (| xpos := n |)" subsubsection {* Some lemmas about records *} @@ -96,8 +90,8 @@ -- "elimination of abstract record equality (manual proof)" proof - assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs") - hence "xpos ?lhs = xpos ?rhs" by simp - thus ?thesis by simp + then have "xpos ?lhs = xpos ?rhs" by simp + then show ?thesis by simp qed @@ -119,7 +113,7 @@ proof (cases r) fix xpos ypos more assume "r = (| xpos = xpos, ypos = ypos, ... = more |)" - thus ?thesis by simp + then show ?thesis by simp qed lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)" @@ -134,13 +128,13 @@ proof (cases r) fix xpos ypos more assume "r = \xpos = xpos, ypos = ypos, \ = more\" - thus ?thesis by simp + then show ?thesis by simp qed lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" proof (cases r) case fields - thus ?thesis by simp + then show ?thesis by simp qed lemma "r (| xpos := n |) (| xpos := m |) = r (| xpos := m |)" @@ -151,16 +145,14 @@ \medskip Concrete records are type instances of record schemes. *} -definition - foo5 :: nat where - "foo5 = getX (| xpos = 1, ypos = 0 |)" +definition foo5 :: nat + where "foo5 = getX (| xpos = 1, ypos = 0 |)" text {* \medskip Manipulating the ``@{text "..."}'' (more) part. *} -definition - incX :: "'a point_scheme => 'a point_scheme" where - "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)" +definition incX :: "'a point_scheme => 'a point_scheme" + where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)" lemma "incX r = setX r (Suc (getX r))" by (simp add: getX_def setX_def incX_def) @@ -168,9 +160,8 @@ text {* An alternative definition. *} -definition - incX' :: "'a point_scheme => 'a point_scheme" where - "incX' r = r (| xpos := xpos r + 1 |)" +definition incX' :: "'a point_scheme => 'a point_scheme" + where "incX' r = r (| xpos := xpos r + 1 |)" subsection {* Coloured points: record extension *} @@ -184,9 +175,9 @@ text {* The record declaration defines a new type constructure and abbreviations: @{text [display] -" cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = +" cpoint = (| xpos :: nat, ypos :: nat, colour :: colour |) = () cpoint_ext_type point_ext_type - 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = + 'a cpoint_scheme = (| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |) = 'a cpoint_ext_type point_ext_type"} *} @@ -200,9 +191,8 @@ Functions on @{text point} schemes work for @{text cpoints} as well. *} -definition - foo10 :: nat where - "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)" +definition foo10 :: nat + where "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)" subsubsection {* Non-coercive structural subtyping *} @@ -212,9 +202,8 @@ Great! *} -definition - foo11 :: cpoint where - "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0" +definition foo11 :: cpoint + where "foo11 = setX (| xpos = 2, ypos = 0, colour = Blue |) 0" subsection {* Other features *} @@ -265,8 +254,7 @@ *} lemma "(\r. P (xpos r)) \ (\x. P x)" - apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1 *}) apply simp done @@ -276,19 +264,17 @@ done lemma "(\r. P (xpos r)) \ (\x. P x)" - apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1 *}) apply simp done lemma "(\r. P (xpos r)) \ (\x. P x)" - apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) + apply (tactic {* Record.split_simp_tac [] (K ~1) 1 *}) apply simp done lemma "\r. P (xpos r) \ (\x. P x)" - apply (tactic {* simp_tac - (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1*}) + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.split_simproc (K ~1)]) 1 *}) apply auto done @@ -302,35 +288,25 @@ apply auto done -lemma fixes r shows "P (xpos r) \ (\x. P x)" - apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) - apply auto - done - - lemma True proof - { fix P r assume pre: "P (xpos r)" - have "\x. P x" - using pre + then have "\x. P x" apply - - apply (tactic {* Record.split_simp_tac [] (K ~1) 1*}) - apply auto + apply (tactic {* Record.split_simp_tac [] (K ~1) 1 *}) + apply auto done } show ?thesis .. qed -text {* The effect of simproc @{ML [source] -"Record.ex_sel_eq_simproc"} is illustrated by the -following lemma. -*} +text {* The effect of simproc @{ML [source] Record.ex_sel_eq_simproc} is + illustrated by the following lemma. *} lemma "\r. xpos r = x" - apply (tactic {*simp_tac - (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1*}) + apply (tactic {* simp_tac (HOL_basic_ss addsimprocs [Record.ex_sel_eq_simproc]) 1 *}) done