--- 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
--- 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
--- 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)
--- 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)