--- a/src/CTT/Arith.thy Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/Arith.thy Sat Oct 10 21:43:07 2015 +0200
@@ -13,31 +13,27 @@
definition
add :: "[i,i]\<Rightarrow>i" (infixr "#+" 65) where
- "a#+b == rec(a, b, \<lambda>u v. succ(v))"
+ "a#+b \<equiv> rec(a, b, \<lambda>u v. succ(v))"
definition
diff :: "[i,i]\<Rightarrow>i" (infixr "-" 65) where
- "a-b == rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
+ "a-b \<equiv> rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
definition
absdiff :: "[i,i]\<Rightarrow>i" (infixr "|-|" 65) where
- "a|-|b == (a-b) #+ (b-a)"
+ "a|-|b \<equiv> (a-b) #+ (b-a)"
definition
mult :: "[i,i]\<Rightarrow>i" (infixr "#*" 70) where
- "a#*b == rec(a, 0, \<lambda>u v. b #+ v)"
+ "a#*b \<equiv> rec(a, 0, \<lambda>u v. b #+ v)"
definition
mod :: "[i,i]\<Rightarrow>i" (infixr "mod" 70) where
- "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
+ "a mod b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(v) |-| b, 0, \<lambda>x y. succ(v)))"
definition
div :: "[i,i]\<Rightarrow>i" (infixr "div" 70) where
- "a div b == rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))"
-
-
-notation (xsymbols)
- mult (infixr "#\<times>" 70)
+ "a div b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))"
lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
@@ -264,12 +260,12 @@
An example of induction over a quantified formula (a product).
Uses rewriting with a quantified, implicative inductive hypothesis.*)
schematic_goal add_diff_inverse_lemma:
- "b:N \<Longrightarrow> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
+ "b:N \<Longrightarrow> ?a : \<Prod>x:N. Eq(N, b-x, 0) \<longrightarrow> Eq(N, b #+ (x-b), x)"
apply (NE b)
(*strip one "universal quantifier" but not the "implication"*)
apply (rule_tac [3] intr_rls)
(*case analysis on x in
- (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
+ (succ(u) <= x) \<longrightarrow> (succ(u)#+(x-succ(u)) = x) *)
prefer 4
apply (NE x)
apply assumption
@@ -334,7 +330,7 @@
done
(*If a+b=0 then a=0. Surprisingly tedious*)
-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 : \<Prod>u: Eq(N,a#+b,0) . Eq(N,a,0)"
apply (NE a)
apply (rule_tac [3] replace_type)
apply arith_rew
@@ -355,7 +351,7 @@
(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
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 : \<Sum>v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
apply (unfold absdiff_def)
apply intr
apply eqintr
@@ -446,7 +442,7 @@
(*for case analysis on whether a number is 0 or a successor*)
lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) :
- Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
+ Eq(N,a,0) + (\<Sum>x:N. Eq(N,a, succ(x)))"
apply (NE a)
apply (rule_tac [3] PlusI_inr)
apply (rule_tac [2] PlusI_inl)
--- a/src/CTT/Bool.thy Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/Bool.thy Sat Oct 10 21:43:07 2015 +0200
@@ -11,19 +11,19 @@
definition
Bool :: "t" where
- "Bool == T+T"
+ "Bool \<equiv> T+T"
definition
true :: "i" where
- "true == inl(tt)"
+ "true \<equiv> inl(tt)"
definition
false :: "i" where
- "false == inr(tt)"
+ "false \<equiv> inr(tt)"
definition
cond :: "[i,i,i]\<Rightarrow>i" where
- "cond(a,b,c) == when(a, \<lambda>u. b, \<lambda>u. c)"
+ "cond(a,b,c) \<equiv> when(a, \<lambda>u. b, \<lambda>u. c)"
lemmas bool_defs = Bool_def true_def false_def cond_def
--- a/src/CTT/CTT.thy Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/CTT.thy Sat Oct 10 21:43:07 2015 +0200
@@ -51,7 +51,7 @@
(*Types*)
(*Functions*)
- lambda :: "(i \<Rightarrow> i) \<Rightarrow> i" (binder "lam " 10)
+ lambda :: "(i \<Rightarrow> i) \<Rightarrow> i" (binder "\<^bold>\<lambda>" 10)
app :: "[i,i]\<Rightarrow>i" (infixl "`" 60)
(*Natural numbers*)
Zero :: "i" ("0")
@@ -59,29 +59,18 @@
pair :: "[i,i]\<Rightarrow>i" ("(1<_,/_>)")
syntax
- "_PROD" :: "[idt,t,t]\<Rightarrow>t" ("(3PROD _:_./ _)" 10)
- "_SUM" :: "[idt,t,t]\<Rightarrow>t" ("(3SUM _:_./ _)" 10)
+ "_PROD" :: "[idt,t,t]\<Rightarrow>t" ("(3\<Prod>_:_./ _)" 10)
+ "_SUM" :: "[idt,t,t]\<Rightarrow>t" ("(3\<Sum>_:_./ _)" 10)
translations
- "PROD x:A. B" == "CONST Prod(A, \<lambda>x. B)"
- "SUM x:A. B" == "CONST Sum(A, \<lambda>x. B)"
+ "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod(A, \<lambda>x. B)"
+ "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum(A, \<lambda>x. B)"
abbreviation
- Arrow :: "[t,t]\<Rightarrow>t" (infixr "-->" 30) where
- "A --> B == PROD _:A. B"
+ Arrow :: "[t,t]\<Rightarrow>t" (infixr "\<longrightarrow>" 30) where
+ "A \<longrightarrow> B \<equiv> \<Prod>_:A. B"
abbreviation
- Times :: "[t,t]\<Rightarrow>t" (infixr "*" 50) where
- "A * B == SUM _:A. B"
-
-notation (xsymbols)
- lambda (binder "\<lambda>\<lambda>" 10) and
- Elem ("(_ /\<in> _)" [10,10] 5) and
- Eqelem ("(2_ =/ _ \<in>/ _)" [10,10,10] 5) and
- Arrow (infixr "\<longrightarrow>" 30) and
- Times (infixr "\<times>" 50)
-
-syntax (xsymbols)
- "_PROD" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Pi> _\<in>_./ _)" 10)
- "_SUM" :: "[idt,t,t] \<Rightarrow> t" ("(3\<Sigma> _\<in>_./ _)" 10)
+ Times :: "[t,t]\<Rightarrow>t" (infixr "\<times>" 50) where
+ "A \<times> B \<equiv> \<Sum>_:A. B"
(*Reduction: a weaker notion than equality; a hack for simplification.
Reduce[a,b] means either that a=b:A for some A or else that "a" and "b"
@@ -146,51 +135,51 @@
"\<And>p a b C. \<lbrakk>p: N; a: C(0); \<And>u v. \<lbrakk>u: N; v: C(u)\<rbrakk> \<Longrightarrow> b(u,v): C(succ(u))\<rbrakk> \<Longrightarrow>
rec(succ(p), a, \<lambda>u v. b(u,v)) = b(p, rec(p, a, \<lambda>u v. b(u,v))) : C(succ(p))" and
- (*The fourth Peano axiom. See page 91 of Martin-Lof's book*)
+ (*The fourth Peano axiom. See page 91 of Martin-Löf's book*)
zero_ne_succ: "\<And>a. \<lbrakk>a: N; 0 = succ(a) : N\<rbrakk> \<Longrightarrow> 0: F" and
(*The Product of a family of types*)
- ProdF: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> PROD x:A. B(x) type" and
+ ProdF: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) type" and
ProdFL:
- "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> PROD x:A. B(x) = PROD x:C. D(x)" and
+ "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) = \<Prod>x:C. D(x)" and
ProdI:
- "\<And>b A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x):B(x)\<rbrakk> \<Longrightarrow> lam x. b(x) : PROD x:A. B(x)" and
+ "\<And>b A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x):B(x)\<rbrakk> \<Longrightarrow> \<^bold>\<lambda>x. b(x) : \<Prod>x:A. B(x)" and
ProdIL: "\<And>b c A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> b(x) = c(x) : B(x)\<rbrakk> \<Longrightarrow>
- lam x. b(x) = lam x. c(x) : PROD x:A. B(x)" and
+ \<^bold>\<lambda>x. b(x) = \<^bold>\<lambda>x. c(x) : \<Prod>x:A. B(x)" and
- ProdE: "\<And>p a A B. \<lbrakk>p : PROD x:A. B(x); a : A\<rbrakk> \<Longrightarrow> p`a : B(a)" and
- ProdEL: "\<And>p q a b A B. \<lbrakk>p = q: PROD x:A. B(x); a = b : A\<rbrakk> \<Longrightarrow> p`a = q`b : B(a)" and
+ ProdE: "\<And>p a A B. \<lbrakk>p : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> p`a : B(a)" and
+ ProdEL: "\<And>p q a b A B. \<lbrakk>p = q: \<Prod>x:A. B(x); a = b : A\<rbrakk> \<Longrightarrow> p`a = q`b : B(a)" and
- ProdC: "\<And>a b A B. \<lbrakk>a : A; \<And>x. x:A \<Longrightarrow> b(x) : B(x)\<rbrakk> \<Longrightarrow> (lam x. b(x)) ` a = b(a) : B(a)" and
+ ProdC: "\<And>a b A B. \<lbrakk>a : A; \<And>x. x:A \<Longrightarrow> b(x) : B(x)\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x. b(x)) ` a = b(a) : B(a)" and
- ProdC2: "\<And>p A B. p : PROD x:A. B(x) \<Longrightarrow> (lam x. p`x) = p : PROD x:A. B(x)" and
+ ProdC2: "\<And>p A B. p : \<Prod>x:A. B(x) \<Longrightarrow> (\<^bold>\<lambda>x. p`x) = p : \<Prod>x:A. B(x)" and
(*The Sum of a family of types*)
- SumF: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> SUM x:A. B(x) type" and
- SumFL: "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> SUM x:A. B(x) = SUM x:C. D(x)" and
+ SumF: "\<And>A B. \<lbrakk>A type; \<And>x. x:A \<Longrightarrow> B(x) type\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) type" and
+ SumFL: "\<And>A B C D. \<lbrakk>A = C; \<And>x. x:A \<Longrightarrow> B(x) = D(x)\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) = \<Sum>x:C. D(x)" and
- SumI: "\<And>a b A B. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> <a,b> : SUM x:A. B(x)" and
- SumIL: "\<And>a b c d A B. \<lbrakk> a = c : A; b = d : B(a)\<rbrakk> \<Longrightarrow> <a,b> = <c,d> : SUM x:A. B(x)" and
+ SumI: "\<And>a b A B. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> <a,b> : \<Sum>x:A. B(x)" and
+ SumIL: "\<And>a b c d A B. \<lbrakk> a = c : A; b = d : B(a)\<rbrakk> \<Longrightarrow> <a,b> = <c,d> : \<Sum>x:A. B(x)" and
- SumE: "\<And>p c A B C. \<lbrakk>p: SUM x:A. B(x); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
+ SumE: "\<And>p c A B C. \<lbrakk>p: \<Sum>x:A. B(x); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
\<Longrightarrow> split(p, \<lambda>x y. c(x,y)) : C(p)" and
- SumEL: "\<And>p q c d A B C. \<lbrakk>p = q : SUM x:A. B(x);
+ SumEL: "\<And>p q c d A B C. \<lbrakk>p = q : \<Sum>x:A. B(x);
\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y)=d(x,y): C(<x,y>)\<rbrakk>
\<Longrightarrow> split(p, \<lambda>x y. c(x,y)) = split(q, \<lambda>x y. d(x,y)) : C(p)" and
SumC: "\<And>a b c A B C. \<lbrakk>a: A; b: B(a); \<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> c(x,y): C(<x,y>)\<rbrakk>
\<Longrightarrow> split(<a,b>, \<lambda>x y. c(x,y)) = c(a,b) : C(<a,b>)" and
- fst_def: "\<And>a. fst(a) == split(a, \<lambda>x y. x)" and
- snd_def: "\<And>a. snd(a) == split(a, \<lambda>x y. y)" and
+ fst_def: "\<And>a. fst(a) \<equiv> split(a, \<lambda>x y. x)" and
+ snd_def: "\<And>a. snd(a) \<equiv> split(a, \<lambda>x y. y)" and
(*The sum of two types*)
@@ -245,7 +234,7 @@
FEL: "\<And>p q C. \<lbrakk>p = q : F; C type\<rbrakk> \<Longrightarrow> contr(p) = contr(q) : C" and
(*The type T
- Martin-Lof's book (page 68) discusses elimination and computation.
+ Martin-Löf's book (page 68) discusses elimination and computation.
Elimination can be derived by computation and equality of types,
but with an extra premise C(x) type x:T.
Also computation can be derived from elimination. *)
@@ -428,7 +417,7 @@
fun add_mp_tac ctxt i =
resolve_tac ctxt @{thms subst_prodE} i THEN assume_tac ctxt i THEN assume_tac ctxt i
-(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+(*Finds P\<longrightarrow>Q and P in the assumptions, replaces implication by Q *)
fun mp_tac ctxt i = eresolve_tac ctxt @{thms subst_prodE} i THEN assume_tac ctxt i
(*"safe" when regarded as predicate calculus rules*)
--- a/src/CTT/ex/Elimination.thy Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Elimination.thy Sat Oct 10 21:43:07 2015 +0200
@@ -14,36 +14,36 @@
text "This finds the functions fst and snd!"
-schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
+schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
apply pc
done
-schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A"
+schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
apply pc
back
done
text "Double negation of the Excluded Middle"
-schematic_goal "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F"
+schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
apply intr
apply (rule ProdE)
apply assumption
apply pc
done
-schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (B*A)"
+schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)"
apply pc
done
(*The sequent version (ITT) could produce an interesting alternative
by backtracking. No longer.*)
text "Binary sums and products"
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A+B --> C) --> (A-->C) * (B-->C)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)"
apply pc
done
(*A distributive law*)
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A * (B+C) --> (A*B + A*C)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A \<times> (B + C) \<longrightarrow> (A \<times> B + A \<times> C)"
apply pc
done
@@ -52,12 +52,12 @@
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
and "\<And>x. x:A \<Longrightarrow> C(x) type"
- shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
+ shows "?a : (\<Sum>x:A. B(x) + C(x)) \<longrightarrow> (\<Sum>x:A. B(x)) + (\<Sum>x:A. C(x))"
apply (pc assms)
done
text "Construction of the currying functional"
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A*B --> C) --> (A--> (B-->C))"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
apply pc
done
@@ -65,14 +65,14 @@
schematic_goal
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
- and "\<And>z. z: (SUM x:A. B(x)) \<Longrightarrow> C(z) type"
- shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
- (PROD x:A . PROD y:B(x) . C(<x,y>))"
+ and "\<And>z. z: (\<Sum>x:A. B(x)) \<Longrightarrow> C(z) type"
+ shows "?a : \<Prod>f: (\<Prod>z : (\<Sum>x:A . B(x)) . C(z)).
+ (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))"
apply (pc assms)
done
-text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
-schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> (B-->C)) --> (A*B --> C)"
+text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
+schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)"
apply pc
done
@@ -80,14 +80,14 @@
schematic_goal
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
- and "\<And>z. z: (SUM x:A . B(x)) \<Longrightarrow> C(z) type"
- shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
- --> (PROD z : (SUM x:A . B(x)) . C(z))"
+ and "\<And>z. z: (\<Sum>x:A . B(x)) \<Longrightarrow> C(z) type"
+ shows "?a : (\<Prod>x:A . \<Prod>y:B(x) . C(<x,y>))
+ \<longrightarrow> (\<Prod>z : (\<Sum>x:A . B(x)) . C(z))"
apply (pc assms)
done
text "Function application"
-schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A --> B) * A) --> B"
+schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"
apply pc
done
@@ -97,46 +97,46 @@
and "B type"
and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type"
shows
- "?a : (SUM y:B . PROD x:A . C(x,y))
- --> (PROD x:A . SUM y:B . C(x,y))"
+ "?a : (\<Sum>y:B . \<Prod>x:A . C(x,y))
+ \<longrightarrow> (\<Prod>x:A . \<Sum>y:B . C(x,y))"
apply (pc assms)
done
-text "Martin-Lof (1984) pages 36-7: the combinator S"
+text "Martin-Löf (1984) pages 36-7: the combinator S"
schematic_goal
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 x:A. PROD y:B(x). C(x,y))
- --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
+ shows "?a : (\<Prod>x:A. \<Prod>y:B(x). C(x,y))
+ \<longrightarrow> (\<Prod>f: (\<Prod>x:A. B(x)). \<Prod>x:A. C(x, f`x))"
apply (pc assms)
done
-text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
+text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
schematic_goal
assumes "A type"
and "B type"
and "\<And>z. z: A+B \<Longrightarrow> C(z) type"
- shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
- --> (PROD z: A+B. C(z))"
+ shows "?a : (\<Prod>x:A. C(inl(x))) \<longrightarrow> (\<Prod>y:B. C(inr(y)))
+ \<longrightarrow> (\<Prod>z: A+B. C(z))"
apply (pc assms)
done
(*towards AXIOM OF CHOICE*)
schematic_goal [folded basic_defs]:
- "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> B*C) --> (A-->B) * (A-->C)"
+ "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> B \<times> C) \<longrightarrow> (A \<longrightarrow> B) \<times> (A \<longrightarrow> C)"
apply pc
done
-(*Martin-Lof (1984) page 50*)
+(*Martin-Löf (1984) page 50*)
text "AXIOM OF CHOICE! Delicate use of elimination rules"
schematic_goal
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>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))"
apply (intr assms)
prefer 2 apply add_mp
prefer 2 apply add_mp
@@ -153,8 +153,8 @@
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>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))"
apply (intr assms)
(*Must not use add_mp as subst_prodE hides the construction.*)
apply (rule ProdE [THEN SumE])
@@ -174,13 +174,13 @@
done
text "Example of sequent_style deduction"
-(*When splitting z:A*B, the assumption C(z) is affected; ?a becomes
- lam u. split(u,\<lambda>v w.split(v,\<lambda>x y.lam z. <x,<y,z>>) ` w) *)
+(*When splitting z:A \<times> B, the assumption C(z) is affected; ?a becomes
+ \<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w) *)
schematic_goal
assumes "A type"
and "B type"
- and "\<And>z. z:A*B \<Longrightarrow> C(z) type"
- shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"
+ and "\<And>z. z:A \<times> B \<Longrightarrow> C(z) type"
+ shows "?a : (\<Sum>z:A \<times> B. C(z)) \<longrightarrow> (\<Sum>u:A. \<Sum>v:B. C(<u,v>))"
apply (rule intr_rls)
apply (tactic \<open>biresolve_tac @{context} safe_brls 2\<close>)
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
--- a/src/CTT/ex/Equality.thy Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Equality.thy Sat Oct 10 21:43:07 2015 +0200
@@ -43,20 +43,20 @@
apply hyp_rew
done
-(*Martin-Lof (1984) page 62: pairing is surjective*)
+(*Martin-Löf (1984) page 62: pairing is surjective*)
lemma "p : Sum(A,B) \<Longrightarrow> <split(p,\<lambda>x y. x), split(p,\<lambda>x y. y)> = p : Sum(A,B)"
apply (rule EqE)
apply (rule elim_rls, assumption)
apply (tactic \<open>DEPTH_SOLVE_1 (rew_tac @{context} [])\<close>) (*!!!!!!!*)
done
-lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (lam u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : SUM x:B. A"
+lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) ` <a,b> = <b,a> : \<Sum>x:B. A"
apply rew
done
(*a contrived, complicated simplication, requires sum-elimination also*)
-lemma "(lam f. lam x. f`(f`x)) ` (lam u. split(u, \<lambda>v w.<w,v>)) =
- lam x. x : PROD x:(SUM y:N. N). (SUM y:N. N)"
+lemma "(\<^bold>\<lambda>f. \<^bold>\<lambda>x. f`(f`x)) ` (\<^bold>\<lambda>u. split(u, \<lambda>v w.<w,v>)) =
+ \<^bold>\<lambda>x. x : \<Prod>x:(\<Sum>y:N. N). (\<Sum>y:N. N)"
apply (rule reduction_rls)
apply (rule_tac [3] intrL_rls)
apply (rule_tac [4] EqE)
--- a/src/CTT/ex/Synthesis.thy Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Synthesis.thy Sat Oct 10 21:43:07 2015 +0200
@@ -10,8 +10,7 @@
begin
text "discovery of predecessor function"
-schematic_goal "?a : SUM pred:?A . Eq(N, pred`0, 0)
- * (PROD n:N. Eq(N, pred ` succ(n), n))"
+schematic_goal "?a : \<Sum>pred:?A . Eq(N, pred`0, 0) \<times> (\<Prod>n:N. Eq(N, pred ` succ(n), n))"
apply intr
apply eqintr
apply (rule_tac [3] reduction_rls)
@@ -21,7 +20,7 @@
text "the function fst as an element of a function type"
schematic_goal [folded basic_defs]:
- "A type \<Longrightarrow> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
+ "A type \<Longrightarrow> ?a: \<Sum>f:?B . \<Prod>i:A. \<Prod>j:A. Eq(A, f ` <i,j>, i)"
apply intr
apply eqintr
apply (rule_tac [2] reduction_rls)
@@ -34,8 +33,8 @@
text "An interesting use of the eliminator, when"
(*The early implementation of unification caused non-rigid path in occur check
See following example.*)
-schematic_goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>)
- * Eq(?A, ?b(inr(i)), <succ(0), i>)"
+schematic_goal "?a : \<Prod>i:N. Eq(?A, ?b(inl(i)), <0 , i>)
+ \<times> Eq(?A, ?b(inr(i)), <succ(0), i>)"
apply intr
apply eqintr
apply (rule comp_rls)
@@ -45,16 +44,16 @@
(*Here we allow the type to depend on i.
This prevents the cycle in the first unification (no longer needed).
Requires flex-flex to preserve the dependence.
- Simpler still: make ?A into a constant type N*N.*)
-schematic_goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>)
- * Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
+ Simpler still: make ?A into a constant type N \<times> N.*)
+schematic_goal "?a : \<Prod>i:N. Eq(?A(i), ?b(inl(i)), <0 , i>)
+ \<times> Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
oops
text "A tricky combination of when and split"
(*Now handled easily, but caused great problems once*)
schematic_goal [folded basic_defs]:
- "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)
- * Eq(?A, ?b(inr(<i,j>)), j)"
+ "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A, ?b(inl(<i,j>)), i)
+ \<times> Eq(?A, ?b(inr(<i,j>)), j)"
apply intr
apply eqintr
apply (rule PlusC_inl [THEN trans_elem])
@@ -65,20 +64,20 @@
done
(*similar but allows the type to depend on i and j*)
-schematic_goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
- * Eq(?A(i,j), ?b(inr(<i,j>)), j)"
+schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
+ \<times> Eq(?A(i,j), ?b(inr(<i,j>)), j)"
oops
(*similar but specifying the type N simplifies the unification problems*)
-schematic_goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)
- * Eq(N, ?b(inr(<i,j>)), j)"
+schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(N, ?b(inl(<i,j>)), i)
+ \<times> Eq(N, ?b(inr(<i,j>)), j)"
oops
text "Deriving the addition operator"
schematic_goal [folded arith_defs]:
- "?c : PROD n:N. Eq(N, ?f(0,n), n)
- * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
+ "?c : \<Prod>n:N. Eq(N, ?f(0,n), n)
+ \<times> (\<Prod>m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
apply intr
apply eqintr
apply (rule comp_rls)
@@ -87,9 +86,9 @@
text "The addition function -- using explicit lambdas"
schematic_goal [folded arith_defs]:
- "?c : SUM plus : ?A .
- PROD x:N. Eq(N, plus`0`x, x)
- * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
+ "?c : \<Sum>plus : ?A .
+ \<Prod>x:N. Eq(N, plus`0`x, x)
+ \<times> (\<Prod>y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
apply intr
apply eqintr
apply (tactic "resolve_tac @{context} [TSimp.split_eqn] 3")
--- a/src/CTT/ex/Typechecking.thy Sat Oct 10 21:14:00 2015 +0200
+++ b/src/CTT/ex/Typechecking.thy Sat Oct 10 21:43:07 2015 +0200
@@ -22,7 +22,7 @@
apply (rule form_rls)
done
-schematic_goal "PROD z:?A . N + ?B(z) type"
+schematic_goal "\<Prod>z:?A . N + ?B(z) type"
apply (rule form_rls)
apply (rule form_rls)
apply (rule form_rls)
@@ -33,7 +33,7 @@
subsection \<open>Multi-step proofs: Type inference\<close>
-lemma "PROD w:N. N + N type"
+lemma "\<Prod>w:N. N + N type"
apply form
done
@@ -41,26 +41,26 @@
apply intr
done
-schematic_goal "PROD w:N . Eq(?A,w,w) type"
+schematic_goal "\<Prod>w:N . Eq(?A,w,w) type"
apply typechk
done
-schematic_goal "PROD x:N . PROD y:N . Eq(?A,x,y) type"
+schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type"
apply typechk
done
text "typechecking an application of fst"
-schematic_goal "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
+schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
apply typechk
done
text "typechecking the predecessor function"
-schematic_goal "lam n. rec(n, 0, \<lambda>x y. x) : ?A"
+schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A"
apply typechk
done
text "typechecking the addition function"
-schematic_goal "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
+schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
apply typechk
done
@@ -69,18 +69,18 @@
method_setup N =
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD (TRYALL (resolve_tac ctxt @{thms NF})))\<close>
-schematic_goal "lam w. <w,w> : ?A"
+schematic_goal "\<^bold>\<lambda>w. <w,w> : ?A"
apply typechk
apply N
done
-schematic_goal "lam x. lam y. x : ?A"
+schematic_goal "\<^bold>\<lambda>x. \<^bold>\<lambda>y. x : ?A"
apply typechk
apply N
done
text "typechecking fst (as a function object)"
-schematic_goal "lam i. split(i, \<lambda>j k. j) : ?A"
+schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A"
apply typechk
apply N
done