# HG changeset patch
# User wenzelm
# Date 1444504138 -7200
# Node ID 92e97b800d1e07ae4c532eafa41aa96c8d6ab5bb
# Parent  f068e84cb9f3f033e36c78f2e095acea323e4f08
tuned syntax -- more symbols;

diff -r f068e84cb9f3 -r 92e97b800d1e src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Sat Oct 10 21:03:35 2015 +0200
+++ b/src/Cube/Cube.thy	Sat Oct 10 21:08:58 2015 +0200
@@ -24,7 +24,7 @@
   Context :: "[typing, context] \<Rightarrow> context" and
   star :: "term"  ("*") and
   box :: "term"  ("\<box>") and
-  app :: "[term, term] \<Rightarrow> term"  (infixl "^" 20) and
+  app :: "[term, term] \<Rightarrow> term"  (infixl "\<cdot>" 20) and
   Has_type :: "[term, term] \<Rightarrow> typing"
 
 nonterminal context' and typing'
@@ -36,8 +36,8 @@
   "_MT_context" :: "context'"  ("")
   "_Context" :: "[typing', context'] \<Rightarrow> context'"  ("_ _")
   "_Has_type" :: "[term, term] \<Rightarrow> typing'"  ("(_:/ _)" [0, 0] 5)
-  "_Lam" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<Lambda> _:_./ _)" [0, 0, 0] 10)
-  "_Pi" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<Pi> _:_./ _)" [0, 0] 10)
+  "_Lam" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<^bold>\<lambda>_:_./ _)" [0, 0, 0] 10)
+  "_Pi" :: "[idt, term, term] \<Rightarrow> term"  ("(3\<Prod>_:_./ _)" [0, 0] 10)
   "_arrow" :: "[term, term] \<Rightarrow> term"  (infixr "\<rightarrow>" 10)
 translations
   "_Trueprop(G, t)" \<rightleftharpoons> "CONST Trueprop(G, t)"
@@ -45,12 +45,12 @@
   "_MT_context" \<rightleftharpoons> "CONST MT_context"
   "_Context" \<rightleftharpoons> "CONST Context"
   "_Has_type" \<rightleftharpoons> "CONST Has_type"
-  "\<Lambda> x:A. B" \<rightleftharpoons> "CONST Abs(A, \<lambda>x. B)"
-  "\<Pi> x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
+  "\<^bold>\<lambda>x:A. B" \<rightleftharpoons> "CONST Abs(A, \<lambda>x. B)"
+  "\<Prod>x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
   "A \<rightarrow> B" \<rightharpoonup> "CONST Prod(A, \<lambda>_. B)"
 
 syntax
-  "_Pi" :: "[idt, term, term] \<Rightarrow> term"    ("(3\<Pi> _:_./ _)" [0, 0] 10)
+  "_Pi" :: "[idt, term, term] \<Rightarrow> term"    ("(3\<Prod>_:_./ _)" [0, 0] 10)
 print_translation \<open>
   [(@{const_syntax Prod},
     fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
@@ -62,23 +62,23 @@
   strip_s: "\<lbrakk>A:*; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and
   strip_b: "\<lbrakk>A:\<box>; a:A \<Longrightarrow> G \<turnstile> x:X\<rbrakk> \<Longrightarrow> a:A G \<turnstile> x:X" and
 
-  app: "\<lbrakk>F:Prod(A, B); C:A\<rbrakk> \<Longrightarrow> F^C: B(C)" and
+  app: "\<lbrakk>F:Prod(A, B); C:A\<rbrakk> \<Longrightarrow> F\<cdot>C: B(C)" and
 
   pi_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> B(x):*\<rbrakk> \<Longrightarrow> Prod(A, B):*" and
 
   lam_ss: "\<lbrakk>A:*; \<And>x. x:A \<Longrightarrow> f(x):B(x); \<And>x. x:A \<Longrightarrow> B(x):* \<rbrakk>
             \<Longrightarrow> Abs(A, f) : Prod(A, B)" and
 
-  beta: "Abs(A, f)^a \<equiv> f(a)"
+  beta: "Abs(A, f)\<cdot>a \<equiv> f(a)"
 
 lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
 
 lemma imp_elim:
-  assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B \<Longrightarrow> PROP P"
+  assumes "f:A\<rightarrow>B" and "a:A" and "f\<cdot>a:B \<Longrightarrow> PROP P"
   shows "PROP P" by (rule app assms)+
 
 lemma pi_elim:
-  assumes "F:Prod(A,B)" and "a:A" and "F^a:B(a) \<Longrightarrow> PROP P"
+  assumes "F:Prod(A,B)" and "a:A" and "F\<cdot>a:B(a) \<Longrightarrow> PROP P"
   shows "PROP P" by (rule app assms)+
 
 
diff -r f068e84cb9f3 -r 92e97b800d1e src/Cube/Example.thy
--- a/src/Cube/Example.thy	Sat Oct 10 21:03:35 2015 +0200
+++ b/src/Cube/Example.thy	Sat Oct 10 21:08:58 2015 +0200
@@ -28,52 +28,52 @@
 schematic_goal "A:* \<turnstile> A\<rightarrow>A : ?T"
   by (depth_solve rules)
 
-schematic_goal "A:* \<turnstile> \<Lambda> a:A. a : ?T"
+schematic_goal "A:* \<turnstile> \<^bold>\<lambda>a:A. a : ?T"
   by (depth_solve rules)
 
-schematic_goal "A:* B:* b:B \<turnstile> \<Lambda> x:A. b : ?T"
+schematic_goal "A:* B:* b:B \<turnstile> \<^bold>\<lambda>x:A. b : ?T"
   by (depth_solve rules)
 
-schematic_goal "A:* b:A \<turnstile> (\<Lambda> a:A. a)^b: ?T"
+schematic_goal "A:* b:A \<turnstile> (\<^bold>\<lambda>a:A. a)\<cdot>b: ?T"
   by (depth_solve rules)
 
-schematic_goal "A:* B:* c:A b:B \<turnstile> (\<Lambda> x:A. b)^ c: ?T"
+schematic_goal "A:* B:* c:A b:B \<turnstile> (\<^bold>\<lambda>x:A. b)\<cdot> c: ?T"
   by (depth_solve rules)
 
-schematic_goal "A:* B:* \<turnstile> \<Lambda> a:A. \<Lambda> b:B. a : ?T"
+schematic_goal "A:* B:* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>b:B. a : ?T"
   by (depth_solve rules)
 
 
 subsection \<open>Second-order types\<close>
 
-schematic_goal (in L2) "\<turnstile> \<Lambda> A:*. \<Lambda> a:A. a : ?T"
+schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>A:*. \<^bold>\<lambda>a:A. a : ?T"
   by (depth_solve rules)
 
-schematic_goal (in L2) "A:* \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b)^A : ?T"
+schematic_goal (in L2) "A:* \<turnstile> (\<^bold>\<lambda>B:*.\<^bold>\<lambda>b:B. b)\<cdot>A : ?T"
   by (depth_solve rules)
 
-schematic_goal (in L2) "A:* b:A \<turnstile> (\<Lambda> B:*.\<Lambda> b:B. b) ^ A ^ b: ?T"
+schematic_goal (in L2) "A:* b:A \<turnstile> (\<^bold>\<lambda>B:*.\<^bold>\<lambda>b:B. b) \<cdot> A \<cdot> b: ?T"
   by (depth_solve rules)
 
-schematic_goal (in L2) "\<turnstile> \<Lambda> B:*.\<Lambda> a:(\<Pi> A:*.A).a ^ ((\<Pi> A:*.A)\<rightarrow>B) ^ a: ?T"
+schematic_goal (in L2) "\<turnstile> \<^bold>\<lambda>B:*.\<^bold>\<lambda>a:(\<Prod>A:*.A).a \<cdot> ((\<Prod>A:*.A)\<rightarrow>B) \<cdot> a: ?T"
   by (depth_solve rules)
 
 
 subsection \<open>Weakly higher-order propositional logic\<close>
 
-schematic_goal (in Lomega) "\<turnstile> \<Lambda> A:*.A\<rightarrow>A : ?T"
+schematic_goal (in Lomega) "\<turnstile> \<^bold>\<lambda>A:*.A\<rightarrow>A : ?T"
   by (depth_solve rules)
 
-schematic_goal (in Lomega) "B:* \<turnstile> (\<Lambda> A:*.A\<rightarrow>A) ^ B : ?T"
+schematic_goal (in Lomega) "B:* \<turnstile> (\<^bold>\<lambda>A:*.A\<rightarrow>A) \<cdot> B : ?T"
   by (depth_solve rules)
 
-schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<Lambda> y:B. b): ?T"
+schematic_goal (in Lomega) "B:* b:B \<turnstile> (\<^bold>\<lambda>y:B. b): ?T"
   by (depth_solve rules)
 
-schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F^(F^A): ?T"
+schematic_goal (in Lomega) "A:* F:*\<rightarrow>* \<turnstile> F\<cdot>(F\<cdot>A): ?T"
   by (depth_solve rules)
 
-schematic_goal (in Lomega) "A:* \<turnstile> \<Lambda> F:*\<rightarrow>*.F^(F^A): ?T"
+schematic_goal (in Lomega) "A:* \<turnstile> \<^bold>\<lambda>F:*\<rightarrow>*.F\<cdot>(F\<cdot>A): ?T"
   by (depth_solve rules)
 
 
@@ -82,41 +82,41 @@
 schematic_goal (in LP) "A:* \<turnstile> A \<rightarrow> * : ?T"
   by (depth_solve rules)
 
-schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* a:A \<turnstile> P\<cdot>a: ?T"
   by (depth_solve rules)
 
-schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Pi> a:A. P^a^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>A\<rightarrow>* a:A \<turnstile> \<Prod>a:A. P\<cdot>a\<cdot>a: ?T"
   by (depth_solve rules)
 
-schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> Q^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> Q\<cdot>a: ?T"
   by (depth_solve rules)
 
-schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Pi> a:A. P^a \<rightarrow> P^a: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Prod>a:A. P\<cdot>a \<rightarrow> P\<cdot>a: ?T"
   by (depth_solve rules)
 
-schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. \<Lambda> x:P^a. x: ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. \<^bold>\<lambda>x:P\<cdot>a. x: ?T"
   by (depth_solve rules)
 
-schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Pi> a:A. P^a\<rightarrow>Q) \<rightarrow> (\<Pi> a:A. P^a) \<rightarrow> Q : ?T"
+schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* \<turnstile> (\<Prod>a:A. P\<cdot>a\<rightarrow>Q) \<rightarrow> (\<Prod>a:A. P\<cdot>a) \<rightarrow> Q : ?T"
   by (depth_solve rules)
 
 schematic_goal (in LP) "A:* P:A\<rightarrow>* Q:* a0:A \<turnstile>
-        \<Lambda> x:\<Pi> a:A. P^a\<rightarrow>Q. \<Lambda> y:\<Pi> a:A. P^a. x^a0^(y^a0): ?T"
+        \<^bold>\<lambda>x:\<Prod>a:A. P\<cdot>a\<rightarrow>Q. \<^bold>\<lambda>y:\<Prod>a:A. P\<cdot>a. x\<cdot>a0\<cdot>(y\<cdot>a0): ?T"
   by (depth_solve rules)
 
 
 subsection \<open>Omega-order types\<close>
 
-schematic_goal (in L2) "A:* B:* \<turnstile> \<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
+schematic_goal (in L2) "A:* B:* \<turnstile> \<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
   by (depth_solve rules)
 
-schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Pi> C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
+schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*.\<^bold>\<lambda>B:*.\<Prod>C:*.(A\<rightarrow>B\<rightarrow>C)\<rightarrow>C : ?T"
   by (depth_solve rules)
 
-schematic_goal (in Lomega2) "\<turnstile> \<Lambda> A:*.\<Lambda> B:*.\<Lambda> x:A. \<Lambda> y:B. x : ?T"
+schematic_goal (in Lomega2) "\<turnstile> \<^bold>\<lambda>A:*.\<^bold>\<lambda>B:*.\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : ?T"
   by (depth_solve rules)
 
-schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Pi> P:*.P)\<rightarrow>(A\<rightarrow>\<Pi> P:*.P))"
+schematic_goal (in Lomega2) "A:* B:* \<turnstile> ?p : (A\<rightarrow>B) \<rightarrow> ((B\<rightarrow>\<Prod>P:*.P)\<rightarrow>(A\<rightarrow>\<Prod>P:*.P))"
   apply (strip_asms rules)
   apply (rule lam_ss)
     apply (depth_solve1 rules)
@@ -140,15 +140,15 @@
 
 subsection \<open>Second-order Predicate Logic\<close>
 
-schematic_goal (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<Lambda> a:A. P^a\<rightarrow>(\<Pi> A:*.A) : ?T"
+schematic_goal (in LP2) "A:* P:A\<rightarrow>* \<turnstile> \<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>(\<Prod>A:*.A) : ?T"
   by (depth_solve rules)
 
 schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
-    (\<Pi> a:A. \<Pi> b:A. P^a^b\<rightarrow>P^b^a\<rightarrow>\<Pi> P:*.P) \<rightarrow> \<Pi> a:A. P^a^a\<rightarrow>\<Pi> P:*.P : ?T"
+    (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P : ?T"
   by (depth_solve rules)
 
 schematic_goal (in LP2) "A:* P:A\<rightarrow>A\<rightarrow>* \<turnstile>
-    ?p: (\<Pi> a:A. \<Pi> b:A. P^a^b\<rightarrow>P^b^a\<rightarrow>\<Pi> P:*.P) \<rightarrow> \<Pi> a:A. P^a^a\<rightarrow>\<Pi> P:*.P"
+    ?p: (\<Prod>a:A. \<Prod>b:A. P\<cdot>a\<cdot>b\<rightarrow>P\<cdot>b\<cdot>a\<rightarrow>\<Prod>P:*.P) \<rightarrow> \<Prod>a:A. P\<cdot>a\<cdot>a\<rightarrow>\<Prod>P:*.P"
   -- \<open>Antisymmetry implies irreflexivity:\<close>
   apply (strip_asms rules)
   apply (rule lam_ss)
@@ -169,22 +169,22 @@
 
 subsection \<open>LPomega\<close>
 
-schematic_goal (in LPomega) "A:* \<turnstile> \<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
+schematic_goal (in LPomega) "A:* \<turnstile> \<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*.\<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T"
   by (depth_solve rules)
 
-schematic_goal (in LPomega) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>A\<rightarrow>*.\<Lambda> a:A. P^a^a : ?T"
+schematic_goal (in LPomega) "\<turnstile> \<^bold>\<lambda>A:*.\<^bold>\<lambda>P:A\<rightarrow>A\<rightarrow>*.\<^bold>\<lambda>a:A. P\<cdot>a\<cdot>a : ?T"
   by (depth_solve rules)
 
 
 subsection \<open>Constructions\<close>
 
-schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Lambda> a:A. P^a\<rightarrow>\<Pi> P:*.P: ?T"
+schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*.\<^bold>\<lambda>P:A\<rightarrow>*.\<^bold>\<lambda>a:A. P\<cdot>a\<rightarrow>\<Prod>P:*.P: ?T"
   by (depth_solve rules)
 
-schematic_goal (in CC) "\<turnstile> \<Lambda> A:*.\<Lambda> P:A\<rightarrow>*.\<Pi> a:A. P^a: ?T"
+schematic_goal (in CC) "\<turnstile> \<^bold>\<lambda>A:*.\<^bold>\<lambda>P:A\<rightarrow>*.\<Prod>a:A. P\<cdot>a: ?T"
   by (depth_solve rules)
 
-schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Pi> a:A. P^a)\<rightarrow>P^a"
+schematic_goal (in CC) "A:* P:A\<rightarrow>* a:A \<turnstile> ?p : (\<Prod>a:A. P\<cdot>a)\<rightarrow>P\<cdot>a"
   apply (strip_asms rules)
   apply (rule lam_ss)
     apply (depth_solve1 rules)
@@ -197,22 +197,22 @@
 subsection \<open>Some random examples\<close>
 
 schematic_goal (in LP2) "A:* c:A f:A\<rightarrow>A \<turnstile>
-    \<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T"
+    \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T"
   by (depth_solve rules)
 
-schematic_goal (in CC) "\<Lambda> A:*.\<Lambda> c:A. \<Lambda> f:A\<rightarrow>A.
-    \<Lambda> a:A. \<Pi> P:A\<rightarrow>*.P^c \<rightarrow> (\<Pi> x:A. P^x\<rightarrow>P^(f^x)) \<rightarrow> P^a : ?T"
+schematic_goal (in CC) "\<^bold>\<lambda>A:*.\<^bold>\<lambda>c:A. \<^bold>\<lambda>f:A\<rightarrow>A.
+    \<^bold>\<lambda>a:A. \<Prod>P:A\<rightarrow>*.P\<cdot>c \<rightarrow> (\<Prod>x:A. P\<cdot>x\<rightarrow>P\<cdot>(f\<cdot>x)) \<rightarrow> P\<cdot>a : ?T"
   by (depth_solve rules)
 
 schematic_goal (in LP2)
-  "A:* a:A b:A \<turnstile> ?p: (\<Pi> P:A\<rightarrow>*.P^a\<rightarrow>P^b) \<rightarrow> (\<Pi> P:A\<rightarrow>*.P^b\<rightarrow>P^a)"
+  "A:* a:A b:A \<turnstile> ?p: (\<Prod>P:A\<rightarrow>*.P\<cdot>a\<rightarrow>P\<cdot>b) \<rightarrow> (\<Prod>P:A\<rightarrow>*.P\<cdot>b\<rightarrow>P\<cdot>a)"
   -- \<open>Symmetry of Leibnitz equality\<close>
   apply (strip_asms rules)
   apply (rule lam_ss)
     apply (depth_solve1 rules)
    prefer 2
    apply (depth_solve1 rules)
-  apply (erule_tac a = "\<Lambda> x:A. \<Pi> Q:A\<rightarrow>*.Q^x\<rightarrow>Q^a" in pi_elim)
+  apply (erule_tac a = "\<^bold>\<lambda>x:A. \<Prod>Q:A\<rightarrow>*.Q\<cdot>x\<rightarrow>Q\<cdot>a" in pi_elim)
    apply (depth_solve1 rules)
   apply (unfold beta)
   apply (erule imp_elim)