diff options
Diffstat (limited to 'Proj.thy')
| -rw-r--r-- | Proj.thy | 104 |
1 files changed, 30 insertions, 74 deletions
@@ -49,7 +49,7 @@ text "Typing judgments and computation rules for the dependent and non-dependent lemma fst_dep_type: assumes "p : \<Sum>x:A. B x" shows "fst[A,B]`p : A" - by (derive lems: fst_dep_def assms) + by (derive lems: assms unfolds: fst_dep_def) lemma fst_dep_comp: @@ -58,7 +58,7 @@ lemma fst_dep_comp: proof - have "fst[A,B]`(a,b) \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" - by (derive lems: fst_dep_def assms) + by (derive lems: assms unfolds: fst_dep_def) also have "indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a" by (derive lems: assms) @@ -67,15 +67,9 @@ proof - qed -text "In proving results about the second dependent projection function we often use the following two lemmas." +text "In proving results about the second dependent projection function we often use the following lemma." -lemma lemma1: - assumes "p : \<Sum>x:A. B x" - shows "B (fst[A,B]`p) : U" - by (derive lems: assms fst_dep_def) - - -lemma lemma2: +lemma lem: assumes "B: A \<rightarrow> U" and "x : A" and "y : B x" shows "y : B (fst[A,B]`(x,y))" @@ -89,18 +83,13 @@ lemma snd_dep_type: assumes "p : \<Sum>x:A. B x" shows "snd[A,B]`p : B (fst[A,B]`p)" -proof (derive lems: assms snd_dep_def) - show "snd[A, B] : \<Prod>p:(\<Sum>x:A. B x). B (fst[A,B]`p)" - proof (unfold snd_dep_def, standard) - show "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)" - proof (standard, elim lemma1) - fix p assume *: "p : \<Sum>x:A. B x" - have **: "B: A \<rightarrow> U" by (wellformed jdgmt: *) - fix x y assume "x : A" and "y : B x" - with ** show "y : B (fst[A,B]`(x,y))" by (rule lemma2) - qed - qed (wellformed jdgmt: assms) -qed (rule assms) +proof (derive lems: assms unfolds: snd_dep_def) + show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def) + + fix x y assume asm: "x : A" "y : B x" + have "B: A \<rightarrow> U" by (wellformed jdgmt: assms) + then show "y : B (fst[A, B]`(x,y))" using asm by (rule lem) +qed (assumption | rule assms)+ lemma snd_dep_comp: @@ -109,22 +98,20 @@ lemma snd_dep_comp: proof - have "snd[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b)" - proof (unfold snd_dep_def, standard) - show "(a,b) : \<Sum>x:A. B x" using assms .. + proof (derive lems: assms unfolds: snd_dep_def) + show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def) - fix p assume *: "p : \<Sum>x:A. B x" - show "indSum[A,B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) p : B (fst[A,B]`p)" - proof (standard, elim lemma1) - fix x y assume "x : A" and "y : B x" - with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2) - qed (rule *) - qed + fix x y assume asm: "x : A" "y : B x" + with assms(1) show "y : B (fst[A, B]`(x,y))" by (rule lem) + qed (assumption | derive lems: assms)+ also have "indSum[A, B] (\<lambda>q. B (fst[A,B]`q)) (\<lambda>x y. y) (a,b) \<equiv> b" - proof (standard, elim lemma1) + proof (simple lems: assms) + show "fst[A, B] : (\<Sum>x:A. B x) \<rightarrow> A" by (derive lems: assms unfolds: fst_dep_def) + fix x y assume "x : A" and "y : B x" - with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lemma2) - qed (rule assms)+ + with assms(1) show "y : B (fst[A,B]`(x,y))" by (rule lem) + qed (assumption | rule assms)+ finally show "snd[A,B]`(a,b) \<equiv> b" . qed @@ -135,17 +122,7 @@ text "For non-dependent projection functions:" lemma fst_nondep_type: assumes "p : A \<times> B" shows "fst[A,B]`p : A" - -proof - show "fst[A,B] : A \<times> B \<rightarrow> A" - proof (unfold fst_nondep_def, standard) - fix q assume *: "q : A \<times> B" - show "indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) q : A" - proof - show "A : U" by (wellformed jdgmt: assms) - qed (assumption, rule *) - qed (wellformed jdgmt: assms) -qed (rule assms) + by (derive lems: assms unfolds: fst_nondep_def) lemma fst_nondep_comp: @@ -154,18 +131,10 @@ lemma fst_nondep_comp: proof - have "fst[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" - proof (unfold fst_nondep_def, standard) - show "(a,b) : A \<times> B" using assms .. - show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) p : A" - proof - show "A : U" by (wellformed jdgmt: assms(1)) - qed - qed + by (derive lems: assms unfolds: fst_nondep_def) also have "indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) (a,b) \<equiv> a" - proof - show "A : U" by (wellformed jdgmt: assms(1)) - qed (assumption, (rule assms)+) + by (derive lems: assms) finally show "fst[A,B]`(a,b) \<equiv> a" . qed @@ -177,15 +146,10 @@ lemma snd_nondep_type: proof show "snd[A,B] : A \<times> B \<rightarrow> B" - proof (unfold snd_nondep_def, standard) - fix q assume *: "q : A \<times> B" - show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B" - proof - have **: "\<lambda>_. B: A \<rightarrow> U" by (wellformed jdgmt: assms) - have "fst[A,B]`p : A" using assms by (rule fst_nondep_type) - then show "B : U" by (rule **) - qed (assumption, rule *) - qed (wellformed jdgmt: assms) + proof (derive unfolds: snd_nondep_def) + fix q assume asm: "q : A \<times> B" + show "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) q : B" by (derive lems: asm) + qed (wellformed jdgmt: assms)+ qed (rule assms) @@ -194,18 +158,10 @@ lemma snd_nondep_comp: shows "snd[A,B]`(a,b) \<equiv> b" proof - have "snd[A,B]`(a,b) \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b)" - proof (unfold snd_nondep_def, standard) - show "(a,b) : A \<times> B" by (simple conds: assms) - show "\<And>p. p : A \<times> B \<Longrightarrow> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p : B" - proof - show "B : U" by (wellformed jdgmt: assms(2)) - qed - qed + by (derive lems: assms unfolds: snd_nondep_def) also have "indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) (a,b) \<equiv> b" - proof - show "B : U" by (wellformed jdgmt: assms(2)) - qed (assumption, (rule assms)+) + by (derive lems: assms) finally show "snd[A,B]`(a,b) \<equiv> b" . qed |