1.1 --- a/src/ZF/IsaMakefile Fri Dec 21 23:20:29 2001 +0100
1.2 +++ b/src/ZF/IsaMakefile Sat Dec 22 19:42:35 2001 +0100
1.3 @@ -95,12 +95,9 @@
1.4
1.5 ZF-Resid: ZF $(LOG)/ZF-Resid.gz
1.6
1.7 -$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \
1.8 - Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
1.9 - Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
1.10 - Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
1.11 - Resid/Substitution.ML \
1.12 - Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
1.13 +$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \
1.14 + Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \
1.15 + Resid/Substitution.thy
1.16 @$(ISATOOL) usedir $(OUT)/ZF Resid
1.17
1.18
2.1 --- a/src/ZF/Resid/Confluence.ML Fri Dec 21 23:20:29 2001 +0100
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,59 +0,0 @@
2.4 -(* Title: Confluence.ML
2.5 - ID: $Id$
2.6 - Author: Ole Rasmussen
2.7 - Copyright 1995 University of Cambridge
2.8 - Logic Image: ZF
2.9 -*)
2.10 -
2.11 -open Confluence;
2.12 -
2.13 -(* ------------------------------------------------------------------------- *)
2.14 -(* strip lemmas *)
2.15 -(* ------------------------------------------------------------------------- *)
2.16 -
2.17 -Goalw [confluence_def,strip_def]
2.18 - "[|confluence(Spar_red1)|]==> strip";
2.19 -by (resolve_tac [impI RS allI RS allI] 1);
2.20 -by (etac Spar_red.induct 1);
2.21 -by (Fast_tac 1);
2.22 -by (fast_tac (claset() addIs [Spar_red.trans]) 1);
2.23 -qed "strip_lemma_r";
2.24 -
2.25 -
2.26 -Goalw [confluence_def,strip_def]
2.27 - "strip==> confluence(Spar_red)";
2.28 -by (resolve_tac [impI RS allI RS allI] 1);
2.29 -by (etac Spar_red.induct 1);
2.30 -by (Blast_tac 1);
2.31 -by (Clarify_tac 1);
2.32 -by (dres_inst_tac [("x1","z")] (spec RS mp) 1);
2.33 -by (blast_tac (claset() addIs [Spar_red.trans]) 2);
2.34 -by (assume_tac 1);
2.35 -qed "strip_lemma_l";
2.36 -
2.37 -(* ------------------------------------------------------------------------- *)
2.38 -(* Confluence *)
2.39 -(* ------------------------------------------------------------------------- *)
2.40 -
2.41 -
2.42 -Goalw [confluence_def] "confluence(Spar_red1)";
2.43 -by (Clarify_tac 1);
2.44 -by (ftac simulation 1);
2.45 -by (forw_inst_tac [("n","z")] simulation 1);
2.46 -by (Clarify_tac 1);
2.47 -by (forw_inst_tac [("v","va")] paving 1);
2.48 -by (TRYALL assume_tac);
2.49 -by (fast_tac (claset() addIs [completeness] addss (simpset())) 1);
2.50 -qed "parallel_moves";
2.51 -
2.52 -bind_thm ("confluence_parallel_reduction",
2.53 - parallel_moves RS strip_lemma_r RS strip_lemma_l);
2.54 -
2.55 -Goalw [confluence_def]
2.56 - "[|confluence(Spar_red)|]==> confluence(Sred)";
2.57 -by (blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
2.58 -val lemma1 = result();
2.59 -
2.60 -bind_thm ("confluence_beta_reduction",
2.61 - confluence_parallel_reduction RS lemma1);
2.62 -
3.1 --- a/src/ZF/Resid/Confluence.thy Fri Dec 21 23:20:29 2001 +0100
3.2 +++ b/src/ZF/Resid/Confluence.thy Sat Dec 22 19:42:35 2001 +0100
3.3 @@ -5,17 +5,119 @@
3.4 Logic Image: ZF
3.5 *)
3.6
3.7 -Confluence = Reduction+
3.8 +theory Confluence = Reduction:
3.9 +
3.10 +constdefs
3.11 + confluence :: "i=>o"
3.12 + "confluence(R) ==
3.13 + \<forall>x y. <x,y> \<in> R --> (\<forall>z.<x,z> \<in> R --> (\<exists>u.<y,u> \<in> R & <z,u> \<in> R))"
3.14 +
3.15 + strip :: "o"
3.16 + "strip == \<forall>x y. (x ===> y) -->
3.17 + (\<forall>z.(x =1=> z) --> (\<exists>u.(y =1=> u) & (z===>u)))"
3.18 +
3.19 +
3.20 +(* ------------------------------------------------------------------------- *)
3.21 +(* strip lemmas *)
3.22 +(* ------------------------------------------------------------------------- *)
3.23 +
3.24 +lemma strip_lemma_r:
3.25 + "[|confluence(Spar_red1)|]==> strip"
3.26 +apply (unfold confluence_def strip_def)
3.27 +apply (rule impI [THEN allI, THEN allI])
3.28 +apply (erule Spar_red.induct)
3.29 +apply fast
3.30 +apply (fast intro: Spar_red.trans)
3.31 +done
3.32 +
3.33 +
3.34 +lemma strip_lemma_l:
3.35 + "strip==> confluence(Spar_red)"
3.36 +apply (unfold confluence_def strip_def)
3.37 +apply (rule impI [THEN allI, THEN allI])
3.38 +apply (erule Spar_red.induct)
3.39 +apply blast
3.40 +apply clarify
3.41 +apply (blast intro: Spar_red.trans)
3.42 +done
3.43 +
3.44 +(* ------------------------------------------------------------------------- *)
3.45 +(* Confluence *)
3.46 +(* ------------------------------------------------------------------------- *)
3.47 +
3.48 +
3.49 +lemma parallel_moves: "confluence(Spar_red1)"
3.50 +apply (unfold confluence_def)
3.51 +apply clarify
3.52 +apply (frule simulation)
3.53 +apply (frule_tac n = "z" in simulation)
3.54 +apply clarify
3.55 +apply (frule_tac v = "va" in paving)
3.56 +apply (force intro: completeness)+
3.57 +done
3.58 +
3.59 +lemmas confluence_parallel_reduction =
3.60 + parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
3.61 +
3.62 +lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
3.63 +apply (unfold confluence_def, blast intro: par_red_red red_par_red)
3.64 +done
3.65 +
3.66 +lemmas confluence_beta_reduction =
3.67 + confluence_parallel_reduction [THEN lemma1, standard]
3.68 +
3.69 +
3.70 +(**** Conversion ****)
3.71
3.72 consts
3.73 - confluence :: i=>o
3.74 - strip :: o
3.75 + Sconv1 :: "i"
3.76 + "<-1->" :: "[i,i]=>o" (infixl 50)
3.77 + Sconv :: "i"
3.78 + "<--->" :: "[i,i]=>o" (infixl 50)
3.79
3.80 -defs
3.81 - confluence_def "confluence(R) ==
3.82 - \\<forall>x y. <x,y>:R --> (\\<forall>z.<x,z>:R -->
3.83 - (\\<exists>u.<y,u>:R & <z,u>:R))"
3.84 - strip_def "strip == \\<forall>x y. (x ===> y) --> (\\<forall>z.(x =1=> z) -->
3.85 - (\\<exists>u.(y =1=> u) & (z===>u)))"
3.86 +translations
3.87 + "a<-1->b" == "<a,b> \<in> Sconv1"
3.88 + "a<--->b" == "<a,b> \<in> Sconv"
3.89 +
3.90 +inductive
3.91 + domains "Sconv1" <= "lambda*lambda"
3.92 + intros
3.93 + red1: "m -1-> n ==> m<-1->n"
3.94 + expl: "n -1-> m ==> m<-1->n"
3.95 + type_intros red1D1 red1D2 lambda.intros bool_typechecks
3.96 +
3.97 +declare Sconv1.intros [intro]
3.98 +
3.99 +inductive
3.100 + domains "Sconv" <= "lambda*lambda"
3.101 + intros
3.102 + one_step: "m<-1->n ==> m<--->n"
3.103 + refl: "m \<in> lambda ==> m<--->m"
3.104 + trans: "[|m<--->n; n<--->p|] ==> m<--->p"
3.105 + type_intros Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks
3.106 +
3.107 +declare Sconv.intros [intro]
3.108 +
3.109 +lemma conv_sym: "m<--->n ==> n<--->m"
3.110 +apply (erule Sconv.induct)
3.111 +apply (erule Sconv1.induct)
3.112 +apply blast+
3.113 +done
3.114 +
3.115 +(* ------------------------------------------------------------------------- *)
3.116 +(* Church_Rosser Theorem *)
3.117 +(* ------------------------------------------------------------------------- *)
3.118 +
3.119 +lemma Church_Rosser: "m<--->n ==> \<exists>p.(m --->p) & (n ---> p)"
3.120 +apply (erule Sconv.induct)
3.121 +apply (erule Sconv1.induct)
3.122 +apply (blast intro: red1D1 redD2)
3.123 +apply (blast intro: red1D1 redD2)
3.124 +apply (blast intro: red1D1 redD2)
3.125 +apply (cut_tac confluence_beta_reduction)
3.126 +apply (unfold confluence_def)
3.127 +apply (blast intro: Sred.trans)
3.128 +done
3.129 +
3.130 end
3.131
4.1 --- a/src/ZF/Resid/Conversion.ML Fri Dec 21 23:20:29 2001 +0100
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,32 +0,0 @@
4.4 -(* Title: Conversion.ML
4.5 - ID: $Id$
4.6 - Author: Ole Rasmussen
4.7 - Copyright 1995 University of Cambridge
4.8 - Logic Image: ZF
4.9 -*)
4.10 -
4.11 -open Conversion;
4.12 -
4.13 -AddIs (Sconv.intrs @ Sconv1.intrs);
4.14 -
4.15 -Goal "m<--->n ==> n<--->m";
4.16 -by (etac Sconv.induct 1);
4.17 -by (etac Sconv1.induct 1);
4.18 -by (ALLGOALS Blast_tac);
4.19 -qed "conv_sym";
4.20 -
4.21 -(* ------------------------------------------------------------------------- *)
4.22 -(* Church_Rosser Theorem *)
4.23 -(* ------------------------------------------------------------------------- *)
4.24 -
4.25 -Goal "m<--->n ==> \\<exists>p.(m --->p) & (n ---> p)";
4.26 -by (etac Sconv.induct 1);
4.27 -by (etac Sconv1.induct 1);
4.28 -by (blast_tac (claset() addIs [red1D1,redD2]) 1);
4.29 -by (blast_tac (claset() addIs [red1D1,redD2]) 1);
4.30 -by (blast_tac (claset() addIs [red1D1,redD2]) 1);
4.31 -by (cut_facts_tac [confluence_beta_reduction] 1);
4.32 -by (rewtac confluence_def);
4.33 -by (blast_tac (claset() addIs [Sred.trans]) 1);
4.34 -qed "Church_Rosser";
4.35 -
5.1 --- a/src/ZF/Resid/Cube.ML Fri Dec 21 23:20:29 2001 +0100
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,68 +0,0 @@
5.4 -(* Title: Cube.ML
5.5 - ID: $Id$
5.6 - Author: Ole Rasmussen
5.7 - Copyright 1995 University of Cambridge
5.8 - Logic Image: ZF
5.9 -*)
5.10 -
5.11 -Addsimps [commutation, residuals_preserve_comp, sub_preserve_reg,
5.12 - residuals_preserve_reg, sub_comp, sub_comp RS comp_sym];
5.13 -
5.14 -(* ------------------------------------------------------------------------- *)
5.15 -(* Prism theorem *)
5.16 -(* ============= *)
5.17 -(* ------------------------------------------------------------------------- *)
5.18 -
5.19 -(* Having more assumptions than needed -- removed below *)
5.20 -Goal "v<==u ==> \
5.21 -\ regular(u) --> (\\<forall>w. w~v --> w~u --> \
5.22 -\ w |> u = (w|>v) |> (u|>v))";
5.23 -by (etac Ssub.induct 1);
5.24 -by Auto_tac;
5.25 -qed_spec_mp "prism_l";
5.26 -
5.27 -Goal "[|v <== u; regular(u); w~v|]==> \
5.28 -\ w |> u = (w|>v) |> (u|>v)";
5.29 -by (rtac prism_l 1);
5.30 -by (rtac comp_trans 4);
5.31 -by Auto_tac;
5.32 -qed "prism";
5.33 -
5.34 -
5.35 -(* ------------------------------------------------------------------------- *)
5.36 -(* Levy's Cube Lemma *)
5.37 -(* ------------------------------------------------------------------------- *)
5.38 -
5.39 -Goal "[|u~v; regular(v); regular(u); w~u|]==> \
5.40 -\ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
5.41 -by (stac preservation 1
5.42 - THEN assume_tac 1 THEN assume_tac 1);
5.43 -by (stac preservation 1
5.44 - THEN etac comp_sym 1 THEN assume_tac 1);
5.45 -by (stac (prism RS sym) 1);
5.46 -by (asm_full_simp_tac (simpset() addsimps
5.47 - [prism RS sym,union_l,union_preserve_regular,
5.48 - comp_sym_iff, union_sym]) 4);
5.49 -by (asm_simp_tac (simpset() addsimps [union_r, comp_sym_iff]) 1);
5.50 -by (asm_simp_tac (simpset() addsimps
5.51 - [union_preserve_regular, comp_sym_iff]) 1);
5.52 -by (etac comp_trans 1);
5.53 -by (atac 1);
5.54 -qed "cube";
5.55 -
5.56 -
5.57 -(* ------------------------------------------------------------------------- *)
5.58 -(* paving theorem *)
5.59 -(* ------------------------------------------------------------------------- *)
5.60 -
5.61 -Goal "[|w~u; w~v; regular(u); regular(v)|]==> \
5.62 -\ \\<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
5.63 -\ regular(vu) & (w|>v)~uv & regular(uv) ";
5.64 -by (subgoal_tac "u~v" 1);
5.65 -by (safe_tac (claset() addSIs [exI]));
5.66 -by (rtac cube 1);
5.67 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [comp_sym_iff])));
5.68 -by (ALLGOALS (blast_tac (claset() addIs [residuals_preserve_comp,
5.69 - comp_trans, comp_sym])));
5.70 -qed "paving";
5.71 -
6.1 --- a/src/ZF/Resid/ROOT.ML Fri Dec 21 23:20:29 2001 +0100
6.2 +++ b/src/ZF/Resid/ROOT.ML Sat Dec 22 19:42:35 2001 +0100
6.3 @@ -12,4 +12,4 @@
6.4 J. Functional Programming 4(3) 1994, 371-394.
6.5 *)
6.6
6.7 -time_use_thy "Conversion";
6.8 +time_use_thy "Confluence";
7.1 --- a/src/ZF/Resid/Redex.ML Fri Dec 21 23:20:29 2001 +0100
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,111 +0,0 @@
7.4 -(* Title: Redex.ML
7.5 - ID: $Id$
7.6 - Author: Ole Rasmussen
7.7 - Copyright 1995 University of Cambridge
7.8 - Logic Image: ZF
7.9 -*)
7.10 -
7.11 -Addsimps redexes.intrs;
7.12 -
7.13 -fun rotate n i = EVERY(replicate n (etac revcut_rl i));
7.14 -(* ------------------------------------------------------------------------- *)
7.15 -(* Specialisation of comp-rules *)
7.16 -(* ------------------------------------------------------------------------- *)
7.17 -
7.18 -val compD1 = Scomp.dom_subset RS subsetD RS SigmaD1;
7.19 -val compD2 = Scomp.dom_subset RS subsetD RS SigmaD2;
7.20 -
7.21 -val regD = Sreg.dom_subset RS subsetD;
7.22 -
7.23 -(* ------------------------------------------------------------------------- *)
7.24 -(* Equality rules for union *)
7.25 -(* ------------------------------------------------------------------------- *)
7.26 -
7.27 -Goal "n \\<in> nat==>Var(n) un Var(n)=Var(n)";
7.28 -by (asm_simp_tac (simpset() addsimps [union_def]) 1);
7.29 -qed "union_Var";
7.30 -
7.31 -Goal "[|u \\<in> redexes; v \\<in> redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
7.32 -by (asm_simp_tac (simpset() addsimps [union_def]) 1);
7.33 -qed "union_Fun";
7.34 -
7.35 -Goal "[|b1 \\<in> bool; b2 \\<in> bool; u1 \\<in> redexes; v1 \\<in> redexes; u2 \\<in> redexes; v2 \\<in> redexes|]==> \
7.36 -\ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
7.37 -by (asm_simp_tac (simpset() addsimps [union_def]) 1);
7.38 -qed "union_App";
7.39 -
7.40 -Addsimps (Ssub.intrs@bool_typechecks@
7.41 - Sreg.intrs@Scomp.intrs@
7.42 - [or_1 RSN (3,or_commute RS trans),
7.43 - or_0 RSN (3,or_commute RS trans),
7.44 - union_App,union_Fun,union_Var,compD2,compD1,regD]);
7.45 -
7.46 -AddIs Scomp.intrs;
7.47 -AddSEs [Sreg.mk_cases "regular(App(b,f,a))",
7.48 - Sreg.mk_cases "regular(Fun(b))",
7.49 - Sreg.mk_cases "regular(Var(b))",
7.50 - Scomp.mk_cases "Fun(u) ~ Fun(t)",
7.51 - Scomp.mk_cases "u ~ Fun(t)",
7.52 - Scomp.mk_cases "u ~ Var(n)",
7.53 - Scomp.mk_cases "u ~ App(b,t,a)",
7.54 - Scomp.mk_cases "Fun(t) ~ v",
7.55 - Scomp.mk_cases "App(b,f,a) ~ v",
7.56 - Scomp.mk_cases "Var(n) ~ u"];
7.57 -
7.58 -
7.59 -
7.60 -(* ------------------------------------------------------------------------- *)
7.61 -(* comp proofs *)
7.62 -(* ------------------------------------------------------------------------- *)
7.63 -
7.64 -Goal "u \\<in> redexes ==> u ~ u";
7.65 -by (etac redexes.induct 1);
7.66 -by (ALLGOALS Fast_tac);
7.67 -qed "comp_refl";
7.68 -
7.69 -Goal "u ~ v ==> v ~ u";
7.70 -by (etac Scomp.induct 1);
7.71 -by (ALLGOALS Fast_tac);
7.72 -qed "comp_sym";
7.73 -
7.74 -Goal "u ~ v <-> v ~ u";
7.75 -by (fast_tac (claset() addIs [comp_sym]) 1);
7.76 -qed "comp_sym_iff";
7.77 -
7.78 -
7.79 -Goal "u ~ v ==> \\<forall>w. v ~ w-->u ~ w";
7.80 -by (etac Scomp.induct 1);
7.81 -by (ALLGOALS Fast_tac);
7.82 -qed_spec_mp "comp_trans";
7.83 -
7.84 -(* ------------------------------------------------------------------------- *)
7.85 -(* union proofs *)
7.86 -(* ------------------------------------------------------------------------- *)
7.87 -
7.88 -Goal "u ~ v ==> u <== (u un v)";
7.89 -by (etac Scomp.induct 1);
7.90 -by (etac boolE 3);
7.91 -by (ALLGOALS Asm_simp_tac);
7.92 -qed "union_l";
7.93 -
7.94 -Goal "u ~ v ==> v <== (u un v)";
7.95 -by (etac Scomp.induct 1);
7.96 -by (eres_inst_tac [("c","b2")] boolE 3);
7.97 -by (ALLGOALS Asm_simp_tac);
7.98 -qed "union_r";
7.99 -
7.100 -Goal "u ~ v ==> u un v = v un u";
7.101 -by (etac Scomp.induct 1);
7.102 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute])));
7.103 -qed "union_sym";
7.104 -
7.105 -(* ------------------------------------------------------------------------- *)
7.106 -(* regular proofs *)
7.107 -(* ------------------------------------------------------------------------- *)
7.108 -
7.109 -Goal "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
7.110 -by (etac Scomp.induct 1);
7.111 -by Auto_tac;
7.112 -by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
7.113 -by (Asm_full_simp_tac 1);
7.114 -qed_spec_mp "union_preserve_regular";
8.1 --- a/src/ZF/Resid/Redex.thy Fri Dec 21 23:20:29 2001 +0100
8.2 +++ b/src/ZF/Resid/Redex.thy Sat Dec 22 19:42:35 2001 +0100
8.3 @@ -5,77 +5,186 @@
8.4 Logic Image: ZF
8.5 *)
8.6
8.7 -Redex = Main +
8.8 +theory Redex = Main:
8.9 consts
8.10 redexes :: i
8.11
8.12 datatype
8.13 - "redexes" = Var ("n \\<in> nat")
8.14 - | Fun ("t \\<in> redexes")
8.15 - | App ("b \\<in> bool" ,"f \\<in> redexes" , "a \\<in> redexes")
8.16 + "redexes" = Var ("n \<in> nat")
8.17 + | Fun ("t \<in> redexes")
8.18 + | App ("b \<in> bool" ,"f \<in> redexes" , "a \<in> redexes")
8.19
8.20
8.21 consts
8.22 - Ssub,Scomp,Sreg :: i
8.23 - "<==","~" :: [i,i]=>o (infixl 70)
8.24 - un :: [i,i]=>i (infixl 70)
8.25 - union_aux :: i=>i
8.26 - regular :: i=>o
8.27 + Ssub :: "i"
8.28 + Scomp :: "i"
8.29 + Sreg :: "i"
8.30 + union_aux :: "i=>i"
8.31 + regular :: "i=>o"
8.32
8.33 +(*syntax??*)
8.34 + un :: "[i,i]=>i" (infixl 70)
8.35 + "<==" :: "[i,i]=>o" (infixl 70)
8.36 + "~" :: "[i,i]=>o" (infixl 70)
8.37 +
8.38 +
8.39 translations
8.40 - "a<==b" == "<a,b>:Ssub"
8.41 - "a ~ b" == "<a,b>:Scomp"
8.42 - "regular(a)" == "a \\<in> Sreg"
8.43 + "a<==b" == "<a,b> \<in> Ssub"
8.44 + "a ~ b" == "<a,b> \<in> Scomp"
8.45 + "regular(a)" == "a \<in> Sreg"
8.46
8.47
8.48 primrec (*explicit lambda is required because both arguments of "un" vary*)
8.49 "union_aux(Var(n)) =
8.50 - (\\<lambda>t \\<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
8.51 + (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
8.52
8.53 "union_aux(Fun(u)) =
8.54 - (\\<lambda>t \\<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
8.55 + (\<lambda>t \<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
8.56 %b y z. 0, t))"
8.57
8.58 "union_aux(App(b,f,a)) =
8.59 - (\\<lambda>t \\<in> redexes.
8.60 + (\<lambda>t \<in> redexes.
8.61 redexes_case(%j. 0, %y. 0,
8.62 %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
8.63
8.64 defs
8.65 - union_def "u un v == union_aux(u)`v"
8.66 + union_def: "u un v == union_aux(u)`v"
8.67
8.68 +syntax (xsymbols)
8.69 + "op un" :: "[i,i]=>i" (infixl "\<squnion>" 70)
8.70 + "op <==" :: "[i,i]=>o" (infixl "\<Longleftarrow>" 70)
8.71 + "op ~" :: "[i,i]=>o" (infixl "\<sim>" 70)
8.72
8.73 inductive
8.74 domains "Ssub" <= "redexes*redexes"
8.75 - intrs
8.76 - Sub_Var "n \\<in> nat ==> Var(n)<== Var(n)"
8.77 - Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
8.78 - Sub_App1 "[|u1<== v1; u2<== v2; b \\<in> bool|]==>
8.79 + intros
8.80 + Sub_Var: "n \<in> nat ==> Var(n)<== Var(n)"
8.81 + Sub_Fun: "[|u<== v|]==> Fun(u)<== Fun(v)"
8.82 + Sub_App1: "[|u1<== v1; u2<== v2; b \<in> bool|]==>
8.83 App(0,u1,u2)<== App(b,v1,v2)"
8.84 - Sub_App2 "[|u1<== v1; u2<== v2|]==>
8.85 - App(1,u1,u2)<== App(1,v1,v2)"
8.86 - type_intrs "redexes.intrs@bool_typechecks"
8.87 + Sub_App2: "[|u1<== v1; u2<== v2|]==> App(1,u1,u2)<== App(1,v1,v2)"
8.88 + type_intros redexes.intros bool_typechecks
8.89
8.90 inductive
8.91 domains "Scomp" <= "redexes*redexes"
8.92 - intrs
8.93 - Comp_Var "n \\<in> nat ==> Var(n) ~ Var(n)"
8.94 - Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
8.95 - Comp_App "[|u1 ~ v1; u2 ~ v2; b1 \\<in> bool; b2 \\<in> bool|]==>
8.96 - App(b1,u1,u2) ~ App(b2,v1,v2)"
8.97 - type_intrs "redexes.intrs@bool_typechecks"
8.98 + intros
8.99 + Comp_Var: "n \<in> nat ==> Var(n) ~ Var(n)"
8.100 + Comp_Fun: "[|u ~ v|]==> Fun(u) ~ Fun(v)"
8.101 + Comp_App: "[|u1 ~ v1; u2 ~ v2; b1 \<in> bool; b2 \<in> bool|]
8.102 + ==> App(b1,u1,u2) ~ App(b2,v1,v2)"
8.103 + type_intros redexes.intros bool_typechecks
8.104
8.105 inductive
8.106 domains "Sreg" <= "redexes"
8.107 - intrs
8.108 - Reg_Var "n \\<in> nat ==> regular(Var(n))"
8.109 - Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
8.110 - Reg_App1 "[|regular(Fun(u)); regular(v)
8.111 - |]==>regular(App(1,Fun(u),v))"
8.112 - Reg_App2 "[|regular(u); regular(v)
8.113 - |]==>regular(App(0,u,v))"
8.114 - type_intrs "redexes.intrs@bool_typechecks"
8.115 + intros
8.116 + Reg_Var: "n \<in> nat ==> regular(Var(n))"
8.117 + Reg_Fun: "[|regular(u)|]==> regular(Fun(u))"
8.118 + Reg_App1: "[|regular(Fun(u)); regular(v) |]==>regular(App(1,Fun(u),v))"
8.119 + Reg_App2: "[|regular(u); regular(v) |]==>regular(App(0,u,v))"
8.120 + type_intros redexes.intros bool_typechecks
8.121
8.122
8.123 +declare redexes.intros [simp]
8.124 +
8.125 +(* ------------------------------------------------------------------------- *)
8.126 +(* Specialisation of comp-rules *)
8.127 +(* ------------------------------------------------------------------------- *)
8.128 +
8.129 +lemmas compD1 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD1]
8.130 +lemmas compD2 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD2]
8.131 +lemmas regD [simp] = Sreg.dom_subset [THEN subsetD]
8.132 +
8.133 +(* ------------------------------------------------------------------------- *)
8.134 +(* Equality rules for union *)
8.135 +(* ------------------------------------------------------------------------- *)
8.136 +
8.137 +lemma union_Var [simp]: "n \<in> nat ==> Var(n) un Var(n)=Var(n)"
8.138 +by (simp add: union_def)
8.139 +
8.140 +lemma union_Fun [simp]: "v \<in> redexes ==> Fun(u) un Fun(v) = Fun(u un v)"
8.141 +by (simp add: union_def)
8.142 +
8.143 +lemma union_App [simp]:
8.144 + "[|b2 \<in> bool; u2 \<in> redexes; v2 \<in> redexes|]
8.145 + ==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"
8.146 +by (simp add: union_def)
8.147 +
8.148 +
8.149 +lemma or_1_right [simp]: "a or 1 = 1"
8.150 +by (simp add: or_def cond_def)
8.151 +
8.152 +lemma or_0_right [simp]: "a \<in> bool \<Longrightarrow> a or 0 = a"
8.153 +by (simp add: or_def cond_def bool_def, auto)
8.154 +
8.155 +
8.156 +
8.157 +declare Ssub.intros [simp]
8.158 +declare bool_typechecks [simp]
8.159 +declare Sreg.intros [simp]
8.160 +declare Scomp.intros [simp]
8.161 +
8.162 +declare Scomp.intros [intro]
8.163 +
8.164 +inductive_cases [elim!]: "regular(App(b,f,a))"
8.165 +inductive_cases [elim!]: "regular(Fun(b))"
8.166 +inductive_cases [elim!]: "regular(Var(b))"
8.167 +inductive_cases [elim!]: "Fun(u) ~ Fun(t)"
8.168 +inductive_cases [elim!]: "u ~ Fun(t)"
8.169 +inductive_cases [elim!]: "u ~ Var(n)"
8.170 +inductive_cases [elim!]: "u ~ App(b,t,a)"
8.171 +inductive_cases [elim!]: "Fun(t) ~ v"
8.172 +inductive_cases [elim!]: "App(b,f,a) ~ v"
8.173 +inductive_cases [elim!]: "Var(n) ~ u"
8.174 +
8.175 +
8.176 +
8.177 +(* ------------------------------------------------------------------------- *)
8.178 +(* comp proofs *)
8.179 +(* ------------------------------------------------------------------------- *)
8.180 +
8.181 +lemma comp_refl [simp]: "u \<in> redexes ==> u ~ u"
8.182 +by (erule redexes.induct, blast+)
8.183 +
8.184 +lemma comp_sym: "u ~ v ==> v ~ u"
8.185 +by (erule Scomp.induct, blast+)
8.186 +
8.187 +lemma comp_sym_iff: "u ~ v <-> v ~ u"
8.188 +by (blast intro: comp_sym)
8.189 +
8.190 +lemma comp_trans [rule_format]: "u ~ v ==> \<forall>w. v ~ w-->u ~ w"
8.191 +by (erule Scomp.induct, blast+)
8.192 +
8.193 +(* ------------------------------------------------------------------------- *)
8.194 +(* union proofs *)
8.195 +(* ------------------------------------------------------------------------- *)
8.196 +
8.197 +lemma union_l: "u ~ v ==> u <== (u un v)"
8.198 +apply (erule Scomp.induct)
8.199 +apply (erule_tac [3] boolE)
8.200 +apply simp_all
8.201 +done
8.202 +
8.203 +lemma union_r: "u ~ v ==> v <== (u un v)"
8.204 +apply (erule Scomp.induct)
8.205 +apply (erule_tac [3] c = "b2" in boolE)
8.206 +apply simp_all
8.207 +done
8.208 +
8.209 +lemma union_sym: "u ~ v ==> u un v = v un u"
8.210 +by (erule Scomp.induct, simp_all add: or_commute)
8.211 +
8.212 +(* ------------------------------------------------------------------------- *)
8.213 +(* regular proofs *)
8.214 +(* ------------------------------------------------------------------------- *)
8.215 +
8.216 +lemma union_preserve_regular [rule_format]:
8.217 + "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"
8.218 +apply (erule Scomp.induct)
8.219 +apply auto
8.220 +(*select the given assumption for simplification*)
8.221 +apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp)
8.222 +apply simp
8.223 +done
8.224 +
8.225 end
8.226
9.1 --- a/src/ZF/Resid/Reduction.ML Fri Dec 21 23:20:29 2001 +0100
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,141 +0,0 @@
9.4 -(* Title: Reduction.ML
9.5 - ID: $Id$
9.6 - Author: Ole Rasmussen
9.7 - Copyright 1995 University of Cambridge
9.8 - Logic Image: ZF
9.9 -*)
9.10 -
9.11 -(* ------------------------------------------------------------------------- *)
9.12 -(* Setting up rulelists for reduction *)
9.13 -(* ------------------------------------------------------------------------- *)
9.14 -
9.15 -val red1D1 = Sred1.dom_subset RS subsetD RS SigmaD1;
9.16 -val red1D2 = Sred1.dom_subset RS subsetD RS SigmaD2;
9.17 -val redD1 = Sred.dom_subset RS subsetD RS SigmaD1;
9.18 -val redD2 = Sred.dom_subset RS subsetD RS SigmaD2;
9.19 -val par_red1D1 = Spar_red1.dom_subset RS subsetD RS SigmaD1;
9.20 -val par_red1D2 = Spar_red1.dom_subset RS subsetD RS SigmaD2;
9.21 -val par_redD1 = Spar_red.dom_subset RS subsetD RS SigmaD1;
9.22 -val par_redD2 = Spar_red.dom_subset RS subsetD RS SigmaD2;
9.23 -
9.24 -
9.25 -AddIs (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
9.26 - [Spar_red.one_step, lambda.dom_subset RS subsetD,
9.27 - unmark_type]@lambda.intrs@bool_typechecks);
9.28 -AddSEs [Spar_red1.mk_cases "Fun(t) =1=> Fun(u)"];
9.29 -
9.30 -Addsimps (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
9.31 - [Spar_red.one_step, substL_type, redD1, redD2, par_redD1,
9.32 - par_redD2, par_red1D2, unmark_type]);
9.33 -
9.34 -
9.35 -(* ------------------------------------------------------------------------- *)
9.36 -(* Lemmas for reduction *)
9.37 -(* ------------------------------------------------------------------------- *)
9.38 -
9.39 -Goal "m--->n ==> Fun(m) ---> Fun(n)";
9.40 -by (etac Sred.induct 1);
9.41 -by (resolve_tac [Sred.trans] 3);
9.42 -by (ALLGOALS (Asm_simp_tac ));
9.43 -qed "red_Fun";
9.44 -
9.45 -Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
9.46 -by (etac Sred.induct 1);
9.47 -by (resolve_tac [Sred.trans] 3);
9.48 -by (ALLGOALS (Asm_simp_tac ));
9.49 -qed "red_Apll";
9.50 -
9.51 -Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
9.52 -by (etac Sred.induct 1);
9.53 -by (resolve_tac [Sred.trans] 3);
9.54 -by (ALLGOALS (Asm_simp_tac ));
9.55 -qed "red_Aplr";
9.56 -
9.57 -Goal "[|m ---> m'; n--->n'|]==> Apl(m,n)--->Apl(m',n')";
9.58 -by (res_inst_tac [("n","Apl(m',n)")] Sred.trans 1);
9.59 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apll,red_Aplr]) ));
9.60 -qed "red_Apl";
9.61 -
9.62 -Goal "[|m \\<in> lambda; m':lambda; n \\<in> lambda; n':lambda; m ---> m'; n--->n'|]==> \
9.63 -\ Apl(Fun(m),n)---> n'/m'";
9.64 -by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1);
9.65 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apl,red_Fun]) ));
9.66 -qed "red_beta";
9.67 -
9.68 -
9.69 -(* ------------------------------------------------------------------------- *)
9.70 -(* Lemmas for parallel reduction *)
9.71 -(* ------------------------------------------------------------------------- *)
9.72 -
9.73 -
9.74 -Goal "m \\<in> lambda==> m =1=> m";
9.75 -by (etac lambda.induct 1);
9.76 -by (ALLGOALS (Asm_simp_tac ));
9.77 -qed "refl_par_red1";
9.78 -
9.79 -Goal "m-1->n ==> m=1=>n";
9.80 -by (etac Sred1.induct 1);
9.81 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [refl_par_red1]) ));
9.82 -qed "red1_par_red1";
9.83 -
9.84 -Goal "m--->n ==> m===>n";
9.85 -by (etac Sred.induct 1);
9.86 -by (resolve_tac [Spar_red.trans] 3);
9.87 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [refl_par_red1,red1_par_red1]) ));
9.88 -qed "red_par_red";
9.89 -
9.90 -Goal "m===>n ==> m--->n";
9.91 -by (etac Spar_red.induct 1);
9.92 -by (etac Spar_red1.induct 1);
9.93 -by (resolve_tac [Sred.trans] 5);
9.94 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Fun,red_beta,red_Apl]) ));
9.95 -qed "par_red_red";
9.96 -
9.97 -
9.98 -(* ------------------------------------------------------------------------- *)
9.99 -(* Simulation *)
9.100 -(* ------------------------------------------------------------------------- *)
9.101 -
9.102 -Goal "m=1=>n ==> \\<exists>v. m|>v = n & m~v & regular(v)";
9.103 -by (etac Spar_red1.induct 1);
9.104 -by Safe_tac;
9.105 -by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
9.106 -by (TRYALL(resolve_tac [res_redex,res_App,res_Fun,res_Var]));
9.107 -by (ALLGOALS (asm_simp_tac (simpset())));
9.108 -qed "simulation";
9.109 -
9.110 -
9.111 -(* ------------------------------------------------------------------------- *)
9.112 -(* commuting of unmark and subst *)
9.113 -(* ------------------------------------------------------------------------- *)
9.114 -
9.115 -Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
9.116 -by (etac redexes.induct 1);
9.117 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
9.118 -qed "unmmark_lift_rec";
9.119 -
9.120 -Goal "v \\<in> redexes ==> \\<forall>k \\<in> nat. \\<forall>u \\<in> redexes. \
9.121 -\ unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
9.122 -by (etac redexes.induct 1);
9.123 -by (ALLGOALS (asm_simp_tac
9.124 - (simpset() addsimps [unmmark_lift_rec, subst_Var])));
9.125 -qed "unmmark_subst_rec";
9.126 -
9.127 -
9.128 -(* ------------------------------------------------------------------------- *)
9.129 -(* Completeness *)
9.130 -(* ------------------------------------------------------------------------- *)
9.131 -
9.132 -Goal "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
9.133 -by (etac Scomp.induct 1);
9.134 -by (auto_tac (claset(),
9.135 - simpset() addsimps [unmmark_subst_rec]));
9.136 -by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
9.137 -by Auto_tac;
9.138 -qed_spec_mp "completeness_l";
9.139 -
9.140 -Goal "[|u \\<in> lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
9.141 -by (dtac completeness_l 1);
9.142 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lambda_unmark]) ));
9.143 -qed "completeness";
9.144 -
10.1 --- a/src/ZF/Resid/Reduction.thy Fri Dec 21 23:20:29 2001 +0100
10.2 +++ b/src/ZF/Resid/Reduction.thy Sat Dec 22 19:42:35 2001 +0100
10.3 @@ -5,56 +5,246 @@
10.4 Logic Image: ZF
10.5 *)
10.6
10.7 -Reduction = Terms+
10.8 +theory Reduction = Residuals:
10.9 +
10.10 +(**** Lambda-terms ****)
10.11
10.12 consts
10.13 - Sred1, Sred, Spar_red1,Spar_red :: i
10.14 - "-1->","--->","=1=>", "===>" :: [i,i]=>o (infixl 50)
10.15 + lambda :: "i"
10.16 + unmark :: "i=>i"
10.17 + Apl :: "[i,i]=>i"
10.18
10.19 translations
10.20 - "a -1-> b" == "<a,b>:Sred1"
10.21 - "a ---> b" == "<a,b>:Sred"
10.22 - "a =1=> b" == "<a,b>:Spar_red1"
10.23 - "a ===> b" == "<a,b>:Spar_red"
10.24 + "Apl(n,m)" == "App(0,n,m)"
10.25 +
10.26 +inductive
10.27 + domains "lambda" <= "redexes"
10.28 + intros
10.29 + Lambda_Var: " n \<in> nat ==> Var(n) \<in> lambda"
10.30 + Lambda_Fun: " u \<in> lambda ==> Fun(u) \<in> lambda"
10.31 + Lambda_App: "[|u \<in> lambda; v \<in> lambda|] ==> Apl(u,v) \<in> lambda"
10.32 + type_intros redexes.intros bool_typechecks
10.33 +
10.34 +declare lambda.intros [intro]
10.35 +
10.36 +primrec
10.37 + "unmark(Var(n)) = Var(n)"
10.38 + "unmark(Fun(u)) = Fun(unmark(u))"
10.39 + "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
10.40 +
10.41 +
10.42 +declare lambda.intros [simp]
10.43 +declare lambda.dom_subset [THEN subsetD, simp, intro]
10.44 +
10.45 +
10.46 +(* ------------------------------------------------------------------------- *)
10.47 +(* unmark lemmas *)
10.48 +(* ------------------------------------------------------------------------- *)
10.49 +
10.50 +lemma unmark_type [intro, simp]:
10.51 + "u \<in> redexes ==> unmark(u) \<in> lambda"
10.52 +by (erule redexes.induct, simp_all)
10.53 +
10.54 +lemma lambda_unmark: "u \<in> lambda ==> unmark(u) = u"
10.55 +by (erule lambda.induct, simp_all)
10.56 +
10.57 +
10.58 +(* ------------------------------------------------------------------------- *)
10.59 +(* lift and subst preserve lambda *)
10.60 +(* ------------------------------------------------------------------------- *)
10.61 +
10.62 +lemma liftL_type [rule_format]:
10.63 + "v \<in> lambda ==> \<forall>k \<in> nat. lift_rec(v,k) \<in> lambda"
10.64 +by (erule lambda.induct, simp_all add: lift_rec_Var)
10.65 +
10.66 +lemma substL_type [rule_format, simp]:
10.67 + "v \<in> lambda ==> \<forall>n \<in> nat. \<forall>u \<in> lambda. subst_rec(u,v,n) \<in> lambda"
10.68 +by (erule lambda.induct, simp_all add: liftL_type subst_Var)
10.69 +
10.70 +
10.71 +(* ------------------------------------------------------------------------- *)
10.72 +(* type-rule for reduction definitions *)
10.73 +(* ------------------------------------------------------------------------- *)
10.74 +
10.75 +lemmas red_typechecks = substL_type nat_typechecks lambda.intros
10.76 + bool_typechecks
10.77 +
10.78 +consts
10.79 + Sred1 :: "i"
10.80 + Sred :: "i"
10.81 + Spar_red1 :: "i"
10.82 + Spar_red :: "i"
10.83 + "-1->" :: "[i,i]=>o" (infixl 50)
10.84 + "--->" :: "[i,i]=>o" (infixl 50)
10.85 + "=1=>" :: "[i,i]=>o" (infixl 50)
10.86 + "===>" :: "[i,i]=>o" (infixl 50)
10.87 +
10.88 +translations
10.89 + "a -1-> b" == "<a,b> \<in> Sred1"
10.90 + "a ---> b" == "<a,b> \<in> Sred"
10.91 + "a =1=> b" == "<a,b> \<in> Spar_red1"
10.92 + "a ===> b" == "<a,b> \<in> Spar_red"
10.93
10.94
10.95 inductive
10.96 domains "Sred1" <= "lambda*lambda"
10.97 - intrs
10.98 - beta "[|m \\<in> lambda; n \\<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
10.99 - rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
10.100 - apl_l "[|m2 \\<in> lambda; m1 -1-> n1|] ==>
10.101 - Apl(m1,m2) -1-> Apl(n1,m2)"
10.102 - apl_r "[|m1 \\<in> lambda; m2 -1-> n2|] ==>
10.103 - Apl(m1,m2) -1-> Apl(m1,n2)"
10.104 - type_intrs "red_typechecks"
10.105 + intros
10.106 + beta: "[|m \<in> lambda; n \<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
10.107 + rfun: "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
10.108 + apl_l: "[|m2 \<in> lambda; m1 -1-> n1|] ==> Apl(m1,m2) -1-> Apl(n1,m2)"
10.109 + apl_r: "[|m1 \<in> lambda; m2 -1-> n2|] ==> Apl(m1,m2) -1-> Apl(m1,n2)"
10.110 + type_intros red_typechecks
10.111 +
10.112 +declare Sred1.intros [intro, simp]
10.113
10.114 inductive
10.115 domains "Sred" <= "lambda*lambda"
10.116 - intrs
10.117 - one_step "[|m-1->n|] ==> m--->n"
10.118 - refl "m \\<in> lambda==>m --->m"
10.119 - trans "[|m--->n; n--->p|]==>m--->p"
10.120 - type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks"
10.121 + intros
10.122 + one_step: "m-1->n ==> m--->n"
10.123 + refl: "m \<in> lambda==>m --->m"
10.124 + trans: "[|m--->n; n--->p|] ==>m--->p"
10.125 + type_intros Sred1.dom_subset [THEN subsetD] red_typechecks
10.126 +
10.127 +declare Sred.one_step [intro, simp]
10.128 +declare Sred.refl [intro, simp]
10.129
10.130 inductive
10.131 domains "Spar_red1" <= "lambda*lambda"
10.132 - intrs
10.133 - beta "[|m =1=> m';
10.134 - n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
10.135 - rvar "n \\<in> nat==> Var(n) =1=> Var(n)"
10.136 - rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
10.137 - rapl "[|m =1=> m';
10.138 - n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
10.139 - type_intrs "red_typechecks"
10.140 + intros
10.141 + beta: "[|m =1=> m'; n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
10.142 + rvar: "n \<in> nat ==> Var(n) =1=> Var(n)"
10.143 + rfun: "m =1=> m' ==> Fun(m) =1=> Fun(m')"
10.144 + rapl: "[|m =1=> m'; n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
10.145 + type_intros red_typechecks
10.146
10.147 - inductive
10.148 - domains "Spar_red" <= "lambda*lambda"
10.149 - intrs
10.150 - one_step "[|m =1=> n|] ==> m ===> n"
10.151 - trans "[|m===>n; n===>p|]==>m===>p"
10.152 - type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
10.153 +declare Spar_red1.intros [intro, simp]
10.154
10.155 +inductive
10.156 + domains "Spar_red" <= "lambda*lambda"
10.157 + intros
10.158 + one_step: "m =1=> n ==> m ===> n"
10.159 + trans: "[|m===>n; n===>p|] ==> m===>p"
10.160 + type_intros Spar_red1.dom_subset [THEN subsetD] red_typechecks
10.161 +
10.162 +declare Spar_red.one_step [intro, simp]
10.163 +
10.164 +
10.165 +
10.166 +(* ------------------------------------------------------------------------- *)
10.167 +(* Setting up rule lists for reduction *)
10.168 +(* ------------------------------------------------------------------------- *)
10.169 +
10.170 +lemmas red1D1 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD1]
10.171 +lemmas red1D2 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD2]
10.172 +lemmas redD1 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD1]
10.173 +lemmas redD2 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD2]
10.174 +
10.175 +lemmas par_red1D1 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD1]
10.176 +lemmas par_red1D2 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD2]
10.177 +lemmas par_redD1 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD1]
10.178 +lemmas par_redD2 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD2]
10.179 +
10.180 +declare bool_typechecks [intro]
10.181 +
10.182 +inductive_cases [elim!]: "Fun(t) =1=> Fun(u)"
10.183 +
10.184 +
10.185 +
10.186 +(* ------------------------------------------------------------------------- *)
10.187 +(* Lemmas for reduction *)
10.188 +(* ------------------------------------------------------------------------- *)
10.189 +
10.190 +lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)"
10.191 +apply (erule Sred.induct)
10.192 +apply (rule_tac [3] Sred.trans)
10.193 +apply simp_all
10.194 +done
10.195 +
10.196 +lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)"
10.197 +apply (erule Sred.induct)
10.198 +apply (rule_tac [3] Sred.trans)
10.199 +apply simp_all
10.200 +done
10.201 +
10.202 +lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')"
10.203 +apply (erule Sred.induct)
10.204 +apply (rule_tac [3] Sred.trans)
10.205 +apply simp_all
10.206 +done
10.207 +
10.208 +lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')"
10.209 +apply (rule_tac n = "Apl (m',n) " in Sred.trans)
10.210 +apply (simp_all add: red_Apll red_Aplr)
10.211 +done
10.212 +
10.213 +lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==>
10.214 + Apl(Fun(m),n)---> n'/m'"
10.215 +apply (rule_tac n = "Apl (Fun (m') ,n') " in Sred.trans)
10.216 +apply (simp_all add: red_Apl red_Fun)
10.217 +done
10.218 +
10.219 +
10.220 +(* ------------------------------------------------------------------------- *)
10.221 +(* Lemmas for parallel reduction *)
10.222 +(* ------------------------------------------------------------------------- *)
10.223 +
10.224 +
10.225 +lemma refl_par_red1: "m \<in> lambda==> m =1=> m"
10.226 +by (erule lambda.induct, simp_all)
10.227 +
10.228 +lemma red1_par_red1: "m-1->n ==> m=1=>n"
10.229 +by (erule Sred1.induct, simp_all add: refl_par_red1)
10.230 +
10.231 +lemma red_par_red: "m--->n ==> m===>n"
10.232 +apply (erule Sred.induct)
10.233 +apply (rule_tac [3] Spar_red.trans)
10.234 +apply (simp_all add: refl_par_red1 red1_par_red1)
10.235 +done
10.236 +
10.237 +lemma par_red_red: "m===>n ==> m--->n"
10.238 +apply (erule Spar_red.induct)
10.239 +apply (erule Spar_red1.induct)
10.240 +apply (rule_tac [5] Sred.trans)
10.241 +apply (simp_all add: red_Fun red_beta red_Apl)
10.242 +done
10.243 +
10.244 +
10.245 +(* ------------------------------------------------------------------------- *)
10.246 +(* Simulation *)
10.247 +(* ------------------------------------------------------------------------- *)
10.248 +
10.249 +lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)"
10.250 +by (erule Spar_red1.induct, force+)
10.251 +
10.252 +
10.253 +(* ------------------------------------------------------------------------- *)
10.254 +(* commuting of unmark and subst *)
10.255 +(* ------------------------------------------------------------------------- *)
10.256 +
10.257 +lemma unmmark_lift_rec:
10.258 + "u \<in> redexes ==> \<forall>k \<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)"
10.259 +by (erule redexes.induct, simp_all add: lift_rec_Var)
10.260 +
10.261 +lemma unmmark_subst_rec:
10.262 + "v \<in> redexes ==> \<forall>k \<in> nat. \<forall>u \<in> redexes.
10.263 + unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)"
10.264 +by (erule redexes.induct, simp_all add: unmmark_lift_rec subst_Var)
10.265 +
10.266 +
10.267 +(* ------------------------------------------------------------------------- *)
10.268 +(* Completeness *)
10.269 +(* ------------------------------------------------------------------------- *)
10.270 +
10.271 +lemma completeness_l [rule_format]:
10.272 + "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"
10.273 +apply (erule Scomp.induct)
10.274 +apply (auto simp add: unmmark_subst_rec)
10.275 +apply (drule_tac psi = "Fun (?u) =1=> ?w" in asm_rl)
10.276 +apply auto
10.277 +done
10.278 +
10.279 +lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"
10.280 +by (drule completeness_l, simp_all add: lambda_unmark)
10.281
10.282 end
10.283
11.1 --- a/src/ZF/Resid/Residuals.ML Fri Dec 21 23:20:29 2001 +0100
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,182 +0,0 @@
11.4 -(* Title: Residuals.ML
11.5 - ID: $Id$
11.6 - Author: Ole Rasmussen
11.7 - Copyright 1995 University of Cambridge
11.8 - Logic Image: ZF
11.9 -*)
11.10 -
11.11 -(* ------------------------------------------------------------------------- *)
11.12 -(* Setting up rule lists *)
11.13 -(* ------------------------------------------------------------------------- *)
11.14 -
11.15 -AddIs (Sres.intrs @ Sreg.intrs @ [subst_type]);
11.16 -AddSEs (map Sres.mk_cases
11.17 - ["residuals(Var(n),Var(n),v)",
11.18 - "residuals(Fun(t),Fun(u),v)",
11.19 - "residuals(App(b, u1, u2), App(0, v1, v2),v)",
11.20 - "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)",
11.21 - "residuals(Var(n),u,v)",
11.22 - "residuals(Fun(t),u,v)",
11.23 - "residuals(App(b, u1, u2), w,v)",
11.24 - "residuals(u,Var(n),v)",
11.25 - "residuals(u,Fun(t),v)",
11.26 - "residuals(w,App(b, u1, u2),v)"]);
11.27 -
11.28 -AddSEs (map Ssub.mk_cases
11.29 - ["Var(n) <== u",
11.30 - "Fun(n) <== u",
11.31 - "u <== Fun(n)",
11.32 - "App(1,Fun(t),a) <== u",
11.33 - "App(0,t,a) <== u"]);
11.34 -
11.35 -AddSEs [redexes.mk_cases "Fun(t):redexes"];
11.36 -
11.37 -Addsimps Sres.intrs;
11.38 -val resD1 = Sres.dom_subset RS subsetD RS SigmaD1;
11.39 -val resD2 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1;
11.40 -val resD3 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2;
11.41 -
11.42 -
11.43 -(* ------------------------------------------------------------------------- *)
11.44 -(* residuals is a partial function *)
11.45 -(* ------------------------------------------------------------------------- *)
11.46 -
11.47 -Goal "residuals(u,v,w) ==> \\<forall>w1. residuals(u,v,w1) --> w1 = w";
11.48 -by (etac Sres.induct 1);
11.49 -by (ALLGOALS Force_tac);
11.50 -qed_spec_mp "residuals_function";
11.51 -
11.52 -Goal "u~v ==> regular(v) --> (\\<exists>w. residuals(u,v,w))";
11.53 -by (etac Scomp.induct 1);
11.54 -by (ALLGOALS Fast_tac);
11.55 -qed "residuals_intro";
11.56 -
11.57 -Goal "[| u~v; regular(v) |] ==> residuals(u,v,THE w. residuals(u, v, w))";
11.58 -by (resolve_tac [residuals_intro RS mp RS exE] 1);
11.59 -by (stac the_equality 3);
11.60 -by (ALLGOALS (blast_tac (claset() addIs [residuals_function])));
11.61 -qed "comp_resfuncD";
11.62 -
11.63 -
11.64 -(* ------------------------------------------------------------------------- *)
11.65 -(* Residual function *)
11.66 -(* ------------------------------------------------------------------------- *)
11.67 -
11.68 -Goalw [res_func_def] "n \\<in> nat ==> Var(n) |> Var(n) = Var(n)";
11.69 -by (Blast_tac 1);
11.70 -qed "res_Var";
11.71 -
11.72 -Goalw [res_func_def]
11.73 - "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)";
11.74 -by (blast_tac (claset() addSDs [comp_resfuncD]
11.75 - addIs [residuals_function]) 1);
11.76 -qed "res_Fun";
11.77 -
11.78 -Goalw [res_func_def]
11.79 - "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
11.80 -\ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
11.81 -by (blast_tac (claset() addSDs [comp_resfuncD]
11.82 - addIs [residuals_function]) 1);
11.83 -qed "res_App";
11.84 -
11.85 -Goalw [res_func_def]
11.86 - "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
11.87 -\ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
11.88 -by (blast_tac (claset() addSEs redexes.free_SEs
11.89 - addSDs [comp_resfuncD]
11.90 - addIs [residuals_function]) 1);
11.91 -qed "res_redex";
11.92 -
11.93 -Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t \\<in> redexes";
11.94 -by (etac Scomp.induct 1);
11.95 -by (auto_tac (claset(),
11.96 - simpset() addsimps [res_Var,res_Fun,res_App,res_redex]));
11.97 -by (dres_inst_tac [("psi", "Fun(?u) |> ?v \\<in> redexes")] asm_rl 1);
11.98 -by (auto_tac (claset(),
11.99 - simpset() addsimps [res_Fun]));
11.100 -qed "resfunc_type";
11.101 -
11.102 -Addsimps [res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
11.103 - lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type,
11.104 - subst_rec_preserve_reg];
11.105 -
11.106 -
11.107 -(* ------------------------------------------------------------------------- *)
11.108 -(* Commutation theorem *)
11.109 -(* ------------------------------------------------------------------------- *)
11.110 -
11.111 -Goal "u<==v ==> u~v";
11.112 -by (etac Ssub.induct 1);
11.113 -by (ALLGOALS Asm_simp_tac);
11.114 -qed "sub_comp";
11.115 -
11.116 -Goal "u<==v ==> regular(v) --> regular(u)";
11.117 -by (etac Ssub.induct 1);
11.118 -by Auto_tac;
11.119 -qed_spec_mp "sub_preserve_reg";
11.120 -
11.121 -Goal "[|u~v; k \\<in> nat|]==> regular(v)--> (\\<forall>n \\<in> nat. \
11.122 -\ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
11.123 -by (etac Scomp.induct 1);
11.124 -by Safe_tac;
11.125 -by (ALLGOALS
11.126 - (asm_full_simp_tac
11.127 - (simpset() addsimps [lift_rec_Var,subst_Var,lift_subst])));
11.128 -by (rotate_tac ~2 1);
11.129 -by (Asm_full_simp_tac 1);
11.130 -qed "residuals_lift_rec";
11.131 -
11.132 -Goal "u1~u2 ==> \\<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
11.133 -\ (\\<forall>n \\<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
11.134 -\ subst_rec(v1 |> v2, u1 |> u2,n))";
11.135 -by (etac Scomp.induct 1);
11.136 -by Safe_tac;
11.137 -by (ALLGOALS
11.138 - (asm_simp_tac
11.139 - (simpset() addsimps [lift_rec_Var,subst_Var,residuals_lift_rec])));
11.140 -by (dres_inst_tac [("psi", "\\<forall>x.?P(x)")] asm_rl 1);
11.141 -by (asm_full_simp_tac (simpset() addsimps [substitution]) 1);
11.142 -qed "residuals_subst_rec";
11.143 -
11.144 -
11.145 -Goal "[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\
11.146 -\ (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)";
11.147 -by (asm_simp_tac (simpset() addsimps [residuals_subst_rec]) 1);
11.148 -qed "commutation";
11.149 -
11.150 -(* ------------------------------------------------------------------------- *)
11.151 -(* Residuals are comp and regular *)
11.152 -(* ------------------------------------------------------------------------- *)
11.153 -
11.154 -Goal "u~v ==> \\<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
11.155 -by (etac Scomp.induct 1);
11.156 -by (ALLGOALS Force_tac);
11.157 -qed_spec_mp "residuals_preserve_comp";
11.158 -
11.159 -
11.160 -Goal "u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
11.161 -by (etac Scomp.induct 1);
11.162 -by Safe_tac;
11.163 -by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
11.164 -by Auto_tac;
11.165 -qed_spec_mp "residuals_preserve_reg";
11.166 -
11.167 -(* ------------------------------------------------------------------------- *)
11.168 -(* Preservation lemma *)
11.169 -(* ------------------------------------------------------------------------- *)
11.170 -
11.171 -Goal "u~v ==> v ~ (u un v)";
11.172 -by (etac Scomp.induct 1);
11.173 -by (ALLGOALS Asm_simp_tac);
11.174 -qed "union_preserve_comp";
11.175 -
11.176 -Goal "u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
11.177 -by (etac Scomp.induct 1);
11.178 -by Safe_tac;
11.179 -by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
11.180 -by (auto_tac (claset(),
11.181 - simpset() addsimps [union_preserve_comp,comp_sym_iff]));
11.182 -by (asm_full_simp_tac (simpset() addsimps
11.183 - [union_preserve_comp RS comp_sym,
11.184 - comp_sym RS union_preserve_comp RS comp_sym]) 1);
11.185 -qed_spec_mp "preservation";
12.1 --- a/src/ZF/Resid/Residuals.thy Fri Dec 21 23:20:29 2001 +0100
12.2 +++ b/src/ZF/Resid/Residuals.thy Sat Dec 22 19:42:35 2001 +0100
12.3 @@ -6,31 +6,249 @@
12.4
12.5 *)
12.6
12.7 -Residuals = Substitution+
12.8 +theory Residuals = Substitution:
12.9
12.10 consts
12.11 - Sres :: i
12.12 - residuals :: [i,i,i]=>i
12.13 - "|>" :: [i,i]=>i (infixl 70)
12.14 -
12.15 + Sres :: "i"
12.16 + residuals :: "[i,i,i]=>i"
12.17 + "|>" :: "[i,i]=>i" (infixl 70)
12.18 +
12.19 translations
12.20 - "residuals(u,v,w)" == "<u,v,w>:Sres"
12.21 + "residuals(u,v,w)" == "<u,v,w> \<in> Sres"
12.22
12.23 inductive
12.24 domains "Sres" <= "redexes*redexes*redexes"
12.25 - intrs
12.26 - Res_Var "n \\<in> nat ==> residuals(Var(n),Var(n),Var(n))"
12.27 - Res_Fun "[|residuals(u,v,w)|]==>
12.28 + intros
12.29 + Res_Var: "n \<in> nat ==> residuals(Var(n),Var(n),Var(n))"
12.30 + Res_Fun: "[|residuals(u,v,w)|]==>
12.31 residuals(Fun(u),Fun(v),Fun(w))"
12.32 - Res_App "[|residuals(u1,v1,w1);
12.33 - residuals(u2,v2,w2); b \\<in> bool|]==>
12.34 + Res_App: "[|residuals(u1,v1,w1);
12.35 + residuals(u2,v2,w2); b \<in> bool|]==>
12.36 residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
12.37 - Res_redex "[|residuals(u1,v1,w1);
12.38 - residuals(u2,v2,w2); b \\<in> bool|]==>
12.39 + Res_redex: "[|residuals(u1,v1,w1);
12.40 + residuals(u2,v2,w2); b \<in> bool|]==>
12.41 residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
12.42 - type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
12.43 + type_intros subst_type nat_typechecks redexes.intros bool_typechecks
12.44
12.45 -rules
12.46 - res_func_def "u |> v == THE w. residuals(u,v,w)"
12.47 +defs
12.48 + res_func_def: "u |> v == THE w. residuals(u,v,w)"
12.49 +
12.50 +
12.51 +(* ------------------------------------------------------------------------- *)
12.52 +(* Setting up rule lists *)
12.53 +(* ------------------------------------------------------------------------- *)
12.54 +
12.55 +declare Sres.intros [intro]
12.56 +declare Sreg.intros [intro]
12.57 +declare subst_type [intro]
12.58 +
12.59 +inductive_cases [elim!]: "residuals(Var(n),Var(n),v)"
12.60 +inductive_cases [elim!]: "residuals(Fun(t),Fun(u),v)"
12.61 +inductive_cases [elim!]: "residuals(App(b, u1, u2), App(0, v1, v2),v)"
12.62 +inductive_cases [elim!]: "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)"
12.63 +inductive_cases [elim!]: "residuals(Var(n),u,v)"
12.64 +inductive_cases [elim!]: "residuals(Fun(t),u,v)"
12.65 +inductive_cases [elim!]: "residuals(App(b, u1, u2), w,v)"
12.66 +inductive_cases [elim!]: "residuals(u,Var(n),v)"
12.67 +inductive_cases [elim!]: "residuals(u,Fun(t),v)"
12.68 +inductive_cases [elim!]: "residuals(w,App(b, u1, u2),v)"
12.69 +
12.70 +
12.71 +inductive_cases [elim!]: "Var(n) <== u"
12.72 +inductive_cases [elim!]: "Fun(n) <== u"
12.73 +inductive_cases [elim!]: "u <== Fun(n)"
12.74 +inductive_cases [elim!]: "App(1,Fun(t),a) <== u"
12.75 +inductive_cases [elim!]: "App(0,t,a) <== u"
12.76 +
12.77 +inductive_cases [elim!]: "Fun(t):redexes"
12.78 +
12.79 +declare Sres.intros [simp]
12.80 +
12.81 +
12.82 +(* ------------------------------------------------------------------------- *)
12.83 +(* residuals is a partial function *)
12.84 +(* ------------------------------------------------------------------------- *)
12.85 +
12.86 +lemma residuals_function [rule_format]:
12.87 + "residuals(u,v,w) ==> \<forall>w1. residuals(u,v,w1) --> w1 = w"
12.88 +by (erule Sres.induct, force+)
12.89 +
12.90 +lemma residuals_intro [rule_format]:
12.91 + "u~v ==> regular(v) --> (\<exists>w. residuals(u,v,w))"
12.92 +by (erule Scomp.induct, force+)
12.93 +
12.94 +lemma comp_resfuncD:
12.95 + "[| u~v; regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
12.96 +apply (frule residuals_intro, assumption)
12.97 +apply clarify
12.98 +apply (subst the_equality)
12.99 +apply (blast intro: residuals_function)+
12.100 +done
12.101 +
12.102 +
12.103 +(* ------------------------------------------------------------------------- *)
12.104 +(* Residual function *)
12.105 +(* ------------------------------------------------------------------------- *)
12.106 +
12.107 +lemma res_Var [simp]: "n \<in> nat ==> Var(n) |> Var(n) = Var(n)"
12.108 +by (unfold res_func_def, blast)
12.109 +
12.110 +lemma res_Fun [simp]:
12.111 + "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"
12.112 +apply (unfold res_func_def)
12.113 +apply (blast intro: comp_resfuncD residuals_function)
12.114 +done
12.115 +
12.116 +lemma res_App [simp]:
12.117 + "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
12.118 + ==> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
12.119 +apply (unfold res_func_def)
12.120 +apply (blast dest!: comp_resfuncD intro: residuals_function)
12.121 +done
12.122 +
12.123 +lemma res_redex [simp]:
12.124 + "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
12.125 + ==> App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"
12.126 +apply (unfold res_func_def)
12.127 +apply (blast elim!: redexes.free_elims dest!: comp_resfuncD
12.128 + intro: residuals_function)
12.129 +done
12.130 +
12.131 +lemma resfunc_type [simp]:
12.132 + "[|s~t; regular(t)|]==> regular(t) --> s |> t \<in> redexes"
12.133 +apply (erule Scomp.induct)
12.134 +apply auto
12.135 +apply (drule_tac psi = "Fun (?u) |> ?v \<in> redexes" in asm_rl)
12.136 +apply auto
12.137 +done
12.138 +
12.139 +(* ------------------------------------------------------------------------- *)
12.140 +(* Commutation theorem *)
12.141 +(* ------------------------------------------------------------------------- *)
12.142 +
12.143 +lemma sub_comp [simp]: "u<==v ==> u~v"
12.144 +by (erule Ssub.induct, simp_all)
12.145 +
12.146 +lemma sub_preserve_reg [rule_format, simp]:
12.147 + "u<==v ==> regular(v) --> regular(u)"
12.148 +by (erule Ssub.induct, auto)
12.149 +
12.150 +lemma residuals_lift_rec: "[|u~v; k \<in> nat|]==> regular(v)--> (\<forall>n \<in> nat.
12.151 + lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
12.152 +apply (erule Scomp.induct)
12.153 +apply safe
12.154 +apply (simp_all add: lift_rec_Var subst_Var lift_subst)
12.155 +apply (rotate_tac -2)
12.156 +apply simp
12.157 +done
12.158 +
12.159 +lemma residuals_subst_rec:
12.160 + "u1~u2 ==> \<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->
12.161 + (\<forall>n \<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) =
12.162 + subst_rec(v1 |> v2, u1 |> u2,n))"
12.163 +apply (erule Scomp.induct)
12.164 +apply safe
12.165 +apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
12.166 +apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
12.167 +apply (simp add: substitution)
12.168 +done
12.169 +
12.170 +
12.171 +lemma commutation [simp]:
12.172 + "[|u1~u2; v1~v2; regular(u2); regular(v2)|]
12.173 + ==> (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"
12.174 +by (simp add: residuals_subst_rec)
12.175 +
12.176 +
12.177 +(* ------------------------------------------------------------------------- *)
12.178 +(* Residuals are comp and regular *)
12.179 +(* ------------------------------------------------------------------------- *)
12.180 +
12.181 +lemma residuals_preserve_comp [rule_format, simp]:
12.182 + "u~v ==> \<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"
12.183 +by (erule Scomp.induct, force+)
12.184 +
12.185 +lemma residuals_preserve_reg [rule_format, simp]:
12.186 + "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"
12.187 +apply (erule Scomp.induct)
12.188 +apply auto
12.189 +apply (drule_tac psi = "regular (Fun (?u) |> ?v)" in asm_rl, force)+
12.190 +done
12.191 +
12.192 +(* ------------------------------------------------------------------------- *)
12.193 +(* Preservation lemma *)
12.194 +(* ------------------------------------------------------------------------- *)
12.195 +
12.196 +lemma union_preserve_comp: "u~v ==> v ~ (u un v)"
12.197 +by (erule Scomp.induct, simp_all)
12.198 +
12.199 +lemma preservation [rule_format]:
12.200 + "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"
12.201 +apply (erule Scomp.induct)
12.202 +apply safe
12.203 +apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
12.204 +apply (auto simp add: union_preserve_comp comp_sym_iff)
12.205 +done
12.206 +
12.207 +
12.208 +(**** And now the Cube ***)
12.209 +
12.210 +declare sub_comp [THEN comp_sym, simp]
12.211 +
12.212 +(* ------------------------------------------------------------------------- *)
12.213 +(* Prism theorem *)
12.214 +(* ============= *)
12.215 +(* ------------------------------------------------------------------------- *)
12.216 +
12.217 +(* Having more assumptions than needed -- removed below *)
12.218 +lemma prism_l [rule_format]:
12.219 + "v<==u ==>
12.220 + regular(u) --> (\<forall>w. w~v --> w~u -->
12.221 + w |> u = (w|>v) |> (u|>v))"
12.222 +apply (erule Ssub.induct)
12.223 +apply force+
12.224 +done
12.225 +
12.226 +lemma prism:
12.227 + "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)"
12.228 +apply (rule prism_l)
12.229 +apply (rule_tac [4] comp_trans)
12.230 +apply auto
12.231 +done
12.232 +
12.233 +
12.234 +(* ------------------------------------------------------------------------- *)
12.235 +(* Levy's Cube Lemma *)
12.236 +(* ------------------------------------------------------------------------- *)
12.237 +
12.238 +lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>
12.239 + (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
12.240 +apply (subst preservation , assumption , assumption)
12.241 +apply (subst preservation , erule comp_sym , assumption)
12.242 +apply (subst prism [symmetric])
12.243 +apply (simp add: union_r comp_sym_iff)
12.244 +apply (simp add: union_preserve_regular comp_sym_iff)
12.245 +apply (erule comp_trans)
12.246 +apply assumption
12.247 +apply (simp add: prism [symmetric] union_l union_preserve_regular
12.248 + comp_sym_iff union_sym)
12.249 +done
12.250 +
12.251 +
12.252 +(* ------------------------------------------------------------------------- *)
12.253 +(* paving theorem *)
12.254 +(* ------------------------------------------------------------------------- *)
12.255 +
12.256 +lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==>
12.257 + \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &
12.258 + regular(vu) & (w|>v)~uv & regular(uv) "
12.259 +apply (subgoal_tac "u~v")
12.260 +apply (safe intro!: exI)
12.261 +apply (rule cube)
12.262 +apply (simp_all add: comp_sym_iff)
12.263 +apply (blast intro: residuals_preserve_comp comp_trans comp_sym)+
12.264 +done
12.265 +
12.266 +
12.267 end
12.268
13.1 --- a/src/ZF/Resid/Substitution.ML Fri Dec 21 23:20:29 2001 +0100
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,257 +0,0 @@
13.4 -(* Title: Substitution.ML
13.5 - ID: $Id$
13.6 - Author: Ole Rasmussen
13.7 - Copyright 1995 University of Cambridge
13.8 - Logic Image: ZF
13.9 -*)
13.10 -
13.11 -(* ------------------------------------------------------------------------- *)
13.12 -(* Arithmetic extensions *)
13.13 -(* ------------------------------------------------------------------------- *)
13.14 -
13.15 -Goal "[| p < n; n \\<in> nat|] ==> n\\<noteq>p";
13.16 -by (Fast_tac 1);
13.17 -qed "gt_not_eq";
13.18 -
13.19 -Goal "[|j \\<in> nat; i \\<in> nat|] ==> i < j --> succ(j #- 1) = j";
13.20 -by (induct_tac "j" 1);
13.21 -by (Fast_tac 1);
13.22 -by (Asm_simp_tac 1);
13.23 -qed "succ_pred";
13.24 -
13.25 -Goal "[|succ(x)<n; n \\<in> nat; x \\<in> nat|] ==> x < n #- 1 ";
13.26 -by (rtac succ_leE 1);
13.27 -by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
13.28 -by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
13.29 -qed "lt_pred";
13.30 -
13.31 -Goal "[|n < succ(x); p<n; p \\<in> nat; n \\<in> nat; x \\<in> nat|] ==> n #- 1 < x ";
13.32 -by (rtac succ_leE 1);
13.33 -by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
13.34 -qed "gt_pred";
13.35 -
13.36 -
13.37 -Addsimps [not_lt_iff_le, if_P, if_not_P];
13.38 -
13.39 -
13.40 -(* ------------------------------------------------------------------------- *)
13.41 -(* lift_rec equality rules *)
13.42 -(* ------------------------------------------------------------------------- *)
13.43 -Goal "[|n \\<in> nat; i \\<in> nat|] \
13.44 -\ ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))";
13.45 -by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
13.46 -qed "lift_rec_Var";
13.47 -
13.48 -Goal "[|n \\<in> nat; i \\<in> nat; k \\<in> nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
13.49 -by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
13.50 -qed "lift_rec_le";
13.51 -
13.52 -Goal "[|i \\<in> nat; k \\<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
13.53 -by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
13.54 -qed "lift_rec_gt";
13.55 -
13.56 -Goal "[|n \\<in> nat; k \\<in> nat|] ==> \
13.57 -\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
13.58 -by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
13.59 -qed "lift_rec_Fun";
13.60 -
13.61 -Goal "[|n \\<in> nat; k \\<in> nat|] ==> \
13.62 -\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
13.63 -by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
13.64 -qed "lift_rec_App";
13.65 -
13.66 -
13.67 -(* ------------------------------------------------------------------------- *)
13.68 -(* substitution quality rules *)
13.69 -(* ------------------------------------------------------------------------- *)
13.70 -
13.71 -Goal "[|i \\<in> nat; k \\<in> nat; u \\<in> redexes|] \
13.72 -\ ==> subst_rec(u,Var(i),k) = \
13.73 -\ (if k<i then Var(i #- 1) else if k=i then u else Var(i))";
13.74 -by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
13.75 -qed "subst_Var";
13.76 -
13.77 -Goal "[|n \\<in> nat; u \\<in> redexes|] ==> subst_rec(u,Var(n),n) = u";
13.78 -by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
13.79 -qed "subst_eq";
13.80 -
13.81 -Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; p<n|] ==> \
13.82 -\ subst_rec(u,Var(n),p) = Var(n #- 1)";
13.83 -by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
13.84 -qed "subst_gt";
13.85 -
13.86 -Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; n<p|] ==> \
13.87 -\ subst_rec(u,Var(n),p) = Var(n)";
13.88 -by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
13.89 -qed "subst_lt";
13.90 -
13.91 -Goal "[|p \\<in> nat; u \\<in> redexes|] ==> \
13.92 -\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
13.93 -by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
13.94 -qed "subst_Fun";
13.95 -
13.96 -Goal "[|p \\<in> nat; u \\<in> redexes|] ==> \
13.97 -\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
13.98 -by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
13.99 -qed "subst_App";
13.100 -
13.101 -(*But not lift_rec_Var, subst_Var: too many case splits*)
13.102 -Addsimps [subst_Fun, subst_App];
13.103 -
13.104 -
13.105 -Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. lift_rec(u,k):redexes";
13.106 -by (etac redexes.induct 1);
13.107 -by (ALLGOALS
13.108 - (asm_simp_tac (simpset() addsimps [lift_rec_Var,
13.109 - lift_rec_Fun, lift_rec_App])));
13.110 -qed_spec_mp "lift_rec_type";
13.111 -
13.112 -Goal "v \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. subst_rec(u,v,n):redexes";
13.113 -by (etac redexes.induct 1);
13.114 -by (ALLGOALS(asm_simp_tac
13.115 - (simpset() addsimps [subst_Var, lift_rec_type])));
13.116 -qed_spec_mp "subst_type";
13.117 -
13.118 -
13.119 -Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
13.120 - lift_rec_le, lift_rec_gt, lift_rec_Fun, lift_rec_App,
13.121 - lift_rec_type];
13.122 -
13.123 -
13.124 -(* ------------------------------------------------------------------------- *)
13.125 -(* lift and substitution proofs *)
13.126 -(* ------------------------------------------------------------------------- *)
13.127 -
13.128 -Goal "u \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>i \\<in> nat. i le n --> \
13.129 -\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
13.130 -by (etac redexes.induct 1);
13.131 -by (ALLGOALS Asm_simp_tac);
13.132 -by Safe_tac;
13.133 -by (case_tac "n < i" 1);
13.134 -by ((ftac lt_trans2 1) THEN (assume_tac 1));
13.135 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
13.136 -qed "lift_lift_rec";
13.137 -
13.138 -Goal "[|u \\<in> redexes; n \\<in> nat|] ==> \
13.139 -\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
13.140 -by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
13.141 -qed "lift_lift";
13.142 -
13.143 -Goal "v \\<in> redexes ==> \
13.144 -\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. n le m-->\
13.145 -\ lift_rec(subst_rec(u,v,n),m) = \
13.146 -\ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
13.147 -by ((etac redexes.induct 1)
13.148 - THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
13.149 -by Safe_tac;
13.150 -by (excluded_middle_tac "n < x" 1);
13.151 -by (Asm_full_simp_tac 1);
13.152 -by (eres_inst_tac [("j","n")] leE 1);
13.153 -by (asm_simp_tac (simpset() setloop (split_inside_tac [split_if])
13.154 - addsimps [lift_rec_Var,subst_Var,
13.155 - leI,gt_pred,succ_pred]) 1);
13.156 -by (hyp_subst_tac 1);
13.157 -by (Asm_simp_tac 1);
13.158 -by (forw_inst_tac [("j","x")] lt_trans2 1);
13.159 -by (assume_tac 1);
13.160 -by (asm_simp_tac (simpset() addsimps [leI]) 1);
13.161 -qed "lift_rec_subst_rec";
13.162 -
13.163 -Goal "[|v \\<in> redexes; u \\<in> redexes; n \\<in> nat|] ==> \
13.164 -\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
13.165 -by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
13.166 -qed "lift_subst";
13.167 -
13.168 -
13.169 -Goal "v \\<in> redexes ==> \
13.170 -\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. m le n-->\
13.171 -\ lift_rec(subst_rec(u,v,n),m) = \
13.172 -\ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
13.173 -by (etac redexes.induct 1
13.174 - THEN ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])));
13.175 -by Safe_tac;
13.176 -by (excluded_middle_tac "n < x" 1);
13.177 -by (Asm_full_simp_tac 1);
13.178 -by (eres_inst_tac [("i","x")] leE 1);
13.179 -by (ftac lt_trans1 1 THEN assume_tac 1);
13.180 -by (ALLGOALS(asm_simp_tac
13.181 - (simpset() addsimps [succ_pred,leI,gt_pred])));
13.182 -by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
13.183 -by (case_tac "n < xa" 1);
13.184 -by (Asm_full_simp_tac 2);
13.185 -by (asm_simp_tac (simpset() addsimps [leI]) 1);
13.186 -qed "lift_rec_subst_rec_lt";
13.187 -
13.188 -
13.189 -Goal "u \\<in> redexes ==> \
13.190 -\ \\<forall>n \\<in> nat. \\<forall>v \\<in> redexes. subst_rec(v,lift_rec(u,n),n) = u";
13.191 -by (etac redexes.induct 1);
13.192 -by Auto_tac;
13.193 -by (case_tac "n < na" 1);
13.194 -by Auto_tac;
13.195 -qed "subst_rec_lift_rec";
13.196 -
13.197 -Goal "v \\<in> redexes ==> \
13.198 -\ \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. \\<forall>w \\<in> redexes. m le n --> \
13.199 -\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
13.200 -\ subst_rec(w,subst_rec(u,v,m),n)";
13.201 -by (etac redexes.induct 1);
13.202 -by (ALLGOALS(asm_simp_tac (simpset() addsimps
13.203 - [lift_lift RS sym,lift_rec_subst_rec_lt])));
13.204 -by Safe_tac;
13.205 -by (excluded_middle_tac "n le succ(xa)" 1);
13.206 -by (Asm_full_simp_tac 1);
13.207 -by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
13.208 -by (etac leE 1);
13.209 -by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2);
13.210 -by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1);
13.211 -by (forw_inst_tac [("i","x")]
13.212 - (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1);
13.213 -by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1);
13.214 -by (eres_inst_tac [("i","n")] leE 1);
13.215 -by (asm_simp_tac (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
13.216 -by (excluded_middle_tac "n < x" 1);
13.217 -by (Asm_full_simp_tac 1);
13.218 -by (eres_inst_tac [("j","n")] leE 1);
13.219 -by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
13.220 -by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
13.221 -by (ftac lt_trans2 1 THEN assume_tac 1);
13.222 -by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
13.223 -qed "subst_rec_subst_rec";
13.224 -
13.225 -
13.226 -Goal "[|v \\<in> redexes; u \\<in> redexes; w \\<in> redexes; n \\<in> nat|] ==> \
13.227 -\ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
13.228 -by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1);
13.229 -qed "substitution";
13.230 -
13.231 -(* ------------------------------------------------------------------------- *)
13.232 -(* Preservation lemmas *)
13.233 -(* Substitution preserves comp and regular *)
13.234 -(* ------------------------------------------------------------------------- *)
13.235 -
13.236 -
13.237 -Goal "[|n \\<in> nat; u ~ v|] ==> \\<forall>m \\<in> nat. lift_rec(u,m) ~ lift_rec(v,m)";
13.238 -by (etac Scomp.induct 1);
13.239 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl])));
13.240 -qed "lift_rec_preserve_comp";
13.241 -
13.242 -Goal "u2 ~ v2 ==> \\<forall>m \\<in> nat. \\<forall>u1 \\<in> redexes. \\<forall>v1 \\<in> redexes.\
13.243 -\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
13.244 -by (etac Scomp.induct 1);
13.245 -by (ALLGOALS
13.246 - (asm_simp_tac
13.247 - (simpset() addsimps [subst_Var, lift_rec_preserve_comp, comp_refl])));
13.248 -qed "subst_rec_preserve_comp";
13.249 -
13.250 -Goal "regular(u) ==> \\<forall>m \\<in> nat. regular(lift_rec(u,m))";
13.251 -by (etac Sreg.induct 1);
13.252 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var])));
13.253 -qed "lift_rec_preserve_reg";
13.254 -
13.255 -Goal "regular(v) ==> \
13.256 -\ \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. regular(u)-->regular(subst_rec(u,v,m))";
13.257 -by (etac Sreg.induct 1);
13.258 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
13.259 - lift_rec_preserve_reg])));
13.260 -qed "subst_rec_preserve_reg";
14.1 --- a/src/ZF/Resid/Substitution.thy Fri Dec 21 23:20:29 2001 +0100
14.2 +++ b/src/ZF/Resid/Substitution.thy Sat Dec 22 19:42:35 2001 +0100
14.3 @@ -5,19 +5,19 @@
14.4 Logic Image: ZF
14.5 *)
14.6
14.7 -Substitution = Redex +
14.8 +theory Substitution = Redex:
14.9
14.10 consts
14.11 - lift_aux :: i=> i
14.12 - lift :: i=> i
14.13 - subst_aux :: i=> i
14.14 - "'/" :: [i,i]=>i (infixl 70) (*subst*)
14.15 + lift_aux :: "i=>i"
14.16 + lift :: "i=>i"
14.17 + subst_aux :: "i=>i"
14.18 + "'/" :: "[i,i]=>i" (infixl 70) (*subst*)
14.19
14.20 constdefs
14.21 - lift_rec :: [i,i]=> i
14.22 + lift_rec :: "[i,i]=> i"
14.23 "lift_rec(r,k) == lift_aux(r)`k"
14.24
14.25 - subst_rec :: [i,i,i]=> i (**NOTE THE ARGUMENT ORDER BELOW**)
14.26 + subst_rec :: "[i,i,i]=> i" (**NOTE THE ARGUMENT ORDER BELOW**)
14.27 "subst_rec(u,r,k) == subst_aux(r)`u`k"
14.28
14.29 translations
14.30 @@ -29,23 +29,246 @@
14.31 in the recursive calls ***)
14.32
14.33 primrec
14.34 - "lift_aux(Var(i)) = (\\<lambda>k \\<in> nat. if i<k then Var(i) else Var(succ(i)))"
14.35 + "lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))"
14.36
14.37 - "lift_aux(Fun(t)) = (\\<lambda>k \\<in> nat. Fun(lift_aux(t) ` succ(k)))"
14.38 + "lift_aux(Fun(t)) = (\<lambda>k \<in> nat. Fun(lift_aux(t) ` succ(k)))"
14.39
14.40 - "lift_aux(App(b,f,a)) = (\\<lambda>k \\<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
14.41 + "lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
14.42
14.43
14.44
14.45 primrec
14.46 "subst_aux(Var(i)) =
14.47 - (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. if k<i then Var(i #- 1)
14.48 + (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1)
14.49 else if k=i then r else Var(i))"
14.50 "subst_aux(Fun(t)) =
14.51 - (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
14.52 + (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
14.53
14.54 "subst_aux(App(b,f,a)) =
14.55 - (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
14.56 + (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
14.57 +
14.58 +
14.59 +(* ------------------------------------------------------------------------- *)
14.60 +(* Arithmetic extensions *)
14.61 +(* ------------------------------------------------------------------------- *)
14.62 +
14.63 +lemma gt_not_eq: "p < n ==> n\<noteq>p"
14.64 +by blast
14.65 +
14.66 +lemma succ_pred [rule_format, simp]: "j \<in> nat ==> i < j --> succ(j #- 1) = j"
14.67 +by (induct_tac "j", auto)
14.68 +
14.69 +lemma lt_pred: "[|succ(x)<n; n \<in> nat|] ==> x < n #- 1 "
14.70 +apply (rule succ_leE)
14.71 +apply (simp add: succ_pred)
14.72 +done
14.73 +
14.74 +lemma gt_pred: "[|n < succ(x); p<n; n \<in> nat|] ==> n #- 1 < x "
14.75 +apply (rule succ_leE)
14.76 +apply (simp add: succ_pred)
14.77 +done
14.78 +
14.79 +
14.80 +declare not_lt_iff_le [simp] if_P [simp] if_not_P [simp]
14.81 +
14.82 +
14.83 +(* ------------------------------------------------------------------------- *)
14.84 +(* lift_rec equality rules *)
14.85 +(* ------------------------------------------------------------------------- *)
14.86 +lemma lift_rec_Var:
14.87 + "n \<in> nat ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))"
14.88 +by (simp add: lift_rec_def)
14.89 +
14.90 +lemma lift_rec_le [simp]:
14.91 + "[|i \<in> nat; k\<le>i|] ==> lift_rec(Var(i),k) = Var(succ(i))"
14.92 +by (simp add: lift_rec_def le_in_nat)
14.93 +
14.94 +lemma lift_rec_gt [simp]: "[| k \<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)"
14.95 +by (simp add: lift_rec_def)
14.96 +
14.97 +lemma lift_rec_Fun [simp]:
14.98 + "k \<in> nat ==> lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"
14.99 +by (simp add: lift_rec_def)
14.100 +
14.101 +lemma lift_rec_App [simp]:
14.102 + "k \<in> nat ==> lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"
14.103 +by (simp add: lift_rec_def)
14.104 +
14.105 +
14.106 +(* ------------------------------------------------------------------------- *)
14.107 +(* substitution quality rules *)
14.108 +(* ------------------------------------------------------------------------- *)
14.109 +
14.110 +lemma subst_Var:
14.111 + "[|k \<in> nat; u \<in> redexes|]
14.112 + ==> subst_rec(u,Var(i),k) =
14.113 + (if k<i then Var(i #- 1) else if k=i then u else Var(i))"
14.114 +by (simp add: subst_rec_def gt_not_eq leI)
14.115 +
14.116 +
14.117 +lemma subst_eq [simp]:
14.118 + "[|n \<in> nat; u \<in> redexes|] ==> subst_rec(u,Var(n),n) = u"
14.119 +by (simp add: subst_rec_def)
14.120 +
14.121 +lemma subst_gt [simp]:
14.122 + "[|u \<in> redexes; p \<in> nat; p<n|] ==> subst_rec(u,Var(n),p) = Var(n #- 1)"
14.123 +by (simp add: subst_rec_def)
14.124 +
14.125 +lemma subst_lt [simp]:
14.126 + "[|u \<in> redexes; p \<in> nat; n<p|] ==> subst_rec(u,Var(n),p) = Var(n)"
14.127 +by (simp add: subst_rec_def gt_not_eq leI lt_nat_in_nat)
14.128 +
14.129 +lemma subst_Fun [simp]:
14.130 + "[|p \<in> nat; u \<in> redexes|]
14.131 + ==> subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "
14.132 +by (simp add: subst_rec_def)
14.133 +
14.134 +lemma subst_App [simp]:
14.135 + "[|p \<in> nat; u \<in> redexes|]
14.136 + ==> subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"
14.137 +by (simp add: subst_rec_def)
14.138 +
14.139 +
14.140 +lemma lift_rec_type [rule_format, simp]:
14.141 + "u \<in> redexes ==> \<forall>k \<in> nat. lift_rec(u,k) \<in> redexes"
14.142 +apply (erule redexes.induct)
14.143 +apply (simp_all add: lift_rec_Var lift_rec_Fun lift_rec_App)
14.144 +done
14.145 +
14.146 +lemma subst_type [rule_format, simp]:
14.147 + "v \<in> redexes ==> \<forall>n \<in> nat. \<forall>u \<in> redexes. subst_rec(u,v,n) \<in> redexes"
14.148 +apply (erule redexes.induct)
14.149 +apply (simp_all add: subst_Var lift_rec_type)
14.150 +done
14.151 +
14.152 +
14.153 +(* ------------------------------------------------------------------------- *)
14.154 +(* lift and substitution proofs *)
14.155 +(* ------------------------------------------------------------------------- *)
14.156 +
14.157 +(*The i\<in>nat is redundant*)
14.158 +lemma lift_lift_rec [rule_format]:
14.159 + "u \<in> redexes
14.160 + ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->
14.161 + (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
14.162 +apply (erule redexes.induct)
14.163 +apply auto
14.164 +apply (case_tac "n < i")
14.165 +apply (frule lt_trans2, assumption)
14.166 +apply (simp_all add: lift_rec_Var leI)
14.167 +done
14.168 +
14.169 +lemma lift_lift:
14.170 + "[|u \<in> redexes; n \<in> nat|]
14.171 + ==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
14.172 +by (simp add: lift_lift_rec)
14.173 +
14.174 +lemma lt_not_m1_lt: "\<lbrakk>m < n; n \<in> nat; m \<in> nat\<rbrakk>\<Longrightarrow> ~ n #- 1 < m"
14.175 +by (erule natE, auto)
14.176 +
14.177 +lemma lift_rec_subst_rec [rule_format]:
14.178 + "v \<in> redexes ==>
14.179 + \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m-->
14.180 + lift_rec(subst_rec(u,v,n),m) =
14.181 + subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
14.182 +apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
14.183 +apply safe
14.184 +apply (case_tac "n < x")
14.185 + apply (frule_tac j = "x" in lt_trans2, assumption)
14.186 + apply (simp add: leI)
14.187 +apply simp
14.188 +apply (erule_tac j = "n" in leE)
14.189 +apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt)
14.190 +done
14.191 +
14.192 +
14.193 +lemma lift_subst:
14.194 + "[|v \<in> redexes; u \<in> redexes; n \<in> nat|]
14.195 + ==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
14.196 +by (simp add: lift_rec_subst_rec)
14.197 +
14.198 +
14.199 +lemma lift_rec_subst_rec_lt [rule_format]:
14.200 + "v \<in> redexes ==>
14.201 + \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n-->
14.202 + lift_rec(subst_rec(u,v,n),m) =
14.203 + subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
14.204 +apply (erule redexes.induct , simp_all (no_asm_simp) add: lift_lift)
14.205 +apply safe
14.206 +apply (case_tac "n < x")
14.207 +apply (case_tac "n < xa")
14.208 +apply (simp_all add: leI)
14.209 +apply (erule_tac i = "x" in leE)
14.210 +apply (frule lt_trans1, assumption)
14.211 +apply (simp_all add: succ_pred leI gt_pred)
14.212 +done
14.213 +
14.214 +
14.215 +lemma subst_rec_lift_rec [rule_format]:
14.216 + "u \<in> redexes ==>
14.217 + \<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
14.218 +apply (erule redexes.induct)
14.219 +apply auto
14.220 +apply (case_tac "n < na")
14.221 +apply auto
14.222 +done
14.223 +
14.224 +lemma subst_rec_subst_rec [rule_format]:
14.225 + "v \<in> redexes ==>
14.226 + \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->
14.227 + subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) =
14.228 + subst_rec(w,subst_rec(u,v,m),n)"
14.229 +apply (erule redexes.induct)
14.230 +apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt)
14.231 +apply safe
14.232 +apply (case_tac "n\<le>succ (xa) ")
14.233 + apply (erule_tac i = "n" in leE)
14.234 + apply (simp_all add: succ_pred subst_rec_lift_rec leI)
14.235 + apply (case_tac "n < x")
14.236 + apply (frule lt_trans2 , assumption, simp add: gt_pred)
14.237 + apply simp
14.238 + apply (erule_tac j = "n" in leE, simp add: gt_pred)
14.239 + apply (simp add: subst_rec_lift_rec)
14.240 +(*final case*)
14.241 +apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans] , assumption)
14.242 +apply (erule leE)
14.243 + apply (frule succ_leI [THEN lt_trans] , assumption)
14.244 + apply (frule_tac i = "x" in nat_into_Ord [THEN le_refl, THEN lt_trans],
14.245 + assumption)
14.246 + apply (simp_all add: succ_pred lt_pred)
14.247 +done
14.248 +
14.249 +
14.250 +lemma substitution:
14.251 + "[|v \<in> redexes; u \<in> redexes; w \<in> redexes; n \<in> nat|]
14.252 + ==> subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"
14.253 +by (simp add: subst_rec_subst_rec)
14.254 +
14.255 +
14.256 +(* ------------------------------------------------------------------------- *)
14.257 +(* Preservation lemmas *)
14.258 +(* Substitution preserves comp and regular *)
14.259 +(* ------------------------------------------------------------------------- *)
14.260 +
14.261 +
14.262 +lemma lift_rec_preserve_comp [rule_format, simp]:
14.263 + "u ~ v ==> \<forall>m \<in> nat. lift_rec(u,m) ~ lift_rec(v,m)"
14.264 +by (erule Scomp.induct, simp_all add: comp_refl)
14.265 +
14.266 +lemma subst_rec_preserve_comp [rule_format, simp]:
14.267 + "u2 ~ v2 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> redexes.
14.268 + u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)"
14.269 +by (erule Scomp.induct,
14.270 + simp_all add: subst_Var lift_rec_preserve_comp comp_refl)
14.271 +
14.272 +lemma lift_rec_preserve_reg [simp]:
14.273 + "regular(u) ==> \<forall>m \<in> nat. regular(lift_rec(u,m))"
14.274 +by (erule Sreg.induct, simp_all add: lift_rec_Var)
14.275 +
14.276 +lemma subst_rec_preserve_reg [simp]:
14.277 + "regular(v) ==>
14.278 + \<forall>m \<in> nat. \<forall>u \<in> redexes. regular(u)-->regular(subst_rec(u,v,m))"
14.279 +by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
14.280
14.281 end
14.282
15.1 --- a/src/ZF/Resid/Terms.ML Fri Dec 21 23:20:29 2001 +0100
15.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
15.3 @@ -1,45 +0,0 @@
15.4 -(* Title: Terms.ML
15.5 - ID: $Id$
15.6 - Author: Ole Rasmussen
15.7 - Copyright 1995 University of Cambridge
15.8 - Logic Image: ZF
15.9 -*)
15.10 -
15.11 -Addsimps ([lambda.dom_subset RS subsetD] @ lambda.intrs);
15.12 -
15.13 -
15.14 -(* ------------------------------------------------------------------------- *)
15.15 -(* unmark lemmas *)
15.16 -(* ------------------------------------------------------------------------- *)
15.17 -
15.18 -Goal "u \\<in> redexes ==> unmark(u):lambda";
15.19 -by (etac redexes.induct 1);
15.20 -by (ALLGOALS Asm_simp_tac);
15.21 -qed "unmark_type";
15.22 -
15.23 -Goal "u \\<in> lambda ==> unmark(u) = u";
15.24 -by (etac lambda.induct 1);
15.25 -by (ALLGOALS Asm_simp_tac);
15.26 -qed "lambda_unmark";
15.27 -
15.28 -
15.29 -(* ------------------------------------------------------------------------- *)
15.30 -(* lift and subst preserve lambda *)
15.31 -(* ------------------------------------------------------------------------- *)
15.32 -
15.33 -Goal "v \\<in> lambda ==> \\<forall>k \\<in> nat. lift_rec(v,k):lambda";
15.34 -by (etac lambda.induct 1);
15.35 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
15.36 -qed_spec_mp "liftL_type";
15.37 -
15.38 -Goal "v \\<in> lambda ==> \\<forall>n \\<in> nat. \\<forall>u \\<in> lambda. subst_rec(u,v,n):lambda";
15.39 -by (etac lambda.induct 1);
15.40 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
15.41 -qed_spec_mp "substL_type";
15.42 -
15.43 -
15.44 -(* ------------------------------------------------------------------------- *)
15.45 -(* type-rule for reduction definitions *)
15.46 -(* ------------------------------------------------------------------------- *)
15.47 -
15.48 -val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks;