Old application syntax incompatible with Eisbach

7 files changed, 74 insertions, 78 deletions

diff --git a/Coprod.thy b/Coprod.thy
index 75e621a..a301e7e 100644
--- a/Coprod.thy
+++ b/Coprod.thy
@@ -14,43 +14,43 @@ section \<open>Constants and type rules\<close>
 
 axiomatization
   Coprod :: "[Term, Term] \<Rightarrow> Term"  (infixr "+" 50) and
-  inl :: "Term \<Rightarrow> Term"  ("(1inl'(_'))") and
-  inr :: "Term \<Rightarrow> Term"  ("(1inr'(_'))") and
-  indCoprod :: "[Term, Term, Typefam, Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>+[_,/ _])")
+  inl :: "Term \<Rightarrow> Term" and
+  inr :: "Term \<Rightarrow> Term" and
+  indCoprod :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>+)")
 where
-  Coprod_form: "\<And>i A B. \<lbrakk>A : U(i); B : U(i)\<rbrakk> \<Longrightarrow> A + B : U(i)"
+  Coprod_form: "\<And>i A B. \<lbrakk>A : U(i); B : U(i)\<rbrakk> \<Longrightarrow> A + B: U(i)"
 and
-  Coprod_intro1: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inl(a) : A + B"
+  Coprod_intro1: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inl(a): A + B"
 and
-  Coprod_intro2: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inr(b) : A + B"
+  Coprod_intro2: "\<And>A B a b. \<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> inr(b): A + B"
 and
   Coprod_elim: "\<And>i A B C c d e. \<lbrakk>
     C: A + B \<longrightarrow> U(i);
-    \<And>x. x : A \<Longrightarrow> c x : C inl(x);
-    \<And>y. y : B \<Longrightarrow> d y : C inr(y);
-    e : A + B
-    \<rbrakk> \<Longrightarrow> ind\<^sub>+[A,B] C c d e : C e"
+    \<And>x. x: A \<Longrightarrow> c(x): C(inl(x));
+    \<And>y. y: B \<Longrightarrow> d(y): C(inr(y));
+    e: A + B
+    \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(e) : C(e)"
 and
   Coprod_comp1: "\<And>i A B C c d a. \<lbrakk>
     C: A + B \<longrightarrow> U(i);
-    \<And>x. x : A \<Longrightarrow> c x : C inl(x);
-    \<And>y. y : B \<Longrightarrow> d y : C inr(y);
-    a : A
-    \<rbrakk> \<Longrightarrow> ind\<^sub>+[A,B] C c d inl(a) \<equiv> c a"
+    \<And>x. x: A \<Longrightarrow> c(x): C(inl(x));
+    \<And>y. y: B \<Longrightarrow> d(y): C(inr(y));
+    a: A
+    \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inl(a)) \<equiv> c(a)"
 and
   Coprod_comp2: "\<And>i A B C c d b. \<lbrakk>
     C: A + B \<longrightarrow> U(i);
-    \<And>x. x : A \<Longrightarrow> c x : C inl(x);
-    \<And>y. y : B \<Longrightarrow> d y : C inr(y);
-    b : B
-    \<rbrakk> \<Longrightarrow> ind\<^sub>+[A,B] C c d inr(b) \<equiv> d b"
+    \<And>x. x: A \<Longrightarrow> c(x): C(inl(x));
+    \<And>y. y: B \<Longrightarrow> d(y): C(inr(y));
+    b: B
+    \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inr(b)) \<equiv> d(b)"
 
 text "Admissible formation inference rules:"
 
 axiomatization where
-  Coprod_form_cond1: "\<And>i A B. A + B : U(i) \<Longrightarrow> A : U(i)"
+  Coprod_form_cond1: "\<And>i A B. A + B: U(i) \<Longrightarrow> A: U(i)"
 and
-  Coprod_form_cond2: "\<And>i A B. A + B : U(i) \<Longrightarrow> B : U(i)"
+  Coprod_form_cond2: "\<And>i A B. A + B: U(i) \<Longrightarrow> B: U(i)"
 
 lemmas Coprod_rules [intro] = Coprod_form Coprod_intro1 Coprod_intro2
                               Coprod_elim Coprod_comp1 Coprod_comp2
diff --git a/Equal.thy b/Equal.thy
index 2b49213..8bd7875 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -14,8 +14,8 @@ section \<open>Constants and syntax\<close>
 
 axiomatization
   Equal :: "[Term, Term, Term] \<Rightarrow> Term" and
-  refl :: "Term \<Rightarrow> Term"  ("(refl'(_'))" 1000) and
-  indEqual :: "[Term, [Term, Term] \<Rightarrow> Typefam, Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>=[_])")
+  refl :: "Term \<Rightarrow> Term" and
+  indEqual :: "[Term \<Rightarrow> Term, Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>=)")
 
 syntax
   "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"        ("(3_ =\<^sub>_/ _)" [101, 0, 101] 100)
@@ -28,32 +28,32 @@ translations
 section \<open>Type rules\<close>
 
 axiomatization where
-  Equal_form: "\<And>i A a b. \<lbrakk>A : U(i); a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)"
+  Equal_form: "\<And>i A a b. \<lbrakk>A: U(i); a: A; b: A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U(i)"
 and
-  Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a) : a =\<^sub>A a"
+  Equal_intro: "\<And>A a. a : A \<Longrightarrow> refl(a): a =\<^sub>A a"
 and
   Equal_elim: "\<And>i A C f a b p. \<lbrakk>
-    \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i);
-    \<And>x. x : A \<Longrightarrow> f x : C x x refl(x);
-    a : A;
-    b : A;
-    p : a =\<^sub>A b
-    \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a b p : C a b p"
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i);
+    \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
+    a: A;
+    b: A;
+    p: a =\<^sub>A b
+    \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(b)(p) : C(a)(b)(p)"
 and
   Equal_comp: "\<And>i A C f a. \<lbrakk>
-    \<And>x y. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C x y: x =\<^sub>A y \<longrightarrow> U(i);
-    \<And>x. x : A \<Longrightarrow> f x : C x x refl(x);
-    a : A
-    \<rbrakk> \<Longrightarrow> ind\<^sub>=[A] C f a a refl(a) \<equiv> f a"
+    \<And>x y. \<lbrakk>x: A; y: A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<longrightarrow> U(i);
+    \<And>x. x: A \<Longrightarrow> f(x) : C(x)(x)(refl x);
+    a: A
+    \<rbrakk> \<Longrightarrow> ind\<^sub>=(f)(a)(a)(refl(a)) \<equiv> f(a)"
 
 text "Admissible inference rules for equality type formation:"
 
 axiomatization where
-  Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> A : U(i)"
+  Equal_form_cond1: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> A: U(i)"
 and
-  Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> a : A"
+  Equal_form_cond2: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> a: A"
 and
-  Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b : U(i) \<Longrightarrow> b : A"
+  Equal_form_cond3: "\<And>i A a b. a =\<^sub>A b: U(i) \<Longrightarrow> b: A"
 
 lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp
 lemmas Equal_form_conds [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index c2bb092..614419e 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -9,10 +9,6 @@ theory HoTT_Base
   imports Pure
 begin
 
-text "Use the syntax \<open>f(x)\<close> instead of \<open>f x\<close> for function application."
-
-setup Pure_Thy.old_appl_syntax_setup
-
 
 section \<open>Foundational definitions\<close>
 
diff --git a/Nat.thy b/Nat.thy
index 93b7a2e..bd2c4ca 100644
--- a/Nat.thy
+++ b/Nat.thy
@@ -14,33 +14,33 @@ axiomatization
   Nat :: Term   ("\<nat>") and
   zero :: Term  ("0") and
   succ :: "Term \<Rightarrow> Term" and
-  indNat :: "[Typefam, [Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<nat>)")
+  indNat :: "[[Term, Term] \<Rightarrow> Term, Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<nat>)")
 where
-  Nat_form: "\<nat> : U(O)"
+  Nat_form: "\<nat>: U(O)"
 and
-  Nat_intro1: "0 : \<nat>"
+  Nat_intro1: "0: \<nat>"
 and
-  Nat_intro2: "\<And>n. n : \<nat> \<Longrightarrow> succ n : \<nat>"
+  Nat_intro2: "\<And>n. n: \<nat> \<Longrightarrow> succ(n): \<nat>"
 and
   Nat_elim: "\<And>i C f a n. \<lbrakk>
     C: \<nat> \<longrightarrow> U(i);
-    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
-    a : C 0;
-    n : \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a n : C n"
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n);
+    a: C(0);
+    n: \<nat>
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(n): C(n)"
 and
   Nat_comp1: "\<And>i C f a. \<lbrakk>
     C: \<nat> \<longrightarrow> U(i);
-    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
-    a : C 0
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a 0 \<equiv> a"
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n);
+    a: C(0)
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(0) \<equiv> a"
 and
   Nat_comp2: "\<And> i C f a n. \<lbrakk>
     C: \<nat> \<longrightarrow> U(i);
-    \<And>n c. \<lbrakk>n : \<nat>; c : C n\<rbrakk> \<Longrightarrow> f n c : C (succ n);
-    a : C 0;
-    n : \<nat>
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat> C f a (succ n) \<equiv> f n (ind\<^sub>\<nat> C f a n)"
+    \<And>n c. \<lbrakk>n: \<nat>; c: C(n)\<rbrakk> \<Longrightarrow> f(n)(c): C(succ n);
+    a: C(0);
+    n: \<nat>
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<nat>(f)(a)(succ n) \<equiv> f(n)(ind\<^sub>\<nat> f a n)"
 
 lemmas Nat_rules [intro] = Nat_form Nat_intro1 Nat_intro2 Nat_elim Nat_comp1 Nat_comp2
 lemmas Nat_comps [comp] = Nat_comp1 Nat_comp2
diff --git a/Prod.thy b/Prod.thy
index 845de4b..01cd006 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -27,10 +27,10 @@ syntax
 text "The translations below bind the variable \<open>x\<close> in the expressions \<open>B\<close> and \<open>b\<close>."
 
 translations
-  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
-  "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda(A, \<lambda>x. b)"
-  "PROD x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
-  "%%x:A. b" \<rightharpoonup> "CONST lambda(A, \<lambda>x. b)"
+  "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)"
+  "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)"
+  "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
+  "%%x:A. b" \<rightharpoonup> "CONST lambda A (\<lambda>x. b)"
 
 text "Nondependent functions are a special case."
 
@@ -84,9 +84,9 @@ where
 and
   Unit_intro: "\<star>: \<one>"
 and
-  Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c, a) : C(a)"
+  Unit_elim: "\<And>i C c a. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(a) : C(a)"
 and
-  Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c, \<star>) \<equiv> c"
+  Unit_comp: "\<And>i C c. \<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c"
 
 lemmas Unit_rules [intro] = Unit_form Unit_intro Unit_elim Unit_comp
 lemmas Unit_comps [comp] = Unit_comp
diff --git a/Sum.thy b/Sum.thy
index 2d6e64b..cdfe5bd 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -22,8 +22,8 @@ syntax
   "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3SUM _:_./ _)" 20)
 
 translations
-  "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
-  "SUM x:A. B" \<rightharpoonup> "CONST Sum(A, \<lambda>x. B)"
+  "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
+  "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
 
 text "Nondependent pair."
 
@@ -40,25 +40,25 @@ and
 and
   Sum_elim: "\<And>i A B C f p. \<lbrakk>
     C: \<Sum>x:A. B(x) \<longrightarrow> U(i);
-    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x, y) : C((x,y));
+    \<And>x y. \<lbrakk>x: A; y: B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C((x,y));
     p : \<Sum>x:A. B(x)
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f, p) : C(p)"  (* What does writing \<lambda>x y. f(x, y) change? *)
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)(p) : C(p)"  (* What does writing \<lambda>x y. f(x, y) change? *)
 and
   Sum_comp: "\<And>i A B C f a b. \<lbrakk>
-    A : U(i);
+    A: U(i);
     B: A \<longrightarrow> U(i);
-    C: \<Sum>x:A. B x \<longrightarrow> U(i);
-    \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
-    a : A;
-    b : B a
-    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>[A,B] C f (a,b) \<equiv> f a b"
+    C: \<Sum>x:A. B(x) \<longrightarrow> U(i);
+    \<And>x y. \<lbrakk>x: A; y :B(x)\<rbrakk> \<Longrightarrow> f(x)(y) : C((x,y));
+    a: A;
+    b: B(a)
+    \<rbrakk> \<Longrightarrow> ind\<^sub>\<Sum>(f)((a,b)) \<equiv> f(a)(b)"
 
 text "Admissible inference rules for sum formation:"
 
 axiomatization where
-  Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> A : U(i)"
+  Sum_form_cond1: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> A: U(i)"
 and
-  Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B x : U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
+  Sum_form_cond2: "\<And>i A B. (\<Sum>x:A. B(x): U(i)) \<Longrightarrow> B: A \<longrightarrow> U(i)"
 
 lemmas Sum_rules [intro] = Sum_form Sum_intro Sum_elim Sum_comp
 lemmas Sum_form_conds [intro (*elim, wellform*)] = Sum_form_cond1 Sum_form_cond2
@@ -69,11 +69,11 @@ section \<open>Empty type\<close>
 
 axiomatization
   Empty :: Term  ("\<zero>") and
-  indEmpty :: "[Typefam, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
+  indEmpty :: "Term \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
 where
   Empty_form: "\<zero> : U(O)"
 and
-  Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z : \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> C z : C z"
+  Empty_elim: "\<And>i C z. \<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
 
 lemmas Empty_rules [intro] = Empty_form Empty_elim
 
diff --git a/scratch.thy b/scratch.thy
index b88a8fc..55e7023 100644
--- a/scratch.thy
+++ b/scratch.thy
@@ -3,9 +3,9 @@ theory scratch
 
 begin
 
-abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. (ind\<^sub>\<nat> (\<lambda>n. \<nat>) (\<lambda>n c. n) 0 n)"
+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"
+schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0"
 apply (subst comp)
 apply (rule Nat_form)
 prefer 4 apply (subst comp)