diff options
Diffstat (limited to 'ex/Methods.thy')
| -rw-r--r-- | ex/Methods.thy | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/ex/Methods.thy b/ex/Methods.thy index 699d620..871964f 100644 --- a/ex/Methods.thy +++ b/ex/Methods.thy @@ -10,6 +10,8 @@ theory Methods begin +text "Wellformedness results, metatheorems written into the object theory using the wellformedness rules." + lemma assumes "A : U(i)" "B: A \<longrightarrow> U(i)" "\<And>x. x : A \<Longrightarrow> C x: B x \<longrightarrow> U(i)" shows "\<Sum>x:A. \<Prod>y:B x. \<Sum>z:C x y. \<Prod>w:A. x =\<^sub>A w : U(i)" @@ -45,4 +47,31 @@ apply (rule Sum_intro) apply assumption+ done + +text " + Function application. + The proof methods are not yet automated as well as I would like; we still often have to explicitly specify types. +" + +lemma + assumes "A: U(i)" "a: A" + shows "(\<^bold>\<lambda>x. <x,0>)`a \<equiv> <a,0>" +proof compute + show "\<And>x. x: A \<Longrightarrow> <x,0>: A \<times> \<nat>" by simple +qed (simple lems: assms) + + +lemma + assumes "A: U(i)" "B: A \<longrightarrow> U(i)" "a: A" "b: B(a)" + shows "(\<^bold>\<lambda>x y. <x,y>)`a`b \<equiv> <a,b>" +proof compute + show "\<And>x. x: A \<Longrightarrow> \<^bold>\<lambda>y. <x,y>: \<Prod>y:B(x). \<Sum>x:A. B(x)" by (simple lems: assms) + + show "(\<^bold>\<lambda>b. <a,b>)`b \<equiv> <a, b>" + proof compute + show "\<And>b. b: B(a) \<Longrightarrow> <a, b>: \<Sum>x:A. B(x)" by (simple lems: assms) + qed fact +qed fact + + end
\ No newline at end of file |