# HG changeset patch
# User wenzelm
# Date 1444509656 -7200
# Node ID 6794de67556813ff8e4fac158e31a7e55215c40e
# Parent  6204c86280ff7f3ba13d602c449e8118175a8bb9
tuned syntax -- more symbols;

diff -r 6204c86280ff -r 6794de675568 src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Sat Oct 10 22:27:33 2015 +0200
+++ b/src/ZF/Resid/Redex.thy	Sat Oct 10 22:40:56 2015 +0200
@@ -18,18 +18,18 @@
   Sreg  :: "i"
 
 abbreviation
-  Ssub_rel  (infixl "<==" 70) where
-  "a<==b == <a,b> \<in> Ssub"
+  Ssub_rel  (infixl "\<Longleftarrow>" 70) where
+  "a \<Longleftarrow> b == <a,b> \<in> Ssub"
 
 abbreviation
-  Scomp_rel  (infixl "~" 70) where
-  "a ~ b == <a,b> \<in> Scomp"
+  Scomp_rel  (infixl "\<sim>" 70) where
+  "a \<sim> b == <a,b> \<in> Scomp"
 
 abbreviation
   "regular(a) == a \<in> Sreg"
 
 consts union_aux        :: "i=>i"
-primrec (*explicit lambda is required because both arguments of "un" vary*)
+primrec (*explicit lambda is required because both arguments of "\<squnion>" vary*)
   "union_aux(Var(n)) =
      (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
 
@@ -43,32 +43,27 @@
                      %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
 
 definition
-  union  (infixl "un" 70) where
-  "u un v == union_aux(u)`v"
-
-notation (xsymbols)
-  union  (infixl "\<squnion>" 70) and
-  Ssub_rel  (infixl "\<Longleftarrow>" 70) and
-  Scomp_rel  (infixl "\<sim>" 70)
+  union  (infixl "\<squnion>" 70) where
+  "u \<squnion> v == union_aux(u)`v"
 
 
 inductive
   domains       "Ssub" \<subseteq> "redexes*redexes"
   intros
-    Sub_Var:     "n \<in> nat ==> Var(n)<== Var(n)"
-    Sub_Fun:     "[|u<== v|]==> Fun(u)<== Fun(v)"
-    Sub_App1:    "[|u1<== v1; u2<== v2; b \<in> bool|]==>   
-                     App(0,u1,u2)<== App(b,v1,v2)"
-    Sub_App2:    "[|u1<== v1; u2<== v2|]==> App(1,u1,u2)<== App(1,v1,v2)"
+    Sub_Var:     "n \<in> nat ==> Var(n) \<Longleftarrow> Var(n)"
+    Sub_Fun:     "[|u \<Longleftarrow> v|]==> Fun(u) \<Longleftarrow> Fun(v)"
+    Sub_App1:    "[|u1 \<Longleftarrow> v1; u2 \<Longleftarrow> v2; b \<in> bool|]==>   
+                     App(0,u1,u2) \<Longleftarrow> App(b,v1,v2)"
+    Sub_App2:    "[|u1 \<Longleftarrow> v1; u2 \<Longleftarrow> v2|]==> App(1,u1,u2) \<Longleftarrow> App(1,v1,v2)"
   type_intros    redexes.intros bool_typechecks
 
 inductive
   domains       "Scomp" \<subseteq> "redexes*redexes"
   intros
-    Comp_Var:    "n \<in> nat ==> Var(n) ~ Var(n)"
-    Comp_Fun:    "[|u ~ v|]==> Fun(u) ~ Fun(v)"
-    Comp_App:    "[|u1 ~ v1; u2 ~ v2; b1 \<in> bool; b2 \<in> bool|]
-                  ==> App(b1,u1,u2) ~ App(b2,v1,v2)"
+    Comp_Var:    "n \<in> nat ==> Var(n) \<sim> Var(n)"
+    Comp_Fun:    "[|u \<sim> v|]==> Fun(u) \<sim> Fun(v)"
+    Comp_App:    "[|u1 \<sim> v1; u2 \<sim> v2; b1 \<in> bool; b2 \<in> bool|]
+                  ==> App(b1,u1,u2) \<sim> App(b2,v1,v2)"
   type_intros    redexes.intros bool_typechecks
 
 inductive
@@ -95,15 +90,15 @@
 (*    Equality rules for union                                               *)
 (* ------------------------------------------------------------------------- *)
 
-lemma union_Var [simp]: "n \<in> nat ==> Var(n) un Var(n)=Var(n)"
+lemma union_Var [simp]: "n \<in> nat ==> Var(n) \<squnion> Var(n)=Var(n)"
 by (simp add: union_def)
 
-lemma union_Fun [simp]: "v \<in> redexes ==> Fun(u) un Fun(v) = Fun(u un v)"
+lemma union_Fun [simp]: "v \<in> redexes ==> Fun(u) \<squnion> Fun(v) = Fun(u \<squnion> v)"
 by (simp add: union_def)
  
 lemma union_App [simp]:
      "[|b2 \<in> bool; u2 \<in> redexes; v2 \<in> redexes|]
-      ==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"
+      ==> App(b1,u1,v1) \<squnion> App(b2,u2,v2)=App(b1 or b2,u1 \<squnion> u2,v1 \<squnion> v2)"
 by (simp add: union_def)
 
 
@@ -126,13 +121,13 @@
   "regular(App(b,f,a))"
   "regular(Fun(b))"
   "regular(Var(b))"
-  "Fun(u) ~ Fun(t)"
-  "u ~ Fun(t)"
-  "u ~ Var(n)"
-  "u ~ App(b,t,a)"
-  "Fun(t) ~ v"
-  "App(b,f,a) ~ v"
-  "Var(n) ~ u"
+  "Fun(u) \<sim> Fun(t)"
+  "u \<sim> Fun(t)"
+  "u \<sim> Var(n)"
+  "u \<sim> App(b,t,a)"
+  "Fun(t) \<sim> v"
+  "App(b,f,a) \<sim> v"
+  "Var(n) \<sim> u"
 
 
 
@@ -140,33 +135,33 @@
 (*    comp proofs                                                            *)
 (* ------------------------------------------------------------------------- *)
 
-lemma comp_refl [simp]: "u \<in> redexes ==> u ~ u"
+lemma comp_refl [simp]: "u \<in> redexes ==> u \<sim> u"
 by (erule redexes.induct, blast+)
 
-lemma comp_sym: "u ~ v ==> v ~ u"
+lemma comp_sym: "u \<sim> v ==> v \<sim> u"
 by (erule Scomp.induct, blast+)
 
-lemma comp_sym_iff: "u ~ v \<longleftrightarrow> v ~ u"
+lemma comp_sym_iff: "u \<sim> v \<longleftrightarrow> v \<sim> u"
 by (blast intro: comp_sym)
 
-lemma comp_trans [rule_format]: "u ~ v ==> \<forall>w. v ~ w\<longrightarrow>u ~ w"
+lemma comp_trans [rule_format]: "u \<sim> v ==> \<forall>w. v \<sim> w\<longrightarrow>u \<sim> w"
 by (erule Scomp.induct, blast+)
 
 (* ------------------------------------------------------------------------- *)
 (*   union proofs                                                            *)
 (* ------------------------------------------------------------------------- *)
 
-lemma union_l: "u ~ v ==> u <== (u un v)"
+lemma union_l: "u \<sim> v \<Longrightarrow> u \<Longleftarrow> (u \<squnion> v)"
 apply (erule Scomp.induct)
 apply (erule_tac [3] boolE, simp_all)
 done
 
-lemma union_r: "u ~ v ==> v <== (u un v)"
+lemma union_r: "u \<sim> v \<Longrightarrow> v \<Longleftarrow> (u \<squnion> v)"
 apply (erule Scomp.induct)
 apply (erule_tac [3] c = b2 in boolE, simp_all)
 done
 
-lemma union_sym: "u ~ v ==> u un v = v un u"
+lemma union_sym: "u \<sim> v \<Longrightarrow> u \<squnion> v = v \<squnion> u"
 by (erule Scomp.induct, simp_all add: or_commute)
 
 (* ------------------------------------------------------------------------- *)
@@ -174,7 +169,7 @@
 (* ------------------------------------------------------------------------- *)
 
 lemma union_preserve_regular [rule_format]:
-     "u ~ v ==> regular(u)\<longrightarrow>regular(v)\<longrightarrow>regular(u un v)"
+     "u \<sim> v \<Longrightarrow> regular(u) \<longrightarrow> regular(v) \<longrightarrow> regular(u \<squnion> v)"
   by (erule Scomp.induct, auto)
 
 end
diff -r 6204c86280ff -r 6794de675568 src/ZF/Resid/Reduction.thy
--- a/src/ZF/Resid/Reduction.thy	Sat Oct 10 22:27:33 2015 +0200
+++ b/src/ZF/Resid/Reduction.thy	Sat Oct 10 22:40:56 2015 +0200
@@ -214,7 +214,7 @@
 (*      Simulation                                                           *)
 (* ------------------------------------------------------------------------- *)
 
-lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)"
+lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m \<sim> v & regular(v)"
 by (erule Spar_red1.induct, force+)
 
 
@@ -237,12 +237,12 @@
 (* ------------------------------------------------------------------------- *)
 
 lemma completeness_l [rule_format]:
-     "u~v ==> regular(v) \<longrightarrow> unmark(u) =1=> unmark(u|>v)"
+     "u \<sim> v ==> regular(v) \<longrightarrow> unmark(u) =1=> unmark(u|>v)"
 apply (erule Scomp.induct)
 apply (auto simp add: unmmark_subst_rec)
 done
 
-lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"
+lemma completeness: "[|u \<in> lambda; u \<sim> v; regular(v)|] ==> u =1=> unmark(u|>v)"
 by (drule completeness_l, simp_all add: lambda_unmark)
 
 end
diff -r 6204c86280ff -r 6794de675568 src/ZF/Resid/Residuals.thy
--- a/src/ZF/Resid/Residuals.thy	Sat Oct 10 22:27:33 2015 +0200
+++ b/src/ZF/Resid/Residuals.thy	Sat Oct 10 22:40:56 2015 +0200
@@ -50,11 +50,11 @@
 
 
 inductive_cases [elim!]:
-  "Var(n) <== u"
-  "Fun(n) <== u"
-  "u <== Fun(n)"
-  "App(1,Fun(t),a) <== u"
-  "App(0,t,a) <== u"
+  "Var(n) \<Longleftarrow> u"
+  "Fun(n) \<Longleftarrow> u"
+  "u \<Longleftarrow> Fun(n)"
+  "App(1,Fun(t),a) \<Longleftarrow> u"
+  "App(0,t,a) \<Longleftarrow> u"
 
 inductive_cases [elim!]:
   "Fun(t) \<in> redexes"
@@ -68,11 +68,11 @@
 by (erule Sres.induct, force+)
 
 lemma residuals_intro [rule_format]:
-     "u~v ==> regular(v) \<longrightarrow> (\<exists>w. residuals(u,v,w))"
+     "u \<sim> v ==> regular(v) \<longrightarrow> (\<exists>w. residuals(u,v,w))"
 by (erule Scomp.induct, force+)
 
 lemma comp_resfuncD:
-     "[| u~v;  regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
+     "[| u \<sim> v;  regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
 apply (frule residuals_intro, assumption, clarify)
 apply (subst the_equality)
 apply (blast intro: residuals_function)+
@@ -84,20 +84,20 @@
 by (unfold res_func_def, blast)
 
 lemma res_Fun [simp]: 
-    "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"
+    "[|s \<sim> t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"
 apply (unfold res_func_def)
 apply (blast intro: comp_resfuncD residuals_function) 
 done
 
 lemma res_App [simp]: 
-    "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
+    "[|s \<sim> u; regular(u); t \<sim> v; regular(v); b \<in> bool|]
      ==> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
 apply (unfold res_func_def) 
 apply (blast dest!: comp_resfuncD intro: residuals_function)
 done
 
 lemma res_redex [simp]: 
-    "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
+    "[|s \<sim> u; regular(u); t \<sim> v; regular(v); b \<in> bool|]
      ==> App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"
 apply (unfold res_func_def)
 apply (blast elim!: redexes.free_elims dest!: comp_resfuncD 
@@ -105,26 +105,26 @@
 done
 
 lemma resfunc_type [simp]:
-     "[|s~t; regular(t)|]==> regular(t) \<longrightarrow> s |> t \<in> redexes"
+     "[|s \<sim> t; regular(t)|]==> regular(t) \<longrightarrow> s |> t \<in> redexes"
   by (erule Scomp.induct, auto)
 
 subsection\<open>Commutation theorem\<close>
 
-lemma sub_comp [simp]: "u<==v ==> u~v"
+lemma sub_comp [simp]: "u \<Longleftarrow> v \<Longrightarrow> u \<sim> v"
 by (erule Ssub.induct, simp_all)
 
 lemma sub_preserve_reg [rule_format, simp]:
-     "u<==v  ==> regular(v) \<longrightarrow> regular(u)"
+     "u \<Longleftarrow> v \<Longrightarrow> regular(v) \<longrightarrow> regular(u)"
 by (erule Ssub.induct, auto)
 
-lemma residuals_lift_rec: "[|u~v; k \<in> nat|]==> regular(v)\<longrightarrow> (\<forall>n \<in> nat.   
+lemma residuals_lift_rec: "[|u \<sim> v; k \<in> nat|]==> regular(v)\<longrightarrow> (\<forall>n \<in> nat.   
          lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
 apply (erule Scomp.induct, safe)
 apply (simp_all add: lift_rec_Var subst_Var lift_subst)
 done
 
 lemma residuals_subst_rec:
-     "u1~u2 ==>  \<forall>v1 v2. v1~v2 \<longrightarrow> regular(v2) \<longrightarrow> regular(u2) \<longrightarrow> 
+     "u1 \<sim> u2 ==>  \<forall>v1 v2. v1 \<sim> v2 \<longrightarrow> regular(v2) \<longrightarrow> regular(u2) \<longrightarrow> 
                   (\<forall>n \<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) =  
                     subst_rec(v1 |> v2, u1 |> u2,n))"
 apply (erule Scomp.induct, safe)
@@ -135,7 +135,7 @@
 
 
 lemma commutation [simp]:
-     "[|u1~u2; v1~v2; regular(u2); regular(v2)|]
+     "[|u1 \<sim> u2; v1 \<sim> v2; regular(u2); regular(v2)|]
       ==> (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"
 by (simp add: residuals_subst_rec)
 
@@ -143,21 +143,21 @@
 subsection\<open>Residuals are comp and regular\<close>
 
 lemma residuals_preserve_comp [rule_format, simp]:
-     "u~v ==> \<forall>w. u~w \<longrightarrow> v~w \<longrightarrow> regular(w) \<longrightarrow> (u|>w) ~ (v|>w)"
+     "u \<sim> v ==> \<forall>w. u \<sim> w \<longrightarrow> v \<sim> w \<longrightarrow> regular(w) \<longrightarrow> (u|>w) \<sim> (v|>w)"
 by (erule Scomp.induct, force+)
 
 lemma residuals_preserve_reg [rule_format, simp]:
-     "u~v ==> regular(u) \<longrightarrow> regular(v) \<longrightarrow> regular(u|>v)"
+     "u \<sim> v ==> regular(u) \<longrightarrow> regular(v) \<longrightarrow> regular(u|>v)"
 apply (erule Scomp.induct, auto)
 done
 
 subsection\<open>Preservation lemma\<close>
 
-lemma union_preserve_comp: "u~v ==> v ~ (u un v)"
+lemma union_preserve_comp: "u \<sim> v ==> v \<sim> (u \<squnion> v)"
 by (erule Scomp.induct, simp_all)
 
 lemma preservation [rule_format]:
-     "u ~ v ==> regular(v) \<longrightarrow> u|>v = (u un v)|>v"
+     "u \<sim> v ==> regular(v) \<longrightarrow> u|>v = (u \<squnion> v)|>v"
 apply (erule Scomp.induct, safe)
 apply (drule_tac [3] psi = "Fun (u) |> v = w" for u v w in asm_rl)
 apply (auto simp add: union_preserve_comp comp_sym_iff)
@@ -170,12 +170,12 @@
 
 (* Having more assumptions than needed -- removed below  *)
 lemma prism_l [rule_format]:
-     "v<==u ==>  
-       regular(u) \<longrightarrow> (\<forall>w. w~v \<longrightarrow> w~u \<longrightarrow>   
+     "v \<Longleftarrow> u \<Longrightarrow>  
+       regular(u) \<longrightarrow> (\<forall>w. w \<sim> v \<longrightarrow> w \<sim> u \<longrightarrow>   
                             w |> u = (w|>v) |> (u|>v))"
 by (erule Ssub.induct, force+)
 
-lemma prism: "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)"
+lemma prism: "[|v \<Longleftarrow> u; regular(u); w \<sim> v|] ==> w |> u = (w|>v) |> (u|>v)"
 apply (rule prism_l)
 apply (rule_tac [4] comp_trans, auto)
 done
@@ -183,7 +183,7 @@
 
 subsection\<open>Levy's Cube Lemma\<close>
 
-lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>   
+lemma cube: "[|u \<sim> v; regular(v); regular(u); w \<sim> u|]==>   
            (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
 apply (subst preservation [of u], assumption, assumption)
 apply (subst preservation [of v], erule comp_sym, assumption)
@@ -198,10 +198,10 @@
 
 subsection\<open>paving theorem\<close>
 
-lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==>  
-           \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu & 
-             regular(vu) & (w|>v)~uv & regular(uv) "
-apply (subgoal_tac "u~v")
+lemma paving: "[|w \<sim> u; w \<sim> v; regular(u); regular(v)|]==>  
+           \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u) \<sim> vu \<and>
+             regular(vu) & (w|>v) \<sim> uv \<and> regular(uv)"
+apply (subgoal_tac "u \<sim> v")
 apply (safe intro!: exI)
 apply (rule cube)
 apply (simp_all add: comp_sym_iff)
diff -r 6204c86280ff -r 6794de675568 src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Sat Oct 10 22:27:33 2015 +0200
+++ b/src/ZF/Resid/Substitution.thy	Sat Oct 10 22:40:56 2015 +0200
@@ -249,12 +249,12 @@
 
 
 lemma lift_rec_preserve_comp [rule_format, simp]:
-     "u ~ v ==> \<forall>m \<in> nat. lift_rec(u,m) ~ lift_rec(v,m)"
+     "u \<sim> v ==> \<forall>m \<in> nat. lift_rec(u,m) \<sim> lift_rec(v,m)"
 by (erule Scomp.induct, simp_all add: comp_refl)
 
 lemma subst_rec_preserve_comp [rule_format, simp]:
-     "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes.
-                  u1 ~ v1\<longrightarrow> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
+     "u2 \<sim> v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes.
+                  u1 \<sim> v1\<longrightarrow> subst_rec(u1,u2,m) \<sim> subst_rec(v1,v2,m)"
 by (erule Scomp.induct,
     simp_all add: subst_Var lift_rec_preserve_comp comp_refl)