equal
deleted
inserted
replaced
636 |
636 |
637 lemma "snd (x, y\<Colon>'a\<times>'b) = y" |
637 lemma "snd (x, y\<Colon>'a\<times>'b) = y" |
638 nitpick [expect = none] |
638 nitpick [expect = none] |
639 by (simp add: snd_def) |
639 by (simp add: snd_def) |
640 |
640 |
641 lemma "fst p = (THE a. \<exists>b. p = Pair a b)" |
|
642 nitpick [expect = none] |
|
643 by (simp add: fst_def) |
|
644 |
|
645 lemma "snd p = (THE b. \<exists>a. p = Pair a b)" |
|
646 nitpick [expect = none] |
|
647 by (simp add: snd_def) |
|
648 |
|
649 lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))" |
641 lemma "I = (\<lambda>x. x) \<Longrightarrow> fst = (\<lambda>x. fst (I x))" |
650 nitpick [expect = none] |
642 nitpick [expect = none] |
651 by auto |
643 by auto |
652 |
644 |
653 lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))" |
645 lemma "I = (\<lambda>x. x) \<Longrightarrow> snd = (\<lambda>x. snd (I x))" |