From ec8e1d9d245950f185f6d4ff1b5e1b8755e7202c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 7 Aug 2018 18:06:10 +0200
Subject: Tweaks

---
 Proj.thy    | 7 +++----
 scratch.thy | 6 ++++++
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/Proj.thy b/Proj.thy
index e6ed0bb..d070ed0 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -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"
-- 
cgit v1.2.3