src/HOL/ex/Records.thy
changeset 61933 cf58b5b794b2
parent 61499 4efe9a6dd212
child 62119 b8c973d90ae7
equal deleted inserted replaced
61932:2e48182cc82c 61933:cf58b5b794b2
    73 
    73 
    74 
    74 
    75 text \<open>\medskip Equality of records.\<close>
    75 text \<open>\medskip Equality of records.\<close>
    76 
    76 
    77 lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
    77 lemma "n = n' ==> p = p' ==> (| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |)"
    78   -- "introduction of concrete record equality"
    78   \<comment> "introduction of concrete record equality"
    79   by simp
    79   by simp
    80 
    80 
    81 lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
    81 lemma "(| xpos = n, ypos = p |) = (| xpos = n', ypos = p' |) ==> n = n'"
    82   -- "elimination of concrete record equality"
    82   \<comment> "elimination of concrete record equality"
    83   by simp
    83   by simp
    84 
    84 
    85 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
    85 lemma "r (| xpos := n |) (| ypos := m |) = r (| ypos := m |) (| xpos := n |)"
    86   -- "introduction of abstract record equality"
    86   \<comment> "introduction of abstract record equality"
    87   by simp
    87   by simp
    88 
    88 
    89 lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
    89 lemma "r (| xpos := n |) = r (| xpos := n' |) ==> n = n'"
    90   -- "elimination of abstract record equality (manual proof)"
    90   \<comment> "elimination of abstract record equality (manual proof)"
    91 proof -
    91 proof -
    92   assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
    92   assume "r (| xpos := n |) = r (| xpos := n' |)" (is "?lhs = ?rhs")
    93   then have "xpos ?lhs = xpos ?rhs" by simp
    93   then have "xpos ?lhs = xpos ?rhs" by simp
    94   then show ?thesis by simp
    94   then show ?thesis by simp
    95 qed
    95 qed
   147 
   147 
   148 definition foo5 :: nat
   148 definition foo5 :: nat
   149   where "foo5 = getX (| xpos = 1, ypos = 0 |)"
   149   where "foo5 = getX (| xpos = 1, ypos = 0 |)"
   150 
   150 
   151 
   151 
   152 text \<open>\medskip Manipulating the ``@{text "..."}'' (more) part.\<close>
   152 text \<open>\medskip Manipulating the ``\<open>...\<close>'' (more) part.\<close>
   153 
   153 
   154 definition incX :: "'a point_scheme => 'a point_scheme"
   154 definition incX :: "'a point_scheme => 'a point_scheme"
   155   where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
   155   where "incX r = (| xpos = xpos r + 1, ypos = ypos r, ... = point.more r |)"
   156 
   156 
   157 lemma "incX r = setX r (Suc (getX r))"
   157 lemma "incX r = setX r (Suc (getX r))"
   186 consts foo8 :: "'a cpoint_scheme"
   186 consts foo8 :: "'a cpoint_scheme"
   187 consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
   187 consts foo9 :: "(| xpos :: nat, ypos :: nat, colour :: colour, ... :: 'a |)"
   188 
   188 
   189 
   189 
   190 text \<open>
   190 text \<open>
   191  Functions on @{text point} schemes work for @{text cpoints} as well.
   191  Functions on \<open>point\<close> schemes work for \<open>cpoints\<close> as well.
   192 \<close>
   192 \<close>
   193 
   193 
   194 definition foo10 :: nat
   194 definition foo10 :: nat
   195   where "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
   195   where "foo10 = getX (| xpos = 2, ypos = 0, colour = Blue |)"
   196 
   196