diff options
Diffstat (limited to '')
| -rw-r--r-- | Proj.thy | 7 | ||||
| -rw-r--r-- | scratch.thy | 6 |
2 files changed, 9 insertions, 4 deletions
@@ -13,9 +13,8 @@ theory Proj begin -consts - fst :: "[Term, 'a] \<Rightarrow> Term" ("(1fst[/_,/ _])") - snd :: "[Term, 'a] \<Rightarrow> Term" ("(1snd[/_,/ _])") +abbreviation fst :: Term where "fst \<equiv> \<^bold>\<lambda>p:\<Sum>x:?A. ?B(x). ind\<^sub>\<Sum>(\<lambda>x y. x)(p)" +abbreviation snd :: "Term \<Rightarrow> Term" where ""snd \<equiv> \<^bold>\<lambda>p: \<Sum>x:A. B(x). ind\<^sub>\<Sum>(\<lambda>x y. y) p" section \<open>Overloaded syntax for dependent and nondependent pairs\<close> @@ -25,7 +24,7 @@ overloading fst_nondep \<equiv> fst begin definition fst_dep :: "[Term, Typefam] \<Rightarrow> Term" where - "fst_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). ind\<^sub>\<Sum>[A,B] (\<lambda>_. A) (\<lambda>x y. x) p" + "fst_dep A B \<equiv> \<^bold>\<lambda>p:\<Sum>x:A. B(x). ind\<^sub>\<Sum>(\<lambda>x y. x)(p)" definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where "fst_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. ind\<^sub>\<Sum>[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) p" diff --git a/scratch.thy b/scratch.thy index 55e7023..e06fb7e 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,6 +3,12 @@ theory scratch begin +lemma + assumes "\<Sum>x:A. B(x): U(i)" "(a,b): \<Sum>x:A. B(x)" + shows "a : A" +proof (rule Sum_form_conds) + + abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)" schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0" |