# HG changeset patch
# User wenzelm
# Date 1486136204 -3600
# Node ID 7dc25cf5793e655a6ea31784a9a1982c77e420b2
# Parent  20a623d03d717d65b20644074e3008c7e5a5e470
misc tuning;

diff -r 20a623d03d71 -r 7dc25cf5793e src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Thu Feb 02 09:55:16 2017 -0500
+++ b/src/CTT/Arith.thy	Fri Feb 03 16:36:44 2017 +0100
@@ -289,7 +289,7 @@
   done
 
 text \<open>If \<open>a + b = 0\<close> then \<open>a = 0\<close>. Surprisingly tedious.\<close>
-schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : \<Prod>u: Eq(N,a#+b,0) .  Eq(N,a,0)"
+schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : Eq(N,a#+b,0) \<longrightarrow> Eq(N,a,0)"
   apply (NE a)
     apply (rule_tac [3] replace_type)
      apply arith_rew
@@ -312,7 +312,7 @@
 
 text \<open>Here is a lemma to infer \<open>a - b = 0\<close> and \<open>b - a = 0\<close> from \<open>a |-| b = 0\<close>, below.\<close>
 schematic_goal absdiff_eq0_lem:
-  "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : \<Sum>v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
+  "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : Eq(N, a-b, 0) \<times> Eq(N, b-a, 0)"
   apply (unfold absdiff_def)
   apply intr
    apply eqintr
diff -r 20a623d03d71 -r 7dc25cf5793e src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Thu Feb 02 09:55:16 2017 -0500
+++ b/src/CTT/Bool.thy	Fri Feb 03 16:36:44 2017 +0100
@@ -19,7 +19,7 @@
   where "false \<equiv> inr(tt)"
 
 definition cond :: "[i,i,i]\<Rightarrow>i"
-  where "cond(a,b,c) \<equiv> when(a, \<lambda>u. b, \<lambda>u. c)"
+  where "cond(a,b,c) \<equiv> when(a, \<lambda>_. b, \<lambda>_. c)"
 
 lemmas bool_defs = Bool_def true_def false_def cond_def
 
diff -r 20a623d03d71 -r 7dc25cf5793e src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Thu Feb 02 09:55:16 2017 -0500
+++ b/src/CTT/CTT.thy	Fri Feb 03 16:36:44 2017 +0100
@@ -208,7 +208,7 @@
     \<Longrightarrow> when(p, \<lambda>x. c(x), \<lambda>y. d(y)) = when(q, \<lambda>x. e(x), \<lambda>y. f(y)) : C(p)" and
 
   PlusC_inl:
-    "\<And>a c d A C. \<lbrakk>a: A;
+    "\<And>a c d A B C. \<lbrakk>a: A;
       \<And>x. x:A \<Longrightarrow> c(x): C(inl(x));
       \<And>y. y:B \<Longrightarrow> d(y): C(inr(y)) \<rbrakk>
     \<Longrightarrow> when(inl(a), \<lambda>x. c(x), \<lambda>y. d(y)) = c(a) : C(inl(a))" and
diff -r 20a623d03d71 -r 7dc25cf5793e src/CTT/Main.thy
--- a/src/CTT/Main.thy	Thu Feb 02 09:55:16 2017 -0500
+++ b/src/CTT/Main.thy	Fri Feb 03 16:36:44 2017 +0100
@@ -1,6 +1,6 @@
 section \<open>Main includes everything\<close>
 
 theory Main
-  imports CTT Arith Bool
+  imports CTT Bool Arith
 begin
 end
diff -r 20a623d03d71 -r 7dc25cf5793e src/CTT/ex/Elimination.thy
--- a/src/CTT/ex/Elimination.thy	Thu Feb 02 09:55:16 2017 -0500
+++ b/src/CTT/ex/Elimination.thy	Fri Feb 03 16:36:44 2017 +0100
@@ -135,8 +135,7 @@
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
-  shows "?a : \<Prod>h: (\<Prod>x:A. \<Sum>y:B(x). C(x,y)).
-                         (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
+  shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
 apply (intr assms)
 prefer 2 apply add_mp
 prefer 2 apply add_mp
@@ -153,8 +152,7 @@
   assumes "A type"
     and "\<And>x. x:A \<Longrightarrow> B(x) type"
     and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type"
-  shows "?a : \<Prod>h: (\<Prod>x:A. \<Sum>y:B(x). C(x,y)).
-                         (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
+  shows "?a : (\<Prod>x:A. \<Sum>y:B(x). C(x,y)) \<longrightarrow> (\<Sum>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
 apply (intr assms)
 (*Must not use add_mp as subst_prodE hides the construction.*)
 apply (rule ProdE [THEN SumE])