From 9b17aac85aa650a7a9d6463d3d01f1eb228d4572 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 11 Sep 2018 08:59:16 +0200
Subject: Go back to higher-order application notation

---
 Proj.thy | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'Proj.thy')

diff --git a/Proj.thy b/Proj.thy
index a1c4c8f..74c561c 100644
--- a/Proj.thy
+++ b/Proj.thy
@@ -12,44 +12,44 @@ theory Proj
 begin
 
 
-definition fst :: "Term \<Rightarrow> Term" where "fst(p) \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p"
-definition snd :: "Term \<Rightarrow> Term" where "snd(p) \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p"
+definition fst :: "Term \<Rightarrow> Term" where "fst p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. x) p"
+definition snd :: "Term \<Rightarrow> Term" where "snd p \<equiv> ind\<^sub>\<Sum> (\<lambda>x y. y) p"
 
 text "Typing judgments and computation rules for the dependent and non-dependent projection functions."
 
 lemma fst_type:
-  assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "fst(p): A"
+  assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "fst p: A"
 unfolding fst_def by (derive lems: assms)
 
 lemma fst_comp:
-  assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "fst(<a,b>) \<equiv> a"
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "fst <a,b> \<equiv> a"
 unfolding fst_def
 proof compute
-  show "a: A" and "b: B(a)" by fact+
+  show "a: A" and "b: B a" by fact+
 qed (routine lems: assms)+
 
 lemma snd_type:
-  assumes "\<Sum>x:A. B(x): U(i)" and "p: \<Sum>x:A. B(x)" shows "snd(p): B(fst p)"
+  assumes "\<Sum>x:A. B x: U i" and "p: \<Sum>x:A. B x" shows "snd p: B (fst p)"
 unfolding snd_def
 proof
-  show "\<And>p. p: \<Sum>x:A. B(x) \<Longrightarrow> B(fst p): U(i)" by (derive lems: assms fst_type)
+  show "\<And>p. p: \<Sum>x:A. B x \<Longrightarrow> B (fst p): U i" by (derive lems: assms fst_type)
   
   fix x y
-  assume asm: "x: A" "y: B(x)"
-  show "y: B(fst <x,y>)"
+  assume asm: "x: A" "y: B x"
+  show "y: B (fst <x,y>)"
   proof (subst fst_comp)
-    show "A: U(i)" by (wellformed lems: assms(1))
-    show "\<And>x. x: A \<Longrightarrow> B(x): U(i)" by (wellformed lems: assms(1))
+    show "A: U i" by (wellformed lems: assms(1))
+    show "\<And>x. x: A \<Longrightarrow> B x: U i" by (wellformed lems: assms(1))
   qed fact+
 qed fact
 
 lemma snd_comp:
-  assumes "A: U(i)" and "B: A \<longrightarrow> U(i)" and "a: A" and "b: B(a)" shows "snd(<a,b>) \<equiv> b"
+  assumes "A: U i" and "B: A \<longrightarrow> U i" and "a: A" and "b: B a" shows "snd <a,b> \<equiv> b"
 unfolding snd_def
 proof compute
-  show "\<And>x y. y: B(x) \<Longrightarrow> y: B(x)" .
+  show "\<And>x y. y: B x \<Longrightarrow> y: B x" .
   show "a: A" by fact
-  show "b: B(a)" by fact
+  show "b: B a" by fact
 qed (routine lems: assms)
 
 
-- 
cgit v1.2.3