src/HOL/ex/Records.thy
changeset 67443 3abf6a722518
parent 62119 b8c973d90ae7
child 69597 ff784d5a5bfb
equal deleted inserted replaced
67442:f075640b8868 67443:3abf6a722518
    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   \<comment> "introduction of concrete record equality"
    78   \<comment> \<open>introduction of concrete record equality\<close>
    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   \<comment> "elimination of concrete record equality"
    82   \<comment> \<open>elimination of concrete record equality\<close>
    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   \<comment> "introduction of abstract record equality"
    86   \<comment> \<open>introduction of abstract record equality\<close>
    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   \<comment> "elimination of abstract record equality (manual proof)"
    90   \<comment> \<open>elimination of abstract record equality (manual proof)\<close>
    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