equal
deleted
inserted
replaced
42 thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis |
42 thus "\<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" using F2 by metis |
43 qed |
43 qed |
44 |
44 |
45 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk> |
45 lemma "\<lbrakk>f c = Intg x; \<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x; (a, b) \<in> R\<^sup>*; (b,c) \<in> R\<^sup>*\<rbrakk> |
46 \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" |
46 \<Longrightarrow> \<exists>c. (b, c) \<in> R \<and> (a, c) \<in> R\<^sup>*" |
47 (* sledgehammer [isar_proofs, isar_shrink = 2] *) |
47 (* sledgehammer [isar_proofs, isar_compress = 2] *) |
48 proof - |
48 proof - |
49 assume A1: "f c = Intg x" |
49 assume A1: "f c = Intg x" |
50 assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x" |
50 assume A2: "\<forall>y. f b = Intg y \<longrightarrow> y \<noteq> x" |
51 assume A3: "(a, b) \<in> R\<^sup>*" |
51 assume A3: "(a, b) \<in> R\<^sup>*" |
52 assume A4: "(b, c) \<in> R\<^sup>*" |
52 assume A4: "(b, c) \<in> R\<^sup>*" |