# 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 == \ Ssub" + Ssub_rel (infixl "\" 70) where + "a \ b == \ Ssub" abbreviation - Scomp_rel (infixl "~" 70) where - "a ~ b == \ Scomp" + Scomp_rel (infixl "\" 70) where + "a \ b == \ Scomp" abbreviation "regular(a) == a \ 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 "\" vary*) "union_aux(Var(n)) = (\t \ 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 "\" 70) and - Ssub_rel (infixl "\" 70) and - Scomp_rel (infixl "\" 70) + union (infixl "\" 70) where + "u \ v == union_aux(u)`v" inductive domains "Ssub" \ "redexes*redexes" intros - Sub_Var: "n \ nat ==> Var(n)<== Var(n)" - Sub_Fun: "[|u<== v|]==> Fun(u)<== Fun(v)" - Sub_App1: "[|u1<== v1; u2<== v2; b \ 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 \ nat ==> Var(n) \ Var(n)" + Sub_Fun: "[|u \ v|]==> Fun(u) \ Fun(v)" + Sub_App1: "[|u1 \ v1; u2 \ v2; b \ bool|]==> + App(0,u1,u2) \ App(b,v1,v2)" + Sub_App2: "[|u1 \ v1; u2 \ v2|]==> App(1,u1,u2) \ App(1,v1,v2)" type_intros redexes.intros bool_typechecks inductive domains "Scomp" \ "redexes*redexes" intros - Comp_Var: "n \ nat ==> Var(n) ~ Var(n)" - Comp_Fun: "[|u ~ v|]==> Fun(u) ~ Fun(v)" - Comp_App: "[|u1 ~ v1; u2 ~ v2; b1 \ bool; b2 \ bool|] - ==> App(b1,u1,u2) ~ App(b2,v1,v2)" + Comp_Var: "n \ nat ==> Var(n) \ Var(n)" + Comp_Fun: "[|u \ v|]==> Fun(u) \ Fun(v)" + Comp_App: "[|u1 \ v1; u2 \ v2; b1 \ bool; b2 \ bool|] + ==> App(b1,u1,u2) \ App(b2,v1,v2)" type_intros redexes.intros bool_typechecks inductive @@ -95,15 +90,15 @@ (* Equality rules for union *) (* ------------------------------------------------------------------------- *) -lemma union_Var [simp]: "n \ nat ==> Var(n) un Var(n)=Var(n)" +lemma union_Var [simp]: "n \ nat ==> Var(n) \ Var(n)=Var(n)" by (simp add: union_def) -lemma union_Fun [simp]: "v \ redexes ==> Fun(u) un Fun(v) = Fun(u un v)" +lemma union_Fun [simp]: "v \ redexes ==> Fun(u) \ Fun(v) = Fun(u \ v)" by (simp add: union_def) lemma union_App [simp]: "[|b2 \ bool; u2 \ redexes; v2 \ redexes|] - ==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)" + ==> App(b1,u1,v1) \ App(b2,u2,v2)=App(b1 or b2,u1 \ u2,v1 \ 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) \ Fun(t)" + "u \ Fun(t)" + "u \ Var(n)" + "u \ App(b,t,a)" + "Fun(t) \ v" + "App(b,f,a) \ v" + "Var(n) \ u" @@ -140,33 +135,33 @@ (* comp proofs *) (* ------------------------------------------------------------------------- *) -lemma comp_refl [simp]: "u \ redexes ==> u ~ u" +lemma comp_refl [simp]: "u \ redexes ==> u \ u" by (erule redexes.induct, blast+) -lemma comp_sym: "u ~ v ==> v ~ u" +lemma comp_sym: "u \ v ==> v \ u" by (erule Scomp.induct, blast+) -lemma comp_sym_iff: "u ~ v \ v ~ u" +lemma comp_sym_iff: "u \ v \ v \ u" by (blast intro: comp_sym) -lemma comp_trans [rule_format]: "u ~ v ==> \w. v ~ w\u ~ w" +lemma comp_trans [rule_format]: "u \ v ==> \w. v \ w\u \ w" by (erule Scomp.induct, blast+) (* ------------------------------------------------------------------------- *) (* union proofs *) (* ------------------------------------------------------------------------- *) -lemma union_l: "u ~ v ==> u <== (u un v)" +lemma union_l: "u \ v \ u \ (u \ 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 \ v \ v \ (u \ 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 \ v \ u \ v = v \ u" by (erule Scomp.induct, simp_all add: or_commute) (* ------------------------------------------------------------------------- *) @@ -174,7 +169,7 @@ (* ------------------------------------------------------------------------- *) lemma union_preserve_regular [rule_format]: - "u ~ v ==> regular(u)\regular(v)\regular(u un v)" + "u \ v \ regular(u) \ regular(v) \ regular(u \ 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 ==> \v. m|>v = n & m~v & regular(v)" +lemma simulation: "m=1=>n ==> \v. m|>v = n & m \ v & regular(v)" by (erule Spar_red1.induct, force+) @@ -237,12 +237,12 @@ (* ------------------------------------------------------------------------- *) lemma completeness_l [rule_format]: - "u~v ==> regular(v) \ unmark(u) =1=> unmark(u|>v)" + "u \ v ==> regular(v) \ unmark(u) =1=> unmark(u|>v)" apply (erule Scomp.induct) apply (auto simp add: unmmark_subst_rec) done -lemma completeness: "[|u \ lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)" +lemma completeness: "[|u \ lambda; u \ 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) \ u" + "Fun(n) \ u" + "u \ Fun(n)" + "App(1,Fun(t),a) \ u" + "App(0,t,a) \ u" inductive_cases [elim!]: "Fun(t) \ redexes" @@ -68,11 +68,11 @@ by (erule Sres.induct, force+) lemma residuals_intro [rule_format]: - "u~v ==> regular(v) \ (\w. residuals(u,v,w))" + "u \ v ==> regular(v) \ (\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 \ 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 \ 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 \ bool|] + "[|s \ u; regular(u); t \ v; regular(v); b \ 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 \ bool|] + "[|s \ u; regular(u); t \ v; regular(v); b \ 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) \ s |> t \ redexes" + "[|s \ t; regular(t)|]==> regular(t) \ s |> t \ redexes" by (erule Scomp.induct, auto) subsection\Commutation theorem\ -lemma sub_comp [simp]: "u<==v ==> u~v" +lemma sub_comp [simp]: "u \ v \ u \ v" by (erule Ssub.induct, simp_all) lemma sub_preserve_reg [rule_format, simp]: - "u<==v ==> regular(v) \ regular(u)" + "u \ v \ regular(v) \ regular(u)" by (erule Ssub.induct, auto) -lemma residuals_lift_rec: "[|u~v; k \ nat|]==> regular(v)\ (\n \ nat. +lemma residuals_lift_rec: "[|u \ v; k \ nat|]==> regular(v)\ (\n \ 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 ==> \v1 v2. v1~v2 \ regular(v2) \ regular(u2) \ + "u1 \ u2 ==> \v1 v2. v1 \ v2 \ regular(v2) \ regular(u2) \ (\n \ 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 \ u2; v1 \ v2; regular(u2); regular(v2)|] ==> (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)" by (simp add: residuals_subst_rec) @@ -143,21 +143,21 @@ subsection\Residuals are comp and regular\ lemma residuals_preserve_comp [rule_format, simp]: - "u~v ==> \w. u~w \ v~w \ regular(w) \ (u|>w) ~ (v|>w)" + "u \ v ==> \w. u \ w \ v \ w \ regular(w) \ (u|>w) \ (v|>w)" by (erule Scomp.induct, force+) lemma residuals_preserve_reg [rule_format, simp]: - "u~v ==> regular(u) \ regular(v) \ regular(u|>v)" + "u \ v ==> regular(u) \ regular(v) \ regular(u|>v)" apply (erule Scomp.induct, auto) done subsection\Preservation lemma\ -lemma union_preserve_comp: "u~v ==> v ~ (u un v)" +lemma union_preserve_comp: "u \ v ==> v \ (u \ v)" by (erule Scomp.induct, simp_all) lemma preservation [rule_format]: - "u ~ v ==> regular(v) \ u|>v = (u un v)|>v" + "u \ v ==> regular(v) \ u|>v = (u \ 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) \ (\w. w~v \ w~u \ + "v \ u \ + regular(u) \ (\w. w \ v \ w \ u \ 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 \ u; regular(u); w \ v|] ==> w |> u = (w|>v) |> (u|>v)" apply (rule prism_l) apply (rule_tac [4] comp_trans, auto) done @@ -183,7 +183,7 @@ subsection\Levy's Cube Lemma\ -lemma cube: "[|u~v; regular(v); regular(u); w~u|]==> +lemma cube: "[|u \ v; regular(v); regular(u); w \ 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\paving theorem\ -lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==> - \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 \ u; w \ v; regular(u); regular(v)|]==> + \uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u) \ vu \ + regular(vu) & (w|>v) \ uv \ regular(uv)" +apply (subgoal_tac "u \ 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 ==> \m \ nat. lift_rec(u,m) ~ lift_rec(v,m)" + "u \ v ==> \m \ nat. lift_rec(u,m) \ lift_rec(v,m)" by (erule Scomp.induct, simp_all add: comp_refl) lemma subst_rec_preserve_comp [rule_format, simp]: - "u2 ~ v2 ==> \m \ nat. \u1 \ redexes. \v1 \ redexes. - u1 ~ v1\ subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)" + "u2 \ v2 ==> \m \ nat. \u1 \ redexes. \v1 \ redexes. + u1 \ v1\ subst_rec(u1,u2,m) \ subst_rec(v1,v2,m)" by (erule Scomp.induct, simp_all add: subst_Var lift_rec_preserve_comp comp_refl)