--- a/src/ZF/IsaMakefile Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/IsaMakefile Sat Dec 22 19:42:35 2001 +0100
@@ -95,12 +95,9 @@
ZF-Resid: ZF $(LOG)/ZF-Resid.gz
-$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/Confluence.ML Resid/Confluence.thy \
- Resid/Conversion.ML Resid/Conversion.thy Resid/Cube.ML Resid/Cube.thy \
- Resid/ROOT.ML Resid/Redex.ML Resid/Redex.thy Resid/Reduction.ML \
- Resid/Reduction.thy Resid/Residuals.ML Resid/Residuals.thy \
- Resid/Substitution.ML \
- Resid/Substitution.thy Resid/Terms.ML Resid/Terms.thy
+$(LOG)/ZF-Resid.gz: $(OUT)/ZF Resid/ROOT.ML Resid/Confluence.thy \
+ Resid/Redex.thy Resid/Reduction.thy Resid/Residuals.thy \
+ Resid/Substitution.thy
@$(ISATOOL) usedir $(OUT)/ZF Resid
--- a/src/ZF/Resid/Confluence.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,59 +0,0 @@
-(* Title: Confluence.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-open Confluence;
-
-(* ------------------------------------------------------------------------- *)
-(* strip lemmas *)
-(* ------------------------------------------------------------------------- *)
-
-Goalw [confluence_def,strip_def]
- "[|confluence(Spar_red1)|]==> strip";
-by (resolve_tac [impI RS allI RS allI] 1);
-by (etac Spar_red.induct 1);
-by (Fast_tac 1);
-by (fast_tac (claset() addIs [Spar_red.trans]) 1);
-qed "strip_lemma_r";
-
-
-Goalw [confluence_def,strip_def]
- "strip==> confluence(Spar_red)";
-by (resolve_tac [impI RS allI RS allI] 1);
-by (etac Spar_red.induct 1);
-by (Blast_tac 1);
-by (Clarify_tac 1);
-by (dres_inst_tac [("x1","z")] (spec RS mp) 1);
-by (blast_tac (claset() addIs [Spar_red.trans]) 2);
-by (assume_tac 1);
-qed "strip_lemma_l";
-
-(* ------------------------------------------------------------------------- *)
-(* Confluence *)
-(* ------------------------------------------------------------------------- *)
-
-
-Goalw [confluence_def] "confluence(Spar_red1)";
-by (Clarify_tac 1);
-by (ftac simulation 1);
-by (forw_inst_tac [("n","z")] simulation 1);
-by (Clarify_tac 1);
-by (forw_inst_tac [("v","va")] paving 1);
-by (TRYALL assume_tac);
-by (fast_tac (claset() addIs [completeness] addss (simpset())) 1);
-qed "parallel_moves";
-
-bind_thm ("confluence_parallel_reduction",
- parallel_moves RS strip_lemma_r RS strip_lemma_l);
-
-Goalw [confluence_def]
- "[|confluence(Spar_red)|]==> confluence(Sred)";
-by (blast_tac (claset() addIs [par_red_red, red_par_red]) 1);
-val lemma1 = result();
-
-bind_thm ("confluence_beta_reduction",
- confluence_parallel_reduction RS lemma1);
-
--- a/src/ZF/Resid/Confluence.thy Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Confluence.thy Sat Dec 22 19:42:35 2001 +0100
@@ -5,17 +5,119 @@
Logic Image: ZF
*)
-Confluence = Reduction+
+theory Confluence = Reduction:
+
+constdefs
+ confluence :: "i=>o"
+ "confluence(R) ==
+ \<forall>x y. <x,y> \<in> R --> (\<forall>z.<x,z> \<in> R --> (\<exists>u.<y,u> \<in> R & <z,u> \<in> R))"
+
+ strip :: "o"
+ "strip == \<forall>x y. (x ===> y) -->
+ (\<forall>z.(x =1=> z) --> (\<exists>u.(y =1=> u) & (z===>u)))"
+
+
+(* ------------------------------------------------------------------------- *)
+(* strip lemmas *)
+(* ------------------------------------------------------------------------- *)
+
+lemma strip_lemma_r:
+ "[|confluence(Spar_red1)|]==> strip"
+apply (unfold confluence_def strip_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule Spar_red.induct)
+apply fast
+apply (fast intro: Spar_red.trans)
+done
+
+
+lemma strip_lemma_l:
+ "strip==> confluence(Spar_red)"
+apply (unfold confluence_def strip_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule Spar_red.induct)
+apply blast
+apply clarify
+apply (blast intro: Spar_red.trans)
+done
+
+(* ------------------------------------------------------------------------- *)
+(* Confluence *)
+(* ------------------------------------------------------------------------- *)
+
+
+lemma parallel_moves: "confluence(Spar_red1)"
+apply (unfold confluence_def)
+apply clarify
+apply (frule simulation)
+apply (frule_tac n = "z" in simulation)
+apply clarify
+apply (frule_tac v = "va" in paving)
+apply (force intro: completeness)+
+done
+
+lemmas confluence_parallel_reduction =
+ parallel_moves [THEN strip_lemma_r, THEN strip_lemma_l, standard]
+
+lemma lemma1: "[|confluence(Spar_red)|]==> confluence(Sred)"
+apply (unfold confluence_def, blast intro: par_red_red red_par_red)
+done
+
+lemmas confluence_beta_reduction =
+ confluence_parallel_reduction [THEN lemma1, standard]
+
+
+(**** Conversion ****)
consts
- confluence :: i=>o
- strip :: o
+ Sconv1 :: "i"
+ "<-1->" :: "[i,i]=>o" (infixl 50)
+ Sconv :: "i"
+ "<--->" :: "[i,i]=>o" (infixl 50)
+
+translations
+ "a<-1->b" == "<a,b> \<in> Sconv1"
+ "a<--->b" == "<a,b> \<in> Sconv"
+
+inductive
+ domains "Sconv1" <= "lambda*lambda"
+ intros
+ red1: "m -1-> n ==> m<-1->n"
+ expl: "n -1-> m ==> m<-1->n"
+ type_intros red1D1 red1D2 lambda.intros bool_typechecks
+
+declare Sconv1.intros [intro]
-defs
- confluence_def "confluence(R) ==
- \\<forall>x y. <x,y>:R --> (\\<forall>z.<x,z>:R -->
- (\\<exists>u.<y,u>:R & <z,u>:R))"
- strip_def "strip == \\<forall>x y. (x ===> y) --> (\\<forall>z.(x =1=> z) -->
- (\\<exists>u.(y =1=> u) & (z===>u)))"
+inductive
+ domains "Sconv" <= "lambda*lambda"
+ intros
+ one_step: "m<-1->n ==> m<--->n"
+ refl: "m \<in> lambda ==> m<--->m"
+ trans: "[|m<--->n; n<--->p|] ==> m<--->p"
+ type_intros Sconv1.dom_subset [THEN subsetD] lambda.intros bool_typechecks
+
+declare Sconv.intros [intro]
+
+lemma conv_sym: "m<--->n ==> n<--->m"
+apply (erule Sconv.induct)
+apply (erule Sconv1.induct)
+apply blast+
+done
+
+(* ------------------------------------------------------------------------- *)
+(* Church_Rosser Theorem *)
+(* ------------------------------------------------------------------------- *)
+
+lemma Church_Rosser: "m<--->n ==> \<exists>p.(m --->p) & (n ---> p)"
+apply (erule Sconv.induct)
+apply (erule Sconv1.induct)
+apply (blast intro: red1D1 redD2)
+apply (blast intro: red1D1 redD2)
+apply (blast intro: red1D1 redD2)
+apply (cut_tac confluence_beta_reduction)
+apply (unfold confluence_def)
+apply (blast intro: Sred.trans)
+done
+
end
--- a/src/ZF/Resid/Conversion.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: Conversion.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-open Conversion;
-
-AddIs (Sconv.intrs @ Sconv1.intrs);
-
-Goal "m<--->n ==> n<--->m";
-by (etac Sconv.induct 1);
-by (etac Sconv1.induct 1);
-by (ALLGOALS Blast_tac);
-qed "conv_sym";
-
-(* ------------------------------------------------------------------------- *)
-(* Church_Rosser Theorem *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "m<--->n ==> \\<exists>p.(m --->p) & (n ---> p)";
-by (etac Sconv.induct 1);
-by (etac Sconv1.induct 1);
-by (blast_tac (claset() addIs [red1D1,redD2]) 1);
-by (blast_tac (claset() addIs [red1D1,redD2]) 1);
-by (blast_tac (claset() addIs [red1D1,redD2]) 1);
-by (cut_facts_tac [confluence_beta_reduction] 1);
-by (rewtac confluence_def);
-by (blast_tac (claset() addIs [Sred.trans]) 1);
-qed "Church_Rosser";
-
--- a/src/ZF/Resid/Cube.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(* Title: Cube.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-Addsimps [commutation, residuals_preserve_comp, sub_preserve_reg,
- residuals_preserve_reg, sub_comp, sub_comp RS comp_sym];
-
-(* ------------------------------------------------------------------------- *)
-(* Prism theorem *)
-(* ============= *)
-(* ------------------------------------------------------------------------- *)
-
-(* Having more assumptions than needed -- removed below *)
-Goal "v<==u ==> \
-\ regular(u) --> (\\<forall>w. w~v --> w~u --> \
-\ w |> u = (w|>v) |> (u|>v))";
-by (etac Ssub.induct 1);
-by Auto_tac;
-qed_spec_mp "prism_l";
-
-Goal "[|v <== u; regular(u); w~v|]==> \
-\ w |> u = (w|>v) |> (u|>v)";
-by (rtac prism_l 1);
-by (rtac comp_trans 4);
-by Auto_tac;
-qed "prism";
-
-
-(* ------------------------------------------------------------------------- *)
-(* Levy's Cube Lemma *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[|u~v; regular(v); regular(u); w~u|]==> \
-\ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)";
-by (stac preservation 1
- THEN assume_tac 1 THEN assume_tac 1);
-by (stac preservation 1
- THEN etac comp_sym 1 THEN assume_tac 1);
-by (stac (prism RS sym) 1);
-by (asm_full_simp_tac (simpset() addsimps
- [prism RS sym,union_l,union_preserve_regular,
- comp_sym_iff, union_sym]) 4);
-by (asm_simp_tac (simpset() addsimps [union_r, comp_sym_iff]) 1);
-by (asm_simp_tac (simpset() addsimps
- [union_preserve_regular, comp_sym_iff]) 1);
-by (etac comp_trans 1);
-by (atac 1);
-qed "cube";
-
-
-(* ------------------------------------------------------------------------- *)
-(* paving theorem *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[|w~u; w~v; regular(u); regular(v)|]==> \
-\ \\<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &\
-\ regular(vu) & (w|>v)~uv & regular(uv) ";
-by (subgoal_tac "u~v" 1);
-by (safe_tac (claset() addSIs [exI]));
-by (rtac cube 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [comp_sym_iff])));
-by (ALLGOALS (blast_tac (claset() addIs [residuals_preserve_comp,
- comp_trans, comp_sym])));
-qed "paving";
-
--- a/src/ZF/Resid/ROOT.ML Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/ROOT.ML Sat Dec 22 19:42:35 2001 +0100
@@ -12,4 +12,4 @@
J. Functional Programming 4(3) 1994, 371-394.
*)
-time_use_thy "Conversion";
+time_use_thy "Confluence";
--- a/src/ZF/Resid/Redex.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,111 +0,0 @@
-(* Title: Redex.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-Addsimps redexes.intrs;
-
-fun rotate n i = EVERY(replicate n (etac revcut_rl i));
-(* ------------------------------------------------------------------------- *)
-(* Specialisation of comp-rules *)
-(* ------------------------------------------------------------------------- *)
-
-val compD1 = Scomp.dom_subset RS subsetD RS SigmaD1;
-val compD2 = Scomp.dom_subset RS subsetD RS SigmaD2;
-
-val regD = Sreg.dom_subset RS subsetD;
-
-(* ------------------------------------------------------------------------- *)
-(* Equality rules for union *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "n \\<in> nat==>Var(n) un Var(n)=Var(n)";
-by (asm_simp_tac (simpset() addsimps [union_def]) 1);
-qed "union_Var";
-
-Goal "[|u \\<in> redexes; v \\<in> redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
-by (asm_simp_tac (simpset() addsimps [union_def]) 1);
-qed "union_Fun";
-
-Goal "[|b1 \\<in> bool; b2 \\<in> bool; u1 \\<in> redexes; v1 \\<in> redexes; u2 \\<in> redexes; v2 \\<in> redexes|]==> \
-\ App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
-by (asm_simp_tac (simpset() addsimps [union_def]) 1);
-qed "union_App";
-
-Addsimps (Ssub.intrs@bool_typechecks@
- Sreg.intrs@Scomp.intrs@
- [or_1 RSN (3,or_commute RS trans),
- or_0 RSN (3,or_commute RS trans),
- union_App,union_Fun,union_Var,compD2,compD1,regD]);
-
-AddIs Scomp.intrs;
-AddSEs [Sreg.mk_cases "regular(App(b,f,a))",
- Sreg.mk_cases "regular(Fun(b))",
- Sreg.mk_cases "regular(Var(b))",
- Scomp.mk_cases "Fun(u) ~ Fun(t)",
- Scomp.mk_cases "u ~ Fun(t)",
- Scomp.mk_cases "u ~ Var(n)",
- Scomp.mk_cases "u ~ App(b,t,a)",
- Scomp.mk_cases "Fun(t) ~ v",
- Scomp.mk_cases "App(b,f,a) ~ v",
- Scomp.mk_cases "Var(n) ~ u"];
-
-
-
-(* ------------------------------------------------------------------------- *)
-(* comp proofs *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> u ~ u";
-by (etac redexes.induct 1);
-by (ALLGOALS Fast_tac);
-qed "comp_refl";
-
-Goal "u ~ v ==> v ~ u";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed "comp_sym";
-
-Goal "u ~ v <-> v ~ u";
-by (fast_tac (claset() addIs [comp_sym]) 1);
-qed "comp_sym_iff";
-
-
-Goal "u ~ v ==> \\<forall>w. v ~ w-->u ~ w";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed_spec_mp "comp_trans";
-
-(* ------------------------------------------------------------------------- *)
-(* union proofs *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u ~ v ==> u <== (u un v)";
-by (etac Scomp.induct 1);
-by (etac boolE 3);
-by (ALLGOALS Asm_simp_tac);
-qed "union_l";
-
-Goal "u ~ v ==> v <== (u un v)";
-by (etac Scomp.induct 1);
-by (eres_inst_tac [("c","b2")] boolE 3);
-by (ALLGOALS Asm_simp_tac);
-qed "union_r";
-
-Goal "u ~ v ==> u un v = v un u";
-by (etac Scomp.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [or_commute])));
-qed "union_sym";
-
-(* ------------------------------------------------------------------------- *)
-(* regular proofs *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
-by (etac Scomp.induct 1);
-by Auto_tac;
-by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
-by (Asm_full_simp_tac 1);
-qed_spec_mp "union_preserve_regular";
--- a/src/ZF/Resid/Redex.thy Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Redex.thy Sat Dec 22 19:42:35 2001 +0100
@@ -5,77 +5,186 @@
Logic Image: ZF
*)
-Redex = Main +
+theory Redex = Main:
consts
redexes :: i
datatype
- "redexes" = Var ("n \\<in> nat")
- | Fun ("t \\<in> redexes")
- | App ("b \\<in> bool" ,"f \\<in> redexes" , "a \\<in> redexes")
+ "redexes" = Var ("n \<in> nat")
+ | Fun ("t \<in> redexes")
+ | App ("b \<in> bool" ,"f \<in> redexes" , "a \<in> redexes")
consts
- Ssub,Scomp,Sreg :: i
- "<==","~" :: [i,i]=>o (infixl 70)
- un :: [i,i]=>i (infixl 70)
- union_aux :: i=>i
- regular :: i=>o
+ Ssub :: "i"
+ Scomp :: "i"
+ Sreg :: "i"
+ union_aux :: "i=>i"
+ regular :: "i=>o"
+(*syntax??*)
+ un :: "[i,i]=>i" (infixl 70)
+ "<==" :: "[i,i]=>o" (infixl 70)
+ "~" :: "[i,i]=>o" (infixl 70)
+
+
translations
- "a<==b" == "<a,b>:Ssub"
- "a ~ b" == "<a,b>:Scomp"
- "regular(a)" == "a \\<in> Sreg"
+ "a<==b" == "<a,b> \<in> Ssub"
+ "a ~ b" == "<a,b> \<in> Scomp"
+ "regular(a)" == "a \<in> Sreg"
primrec (*explicit lambda is required because both arguments of "un" vary*)
"union_aux(Var(n)) =
- (\\<lambda>t \\<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
+ (\<lambda>t \<in> redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
"union_aux(Fun(u)) =
- (\\<lambda>t \\<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
+ (\<lambda>t \<in> redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
%b y z. 0, t))"
"union_aux(App(b,f,a)) =
- (\\<lambda>t \\<in> redexes.
+ (\<lambda>t \<in> redexes.
redexes_case(%j. 0, %y. 0,
%c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
defs
- union_def "u un v == union_aux(u)`v"
+ union_def: "u un v == union_aux(u)`v"
+syntax (xsymbols)
+ "op un" :: "[i,i]=>i" (infixl "\<squnion>" 70)
+ "op <==" :: "[i,i]=>o" (infixl "\<Longleftarrow>" 70)
+ "op ~" :: "[i,i]=>o" (infixl "\<sim>" 70)
inductive
domains "Ssub" <= "redexes*redexes"
- intrs
- Sub_Var "n \\<in> nat ==> Var(n)<== Var(n)"
- Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
- Sub_App1 "[|u1<== v1; u2<== v2; b \\<in> bool|]==>
+ intros
+ Sub_Var: "n \<in> nat ==> Var(n)<== Var(n)"
+ Sub_Fun: "[|u<== v|]==> Fun(u)<== Fun(v)"
+ Sub_App1: "[|u1<== v1; u2<== v2; b \<in> bool|]==>
App(0,u1,u2)<== App(b,v1,v2)"
- Sub_App2 "[|u1<== v1; u2<== v2|]==>
- App(1,u1,u2)<== App(1,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
+ 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"
- intrs
- Comp_Var "n \\<in> nat ==> Var(n) ~ Var(n)"
- Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
- Comp_App "[|u1 ~ v1; u2 ~ v2; b1 \\<in> bool; b2 \\<in> bool|]==>
- App(b1,u1,u2) ~ App(b2,v1,v2)"
- type_intrs "redexes.intrs@bool_typechecks"
+ intros
+ Comp_Var: "n \<in> nat ==> Var(n) ~ Var(n)"
+ Comp_Fun: "[|u ~ v|]==> Fun(u) ~ Fun(v)"
+ Comp_App: "[|u1 ~ v1; u2 ~ v2; b1 \<in> bool; b2 \<in> bool|]
+ ==> App(b1,u1,u2) ~ App(b2,v1,v2)"
+ type_intros redexes.intros bool_typechecks
inductive
domains "Sreg" <= "redexes"
- intrs
- Reg_Var "n \\<in> nat ==> regular(Var(n))"
- Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
- Reg_App1 "[|regular(Fun(u)); regular(v)
- |]==>regular(App(1,Fun(u),v))"
- Reg_App2 "[|regular(u); regular(v)
- |]==>regular(App(0,u,v))"
- type_intrs "redexes.intrs@bool_typechecks"
+ intros
+ Reg_Var: "n \<in> nat ==> regular(Var(n))"
+ Reg_Fun: "[|regular(u)|]==> regular(Fun(u))"
+ Reg_App1: "[|regular(Fun(u)); regular(v) |]==>regular(App(1,Fun(u),v))"
+ Reg_App2: "[|regular(u); regular(v) |]==>regular(App(0,u,v))"
+ type_intros redexes.intros bool_typechecks
+
+
+declare redexes.intros [simp]
+
+(* ------------------------------------------------------------------------- *)
+(* Specialisation of comp-rules *)
+(* ------------------------------------------------------------------------- *)
+
+lemmas compD1 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas compD2 [simp] = Scomp.dom_subset [THEN subsetD, THEN SigmaD2]
+lemmas regD [simp] = Sreg.dom_subset [THEN subsetD]
+
+(* ------------------------------------------------------------------------- *)
+(* Equality rules for union *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_Var [simp]: "n \<in> nat ==> Var(n) un Var(n)=Var(n)"
+by (simp add: union_def)
+
+lemma union_Fun [simp]: "v \<in> redexes ==> Fun(u) un Fun(v) = Fun(u un v)"
+by (simp add: union_def)
+
+lemma union_App [simp]:
+ "[|b2 \<in> bool; u2 \<in> redexes; v2 \<in> redexes|]
+ ==> App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)"
+by (simp add: union_def)
+
+
+lemma or_1_right [simp]: "a or 1 = 1"
+by (simp add: or_def cond_def)
+
+lemma or_0_right [simp]: "a \<in> bool \<Longrightarrow> a or 0 = a"
+by (simp add: or_def cond_def bool_def, auto)
+
+
+
+declare Ssub.intros [simp]
+declare bool_typechecks [simp]
+declare Sreg.intros [simp]
+declare Scomp.intros [simp]
+
+declare Scomp.intros [intro]
+inductive_cases [elim!]: "regular(App(b,f,a))"
+inductive_cases [elim!]: "regular(Fun(b))"
+inductive_cases [elim!]: "regular(Var(b))"
+inductive_cases [elim!]: "Fun(u) ~ Fun(t)"
+inductive_cases [elim!]: "u ~ Fun(t)"
+inductive_cases [elim!]: "u ~ Var(n)"
+inductive_cases [elim!]: "u ~ App(b,t,a)"
+inductive_cases [elim!]: "Fun(t) ~ v"
+inductive_cases [elim!]: "App(b,f,a) ~ v"
+inductive_cases [elim!]: "Var(n) ~ u"
+
+
+
+(* ------------------------------------------------------------------------- *)
+(* comp proofs *)
+(* ------------------------------------------------------------------------- *)
+
+lemma comp_refl [simp]: "u \<in> redexes ==> u ~ u"
+by (erule redexes.induct, blast+)
+
+lemma comp_sym: "u ~ v ==> v ~ u"
+by (erule Scomp.induct, blast+)
+
+lemma comp_sym_iff: "u ~ v <-> v ~ u"
+by (blast intro: comp_sym)
+
+lemma comp_trans [rule_format]: "u ~ v ==> \<forall>w. v ~ w-->u ~ w"
+by (erule Scomp.induct, blast+)
+
+(* ------------------------------------------------------------------------- *)
+(* union proofs *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_l: "u ~ v ==> u <== (u un v)"
+apply (erule Scomp.induct)
+apply (erule_tac [3] boolE)
+apply simp_all
+done
+
+lemma union_r: "u ~ v ==> v <== (u un v)"
+apply (erule Scomp.induct)
+apply (erule_tac [3] c = "b2" in boolE)
+apply simp_all
+done
+
+lemma union_sym: "u ~ v ==> u un v = v un u"
+by (erule Scomp.induct, simp_all add: or_commute)
+
+(* ------------------------------------------------------------------------- *)
+(* regular proofs *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_preserve_regular [rule_format]:
+ "u ~ v ==> regular(u)-->regular(v)-->regular(u un v)"
+apply (erule Scomp.induct)
+apply auto
+(*select the given assumption for simplification*)
+apply (erule_tac P = "regular (Fun (?u) un ?v) " in rev_mp)
+apply simp
+done
end
--- a/src/ZF/Resid/Reduction.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-(* Title: Reduction.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-(* ------------------------------------------------------------------------- *)
-(* Setting up rulelists for reduction *)
-(* ------------------------------------------------------------------------- *)
-
-val red1D1 = Sred1.dom_subset RS subsetD RS SigmaD1;
-val red1D2 = Sred1.dom_subset RS subsetD RS SigmaD2;
-val redD1 = Sred.dom_subset RS subsetD RS SigmaD1;
-val redD2 = Sred.dom_subset RS subsetD RS SigmaD2;
-val par_red1D1 = Spar_red1.dom_subset RS subsetD RS SigmaD1;
-val par_red1D2 = Spar_red1.dom_subset RS subsetD RS SigmaD2;
-val par_redD1 = Spar_red.dom_subset RS subsetD RS SigmaD1;
-val par_redD2 = Spar_red.dom_subset RS subsetD RS SigmaD2;
-
-
-AddIs (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
- [Spar_red.one_step, lambda.dom_subset RS subsetD,
- unmark_type]@lambda.intrs@bool_typechecks);
-AddSEs [Spar_red1.mk_cases "Fun(t) =1=> Fun(u)"];
-
-Addsimps (Sred1.intrs@[Sred.one_step, Sred.refl]@Spar_red1.intrs@
- [Spar_red.one_step, substL_type, redD1, redD2, par_redD1,
- par_redD2, par_red1D2, unmark_type]);
-
-
-(* ------------------------------------------------------------------------- *)
-(* Lemmas for reduction *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "m--->n ==> Fun(m) ---> Fun(n)";
-by (etac Sred.induct 1);
-by (resolve_tac [Sred.trans] 3);
-by (ALLGOALS (Asm_simp_tac ));
-qed "red_Fun";
-
-Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(m,n)--->Apl(m',n)";
-by (etac Sred.induct 1);
-by (resolve_tac [Sred.trans] 3);
-by (ALLGOALS (Asm_simp_tac ));
-qed "red_Apll";
-
-Goal "[|n \\<in> lambda; m ---> m'|]==> Apl(n,m)--->Apl(n,m')";
-by (etac Sred.induct 1);
-by (resolve_tac [Sred.trans] 3);
-by (ALLGOALS (Asm_simp_tac ));
-qed "red_Aplr";
-
-Goal "[|m ---> m'; n--->n'|]==> Apl(m,n)--->Apl(m',n')";
-by (res_inst_tac [("n","Apl(m',n)")] Sred.trans 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apll,red_Aplr]) ));
-qed "red_Apl";
-
-Goal "[|m \\<in> lambda; m':lambda; n \\<in> lambda; n':lambda; m ---> m'; n--->n'|]==> \
-\ Apl(Fun(m),n)---> n'/m'";
-by (res_inst_tac [("n","Apl(Fun(m'),n')")] Sred.trans 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Apl,red_Fun]) ));
-qed "red_beta";
-
-
-(* ------------------------------------------------------------------------- *)
-(* Lemmas for parallel reduction *)
-(* ------------------------------------------------------------------------- *)
-
-
-Goal "m \\<in> lambda==> m =1=> m";
-by (etac lambda.induct 1);
-by (ALLGOALS (Asm_simp_tac ));
-qed "refl_par_red1";
-
-Goal "m-1->n ==> m=1=>n";
-by (etac Sred1.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [refl_par_red1]) ));
-qed "red1_par_red1";
-
-Goal "m--->n ==> m===>n";
-by (etac Sred.induct 1);
-by (resolve_tac [Spar_red.trans] 3);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [refl_par_red1,red1_par_red1]) ));
-qed "red_par_red";
-
-Goal "m===>n ==> m--->n";
-by (etac Spar_red.induct 1);
-by (etac Spar_red1.induct 1);
-by (resolve_tac [Sred.trans] 5);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [red_Fun,red_beta,red_Apl]) ));
-qed "par_red_red";
-
-
-(* ------------------------------------------------------------------------- *)
-(* Simulation *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "m=1=>n ==> \\<exists>v. m|>v = n & m~v & regular(v)";
-by (etac Spar_red1.induct 1);
-by Safe_tac;
-by (ALLGOALS (REPEAT o (resolve_tac [exI,conjI])));
-by (TRYALL(resolve_tac [res_redex,res_App,res_Fun,res_Var]));
-by (ALLGOALS (asm_simp_tac (simpset())));
-qed "simulation";
-
-
-(* ------------------------------------------------------------------------- *)
-(* commuting of unmark and subst *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)";
-by (etac redexes.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
-qed "unmmark_lift_rec";
-
-Goal "v \\<in> redexes ==> \\<forall>k \\<in> nat. \\<forall>u \\<in> redexes. \
-\ unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)";
-by (etac redexes.induct 1);
-by (ALLGOALS (asm_simp_tac
- (simpset() addsimps [unmmark_lift_rec, subst_Var])));
-qed "unmmark_subst_rec";
-
-
-(* ------------------------------------------------------------------------- *)
-(* Completeness *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)";
-by (etac Scomp.induct 1);
-by (auto_tac (claset(),
- simpset() addsimps [unmmark_subst_rec]));
-by (dres_inst_tac [("psi", "Fun(?u) =1=> ?w")] asm_rl 1);
-by Auto_tac;
-qed_spec_mp "completeness_l";
-
-Goal "[|u \\<in> lambda; u~v; regular(v)|]==> u =1=> unmark(u|>v)";
-by (dtac completeness_l 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lambda_unmark]) ));
-qed "completeness";
-
--- a/src/ZF/Resid/Reduction.thy Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Reduction.thy Sat Dec 22 19:42:35 2001 +0100
@@ -5,56 +5,246 @@
Logic Image: ZF
*)
-Reduction = Terms+
+theory Reduction = Residuals:
+
+(**** Lambda-terms ****)
consts
- Sred1, Sred, Spar_red1,Spar_red :: i
- "-1->","--->","=1=>", "===>" :: [i,i]=>o (infixl 50)
+ lambda :: "i"
+ unmark :: "i=>i"
+ Apl :: "[i,i]=>i"
translations
- "a -1-> b" == "<a,b>:Sred1"
- "a ---> b" == "<a,b>:Sred"
- "a =1=> b" == "<a,b>:Spar_red1"
- "a ===> b" == "<a,b>:Spar_red"
+ "Apl(n,m)" == "App(0,n,m)"
+
+inductive
+ domains "lambda" <= "redexes"
+ intros
+ Lambda_Var: " n \<in> nat ==> Var(n) \<in> lambda"
+ Lambda_Fun: " u \<in> lambda ==> Fun(u) \<in> lambda"
+ Lambda_App: "[|u \<in> lambda; v \<in> lambda|] ==> Apl(u,v) \<in> lambda"
+ type_intros redexes.intros bool_typechecks
+
+declare lambda.intros [intro]
+
+primrec
+ "unmark(Var(n)) = Var(n)"
+ "unmark(Fun(u)) = Fun(unmark(u))"
+ "unmark(App(b,f,a)) = Apl(unmark(f), unmark(a))"
+
+
+declare lambda.intros [simp]
+declare lambda.dom_subset [THEN subsetD, simp, intro]
+
+
+(* ------------------------------------------------------------------------- *)
+(* unmark lemmas *)
+(* ------------------------------------------------------------------------- *)
+
+lemma unmark_type [intro, simp]:
+ "u \<in> redexes ==> unmark(u) \<in> lambda"
+by (erule redexes.induct, simp_all)
+
+lemma lambda_unmark: "u \<in> lambda ==> unmark(u) = u"
+by (erule lambda.induct, simp_all)
+
+
+(* ------------------------------------------------------------------------- *)
+(* lift and subst preserve lambda *)
+(* ------------------------------------------------------------------------- *)
+
+lemma liftL_type [rule_format]:
+ "v \<in> lambda ==> \<forall>k \<in> nat. lift_rec(v,k) \<in> lambda"
+by (erule lambda.induct, simp_all add: lift_rec_Var)
+
+lemma substL_type [rule_format, simp]:
+ "v \<in> lambda ==> \<forall>n \<in> nat. \<forall>u \<in> lambda. subst_rec(u,v,n) \<in> lambda"
+by (erule lambda.induct, simp_all add: liftL_type subst_Var)
+
+
+(* ------------------------------------------------------------------------- *)
+(* type-rule for reduction definitions *)
+(* ------------------------------------------------------------------------- *)
+
+lemmas red_typechecks = substL_type nat_typechecks lambda.intros
+ bool_typechecks
+
+consts
+ Sred1 :: "i"
+ Sred :: "i"
+ Spar_red1 :: "i"
+ Spar_red :: "i"
+ "-1->" :: "[i,i]=>o" (infixl 50)
+ "--->" :: "[i,i]=>o" (infixl 50)
+ "=1=>" :: "[i,i]=>o" (infixl 50)
+ "===>" :: "[i,i]=>o" (infixl 50)
+
+translations
+ "a -1-> b" == "<a,b> \<in> Sred1"
+ "a ---> b" == "<a,b> \<in> Sred"
+ "a =1=> b" == "<a,b> \<in> Spar_red1"
+ "a ===> b" == "<a,b> \<in> Spar_red"
inductive
domains "Sred1" <= "lambda*lambda"
- intrs
- beta "[|m \\<in> lambda; n \\<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
- rfun "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
- apl_l "[|m2 \\<in> lambda; m1 -1-> n1|] ==>
- Apl(m1,m2) -1-> Apl(n1,m2)"
- apl_r "[|m1 \\<in> lambda; m2 -1-> n2|] ==>
- Apl(m1,m2) -1-> Apl(m1,n2)"
- type_intrs "red_typechecks"
+ intros
+ beta: "[|m \<in> lambda; n \<in> lambda|] ==> Apl(Fun(m),n) -1-> n/m"
+ rfun: "[|m -1-> n|] ==> Fun(m) -1-> Fun(n)"
+ apl_l: "[|m2 \<in> lambda; m1 -1-> n1|] ==> Apl(m1,m2) -1-> Apl(n1,m2)"
+ apl_r: "[|m1 \<in> lambda; m2 -1-> n2|] ==> Apl(m1,m2) -1-> Apl(m1,n2)"
+ type_intros red_typechecks
+
+declare Sred1.intros [intro, simp]
inductive
domains "Sred" <= "lambda*lambda"
- intrs
- one_step "[|m-1->n|] ==> m--->n"
- refl "m \\<in> lambda==>m --->m"
- trans "[|m--->n; n--->p|]==>m--->p"
- type_intrs "[Sred1.dom_subset RS subsetD]@red_typechecks"
+ intros
+ one_step: "m-1->n ==> m--->n"
+ refl: "m \<in> lambda==>m --->m"
+ trans: "[|m--->n; n--->p|] ==>m--->p"
+ type_intros Sred1.dom_subset [THEN subsetD] red_typechecks
+
+declare Sred.one_step [intro, simp]
+declare Sred.refl [intro, simp]
inductive
domains "Spar_red1" <= "lambda*lambda"
- intrs
- beta "[|m =1=> m';
- n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
- rvar "n \\<in> nat==> Var(n) =1=> Var(n)"
- rfun "[|m =1=> m'|]==> Fun(m) =1=> Fun(m')"
- rapl "[|m =1=> m';
- n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
- type_intrs "red_typechecks"
+ intros
+ beta: "[|m =1=> m'; n =1=> n'|] ==> Apl(Fun(m),n) =1=> n'/m'"
+ rvar: "n \<in> nat ==> Var(n) =1=> Var(n)"
+ rfun: "m =1=> m' ==> Fun(m) =1=> Fun(m')"
+ rapl: "[|m =1=> m'; n =1=> n'|] ==> Apl(m,n) =1=> Apl(m',n')"
+ type_intros red_typechecks
+
+declare Spar_red1.intros [intro, simp]
+
+inductive
+ domains "Spar_red" <= "lambda*lambda"
+ intros
+ one_step: "m =1=> n ==> m ===> n"
+ trans: "[|m===>n; n===>p|] ==> m===>p"
+ type_intros Spar_red1.dom_subset [THEN subsetD] red_typechecks
+
+declare Spar_red.one_step [intro, simp]
+
+
+
+(* ------------------------------------------------------------------------- *)
+(* Setting up rule lists for reduction *)
+(* ------------------------------------------------------------------------- *)
+
+lemmas red1D1 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas red1D2 [simp] = Sred1.dom_subset [THEN subsetD, THEN SigmaD2]
+lemmas redD1 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas redD2 [simp] = Sred.dom_subset [THEN subsetD, THEN SigmaD2]
+
+lemmas par_red1D1 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas par_red1D2 [simp] = Spar_red1.dom_subset [THEN subsetD, THEN SigmaD2]
+lemmas par_redD1 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas par_redD2 [simp] = Spar_red.dom_subset [THEN subsetD, THEN SigmaD2]
+
+declare bool_typechecks [intro]
+
+inductive_cases [elim!]: "Fun(t) =1=> Fun(u)"
+
+
+
+(* ------------------------------------------------------------------------- *)
+(* Lemmas for reduction *)
+(* ------------------------------------------------------------------------- *)
+
+lemma red_Fun: "m--->n ==> Fun(m) ---> Fun(n)"
+apply (erule Sred.induct)
+apply (rule_tac [3] Sred.trans)
+apply simp_all
+done
+
+lemma red_Apll: "[|n \<in> lambda; m ---> m'|] ==> Apl(m,n)--->Apl(m',n)"
+apply (erule Sred.induct)
+apply (rule_tac [3] Sred.trans)
+apply simp_all
+done
+
+lemma red_Aplr: "[|n \<in> lambda; m ---> m'|] ==> Apl(n,m)--->Apl(n,m')"
+apply (erule Sred.induct)
+apply (rule_tac [3] Sred.trans)
+apply simp_all
+done
+
+lemma red_Apl: "[|m ---> m'; n--->n'|] ==> Apl(m,n)--->Apl(m',n')"
+apply (rule_tac n = "Apl (m',n) " in Sred.trans)
+apply (simp_all add: red_Apll red_Aplr)
+done
- inductive
- domains "Spar_red" <= "lambda*lambda"
- intrs
- one_step "[|m =1=> n|] ==> m ===> n"
- trans "[|m===>n; n===>p|]==>m===>p"
- type_intrs "[Spar_red1.dom_subset RS subsetD]@red_typechecks"
+lemma red_beta: "[|m \<in> lambda; m':lambda; n \<in> lambda; n':lambda; m ---> m'; n--->n'|] ==>
+ Apl(Fun(m),n)---> n'/m'"
+apply (rule_tac n = "Apl (Fun (m') ,n') " in Sred.trans)
+apply (simp_all add: red_Apl red_Fun)
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* Lemmas for parallel reduction *)
+(* ------------------------------------------------------------------------- *)
+
+
+lemma refl_par_red1: "m \<in> lambda==> m =1=> m"
+by (erule lambda.induct, simp_all)
+
+lemma red1_par_red1: "m-1->n ==> m=1=>n"
+by (erule Sred1.induct, simp_all add: refl_par_red1)
+
+lemma red_par_red: "m--->n ==> m===>n"
+apply (erule Sred.induct)
+apply (rule_tac [3] Spar_red.trans)
+apply (simp_all add: refl_par_red1 red1_par_red1)
+done
+
+lemma par_red_red: "m===>n ==> m--->n"
+apply (erule Spar_red.induct)
+apply (erule Spar_red1.induct)
+apply (rule_tac [5] Sred.trans)
+apply (simp_all add: red_Fun red_beta red_Apl)
+done
+
+(* ------------------------------------------------------------------------- *)
+(* Simulation *)
+(* ------------------------------------------------------------------------- *)
+
+lemma simulation: "m=1=>n ==> \<exists>v. m|>v = n & m~v & regular(v)"
+by (erule Spar_red1.induct, force+)
+
+
+(* ------------------------------------------------------------------------- *)
+(* commuting of unmark and subst *)
+(* ------------------------------------------------------------------------- *)
+
+lemma unmmark_lift_rec:
+ "u \<in> redexes ==> \<forall>k \<in> nat. unmark(lift_rec(u,k)) = lift_rec(unmark(u),k)"
+by (erule redexes.induct, simp_all add: lift_rec_Var)
+
+lemma unmmark_subst_rec:
+ "v \<in> redexes ==> \<forall>k \<in> nat. \<forall>u \<in> redexes.
+ unmark(subst_rec(u,v,k)) = subst_rec(unmark(u),unmark(v),k)"
+by (erule redexes.induct, simp_all add: unmmark_lift_rec subst_Var)
+
+
+(* ------------------------------------------------------------------------- *)
+(* Completeness *)
+(* ------------------------------------------------------------------------- *)
+
+lemma completeness_l [rule_format]:
+ "u~v ==> regular(v) --> unmark(u) =1=> unmark(u|>v)"
+apply (erule Scomp.induct)
+apply (auto simp add: unmmark_subst_rec)
+apply (drule_tac psi = "Fun (?u) =1=> ?w" in asm_rl)
+apply auto
+done
+
+lemma completeness: "[|u \<in> lambda; u~v; regular(v)|] ==> u =1=> unmark(u|>v)"
+by (drule completeness_l, simp_all add: lambda_unmark)
end
--- a/src/ZF/Resid/Residuals.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,182 +0,0 @@
-(* Title: Residuals.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-(* ------------------------------------------------------------------------- *)
-(* Setting up rule lists *)
-(* ------------------------------------------------------------------------- *)
-
-AddIs (Sres.intrs @ Sreg.intrs @ [subst_type]);
-AddSEs (map Sres.mk_cases
- ["residuals(Var(n),Var(n),v)",
- "residuals(Fun(t),Fun(u),v)",
- "residuals(App(b, u1, u2), App(0, v1, v2),v)",
- "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)",
- "residuals(Var(n),u,v)",
- "residuals(Fun(t),u,v)",
- "residuals(App(b, u1, u2), w,v)",
- "residuals(u,Var(n),v)",
- "residuals(u,Fun(t),v)",
- "residuals(w,App(b, u1, u2),v)"]);
-
-AddSEs (map Ssub.mk_cases
- ["Var(n) <== u",
- "Fun(n) <== u",
- "u <== Fun(n)",
- "App(1,Fun(t),a) <== u",
- "App(0,t,a) <== u"]);
-
-AddSEs [redexes.mk_cases "Fun(t):redexes"];
-
-Addsimps Sres.intrs;
-val resD1 = Sres.dom_subset RS subsetD RS SigmaD1;
-val resD2 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1;
-val resD3 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2;
-
-
-(* ------------------------------------------------------------------------- *)
-(* residuals is a partial function *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "residuals(u,v,w) ==> \\<forall>w1. residuals(u,v,w1) --> w1 = w";
-by (etac Sres.induct 1);
-by (ALLGOALS Force_tac);
-qed_spec_mp "residuals_function";
-
-Goal "u~v ==> regular(v) --> (\\<exists>w. residuals(u,v,w))";
-by (etac Scomp.induct 1);
-by (ALLGOALS Fast_tac);
-qed "residuals_intro";
-
-Goal "[| u~v; regular(v) |] ==> residuals(u,v,THE w. residuals(u, v, w))";
-by (resolve_tac [residuals_intro RS mp RS exE] 1);
-by (stac the_equality 3);
-by (ALLGOALS (blast_tac (claset() addIs [residuals_function])));
-qed "comp_resfuncD";
-
-
-(* ------------------------------------------------------------------------- *)
-(* Residual function *)
-(* ------------------------------------------------------------------------- *)
-
-Goalw [res_func_def] "n \\<in> nat ==> Var(n) |> Var(n) = Var(n)";
-by (Blast_tac 1);
-qed "res_Var";
-
-Goalw [res_func_def]
- "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)";
-by (blast_tac (claset() addSDs [comp_resfuncD]
- addIs [residuals_function]) 1);
-qed "res_Fun";
-
-Goalw [res_func_def]
- "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
-\ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)";
-by (blast_tac (claset() addSDs [comp_resfuncD]
- addIs [residuals_function]) 1);
-qed "res_App";
-
-Goalw [res_func_def]
- "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \
-\ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)";
-by (blast_tac (claset() addSEs redexes.free_SEs
- addSDs [comp_resfuncD]
- addIs [residuals_function]) 1);
-qed "res_redex";
-
-Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t \\<in> redexes";
-by (etac Scomp.induct 1);
-by (auto_tac (claset(),
- simpset() addsimps [res_Var,res_Fun,res_App,res_redex]));
-by (dres_inst_tac [("psi", "Fun(?u) |> ?v \\<in> redexes")] asm_rl 1);
-by (auto_tac (claset(),
- simpset() addsimps [res_Fun]));
-qed "resfunc_type";
-
-Addsimps [res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp,
- lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type,
- subst_rec_preserve_reg];
-
-
-(* ------------------------------------------------------------------------- *)
-(* Commutation theorem *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u<==v ==> u~v";
-by (etac Ssub.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "sub_comp";
-
-Goal "u<==v ==> regular(v) --> regular(u)";
-by (etac Ssub.induct 1);
-by Auto_tac;
-qed_spec_mp "sub_preserve_reg";
-
-Goal "[|u~v; k \\<in> nat|]==> regular(v)--> (\\<forall>n \\<in> nat. \
-\ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps [lift_rec_Var,subst_Var,lift_subst])));
-by (rotate_tac ~2 1);
-by (Asm_full_simp_tac 1);
-qed "residuals_lift_rec";
-
-Goal "u1~u2 ==> \\<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\
-\ (\\<forall>n \\<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \
-\ subst_rec(v1 |> v2, u1 |> u2,n))";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps [lift_rec_Var,subst_Var,residuals_lift_rec])));
-by (dres_inst_tac [("psi", "\\<forall>x.?P(x)")] asm_rl 1);
-by (asm_full_simp_tac (simpset() addsimps [substitution]) 1);
-qed "residuals_subst_rec";
-
-
-Goal "[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\
-\ (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)";
-by (asm_simp_tac (simpset() addsimps [residuals_subst_rec]) 1);
-qed "commutation";
-
-(* ------------------------------------------------------------------------- *)
-(* Residuals are comp and regular *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u~v ==> \\<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
-by (etac Scomp.induct 1);
-by (ALLGOALS Force_tac);
-qed_spec_mp "residuals_preserve_comp";
-
-
-Goal "u~v ==> regular(u) --> regular(v) --> regular(u|>v)";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl));
-by Auto_tac;
-qed_spec_mp "residuals_preserve_reg";
-
-(* ------------------------------------------------------------------------- *)
-(* Preservation lemma *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u~v ==> v ~ (u un v)";
-by (etac Scomp.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "union_preserve_comp";
-
-Goal "u ~ v ==> regular(v) --> u|>v = (u un v)|>v";
-by (etac Scomp.induct 1);
-by Safe_tac;
-by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3);
-by (auto_tac (claset(),
- simpset() addsimps [union_preserve_comp,comp_sym_iff]));
-by (asm_full_simp_tac (simpset() addsimps
- [union_preserve_comp RS comp_sym,
- comp_sym RS union_preserve_comp RS comp_sym]) 1);
-qed_spec_mp "preservation";
--- a/src/ZF/Resid/Residuals.thy Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Residuals.thy Sat Dec 22 19:42:35 2001 +0100
@@ -6,31 +6,249 @@
*)
-Residuals = Substitution+
+theory Residuals = Substitution:
consts
- Sres :: i
- residuals :: [i,i,i]=>i
- "|>" :: [i,i]=>i (infixl 70)
-
+ Sres :: "i"
+ residuals :: "[i,i,i]=>i"
+ "|>" :: "[i,i]=>i" (infixl 70)
+
translations
- "residuals(u,v,w)" == "<u,v,w>:Sres"
+ "residuals(u,v,w)" == "<u,v,w> \<in> Sres"
inductive
domains "Sres" <= "redexes*redexes*redexes"
- intrs
- Res_Var "n \\<in> nat ==> residuals(Var(n),Var(n),Var(n))"
- Res_Fun "[|residuals(u,v,w)|]==>
+ intros
+ Res_Var: "n \<in> nat ==> residuals(Var(n),Var(n),Var(n))"
+ Res_Fun: "[|residuals(u,v,w)|]==>
residuals(Fun(u),Fun(v),Fun(w))"
- Res_App "[|residuals(u1,v1,w1);
- residuals(u2,v2,w2); b \\<in> bool|]==>
+ Res_App: "[|residuals(u1,v1,w1);
+ residuals(u2,v2,w2); b \<in> bool|]==>
residuals(App(b,u1,u2),App(0,v1,v2),App(b,w1,w2))"
- Res_redex "[|residuals(u1,v1,w1);
- residuals(u2,v2,w2); b \\<in> bool|]==>
+ Res_redex: "[|residuals(u1,v1,w1);
+ residuals(u2,v2,w2); b \<in> bool|]==>
residuals(App(b,Fun(u1),u2),App(1,Fun(v1),v2),w2/w1)"
- type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks"
+ type_intros subst_type nat_typechecks redexes.intros bool_typechecks
+
+defs
+ res_func_def: "u |> v == THE w. residuals(u,v,w)"
+
+
+(* ------------------------------------------------------------------------- *)
+(* Setting up rule lists *)
+(* ------------------------------------------------------------------------- *)
+
+declare Sres.intros [intro]
+declare Sreg.intros [intro]
+declare subst_type [intro]
+
+inductive_cases [elim!]: "residuals(Var(n),Var(n),v)"
+inductive_cases [elim!]: "residuals(Fun(t),Fun(u),v)"
+inductive_cases [elim!]: "residuals(App(b, u1, u2), App(0, v1, v2),v)"
+inductive_cases [elim!]: "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)"
+inductive_cases [elim!]: "residuals(Var(n),u,v)"
+inductive_cases [elim!]: "residuals(Fun(t),u,v)"
+inductive_cases [elim!]: "residuals(App(b, u1, u2), w,v)"
+inductive_cases [elim!]: "residuals(u,Var(n),v)"
+inductive_cases [elim!]: "residuals(u,Fun(t),v)"
+inductive_cases [elim!]: "residuals(w,App(b, u1, u2),v)"
+
+
+inductive_cases [elim!]: "Var(n) <== u"
+inductive_cases [elim!]: "Fun(n) <== u"
+inductive_cases [elim!]: "u <== Fun(n)"
+inductive_cases [elim!]: "App(1,Fun(t),a) <== u"
+inductive_cases [elim!]: "App(0,t,a) <== u"
+
+inductive_cases [elim!]: "Fun(t):redexes"
+
+declare Sres.intros [simp]
+
+
+(* ------------------------------------------------------------------------- *)
+(* residuals is a partial function *)
+(* ------------------------------------------------------------------------- *)
+
+lemma residuals_function [rule_format]:
+ "residuals(u,v,w) ==> \<forall>w1. residuals(u,v,w1) --> w1 = w"
+by (erule Sres.induct, force+)
+
+lemma residuals_intro [rule_format]:
+ "u~v ==> regular(v) --> (\<exists>w. residuals(u,v,w))"
+by (erule Scomp.induct, force+)
+
+lemma comp_resfuncD:
+ "[| u~v; regular(v) |] ==> residuals(u, v, THE w. residuals(u, v, w))"
+apply (frule residuals_intro, assumption)
+apply clarify
+apply (subst the_equality)
+apply (blast intro: residuals_function)+
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* Residual function *)
+(* ------------------------------------------------------------------------- *)
+
+lemma res_Var [simp]: "n \<in> nat ==> Var(n) |> Var(n) = Var(n)"
+by (unfold res_func_def, blast)
+
+lemma res_Fun [simp]:
+ "[|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 \<in> bool|]
+ ==> App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"
+apply (unfold res_func_def)
+apply (blast dest!: comp_resfuncD intro: residuals_function)
+done
+
+lemma res_redex [simp]:
+ "[|s~u; regular(u); t~v; regular(v); b \<in> bool|]
+ ==> 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
+ intro: residuals_function)
+done
+
+lemma resfunc_type [simp]:
+ "[|s~t; regular(t)|]==> regular(t) --> s |> t \<in> redexes"
+apply (erule Scomp.induct)
+apply auto
+apply (drule_tac psi = "Fun (?u) |> ?v \<in> redexes" in asm_rl)
+apply auto
+done
+
+(* ------------------------------------------------------------------------- *)
+(* Commutation theorem *)
+(* ------------------------------------------------------------------------- *)
+
+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)"
+by (erule Ssub.induct, auto)
-rules
- res_func_def "u |> v == THE w. residuals(u,v,w)"
+lemma residuals_lift_rec: "[|u~v; k \<in> nat|]==> regular(v)--> (\<forall>n \<in> nat.
+ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"
+apply (erule Scomp.induct)
+apply safe
+apply (simp_all add: lift_rec_Var subst_Var lift_subst)
+apply (rotate_tac -2)
+apply simp
+done
+
+lemma residuals_subst_rec:
+ "u1~u2 ==> \<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->
+ (\<forall>n \<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) =
+ subst_rec(v1 |> v2, u1 |> u2,n))"
+apply (erule Scomp.induct)
+apply safe
+apply (simp_all add: lift_rec_Var subst_Var residuals_lift_rec)
+apply (drule_tac psi = "\<forall>x.?P (x) " in asm_rl)
+apply (simp add: substitution)
+done
+
+
+lemma commutation [simp]:
+ "[|u1~u2; v1~v2; regular(u2); regular(v2)|]
+ ==> (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"
+by (simp add: residuals_subst_rec)
+
+
+(* ------------------------------------------------------------------------- *)
+(* Residuals are comp and regular *)
+(* ------------------------------------------------------------------------- *)
+
+lemma residuals_preserve_comp [rule_format, simp]:
+ "u~v ==> \<forall>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)"
+apply (erule Scomp.induct)
+apply auto
+apply (drule_tac psi = "regular (Fun (?u) |> ?v)" in asm_rl, force)+
+done
+
+(* ------------------------------------------------------------------------- *)
+(* Preservation lemma *)
+(* ------------------------------------------------------------------------- *)
+
+lemma union_preserve_comp: "u~v ==> v ~ (u un v)"
+by (erule Scomp.induct, simp_all)
+
+lemma preservation [rule_format]:
+ "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"
+apply (erule Scomp.induct)
+apply safe
+apply (drule_tac [3] psi = "Fun (?u) |> ?v = ?w" in asm_rl)
+apply (auto simp add: union_preserve_comp comp_sym_iff)
+done
+
+
+(**** And now the Cube ***)
+
+declare sub_comp [THEN comp_sym, simp]
+
+(* ------------------------------------------------------------------------- *)
+(* Prism theorem *)
+(* ============= *)
+(* ------------------------------------------------------------------------- *)
+
+(* Having more assumptions than needed -- removed below *)
+lemma prism_l [rule_format]:
+ "v<==u ==>
+ regular(u) --> (\<forall>w. w~v --> w~u -->
+ w |> u = (w|>v) |> (u|>v))"
+apply (erule Ssub.induct)
+apply force+
+done
+
+lemma prism:
+ "[|v <== u; regular(u); w~v|] ==> w |> u = (w|>v) |> (u|>v)"
+apply (rule prism_l)
+apply (rule_tac [4] comp_trans)
+apply auto
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* Levy's Cube Lemma *)
+(* ------------------------------------------------------------------------- *)
+
+lemma cube: "[|u~v; regular(v); regular(u); w~u|]==>
+ (w|>u) |> (v|>u) = (w|>v) |> (u|>v)"
+apply (subst preservation , assumption , assumption)
+apply (subst preservation , erule comp_sym , assumption)
+apply (subst prism [symmetric])
+apply (simp add: union_r comp_sym_iff)
+apply (simp add: union_preserve_regular comp_sym_iff)
+apply (erule comp_trans)
+apply assumption
+apply (simp add: prism [symmetric] union_l union_preserve_regular
+ comp_sym_iff union_sym)
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* paving theorem *)
+(* ------------------------------------------------------------------------- *)
+
+lemma paving: "[|w~u; w~v; regular(u); regular(v)|]==>
+ \<exists>uv vu. (w|>u) |> vu = (w|>v) |> uv & (w|>u)~vu &
+ regular(vu) & (w|>v)~uv & regular(uv) "
+apply (subgoal_tac "u~v")
+apply (safe intro!: exI)
+apply (rule cube)
+apply (simp_all add: comp_sym_iff)
+apply (blast intro: residuals_preserve_comp comp_trans comp_sym)+
+done
+
+
end
--- a/src/ZF/Resid/Substitution.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,257 +0,0 @@
-(* Title: Substitution.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-(* ------------------------------------------------------------------------- *)
-(* Arithmetic extensions *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[| p < n; n \\<in> nat|] ==> n\\<noteq>p";
-by (Fast_tac 1);
-qed "gt_not_eq";
-
-Goal "[|j \\<in> nat; i \\<in> nat|] ==> i < j --> succ(j #- 1) = j";
-by (induct_tac "j" 1);
-by (Fast_tac 1);
-by (Asm_simp_tac 1);
-qed "succ_pred";
-
-Goal "[|succ(x)<n; n \\<in> nat; x \\<in> nat|] ==> x < n #- 1 ";
-by (rtac succ_leE 1);
-by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
-qed "lt_pred";
-
-Goal "[|n < succ(x); p<n; p \\<in> nat; n \\<in> nat; x \\<in> nat|] ==> n #- 1 < x ";
-by (rtac succ_leE 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
-qed "gt_pred";
-
-
-Addsimps [not_lt_iff_le, if_P, if_not_P];
-
-
-(* ------------------------------------------------------------------------- *)
-(* lift_rec equality rules *)
-(* ------------------------------------------------------------------------- *)
-Goal "[|n \\<in> nat; i \\<in> nat|] \
-\ ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_Var";
-
-Goal "[|n \\<in> nat; i \\<in> nat; k \\<in> nat; k le i|] ==> lift_rec(Var(i),k) = Var(succ(i))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_le";
-
-Goal "[|i \\<in> nat; k \\<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_gt";
-
-Goal "[|n \\<in> nat; k \\<in> nat|] ==> \
-\ lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_Fun";
-
-Goal "[|n \\<in> nat; k \\<in> nat|] ==> \
-\ lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_def]) 1);
-qed "lift_rec_App";
-
-
-(* ------------------------------------------------------------------------- *)
-(* substitution quality rules *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "[|i \\<in> nat; k \\<in> nat; u \\<in> redexes|] \
-\ ==> subst_rec(u,Var(i),k) = \
-\ (if k<i then Var(i #- 1) else if k=i then u else Var(i))";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
-qed "subst_Var";
-
-Goal "[|n \\<in> nat; u \\<in> redexes|] ==> subst_rec(u,Var(n),n) = u";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_eq";
-
-Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; p<n|] ==> \
-\ subst_rec(u,Var(n),p) = Var(n #- 1)";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_gt";
-
-Goal "[|n \\<in> nat; u \\<in> redexes; p \\<in> nat; n<p|] ==> \
-\ subst_rec(u,Var(n),p) = Var(n)";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def, gt_not_eq, leI]) 1);
-qed "subst_lt";
-
-Goal "[|p \\<in> nat; u \\<in> redexes|] ==> \
-\ subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) ";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_Fun";
-
-Goal "[|p \\<in> nat; u \\<in> redexes|] ==> \
-\ subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))";
-by (asm_simp_tac (simpset() addsimps [subst_rec_def]) 1);
-qed "subst_App";
-
-(*But not lift_rec_Var, subst_Var: too many case splits*)
-Addsimps [subst_Fun, subst_App];
-
-
-Goal "u \\<in> redexes ==> \\<forall>k \\<in> nat. lift_rec(u,k):redexes";
-by (etac redexes.induct 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [lift_rec_Var,
- lift_rec_Fun, lift_rec_App])));
-qed_spec_mp "lift_rec_type";
-
-Goal "v \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. subst_rec(u,v,n):redexes";
-by (etac redexes.induct 1);
-by (ALLGOALS(asm_simp_tac
- (simpset() addsimps [subst_Var, lift_rec_type])));
-qed_spec_mp "subst_type";
-
-
-Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
- lift_rec_le, lift_rec_gt, lift_rec_Fun, lift_rec_App,
- lift_rec_type];
-
-
-(* ------------------------------------------------------------------------- *)
-(* lift and substitution proofs *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> \\<forall>n \\<in> nat. \\<forall>i \\<in> nat. i le n --> \
-\ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))";
-by (etac redexes.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by Safe_tac;
-by (case_tac "n < i" 1);
-by ((ftac lt_trans2 1) THEN (assume_tac 1));
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI])));
-qed "lift_lift_rec";
-
-Goal "[|u \\<in> redexes; n \\<in> nat|] ==> \
-\ lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))";
-by (asm_simp_tac (simpset() addsimps [lift_lift_rec]) 1);
-qed "lift_lift";
-
-Goal "v \\<in> redexes ==> \
-\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. n le m-->\
-\ lift_rec(subst_rec(u,v,n),m) = \
-\ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)";
-by ((etac redexes.induct 1)
- THEN (ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift]))));
-by Safe_tac;
-by (excluded_middle_tac "n < x" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("j","n")] leE 1);
-by (asm_simp_tac (simpset() setloop (split_inside_tac [split_if])
- addsimps [lift_rec_Var,subst_Var,
- leI,gt_pred,succ_pred]) 1);
-by (hyp_subst_tac 1);
-by (Asm_simp_tac 1);
-by (forw_inst_tac [("j","x")] lt_trans2 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [leI]) 1);
-qed "lift_rec_subst_rec";
-
-Goal "[|v \\<in> redexes; u \\<in> redexes; n \\<in> nat|] ==> \
-\ lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))";
-by (asm_simp_tac (simpset() addsimps [lift_rec_subst_rec]) 1);
-qed "lift_subst";
-
-
-Goal "v \\<in> redexes ==> \
-\ \\<forall>n \\<in> nat. \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. m le n-->\
-\ lift_rec(subst_rec(u,v,n),m) = \
-\ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))";
-by (etac redexes.induct 1
- THEN ALLGOALS(asm_simp_tac (simpset() addsimps [lift_lift])));
-by Safe_tac;
-by (excluded_middle_tac "n < x" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("i","x")] leE 1);
-by (ftac lt_trans1 1 THEN assume_tac 1);
-by (ALLGOALS(asm_simp_tac
- (simpset() addsimps [succ_pred,leI,gt_pred])));
-by (asm_full_simp_tac (simpset() addsimps [leI]) 1);
-by (case_tac "n < xa" 1);
-by (Asm_full_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [leI]) 1);
-qed "lift_rec_subst_rec_lt";
-
-
-Goal "u \\<in> redexes ==> \
-\ \\<forall>n \\<in> nat. \\<forall>v \\<in> redexes. subst_rec(v,lift_rec(u,n),n) = u";
-by (etac redexes.induct 1);
-by Auto_tac;
-by (case_tac "n < na" 1);
-by Auto_tac;
-qed "subst_rec_lift_rec";
-
-Goal "v \\<in> redexes ==> \
-\ \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. \\<forall>u \\<in> redexes. \\<forall>w \\<in> redexes. m le n --> \
-\ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m)=\
-\ subst_rec(w,subst_rec(u,v,m),n)";
-by (etac redexes.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps
- [lift_lift RS sym,lift_rec_subst_rec_lt])));
-by Safe_tac;
-by (excluded_middle_tac "n le succ(xa)" 1);
-by (Asm_full_simp_tac 1);
-by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
-by (etac leE 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 2);
-by (forward_tac [succ_leI RS lt_trans] 1 THEN assume_tac 1);
-by (forw_inst_tac [("i","x")]
- (nat_into_Ord RS le_refl RS lt_trans) 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred,lt_pred]) 1);
-by (eres_inst_tac [("i","n")] leE 1);
-by (asm_simp_tac (simpset() addsimps [succ_pred,subst_rec_lift_rec,leI]) 2);
-by (excluded_middle_tac "n < x" 1);
-by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("j","n")] leE 1);
-by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
-by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1);
-by (ftac lt_trans2 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [gt_pred]) 1);
-qed "subst_rec_subst_rec";
-
-
-Goal "[|v \\<in> redexes; u \\<in> redexes; w \\<in> redexes; n \\<in> nat|] ==> \
-\ subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)";
-by (asm_simp_tac (simpset() addsimps [subst_rec_subst_rec]) 1);
-qed "substitution";
-
-(* ------------------------------------------------------------------------- *)
-(* Preservation lemmas *)
-(* Substitution preserves comp and regular *)
-(* ------------------------------------------------------------------------- *)
-
-
-Goal "[|n \\<in> nat; u ~ v|] ==> \\<forall>m \\<in> nat. lift_rec(u,m) ~ lift_rec(v,m)";
-by (etac Scomp.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [comp_refl])));
-qed "lift_rec_preserve_comp";
-
-Goal "u2 ~ v2 ==> \\<forall>m \\<in> nat. \\<forall>u1 \\<in> redexes. \\<forall>v1 \\<in> redexes.\
-\ u1 ~ v1--> subst_rec(u1,u2,m) ~ subst_rec(v1,v2,m)";
-by (etac Scomp.induct 1);
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps [subst_Var, lift_rec_preserve_comp, comp_refl])));
-qed "subst_rec_preserve_comp";
-
-Goal "regular(u) ==> \\<forall>m \\<in> nat. regular(lift_rec(u,m))";
-by (etac Sreg.induct 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var])));
-qed "lift_rec_preserve_reg";
-
-Goal "regular(v) ==> \
-\ \\<forall>m \\<in> nat. \\<forall>u \\<in> redexes. regular(u)-->regular(subst_rec(u,v,m))";
-by (etac Sreg.induct 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_Var,
- lift_rec_preserve_reg])));
-qed "subst_rec_preserve_reg";
--- a/src/ZF/Resid/Substitution.thy Fri Dec 21 23:20:29 2001 +0100
+++ b/src/ZF/Resid/Substitution.thy Sat Dec 22 19:42:35 2001 +0100
@@ -5,19 +5,19 @@
Logic Image: ZF
*)
-Substitution = Redex +
+theory Substitution = Redex:
consts
- lift_aux :: i=> i
- lift :: i=> i
- subst_aux :: i=> i
- "'/" :: [i,i]=>i (infixl 70) (*subst*)
+ lift_aux :: "i=>i"
+ lift :: "i=>i"
+ subst_aux :: "i=>i"
+ "'/" :: "[i,i]=>i" (infixl 70) (*subst*)
constdefs
- lift_rec :: [i,i]=> i
+ lift_rec :: "[i,i]=> i"
"lift_rec(r,k) == lift_aux(r)`k"
- subst_rec :: [i,i,i]=> i (**NOTE THE ARGUMENT ORDER BELOW**)
+ subst_rec :: "[i,i,i]=> i" (**NOTE THE ARGUMENT ORDER BELOW**)
"subst_rec(u,r,k) == subst_aux(r)`u`k"
translations
@@ -29,23 +29,246 @@
in the recursive calls ***)
primrec
- "lift_aux(Var(i)) = (\\<lambda>k \\<in> nat. if i<k then Var(i) else Var(succ(i)))"
+ "lift_aux(Var(i)) = (\<lambda>k \<in> nat. if i<k then Var(i) else Var(succ(i)))"
- "lift_aux(Fun(t)) = (\\<lambda>k \\<in> nat. Fun(lift_aux(t) ` succ(k)))"
+ "lift_aux(Fun(t)) = (\<lambda>k \<in> nat. Fun(lift_aux(t) ` succ(k)))"
- "lift_aux(App(b,f,a)) = (\\<lambda>k \\<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
+ "lift_aux(App(b,f,a)) = (\<lambda>k \<in> nat. App(b, lift_aux(f)`k, lift_aux(a)`k))"
primrec
"subst_aux(Var(i)) =
- (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. if k<i then Var(i #- 1)
+ (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. if k<i then Var(i #- 1)
else if k=i then r else Var(i))"
"subst_aux(Fun(t)) =
- (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
+ (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
"subst_aux(App(b,f,a)) =
- (\\<lambda>r \\<in> redexes. \\<lambda>k \\<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
+ (\<lambda>r \<in> redexes. \<lambda>k \<in> nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
+
+
+(* ------------------------------------------------------------------------- *)
+(* Arithmetic extensions *)
+(* ------------------------------------------------------------------------- *)
+
+lemma gt_not_eq: "p < n ==> n\<noteq>p"
+by blast
+
+lemma succ_pred [rule_format, simp]: "j \<in> nat ==> i < j --> succ(j #- 1) = j"
+by (induct_tac "j", auto)
+
+lemma lt_pred: "[|succ(x)<n; n \<in> nat|] ==> x < n #- 1 "
+apply (rule succ_leE)
+apply (simp add: succ_pred)
+done
+
+lemma gt_pred: "[|n < succ(x); p<n; n \<in> nat|] ==> n #- 1 < x "
+apply (rule succ_leE)
+apply (simp add: succ_pred)
+done
+
+
+declare not_lt_iff_le [simp] if_P [simp] if_not_P [simp]
+
+
+(* ------------------------------------------------------------------------- *)
+(* lift_rec equality rules *)
+(* ------------------------------------------------------------------------- *)
+lemma lift_rec_Var:
+ "n \<in> nat ==> lift_rec(Var(i),n) = (if i<n then Var(i) else Var(succ(i)))"
+by (simp add: lift_rec_def)
+
+lemma lift_rec_le [simp]:
+ "[|i \<in> nat; k\<le>i|] ==> lift_rec(Var(i),k) = Var(succ(i))"
+by (simp add: lift_rec_def le_in_nat)
+
+lemma lift_rec_gt [simp]: "[| k \<in> nat; i<k |] ==> lift_rec(Var(i),k) = Var(i)"
+by (simp add: lift_rec_def)
+
+lemma lift_rec_Fun [simp]:
+ "k \<in> nat ==> lift_rec(Fun(t),k) = Fun(lift_rec(t,succ(k)))"
+by (simp add: lift_rec_def)
+
+lemma lift_rec_App [simp]:
+ "k \<in> nat ==> lift_rec(App(b,f,a),k) = App(b,lift_rec(f,k),lift_rec(a,k))"
+by (simp add: lift_rec_def)
+
+
+(* ------------------------------------------------------------------------- *)
+(* substitution quality rules *)
+(* ------------------------------------------------------------------------- *)
+
+lemma subst_Var:
+ "[|k \<in> nat; u \<in> redexes|]
+ ==> subst_rec(u,Var(i),k) =
+ (if k<i then Var(i #- 1) else if k=i then u else Var(i))"
+by (simp add: subst_rec_def gt_not_eq leI)
+
+
+lemma subst_eq [simp]:
+ "[|n \<in> nat; u \<in> redexes|] ==> subst_rec(u,Var(n),n) = u"
+by (simp add: subst_rec_def)
+
+lemma subst_gt [simp]:
+ "[|u \<in> redexes; p \<in> nat; p<n|] ==> subst_rec(u,Var(n),p) = Var(n #- 1)"
+by (simp add: subst_rec_def)
+
+lemma subst_lt [simp]:
+ "[|u \<in> redexes; p \<in> nat; n<p|] ==> subst_rec(u,Var(n),p) = Var(n)"
+by (simp add: subst_rec_def gt_not_eq leI lt_nat_in_nat)
+
+lemma subst_Fun [simp]:
+ "[|p \<in> nat; u \<in> redexes|]
+ ==> subst_rec(u,Fun(t),p) = Fun(subst_rec(lift(u),t,succ(p))) "
+by (simp add: subst_rec_def)
+
+lemma subst_App [simp]:
+ "[|p \<in> nat; u \<in> redexes|]
+ ==> subst_rec(u,App(b,f,a),p) = App(b,subst_rec(u,f,p),subst_rec(u,a,p))"
+by (simp add: subst_rec_def)
+
+
+lemma lift_rec_type [rule_format, simp]:
+ "u \<in> redexes ==> \<forall>k \<in> nat. lift_rec(u,k) \<in> redexes"
+apply (erule redexes.induct)
+apply (simp_all add: lift_rec_Var lift_rec_Fun lift_rec_App)
+done
+
+lemma subst_type [rule_format, simp]:
+ "v \<in> redexes ==> \<forall>n \<in> nat. \<forall>u \<in> redexes. subst_rec(u,v,n) \<in> redexes"
+apply (erule redexes.induct)
+apply (simp_all add: subst_Var lift_rec_type)
+done
+
+
+(* ------------------------------------------------------------------------- *)
+(* lift and substitution proofs *)
+(* ------------------------------------------------------------------------- *)
+
+(*The i\<in>nat is redundant*)
+lemma lift_lift_rec [rule_format]:
+ "u \<in> redexes
+ ==> \<forall>n \<in> nat. \<forall>i \<in> nat. i\<le>n -->
+ (lift_rec(lift_rec(u,i),succ(n)) = lift_rec(lift_rec(u,n),i))"
+apply (erule redexes.induct)
+apply auto
+apply (case_tac "n < i")
+apply (frule lt_trans2, assumption)
+apply (simp_all add: lift_rec_Var leI)
+done
+
+lemma lift_lift:
+ "[|u \<in> redexes; n \<in> nat|]
+ ==> lift_rec(lift(u),succ(n)) = lift(lift_rec(u,n))"
+by (simp add: lift_lift_rec)
+
+lemma lt_not_m1_lt: "\<lbrakk>m < n; n \<in> nat; m \<in> nat\<rbrakk>\<Longrightarrow> ~ n #- 1 < m"
+by (erule natE, auto)
+
+lemma lift_rec_subst_rec [rule_format]:
+ "v \<in> redexes ==>
+ \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. n\<le>m-->
+ lift_rec(subst_rec(u,v,n),m) =
+ subst_rec(lift_rec(u,m),lift_rec(v,succ(m)),n)"
+apply (erule redexes.induct, simp_all (no_asm_simp) add: lift_lift)
+apply safe
+apply (case_tac "n < x")
+ apply (frule_tac j = "x" in lt_trans2, assumption)
+ apply (simp add: leI)
+apply simp
+apply (erule_tac j = "n" in leE)
+apply (auto simp add: lift_rec_Var subst_Var leI lt_not_m1_lt)
+done
+
+
+lemma lift_subst:
+ "[|v \<in> redexes; u \<in> redexes; n \<in> nat|]
+ ==> lift_rec(u/v,n) = lift_rec(u,n)/lift_rec(v,succ(n))"
+by (simp add: lift_rec_subst_rec)
+
+
+lemma lift_rec_subst_rec_lt [rule_format]:
+ "v \<in> redexes ==>
+ \<forall>n \<in> nat. \<forall>m \<in> nat. \<forall>u \<in> redexes. m\<le>n-->
+ lift_rec(subst_rec(u,v,n),m) =
+ subst_rec(lift_rec(u,m),lift_rec(v,m),succ(n))"
+apply (erule redexes.induct , simp_all (no_asm_simp) add: lift_lift)
+apply safe
+apply (case_tac "n < x")
+apply (case_tac "n < xa")
+apply (simp_all add: leI)
+apply (erule_tac i = "x" in leE)
+apply (frule lt_trans1, assumption)
+apply (simp_all add: succ_pred leI gt_pred)
+done
+
+
+lemma subst_rec_lift_rec [rule_format]:
+ "u \<in> redexes ==>
+ \<forall>n \<in> nat. \<forall>v \<in> redexes. subst_rec(v,lift_rec(u,n),n) = u"
+apply (erule redexes.induct)
+apply auto
+apply (case_tac "n < na")
+apply auto
+done
+
+lemma subst_rec_subst_rec [rule_format]:
+ "v \<in> redexes ==>
+ \<forall>m \<in> nat. \<forall>n \<in> nat. \<forall>u \<in> redexes. \<forall>w \<in> redexes. m\<le>n -->
+ subst_rec(subst_rec(w,u,n),subst_rec(lift_rec(w,m),v,succ(n)),m) =
+ subst_rec(w,subst_rec(u,v,m),n)"
+apply (erule redexes.induct)
+apply (simp_all add: lift_lift [symmetric] lift_rec_subst_rec_lt)
+apply safe
+apply (case_tac "n\<le>succ (xa) ")
+ apply (erule_tac i = "n" in leE)
+ apply (simp_all add: succ_pred subst_rec_lift_rec leI)
+ apply (case_tac "n < x")
+ apply (frule lt_trans2 , assumption, simp add: gt_pred)
+ apply simp
+ apply (erule_tac j = "n" in leE, simp add: gt_pred)
+ apply (simp add: subst_rec_lift_rec)
+(*final case*)
+apply (frule nat_into_Ord [THEN le_refl, THEN lt_trans] , assumption)
+apply (erule leE)
+ apply (frule succ_leI [THEN lt_trans] , assumption)
+ apply (frule_tac i = "x" in nat_into_Ord [THEN le_refl, THEN lt_trans],
+ assumption)
+ apply (simp_all add: succ_pred lt_pred)
+done
+
+
+lemma substitution:
+ "[|v \<in> redexes; u \<in> redexes; w \<in> redexes; n \<in> nat|]
+ ==> subst_rec(w,u,n)/subst_rec(lift(w),v,succ(n)) = subst_rec(w,u/v,n)"
+by (simp add: subst_rec_subst_rec)
+
+
+(* ------------------------------------------------------------------------- *)
+(* Preservation lemmas *)
+(* Substitution preserves comp and regular *)
+(* ------------------------------------------------------------------------- *)
+
+
+lemma lift_rec_preserve_comp [rule_format, simp]:
+ "u ~ v ==> \<forall>m \<in> 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 ==> \<forall>m \<in> nat. \<forall>u1 \<in> redexes. \<forall>v1 \<in> 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)
+
+lemma lift_rec_preserve_reg [simp]:
+ "regular(u) ==> \<forall>m \<in> nat. regular(lift_rec(u,m))"
+by (erule Sreg.induct, simp_all add: lift_rec_Var)
+
+lemma subst_rec_preserve_reg [simp]:
+ "regular(v) ==>
+ \<forall>m \<in> nat. \<forall>u \<in> redexes. regular(u)-->regular(subst_rec(u,v,m))"
+by (erule Sreg.induct, simp_all add: subst_Var lift_rec_preserve_reg)
end
--- a/src/ZF/Resid/Terms.ML Fri Dec 21 23:20:29 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: Terms.ML
- ID: $Id$
- Author: Ole Rasmussen
- Copyright 1995 University of Cambridge
- Logic Image: ZF
-*)
-
-Addsimps ([lambda.dom_subset RS subsetD] @ lambda.intrs);
-
-
-(* ------------------------------------------------------------------------- *)
-(* unmark lemmas *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "u \\<in> redexes ==> unmark(u):lambda";
-by (etac redexes.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "unmark_type";
-
-Goal "u \\<in> lambda ==> unmark(u) = u";
-by (etac lambda.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "lambda_unmark";
-
-
-(* ------------------------------------------------------------------------- *)
-(* lift and subst preserve lambda *)
-(* ------------------------------------------------------------------------- *)
-
-Goal "v \\<in> lambda ==> \\<forall>k \\<in> nat. lift_rec(v,k):lambda";
-by (etac lambda.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
-qed_spec_mp "liftL_type";
-
-Goal "v \\<in> lambda ==> \\<forall>n \\<in> nat. \\<forall>u \\<in> lambda. subst_rec(u,v,n):lambda";
-by (etac lambda.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
-qed_spec_mp "substL_type";
-
-
-(* ------------------------------------------------------------------------- *)
-(* type-rule for reduction definitions *)
-(* ------------------------------------------------------------------------- *)
-
-val red_typechecks = [substL_type]@nat_typechecks@lambda.intrs@bool_typechecks;