--- a/src/HOL/IsaMakefile Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/IsaMakefile Sat Sep 02 21:56:24 2000 +0200
@@ -303,11 +303,10 @@
HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
-$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \
- Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy \
- Lambda/InductTermi.thy Lambda/Lambda.ML Lambda/Lambda.thy \
+$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Induct/Acc.thy Lambda/Commutation.thy \
+ Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
- Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
+ Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
@$(ISATOOL) usedir $(OUT)/HOL Lambda
--- a/src/HOL/Lambda/Commutation.ML Sat Sep 02 21:53:03 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,97 +0,0 @@
-(* Title: HOL/Lambda/Commutation.thy
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1995 TU Muenchen
-
-Basic commutation lemmas.
-*)
-
-open Commutation;
-
-(*** square ***)
-
-Goalw [square_def] "square R S T U ==> square S R U T";
-by (Blast_tac 1);
-qed "square_sym";
-
-Goalw [square_def]
- "[| square R S T U; T <= T' |] ==> square R S T' U";
-by (Blast_tac 1);
-qed "square_subset";
-
-Goalw [square_def]
- "[| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
-by (Blast_tac 1);
-qed "square_reflcl";
-
-Goalw [square_def]
- "square R S S T ==> square (R^*) S S (T^*)";
-by (strip_tac 1);
-by (etac rtrancl_induct 1);
-by (Blast_tac 1);
-by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-qed "square_rtrancl";
-
-Goalw [commute_def]
- "square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
-by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl]
- addEs [r_into_rtrancl]
- addss simpset()) 1);
-qed "square_rtrancl_reflcl_commute";
-
-(*** commute ***)
-
-Goalw [commute_def] "commute R S ==> commute S R";
-by (blast_tac (claset() addIs [square_sym]) 1);
-qed "commute_sym";
-
-Goalw [commute_def] "commute R S ==> commute (R^*) (S^*)";
-by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1);
-qed "commute_rtrancl";
-
-Goalw [commute_def,square_def]
- "[| commute R T; commute S T |] ==> commute (R Un S) T";
-by (Blast_tac 1);
-qed "commute_Un";
-
-(*** diamond, confluence and union ***)
-
-Goalw [diamond_def]
- "[| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
-by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
-qed "diamond_Un";
-
-Goalw [diamond_def] "diamond R ==> confluent (R)";
-by (etac commute_rtrancl 1);
-qed "diamond_confluent";
-
-Goalw [diamond_def]
- "square R R (R^=) (R^=) ==> confluent R";
-by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
- addEs [square_subset]) 1);
-qed "square_reflcl_confluent";
-
-Goal
- "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent(R Un S)";
-by (rtac (rtrancl_Un_rtrancl RS subst) 1);
-by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1);
-qed "confluent_Un";
-
-Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
-by (force_tac (claset() addIs [diamond_confluent]
- addDs [rtrancl_subset RS sym], simpset()) 1);
-qed "diamond_to_confluence";
-
-(*** Church_Rosser ***)
-
-Goalw [square_def,commute_def,diamond_def,Church_Rosser_def]
- "Church_Rosser(R) = confluent(R)";
-by (safe_tac HOL_cs);
- by (blast_tac (HOL_cs addIs
- [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
- rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
-by (etac rtrancl_induct 1);
- by (Blast_tac 1);
-by (blast_tac (claset() delrules [rtrancl_refl]
- addIs [r_into_rtrancl, rtrancl_trans]) 1);
-qed "Church_Rosser_confluent";
--- a/src/HOL/Lambda/Commutation.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/Commutation.thy Sat Sep 02 21:56:24 2000 +0200
@@ -2,28 +2,137 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TU Muenchen
-
-Abstract commutation and confluence notions.
*)
-Commutation = Main +
+header {* Abstract commutation and confluence notions *}
+
+theory Commutation = Main:
+
+subsection {* Basic definitions *}
+
+constdefs
+ square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
+ "square R S T U ==
+ \<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))"
+
+ commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
+ "commute R S == square R S S R"
+
+ diamond :: "('a \<times> 'a) set => bool"
+ "diamond R == commute R R"
+
+ Church_Rosser :: "('a \<times> 'a) set => bool"
+ "Church_Rosser R ==
+ \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
+
+syntax
+ confluent :: "('a \<times> 'a) set => bool"
+translations
+ "confluent R" == "diamond (R^*)"
+
+
+subsection {* Basic lemmas *}
+
+subsubsection {* square *}
-consts
- square :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
- commute :: "[('a*'a)set,('a*'a)set] => bool"
- confluent, diamond, Church_Rosser :: "('a*'a)set => bool"
+lemma square_sym: "square R S T U ==> square S R U T"
+ apply (unfold square_def)
+ apply blast
+ done
+
+lemma square_subset:
+ "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
+ apply (unfold square_def)
+ apply blast
+ done
+
+lemma square_reflcl:
+ "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
+ apply (unfold square_def)
+ apply blast
+ done
-defs
- square_def
- "square R S T U == !x y.(x,y):R --> (!z.(x,z):S --> (? u. (y,u):T & (z,u):U))"
+lemma square_rtrancl:
+ "square R S S T ==> square (R^*) S S (T^*)"
+ apply (unfold square_def)
+ apply (intro strip)
+ apply (erule rtrancl_induct)
+ apply blast
+ apply (blast intro: rtrancl_into_rtrancl)
+ done
+
+lemma square_rtrancl_reflcl_commute:
+ "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
+ apply (unfold commute_def)
+ apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
+ elim: r_into_rtrancl)
+ done
+
- commute_def "commute R S == square R S S R"
- diamond_def "diamond R == commute R R"
+subsubsection {* commute *}
+
+lemma commute_sym: "commute R S ==> commute S R"
+ apply (unfold commute_def)
+ apply (blast intro: square_sym)
+ done
+
+lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
+ apply (unfold commute_def)
+ apply (blast intro: square_rtrancl square_sym)
+ done
+
+lemma commute_Un:
+ "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
+ apply (unfold commute_def square_def)
+ apply blast
+ done
+
+
+subsubsection {* diamond, confluence, and union *}
+
+lemma diamond_Un:
+ "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
+ apply (unfold diamond_def)
+ apply (assumption | rule commute_Un commute_sym)+
+ done
+
+lemma diamond_confluent: "diamond R ==> confluent R"
+ apply (unfold diamond_def)
+ apply (erule commute_rtrancl)
+ done
- Church_Rosser_def "Church_Rosser(R) ==
- !x y. (x,y) : (R Un R^-1)^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
+lemma square_reflcl_confluent:
+ "square R R (R^=) (R^=) ==> confluent R"
+ apply (unfold diamond_def)
+ apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
+ elim: square_subset)
+ done
+
+lemma confluent_Un:
+ "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
+ apply (rule rtrancl_Un_rtrancl [THEN subst])
+ apply (blast dest: diamond_Un intro: diamond_confluent)
+ done
-translations
- "confluent R" == "diamond(R^*)"
+lemma diamond_to_confluence:
+ "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
+ apply (force intro: diamond_confluent
+ dest: rtrancl_subset [symmetric])
+ done
+
+
+subsection {* Church-Rosser *}
-end
+lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
+ apply (unfold square_def commute_def diamond_def Church_Rosser_def)
+ apply (tactic {* safe_tac HOL_cs *})
+ apply (tactic {*
+ blast_tac (HOL_cs addIs
+ [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
+ rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
+ apply (erule rtrancl_induct)
+ apply blast
+ apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)
+ done
+
+end
\ No newline at end of file
--- a/src/HOL/Lambda/Eta.ML Sat Sep 02 21:53:03 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,208 +0,0 @@
-(* Title: HOL/Lambda/Eta.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1995 TU Muenchen
-
-Eta reduction,
-confluence of eta,
-commutation of beta/eta,
-confluence of beta+eta
-*)
-
-Addsimps eta.intrs;
-AddIs eta.intrs;
-
-val eta_cases = map eta.mk_cases ["Abs s -e> z", "s $ t -e> u", "Var i -e> t"];
-AddSEs eta_cases;
-
-section "eta, subst and free";
-
-Goal "!i t u. ~free s i --> s[t/i] = s[u/i]";
-by (induct_tac "s" 1);
-by (ALLGOALS(simp_tac (addsplit (simpset()))));
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "subst_not_free";
-Addsimps [subst_not_free RS eqTrueI];
-
-Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
-by (induct_tac "t" 1);
- by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
- by (arith_tac 1);
-by (Auto_tac);
-qed "free_lift";
-Addsimps [free_lift];
-
-Goal "!i k t. free (s[t/k]) i = \
-\ (free s k & free t i | free s (if i<k then i else i+1))";
-by (induct_tac "s" 1);
-by (Asm_simp_tac 2);
-by (Blast_tac 2);
-by (asm_full_simp_tac (addsplit (simpset())) 2);
-by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
- addsplits [nat.split]) 1);
-by (safe_tac (HOL_cs addSEs [linorder_neqE]));
-by (ALLGOALS Simp_tac);
-qed "free_subst";
-Addsimps [free_subst];
-
-Goal "s -e> t ==> !i. free t i = free s i";
-by (etac eta.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addcongs [conj_cong])));
-qed_spec_mp "free_eta";
-
-Goal "[| s -e> t; ~free s i |] ==> ~free t i";
-by (asm_simp_tac (simpset() addsimps [free_eta]) 1);
-qed "not_free_eta";
-
-Goal "s -e> t ==> !u i. s[u/i] -e> t[u/i]";
-by (etac eta.induct 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
-qed_spec_mp "eta_subst";
-Addsimps [eta_subst];
-
-section "Confluence of -e>";
-
-Goalw [square_def,id_def] "square eta eta (eta^=) (eta^=)";
-by (rtac (impI RS allI RS allI) 1);
-by (Simp_tac 1);
-by (etac eta.induct 1);
-by (slow_tac (claset() addIs [subst_not_free,eta_subst]
- addIs [free_eta RS iffD1] addss simpset()) 1);
-by Safe_tac;
-by (blast_tac (claset() addSIs [eta_subst] addIs [free_eta RS iffD1]) 5);
-by (ALLGOALS Blast_tac);
-qed "square_eta";
-
-Goal "confluent(eta)";
-by (rtac (square_eta RS square_reflcl_confluent) 1);
-qed "eta_confluent";
-
-section "Congruence rules for -e>>";
-
-Goal "s -e>> s' ==> Abs s -e>> Abs s'";
-by (etac rtrancl_induct 1);
-by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
-qed "rtrancl_eta_Abs";
-
-Goal "s -e>> s' ==> s $ t -e>> s' $ t";
-by (etac rtrancl_induct 1);
-by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
-qed "rtrancl_eta_AppL";
-
-Goal "t -e>> t' ==> s $ t -e>> s $ t'";
-by (etac rtrancl_induct 1);
-by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
-qed "rtrancl_eta_AppR";
-
-Goal "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'";
-by (blast_tac (claset() addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
- addIs [rtrancl_trans]) 1);
-qed "rtrancl_eta_App";
-
-section "Commutation of -> and -e>";
-
-Goal "s -> t ==> (!i. free t i --> free s i)";
-by (etac beta.induct 1);
-by (ALLGOALS(Asm_full_simp_tac));
-qed_spec_mp "free_beta";
-
-Goal "s -> t ==> !u i. s[u/i] -> t[u/i]";
-by (etac beta.induct 1);
-by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_subst RS sym])));
-qed_spec_mp "beta_subst";
-AddIs [beta_subst];
-
-Goal "!i. t[Var i/i] = t[Var(i)/i+1]";
-by (induct_tac "t" 1);
-by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
-qed_spec_mp "subst_Var_Suc";
-Addsimps [subst_Var_Suc];
-
-Goal "s -e> t ==> (!i. lift s i -e> lift t i)";
-by (etac eta.induct 1);
-by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
-qed_spec_mp "eta_lift";
-Addsimps [eta_lift];
-
-Goal "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
-by (induct_tac "u" 1);
-by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
-by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
-by (blast_tac (claset() addSIs [rtrancl_eta_App]) 1);
-by (blast_tac (claset() addSIs [rtrancl_eta_Abs,eta_lift]) 1);
-qed_spec_mp "rtrancl_eta_subst";
-
-Goalw [square_def] "square beta eta (eta^*) (beta^=)";
-by (rtac (impI RS allI RS allI) 1);
-by (etac beta.induct 1);
-by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
- addss simpset()) 1);
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
-by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
-(*23 seconds?*)
-DelIffs dB.distinct;
-Addsimps dB.distinct;
-by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
- addss simpset()) 1);
-qed "square_beta_eta";
-
-Goal "confluent(beta Un eta)";
-by (REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un,
- beta_confluent,eta_confluent,square_beta_eta] 1));
-qed "confluent_beta_eta";
-
-section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
-
-Goal "!i. (~free s i) = (? t. s = lift t i)";
-by (induct_tac "s" 1);
- by (Simp_tac 1);
- by (SELECT_GOAL(safe_tac HOL_cs)1);
- by (etac linorder_neqE 1);
- by (res_inst_tac [("x","Var nat")] exI 1);
- by (Asm_simp_tac 1);
- by (res_inst_tac [("x","Var(nat-1)")] exI 1);
- by (Asm_simp_tac 1);
- by (rtac notE 1);
- by (assume_tac 2);
- by (etac thin_rl 1);
- by (case_tac "t" 1);
- by (Asm_simp_tac 1);
- by (Asm_simp_tac 1);
- by (Asm_simp_tac 1);
- by (Asm_simp_tac 1);
- by (etac thin_rl 1);
- by (etac thin_rl 1);
- by (rtac allI 1);
- by (rtac iffI 1);
- by (REPEAT(eresolve_tac [conjE,exE] 1));
- by (rename_tac "u1 u2" 1);
- by (res_inst_tac [("x","u1$u2")] exI 1);
- by (Asm_simp_tac 1);
- by (etac exE 1);
- by (etac rev_mp 1);
- by (case_tac "t" 1);
- by (Asm_simp_tac 1);
- by (Asm_simp_tac 1);
- by (Blast_tac 1);
- by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
-by (etac thin_rl 1);
-by (rtac allI 1);
-by (rtac iffI 1);
- by (etac exE 1);
- by (res_inst_tac [("x","Abs t")] exI 1);
- by (Asm_simp_tac 1);
-by (etac exE 1);
-by (etac rev_mp 1);
-by (case_tac "t" 1);
- by (Asm_simp_tac 1);
- by (Asm_simp_tac 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "not_free_iff_lifted";
-
-Goal "(!s u. (~free s 0) --> R(Abs(s $ Var 0))(s[u/0])) = \
-\ (!s. R(Abs(lift s 0 $ Var 0))(s))";
-by (fast_tac (HOL_cs addss (simpset() addsimps [not_free_iff_lifted])) 1);
-qed "explicit_is_implicit";
--- a/src/HOL/Lambda/Eta.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy Sat Sep 02 21:56:24 2000 +0200
@@ -2,33 +2,250 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TU Muenchen
-
-Eta-reduction and relatives.
*)
-Eta = ParRed +
-consts free :: dB => nat => bool
- decr :: dB => dB
- eta :: "(dB * dB) set"
+header {* Eta-reduction *}
+
+theory Eta = ParRed:
+
+
+subsection {* Definition of eta-reduction and relatives *}
-syntax "-e>", "-e>>", "-e>=" , "->=" :: [dB,dB] => bool (infixl 50)
+consts
+ free :: "dB => nat => bool"
+primrec
+ "free (Var j) i = (j = i)"
+ "free (s $ t) i = (free s i \<or> free t i)"
+ "free (Abs s) i = free s (i + 1)"
+consts
+ eta :: "(dB \<times> dB) set"
+
+syntax
+ "_eta" :: "[dB, dB] => bool" (infixl "-e>" 50)
+ "_eta_rtrancl" :: "[dB, dB] => bool" (infixl "-e>>" 50)
+ "_eta_reflcl" :: "[dB, dB] => bool" (infixl "-e>=" 50)
translations
- "s -e> t" == "(s,t) : eta"
- "s -e>> t" == "(s,t) : eta^*"
- "s -e>= t" == "(s,t) : eta^="
- "s ->= t" == "(s,t) : beta^="
-
-primrec
- "free (Var j) i = (j=i)"
- "free (s $ t) i = (free s i | free t i)"
- "free (Abs s) i = free s (i+1)"
+ "s -e> t" == "(s,t) \<in> eta"
+ "s -e>> t" == "(s,t) \<in> eta^*"
+ "s -e>= t" == "(s,t) \<in> eta^="
inductive eta
-intrs
- eta "~free s 0 ==> Abs(s $ Var 0) -e> s[dummy/0]"
- appL "s -e> t ==> s$u -e> t$u"
- appR "s -e> t ==> u$s -e> u$t"
- abs "s -e> t ==> Abs s -e> Abs t"
-end
+ intros [simp, intro]
+ eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
+ appL: "s -e> t ==> s $ u -e> t $ u"
+ appR: "s -e> t ==> u $ s -e> u $ t"
+ abs: "s -e> t ==> Abs s -e> Abs t"
+
+inductive_cases eta_cases [elim!]:
+ "Abs s -e> z"
+ "s $ t -e> u"
+ "Var i -e> t"
+
+
+subsection "Properties of eta, subst and free"
+
+lemma subst_not_free [rulify, simp]:
+ "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
+ apply (induct_tac s)
+ apply (simp_all add: subst_Var)
+ done
+
+lemma free_lift [simp]:
+ "\<forall>i k. free (lift t k) i =
+ (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
+ apply (induct_tac t)
+ apply (auto cong: conj_cong)
+ apply arith
+ done
+
+lemma free_subst [simp]:
+ "\<forall>i k t. free (s[t/k]) i =
+ (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
+ apply (induct_tac s)
+ prefer 2
+ apply simp
+ apply blast
+ prefer 2
+ apply simp
+ apply (simp add: diff_Suc subst_Var split: nat.split)
+ apply clarify
+ apply (erule linorder_neqE)
+ apply simp_all
+ done
+
+lemma free_eta [rulify]:
+ "s -e> t ==> \<forall>i. free t i = free s i"
+ apply (erule eta.induct)
+ apply (simp_all cong: conj_cong)
+ done
+
+lemma not_free_eta:
+ "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
+ apply (simp add: free_eta)
+ done
+
+lemma eta_subst [rulify, simp]:
+ "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
+ apply (erule eta.induct)
+ apply (simp_all add: subst_subst [symmetric])
+ done
+
+
+subsection "Confluence of eta"
+
+lemma square_eta: "square eta eta (eta^=) (eta^=)"
+ apply (unfold square_def id_def)
+ apply (rule impI [THEN allI [THEN allI]])
+ apply simp
+ apply (erule eta.induct)
+ apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
+ apply safe
+ prefer 5
+ apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
+ apply blast+
+ done
+
+theorem eta_confluent: "confluent eta"
+ apply (rule square_eta [THEN square_reflcl_confluent])
+ done
+
+
+subsection "Congruence rules for eta*"
+
+lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
+ apply (erule rtrancl_induct)
+ apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
+ done
+
+lemma rtrancl_eta_AppL: "s -e>> s' ==> s $ t -e>> s' $ t"
+ apply (erule rtrancl_induct)
+ apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
+ done
+
+lemma rtrancl_eta_AppR: "t -e>> t' ==> s $ t -e>> s $ t'"
+ apply (erule rtrancl_induct)
+ apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
+ done
+
+lemma rtrancl_eta_App:
+ "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"
+ apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
+ done
+
+
+subsection "Commutation of beta and eta"
+lemma free_beta [rulify]:
+ "s -> t ==> \<forall>i. free t i --> free s i"
+ apply (erule beta.induct)
+ apply simp_all
+ done
+
+lemma beta_subst [rulify, intro]:
+ "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
+ apply (erule beta.induct)
+ apply (simp_all add: subst_subst [symmetric])
+ done
+
+lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]"
+ apply (induct_tac t)
+ apply (auto elim!: linorder_neqE simp: subst_Var)
+ done
+
+lemma eta_lift [rulify, simp]:
+ "s -e> t ==> \<forall>i. lift s i -e> lift t i"
+ apply (erule eta.induct)
+ apply simp_all
+ done
+
+lemma rtrancl_eta_subst [rulify]:
+ "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
+ apply (induct_tac u)
+ apply (simp_all add: subst_Var)
+ apply (blast intro: r_into_rtrancl)
+ apply (blast intro: rtrancl_eta_App)
+ apply (blast intro!: rtrancl_eta_Abs eta_lift)
+ done
+
+lemma square_beta_eta: "square beta eta (eta^*) (beta^=)"
+ apply (unfold square_def)
+ apply (rule impI [THEN allI [THEN allI]])
+ apply (erule beta.induct)
+ apply (slowsimp intro: r_into_rtrancl rtrancl_eta_subst eta_subst)
+ apply (blast intro: r_into_rtrancl rtrancl_eta_AppL)
+ apply (blast intro: r_into_rtrancl rtrancl_eta_AppR)
+ apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta
+ other: dB.distinct [iff del, simp]) (*23 seconds?*)
+ done
+
+lemma confluent_beta_eta: "confluent (beta \<union> eta)"
+ apply (assumption |
+ rule square_rtrancl_reflcl_commute confluent_Un
+ beta_confluent eta_confluent square_beta_eta)+
+ done
+
+
+subsection "Implicit definition of eta"
+
+text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
+
+lemma not_free_iff_lifted [rulify]:
+ "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
+ apply (induct_tac s)
+ apply simp
+ apply clarify
+ apply (rule iffI)
+ apply (erule linorder_neqE)
+ apply (rule_tac x = "Var nat" in exI)
+ apply simp
+ apply (rule_tac x = "Var (nat - 1)" in exI)
+ apply simp
+ apply clarify
+ apply (rule notE)
+ prefer 2
+ apply assumption
+ apply (erule thin_rl)
+ apply (case_tac t)
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ apply (erule thin_rl)
+ apply (erule thin_rl)
+ apply (rule allI)
+ apply (rule iffI)
+ apply (elim conjE exE)
+ apply (rename_tac u1 u2)
+ apply (rule_tac x = "u1 $ u2" in exI)
+ apply simp
+ apply (erule exE)
+ apply (erule rev_mp)
+ apply (case_tac t)
+ apply simp
+ apply simp
+ apply blast
+ apply simp
+ apply simp
+ apply (erule thin_rl)
+ apply (rule allI)
+ apply (rule iffI)
+ apply (erule exE)
+ apply (rule_tac x = "Abs t" in exI)
+ apply simp
+ apply (erule exE)
+ apply (erule rev_mp)
+ apply (case_tac t)
+ apply simp
+ apply simp
+ apply simp
+ apply blast
+ done
+
+theorem explicit_is_implicit:
+ "(\<forall>s u. (\<not> free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) =
+ (\<forall>s. R (Abs (lift s 0 $ Var 0)) s)"
+ apply (auto simp add: not_free_iff_lifted)
+ done
+
+end
\ No newline at end of file
--- a/src/HOL/Lambda/InductTermi.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy Sat Sep 02 21:56:24 2000 +0200
@@ -3,14 +3,17 @@
Author: Tobias Nipkow
Copyright 1998 TU Muenchen
-Inductive characterization of terminating lambda terms.
-Goes back to
-Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
-Also rediscovered by Matthes and Joachimski.
+Inductive characterization of terminating lambda terms. Goes back to
+Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995. Also
+rediscovered by Matthes and Joachimski.
*)
+header {* Inductive characterization of terminating lambda terms *}
+
theory InductTermi = ListBeta:
+subsection {* Terminating lambda terms *}
+
consts
IT :: "dB set"
@@ -18,10 +21,10 @@
intros
Var: "rs : lists IT ==> Var n $$ rs : IT"
Lambda: "r : IT ==> Abs r : IT"
- Beta: "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
+ Beta: "[| (r[s/0]) $$ ss : IT; s : IT |] ==> (Abs r $ s) $$ ss : IT"
-text {* Every term in IT terminates. *}
+subsection {* Every term in IT terminates *}
lemma double_induction_lemma [rulify]:
"s : termi beta ==> \<forall>t. t : termi beta -->
@@ -58,7 +61,7 @@
done
-text {* Every terminating term is in IT *}
+subsection {* Every terminating term is in IT *}
declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
@@ -67,7 +70,7 @@
done
lemma [simp]:
- "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' \<and> s=s' \<and> ss=ss')"
+ "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \<and> s = s' \<and> ss = ss')"
apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
done
@@ -76,7 +79,6 @@
"Abs t : IT"
"Abs r $ s $$ ts : IT"
-
theorem termi_implies_IT: "r : termi beta ==> r : IT"
apply (erule acc_induct)
apply (rename_tac r)
@@ -112,4 +114,4 @@
apply force
done
-end
+end
\ No newline at end of file
--- a/src/HOL/Lambda/Lambda.ML Sat Sep 02 21:53:03 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,146 +0,0 @@
-(* Title: HOL/Lambda/Lambda.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1995 TU Muenchen
-
-Substitution-lemmas.
-*)
-
-(*** Lambda ***)
-
-val beta_cases = map beta.mk_cases ["Var i -> t", "Abs r -> s", "s $ t -> u"];
-AddSEs beta_cases;
-
-Delsimps [subst_Var];
-Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
-
-(* don't add r_into_rtrancl! *)
-AddSIs beta.intrs;
-
-(*** Congruence rules for ->> ***)
-
-Goal "s ->> s' ==> Abs s ->> Abs s'";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
-qed "rtrancl_beta_Abs";
-AddSIs [rtrancl_beta_Abs];
-
-Goal "s ->> s' ==> s $ t ->> s' $ t";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
-qed "rtrancl_beta_AppL";
-
-Goal "t ->> t' ==> s $ t ->> s $ t'";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
-qed "rtrancl_beta_AppR";
-
-Goal "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'";
-by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
- addIs [rtrancl_trans]) 1);
-qed "rtrancl_beta_App";
-AddIs [rtrancl_beta_App];
-
-(*** subst and lift ***)
-
-fun addsplit ss = ss addsimps [subst_Var]
- delsplits [split_if]
- setloop (split_inside_tac [split_if]);
-
-Goal "(Var k)[u/k] = u";
-by (asm_full_simp_tac(addsplit(simpset())) 1);
-qed "subst_eq";
-
-Goal "i<j ==> (Var j)[u/i] = Var(j-1)";
-by (asm_full_simp_tac(addsplit(simpset())) 1);
-qed "subst_gt";
-
-Goal "j<i ==> (Var j)[u/i] = Var(j)";
-by (asm_full_simp_tac (addsplit(simpset()) addsimps [less_not_refl3]) 1);
-qed "subst_lt";
-
-Addsimps [subst_eq,subst_gt,subst_lt];
-
-Goal
- "!i k. i < k+1 --> lift (lift t i) (Suc k) = lift (lift t k) i";
-by (induct_tac "t" 1);
-by (Auto_tac);
-qed_spec_mp "lift_lift";
-
-Goal "!i j s. j < i+1 --> lift (t[s/j]) i = (lift t (i+1)) [lift s i / j]";
-by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
- addsplits [nat.split])));
-by (Auto_tac);
-qed "lift_subst";
-Addsimps [lift_subst];
-
-Goal
- "!i j s. i < j+1 --> lift (t[s/j]) i = (lift t i) [lift s i / j+1]";
-by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift])));
-qed "lift_subst_lt";
-
-Goal "!k s. (lift t k)[s/k] = t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "subst_lift";
-Addsimps [subst_lift];
-
-
-Goal "!i j u v. i < j+1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
-by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac
- (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
- addsplits [nat.split])));
-by (safe_tac (HOL_cs addSEs [nat_neqE]));
-by (ALLGOALS Simp_tac);
-qed_spec_mp "subst_subst";
-
-
-(*** Equivalence proof for optimized substitution ***)
-
-Goal "!k. liftn 0 t k = t";
-by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
-qed "liftn_0";
-Addsimps [liftn_0];
-
-Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k";
-by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
-qed "liftn_lift";
-Addsimps [liftn_lift];
-
-Goal "!n. substn t s n = t[liftn n s 0 / n]";
-by (induct_tac "t" 1);
-by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
-qed "substn_subst_n";
-Addsimps [substn_subst_n];
-
-Goal "substn t s 0 = t[s/0]";
-by (Simp_tac 1);
-qed "substn_subst_0";
-
-(*** Preservation thms ***)
-(* Not used in CR-proof but in SN-proof *)
-
-Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
-by (etac beta.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
-qed_spec_mp "subst_preserves_beta";
-Addsimps [subst_preserves_beta];
-
-Goal "r -> s ==> !i. lift r i -> lift s i";
-by (etac beta.induct 1);
-by (Auto_tac);
-qed_spec_mp "lift_preserves_beta";
-Addsimps [lift_preserves_beta];
-
-Goal "!r s i. r -> s --> t[r/i] ->> t[s/i]";
-by (induct_tac "t" 1);
-by (asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
-by (asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
-by (asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
-qed_spec_mp "subst_preserves_beta2";
-Addsimps [subst_preserves_beta2];
--- a/src/HOL/Lambda/Lambda.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/Lambda.thy Sat Sep 02 21:56:24 2000 +0200
@@ -2,56 +2,205 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TU Muenchen
-
-Lambda-terms in de Bruijn notation,
-substitution and beta-reduction.
*)
-Lambda = Main +
+header {* Basic definitions of Lambda-calculus *}
+
+theory Lambda = Main:
+
-datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
+subsection {* Lambda-terms in de Bruijn notation and substitution *}
+
+datatype dB =
+ Var nat
+ | App dB dB (infixl "$" 200)
+ | Abs dB
consts
- subst :: [dB,dB,nat]=>dB ("_[_'/_]" [300,0,0] 300)
- lift :: [dB,nat] => dB
- (* optimized versions *)
- substn :: [dB,dB,nat] => dB
- liftn :: [nat,dB,nat] => dB
+ subst :: "[dB, dB, nat] => dB" ("_[_'/_]" [300, 0, 0] 300)
+ lift :: "[dB, nat] => dB"
primrec
- "lift (Var i) k = (if i < k then Var i else Var(i+1))"
- "lift (s $ t) k = (lift s k) $ (lift t k)"
- "lift (Abs s) k = Abs(lift s (k+1))"
+ "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
+ "lift (s $ t) k = lift s k $ lift t k"
+ "lift (Abs s) k = Abs (lift s (k + 1))"
+
+primrec (* FIXME base names *)
+ subst_Var: "(Var i)[s/k] =
+ (if k < i then Var (i - 1) else if i = k then s else Var i)"
+ subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]"
+ subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
+
+declare subst_Var [simp del]
+
+text {* Optimized versions of @{term subst} and @{term lift}. *}
+
+consts
+ substn :: "[dB, dB, nat] => dB"
+ liftn :: "[nat, dB, nat] => dB"
+
+primrec
+ "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
+ "liftn n (s $ t) k = liftn n s k $ liftn n t k"
+ "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
primrec
- subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
- else if i = k then s else Var i)"
- subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
- subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
+ "substn (Var i) s k =
+ (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
+ "substn (t $ u) s k = substn t s k $ substn u s k"
+ "substn (Abs t) s k = Abs (substn t s (k + 1))"
-primrec
- "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
- "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
- "liftn n (Abs s) k = Abs(liftn n s (k+1))"
+
+subsection {* Beta-reduction *}
-primrec
- "substn (Var i) s k = (if k < i then Var(i-1)
- else if i = k then liftn k s 0 else Var i)"
- "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
- "substn (Abs t) s k = Abs (substn t s (k+1))"
+consts
+ beta :: "(dB \<times> dB) set"
-consts beta :: "(dB * dB) set"
-
-syntax "->", "->>" :: [dB,dB] => bool (infixl 50)
-
+syntax
+ "_beta" :: "[dB, dB] => bool" (infixl "->" 50)
+ "_beta_rtrancl" :: "[dB, dB] => bool" (infixl "->>" 50)
translations
- "s -> t" == "(s,t) : beta"
- "s ->> t" == "(s,t) : beta^*"
+ "s -> t" == "(s,t) \<in> beta"
+ "s ->> t" == "(s,t) \<in> beta^*"
inductive beta
-intrs
- beta "(Abs s) $ t -> s[t/0]"
- appL "s -> t ==> s$u -> t$u"
- appR "s -> t ==> u$s -> u$t"
- abs "s -> t ==> Abs s -> Abs t"
-end
+ intros [simp, intro!]
+ beta: "Abs s $ t -> s[t/0]"
+ appL: "s -> t ==> s $ u -> t $ u"
+ appR: "s -> t ==> u $ s -> u $ t"
+ abs: "s -> t ==> Abs s -> Abs t"
+
+inductive_cases beta_cases [elim!]:
+ "Var i -> t"
+ "Abs r -> s"
+ "s $ t -> u"
+
+declare if_not_P [simp] not_less_eq [simp]
+ -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
+
+
+subsection {* Congruence rules *}
+
+lemma rtrancl_beta_Abs [intro!]:
+ "s ->> s' ==> Abs s ->> Abs s'"
+ apply (erule rtrancl_induct)
+ apply (blast intro: rtrancl_into_rtrancl)+
+ done
+
+lemma rtrancl_beta_AppL:
+ "s ->> s' ==> s $ t ->> s' $ t"
+ apply (erule rtrancl_induct)
+ apply (blast intro: rtrancl_into_rtrancl)+
+ done
+
+lemma rtrancl_beta_AppR:
+ "t ->> t' ==> s $ t ->> s $ t'"
+ apply (erule rtrancl_induct)
+ apply (blast intro: rtrancl_into_rtrancl)+
+ done
+
+lemma rtrancl_beta_App [intro]:
+ "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'"
+ apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
+ intro: rtrancl_trans)
+ done
+
+
+subsection {* Substitution-lemmas *}
+
+lemma subst_eq [simp]: "(Var k)[u/k] = u"
+ apply (simp add: subst_Var)
+ done
+
+lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
+ apply (simp add: subst_Var)
+ done
+
+lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
+ apply (simp add: subst_Var)
+ done
+
+lemma lift_lift [rulify]:
+ "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
+ apply (induct_tac t)
+ apply auto
+ done
+
+lemma lift_subst [simp]:
+ "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
+ apply (induct_tac t)
+ apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
+ done
+
+lemma lift_subst_lt:
+ "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
+ apply (induct_tac t)
+ apply (simp_all add: subst_Var lift_lift)
+ done
+
+lemma subst_lift [simp]:
+ "\<forall>k s. (lift t k)[s/k] = t"
+ apply (induct_tac t)
+ apply simp_all
+ done
+
+lemma subst_subst [rulify]:
+ "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
+ apply (induct_tac t)
+ apply (simp_all
+ add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
+ split: nat.split)
+ apply (auto elim: nat_neqE)
+ done
+
+
+subsection {* Equivalence proof for optimized substitution *}
+
+lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
+ apply (induct_tac t)
+ apply (simp_all add: subst_Var)
+ done
+
+lemma liftn_lift [simp]:
+ "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
+ apply (induct_tac t)
+ apply (simp_all add: subst_Var)
+ done
+
+lemma substn_subst_n [simp]:
+ "\<forall>n. substn t s n = t[liftn n s 0 / n]"
+ apply (induct_tac t)
+ apply (simp_all add: subst_Var)
+ done
+
+theorem substn_subst_0: "substn t s 0 = t[s/0]"
+ apply simp
+ done
+
+
+subsection {* Preservation theorems *}
+
+text {* Not used in Church-Rosser proof, but in Strong
+ Normalization. \medskip *}
+
+theorem subst_preserves_beta [rulify, simp]:
+ "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
+ apply (erule beta.induct)
+ apply (simp_all add: subst_subst [symmetric])
+ done
+
+theorem lift_preserves_beta [rulify, simp]:
+ "r -> s ==> \<forall>i. lift r i -> lift s i"
+ apply (erule beta.induct)
+ apply auto
+ done
+
+theorem subst_preserves_beta2 [rulify, simp]:
+ "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
+ apply (induct_tac t)
+ apply (simp add: subst_Var r_into_rtrancl)
+ apply (simp add: rtrancl_beta_App)
+ apply (simp add: rtrancl_beta_Abs)
+ done
+
+end
\ No newline at end of file
--- a/src/HOL/Lambda/ListApplication.ML Sat Sep 02 21:53:03 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,135 +0,0 @@
-(* Title: HOL/Lambda/ListApplication.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1998 TU Muenchen
-*)
-
-Goal "(r$$ts = s$$ts) = (r = s)";
-by (rev_induct_tac "ts" 1);
-by (Auto_tac);
-qed "apps_eq_tail_conv";
-AddIffs [apps_eq_tail_conv];
-
-Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
-by (induct_tac "ss" 1);
-by (Auto_tac);
-qed_spec_mp "Var_eq_apps_conv";
-AddIffs [Var_eq_apps_conv];
-
-Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
-by (rev_induct_tac "rs" 1);
- by (Simp_tac 1);
- by (Blast_tac 1);
-by (rtac allI 1);
-by (rev_induct_tac "ss" 1);
-by (Auto_tac);
-qed_spec_mp "Var_apps_eq_Var_apps_conv";
-AddIffs [Var_apps_eq_Var_apps_conv];
-
-Goal "(r$s = t$$ts) = \
-\ (if ts = [] then r$s = t \
-\ else (? ss. ts = ss@[s] & r = t$$ss))";
-by (res_inst_tac [("xs","ts")] rev_exhaust 1);
-by (Auto_tac);
-qed "App_eq_foldl_conv";
-
-Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
-by (rev_induct_tac "ss" 1);
-by (Auto_tac);
-qed "Abs_eq_apps_conv";
-AddIffs [Abs_eq_apps_conv];
-
-Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
-by (rev_induct_tac "ss" 1);
-by (Auto_tac);
-qed "apps_eq_Abs_conv";
-AddIffs [apps_eq_Abs_conv];
-
-Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
-by (rev_induct_tac "rs" 1);
- by (Simp_tac 1);
- by (Blast_tac 1);
-by (rtac allI 1);
-by (rev_induct_tac "ss" 1);
-by (Auto_tac);
-qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
-AddIffs [Abs_apps_eq_Abs_apps_conv];
-
-Goal "!s t. Abs s $ t ~= (Var n)$$ss";
-by (rev_induct_tac "ss" 1);
-by (Auto_tac);
-qed_spec_mp "Abs_App_neq_Var_apps";
-AddIffs [Abs_App_neq_Var_apps];
-
-Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
-by (rev_induct_tac "ss" 1);
- by (Simp_tac 1);
-by (rtac allI 1);
-by (rev_induct_tac "ts" 1);
-by (Auto_tac);
-qed_spec_mp "Var_apps_neq_Abs_apps";
-AddIffs [Var_apps_neq_Abs_apps];
-
-Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
-by (induct_tac "t" 1);
- by (res_inst_tac[("x","[]")] exI 1);
- by (Simp_tac 1);
- by (Clarify_tac 1);
- by (rename_tac "ts1 ts2 h1 h2" 1);
- by (res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
- by (Simp_tac 1);
-by (Simp_tac 1);
-qed "ex_head_tail";
-
-Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
-by (rev_induct_tac "rs" 1);
-by (Auto_tac);
-qed "size_apps";
-Addsimps [size_apps];
-
-Goal "[| (0::nat) < k; m <= n |] ==> m < n+k";
-by (fast_arith_tac 1);
-val lemma0 = result();
-
-(* a customized induction schema for $$ *)
-
-val prems = Goal
-"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
-\ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
-\|] ==> !t. size t = n --> P t";
-by (induct_thm_tac less_induct "n" 1);
-by (rtac allI 1);
-by (cut_inst_tac [("t","t")] ex_head_tail 1);
-by (Clarify_tac 1);
-by (etac disjE 1);
- by (Clarify_tac 1);
- by (resolve_tac prems 1);
- by (Clarify_tac 1);
- by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
- by (Simp_tac 1);
- by (rtac lemma0 1);
- by (Force_tac 1);
- by (rtac elem_le_sum 1);
- by (Force_tac 1);
-by (Clarify_tac 1);
-by (resolve_tac prems 1);
-by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
-by (Simp_tac 1);
-by (Clarify_tac 1);
-by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
-by (Simp_tac 1);
-by (rtac le_imp_less_Suc 1);
-by (rtac trans_le_add1 1);
-by (rtac trans_le_add2 1);
-by (rtac elem_le_sum 1);
-by (Force_tac 1);
-val lemma = result() RS spec RS mp;
-
-val prems = Goal
-"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
-\ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
-\|] ==> P t";
-by (res_inst_tac [("x1","t")] lemma 1);
-by (rtac refl 3);
-by (REPEAT(ares_tac prems 1));
-qed "Apps_dB_induct";
--- a/src/HOL/Lambda/ListApplication.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Sat Sep 02 21:56:24 2000 +0200
@@ -2,9 +2,9 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1998 TU Muenchen
+*)
-Application of a term to a list of terms
-*)
+header {* Application of a term to a list of terms *}
theory ListApplication = Lambda:
@@ -13,7 +13,6 @@
translations
"t $$ ts" == "foldl (op $) t ts"
-
lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
apply (induct_tac ts rule: rev_induct)
apply auto
@@ -101,11 +100,12 @@
apply simp
done
-text {* A customized induction schema for @{text "$$"} *}
+
+text {* \medskip A customized induction schema for @{text "$$"}. *}
lemma lem [rulify]:
"[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
- !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+ !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
|] ==> \<forall>t. size t = n --> P t"
proof -
case antecedent
@@ -145,9 +145,9 @@
done
qed
-lemma Apps_dB_induct:
+theorem Apps_dB_induct:
"[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
- !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+ !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
|] ==> P t"
proof -
case antecedent
@@ -159,4 +159,4 @@
done
qed
-end
+end
\ No newline at end of file
--- a/src/HOL/Lambda/ListBeta.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Sat Sep 02 21:56:24 2000 +0200
@@ -2,12 +2,16 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1998 TU Muenchen
-
-Lifting beta-reduction to lists of terms, reducing exactly one element
*)
+header {* Lifting beta-reduction to lists *}
+
theory ListBeta = ListApplication + ListOrder:
+text {*
+ Lifting beta-reduction to lists of terms, reducing exactly one element.
+*}
+
syntax
"_list_beta" :: "dB => dB => bool" (infixl "=>" 50)
translations
@@ -27,7 +31,6 @@
apply (auto 0 3 intro: disjI2 [THEN append_step1I])
done
-
lemma head_Var_reduction:
"Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
apply (drule head_Var_reduction_aux)
@@ -44,33 +47,33 @@
apply (case_tac r)
apply simp
apply (simp add: App_eq_foldl_conv)
- apply (simp only: split: split_if_asm)
+ apply (split (asm) split_if_asm)
apply simp
apply blast
apply simp
apply (simp add: App_eq_foldl_conv)
- apply (simp only: split: split_if_asm)
+ apply (split (asm) split_if_asm)
apply simp
apply simp
apply (clarify del: disjCI)
apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (simp only: split: split_if_asm)
+ apply (split (asm) split_if_asm)
apply simp
apply blast
apply (force intro: disjI1 [THEN append_step1I])
apply (clarify del: disjCI)
apply (drule App_eq_foldl_conv [THEN iffD1])
- apply (simp only: split: split_if_asm)
+ apply (split (asm) split_if_asm)
apply simp
apply blast
apply (auto 0 3 intro: disjI2 [THEN append_step1I])
done
lemma apps_betasE [elim!]:
-"[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
- !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
- !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
- ==> R"
+ "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
+ !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
+ !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
+ ==> R"
proof -
assume major: "r $$ rs -> s"
case antecedent
@@ -94,7 +97,7 @@
done
lemma apps_preserves_betas [rulify, simp]:
- "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
+ "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
apply (induct_tac rs rule: rev_induct)
apply simp
apply simp
@@ -106,4 +109,4 @@
apply blast
done
-end
+end
\ No newline at end of file
--- a/src/HOL/Lambda/ListOrder.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Sat Sep 02 21:56:24 2000 +0200
@@ -2,16 +2,22 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1998 TU Muenchen
-
-Lifting an order to lists of elements, relating exactly one element
*)
+header {* Lifting an order to lists of elements *}
+
theory ListOrder = Acc:
+text {*
+ Lifting an order to lists of elements, relating exactly one
+ element.
+*}
+
constdefs
step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
"step1 r ==
- {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = us @ z' # vs}"
+ {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
+ us @ z' # vs}"
lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
@@ -34,7 +40,8 @@
done
lemma Cons_step1_Cons [iff]:
- "((y # ys, x # xs) \<in> step1 r) = ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
+ "((y # ys, x # xs) \<in> step1 r) =
+ ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
apply (unfold step1_def)
apply simp
apply (rule iffI)
@@ -59,8 +66,8 @@
lemma Cons_step1E [rulify_prems, elim!]:
"[| (ys, x # xs) \<in> step1 r;
- \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
- \<forall>zs. ys = x # zs --> (zs, xs) : step1 r --> R
+ \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
+ \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
|] ==> R"
apply (case_tac ys)
apply (simp add: step1_def)
@@ -98,7 +105,8 @@
apply (fast dest: acc_downward)
done
-lemma ex_step1I: "[| x \<in> set xs; (y, x) \<in> r |]
+lemma ex_step1I:
+ "[| x \<in> set xs; (y, x) \<in> r |]
==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
apply (unfold step1_def)
apply (drule in_set_conv_decomp [THEN iffD1])
@@ -113,4 +121,4 @@
apply blast
done
-end
+end
\ No newline at end of file
--- a/src/HOL/Lambda/ParRed.ML Sat Sep 02 21:53:03 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-(* Title: HOL/Lambda/ParRed.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1995 TU Muenchen
-
-Properties of => and cd, in particular the diamond property of => and
-confluence of beta.
-*)
-
-Addsimps par_beta.intrs;
-
-val par_beta_cases =
- map par_beta.mk_cases
- ["Var n => t",
- "Abs s => Abs t",
- "(Abs s) $ t => u",
- "s $ t => u",
- "Abs s => t"];
-
-AddSIs par_beta.intrs;
-AddSEs par_beta_cases;
-
-(*** beta <= par_beta <= beta^* ***)
-
-Goal "(Var n => t) = (t = Var n)";
-by (Blast_tac 1);
-qed "par_beta_varL";
-Addsimps [par_beta_varL];
-
-Goal "t => t";
-by (induct_tac "t" 1);
-by (ALLGOALS Asm_simp_tac);
-qed"par_beta_refl";
-Addsimps [par_beta_refl];
-(* AddSIs [par_beta_refl]; causes search to blow up *)
-
-Goal "beta <= par_beta";
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (etac beta.induct 1);
-by (ALLGOALS(blast_tac (claset() addSIs [par_beta_refl])));
-qed "beta_subset_par_beta";
-
-Goal "par_beta <= beta^*";
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (etac par_beta.induct 1);
-by (Blast_tac 1);
-(* rtrancl_refl complicates the proof by increasing the branching factor*)
-by (ALLGOALS (blast_tac (claset() delrules [rtrancl_refl]
- addIs [rtrancl_into_rtrancl])));
-qed "par_beta_subset_beta";
-
-(*** => ***)
-
-Goal "!t' n. t => t' --> lift t n => lift t' n";
-by (induct_tac "t" 1);
-by (ALLGOALS(fast_tac (claset() addss (simpset()))));
-qed_spec_mp "par_beta_lift";
-Addsimps [par_beta_lift];
-
-Goal
- "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
-by (induct_tac "t" 1);
- by (asm_simp_tac (addsplit(simpset())) 1);
- by (strip_tac 1);
- by (eresolve_tac par_beta_cases 1);
- by (Asm_simp_tac 1);
- by (asm_simp_tac (simpset() addsimps [subst_subst RS sym]) 1);
- by (fast_tac (claset() addSIs [par_beta_lift] addss (simpset())) 1);
-by (fast_tac (claset() addss (simpset())) 1);
-qed_spec_mp "par_beta_subst";
-
-(*** Confluence (directly) ***)
-
-Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by (rtac (impI RS allI RS allI) 1);
-by (etac par_beta.induct 1);
-by (ALLGOALS(blast_tac (claset() addSIs [par_beta_subst])));
-qed "diamond_par_beta";
-
-
-(*** cd ***)
-
-Goal "!t. s => t --> t => cd s";
-by (induct_thm_tac cd.induct "s" 1);
-by (Auto_tac);
-by (fast_tac (claset() addSIs [par_beta_subst]) 1);
-qed_spec_mp "par_beta_cd";
-
-(*** Confluence (via cd) ***)
-
-Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)";
-by (blast_tac (claset() addIs [par_beta_cd]) 1);
-qed "diamond_par_beta2";
-
-Goal "confluent(beta)";
-by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
- par_beta_subset_beta, beta_subset_par_beta]) 1);
-qed"beta_confluent";
--- a/src/HOL/Lambda/ParRed.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/ParRed.thy Sat Sep 02 21:56:24 2000 +0200
@@ -3,32 +3,131 @@
Author: Tobias Nipkow
Copyright 1995 TU Muenchen
-Parallel reduction and a complete developments function "cd".
+Properties of => and "cd", in particular the diamond property of => and
+confluence of beta.
*)
-ParRed = Lambda + Commutation +
+header {* Parallel reduction and a complete developments *}
-consts par_beta :: "(dB * dB) set"
+theory ParRed = Lambda + Commutation:
+
+
+subsection {* Parallel reduction *}
-syntax "=>" :: [dB,dB] => bool (infixl 50)
+consts
+ par_beta :: "(dB \<times> dB) set"
+syntax
+ par_beta :: "[dB, dB] => bool" (infixl "=>" 50)
translations
- "s => t" == "(s,t) : par_beta"
+ "s => t" == "(s, t) \<in> par_beta"
inductive par_beta
- intrs
- var "Var n => Var n"
- abs "s => t ==> Abs s => Abs t"
- app "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
- beta "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
+ intros [simp, intro!]
+ var: "Var n => Var n"
+ abs: "s => t ==> Abs s => Abs t"
+ app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
+ beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
+
+inductive_cases par_beta_cases [elim!]:
+ "Var n => t"
+ "Abs s => Abs t"
+ "(Abs s) $ t => u"
+ "s $ t => u"
+ "Abs s => t"
+
+
+subsection {* Inclusions *}
+
+text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
+
+lemma par_beta_varL [simp]:
+ "(Var n => t) = (t = Var n)"
+ apply blast
+ done
+
+lemma par_beta_refl [simp]: "t => t" (* par_beta_refl [intro!] causes search to blow up *)
+ apply (induct_tac t)
+ apply simp_all
+ done
+
+lemma beta_subset_par_beta: "beta <= par_beta"
+ apply (rule subsetI)
+ apply clarify
+ apply (erule beta.induct)
+ apply (blast intro!: par_beta_refl)+
+ done
+
+lemma par_beta_subset_beta: "par_beta <= beta^*"
+ apply (rule subsetI)
+ apply clarify
+ apply (erule par_beta.induct)
+ apply blast
+ apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
+ -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
+ done
+
+
+subsection {* Misc properties of par-beta *}
+
+lemma par_beta_lift [rulify, simp]:
+ "\<forall>t' n. t => t' --> lift t n => lift t' n"
+ apply (induct_tac t)
+ apply fastsimp+
+ done
+
+lemma par_beta_subst [rulify]:
+ "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
+ apply (induct_tac t)
+ apply (simp add: subst_Var)
+ apply (intro strip)
+ apply (erule par_beta_cases)
+ apply simp
+ apply (simp add: subst_subst [symmetric])
+ apply (fastsimp intro!: par_beta_lift)
+ apply fastsimp
+ done
+
+
+subsection {* Confluence (directly) *}
+
+lemma diamond_par_beta: "diamond par_beta"
+ apply (unfold diamond_def commute_def square_def)
+ apply (rule impI [THEN allI [THEN allI]])
+ apply (erule par_beta.induct)
+ apply (blast intro!: par_beta_subst)+
+ done
+
+
+subsection {* Complete developments *}
consts
- cd :: dB => dB
+ "cd" :: "dB => dB"
+recdef "cd" "measure size"
+ "cd (Var n) = Var n"
+ "cd (Var n $ t) = Var n $ cd t"
+ "cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t"
+ "cd (Abs u $ t) = (cd u)[cd t/0]"
+ "cd (Abs s) = Abs (cd s)"
+
+lemma par_beta_cd [rulify]:
+ "\<forall>t. s => t --> t => cd s"
+ apply (induct_tac s rule: cd.induct)
+ apply auto
+ apply (fast intro!: par_beta_subst)
+ done
-recdef cd "measure size"
- "cd(Var n) = Var n"
- "cd(Var n $ t) = Var n $ cd t"
- "cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t"
- "cd(Abs u $ t) = (cd u)[cd t/0]"
- "cd(Abs s) = Abs(cd s)"
-end
+
+subsection {* Confluence (via complete developments) *}
+
+lemma diamond_par_beta2: "diamond par_beta"
+ apply (unfold diamond_def commute_def square_def)
+ apply (blast intro: par_beta_cd)
+ done
+
+theorem beta_confluent: "confluent beta"
+ apply (rule diamond_par_beta2 diamond_to_confluence
+ par_beta_subset_beta beta_subset_par_beta)+
+ done
+
+end
\ No newline at end of file
--- a/src/HOL/Lambda/Type.thy Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/Lambda/Type.thy Sat Sep 02 21:56:24 2000 +0200
@@ -2,34 +2,40 @@
ID: $Id$
Author: Stefan Berghofer
Copyright 2000 TU Muenchen
+*)
-Simply-typed lambda terms. Subject reduction and strong normalization
-of simply-typed lambda terms. Partly based on a paper proof by Ralph
-Matthes.
-*)
+header {* Simply-typed lambda terms: subject reduction and strong
+ normalization *}
theory Type = InductTermi:
+text_raw {*
+ \footnote{Formalization by Stefan Berghofer. Partly based on a
+ paper proof by Ralph Matthes.}
+*}
+
+
+subsection {* Types and typing rules *}
+
datatype type =
Atom nat
- | Fun type type (infixr "=>" 200)
+ | Fun type type (infixr "=>" 200)
consts
typing :: "((nat => type) \<times> dB \<times> type) set"
syntax
- "_typing" :: "[nat => type, dB, type] => bool" ("_ |- _ : _" [50,50,50] 50)
- "_funs" :: "[type list, type] => type" (infixl "=>>" 150)
-
+ "_typing" :: "[nat => type, dB, type] => bool" ("_ |- _ : _" [50,50,50] 50)
+ "_funs" :: "[type list, type] => type" (infixl "=>>" 150)
translations
- "env |- t : T" == "(env, t, T) : typing"
+ "env |- t : T" == "(env, t, T) \<in> typing"
"Ts =>> T" == "foldr Fun Ts T"
inductive typing
-intros [intro!]
- Var: "env x = T ==> env |- Var x : T"
- Abs: "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)"
- App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
+ intros [intro!]
+ Var: "env x = T ==> env |- Var x : T"
+ Abs: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
+ App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
inductive_cases [elim!]:
"e |- Var i : T"
@@ -46,12 +52,12 @@
| T # Ts => e |- t : T \<and> types e ts Ts)"
inductive_cases [elim!]:
- "x # xs : lists S"
+ "x # xs \<in> lists S"
declare IT.intros [intro!]
-text {* Some tests. *}
+subsection {* Some examples *}
lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \<and> U = T"
apply (intro exI conjI)
@@ -66,7 +72,7 @@
done
-text {* n-ary function types *}
+text {* Iterated function types *}
lemma list_app_typeD [rulify]:
"\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
@@ -85,7 +91,7 @@
done
lemma list_app_typeI [rulify]:
- "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
+ "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
apply (induct_tac ts)
apply (intro strip)
apply simp
@@ -104,7 +110,7 @@
done
lemma lists_types [rulify]:
- "\<forall>Ts. types e ts Ts --> ts : lists {t. \<exists>T. e |- t : T}"
+ "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
apply (induct_tac ts)
apply (intro strip)
apply (case_tac Ts)
@@ -121,7 +127,7 @@
done
-text {* lifting preserves termination and well-typedness *}
+subsection {* Lifting preserves termination and well-typedness *}
lemma lift_map [rulify, simp]:
"\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
@@ -136,7 +142,7 @@
done
lemma lift_IT [rulify, intro!]:
- "t : IT ==> \<forall>i. lift t i : IT"
+ "t \<in> IT ==> \<forall>i. lift t i \<in> IT"
apply (erule IT.induct)
apply (rule allI)
apply (simp (no_asm))
@@ -156,14 +162,14 @@
done
lemma lifts_IT [rulify]:
- "ts : lists IT --> map (\<lambda>t. lift t 0) ts : lists IT"
+ "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
apply (induct_tac ts)
apply auto
done
lemma shift_env [simp]:
- "nat_case T
+ "nat_case T
(\<lambda>j. if j < i then e j else if j = i then Ua else e (j - 1)) =
(\<lambda>j. if j < Suc i then nat_case T e j else if j = Suc i then Ua
else nat_case T e (j - 1))"
@@ -184,7 +190,7 @@
done
lemma lift_type [intro!]:
- "e |- t : T ==> nat_case U e |- lift t 0 : T"
+ "e |- t : T ==> nat_case U e |- lift t 0 : T"
apply (subgoal_tac
"nat_case U e =
(\<lambda>j. if j < 0 then e j
@@ -211,10 +217,10 @@
done
-text {* substitution lemma *}
+subsection {* Substitution lemmas *}
lemma subst_lemma [rulify]:
- "e |- t : T ==> \<forall>e' i U u.
+ "e |- t : T ==> \<forall>e' i U u.
e = (\<lambda>j. if j < i then e' j
else if j = i then U
else e' (j-1)) -->
@@ -257,7 +263,7 @@
done
-text {* subject reduction *}
+subsection {* Subject reduction *}
lemma subject_reduction [rulify]:
"e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
@@ -277,15 +283,16 @@
apply auto
done
-text {* additional lemmas *}
+
+subsection {* Additional lemmas *}
lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
apply simp
done
-lemma subst_Var_IT [rulify]: "r : IT ==> \<forall>i j. r[Var i/j] : IT"
+lemma subst_Var_IT [rulify]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
apply (erule IT.induct)
- txt {* @{term Var} *}
+ txt {* Case @{term Var}: *}
apply (intro strip)
apply (simp (no_asm) add: subst_Var)
apply
@@ -300,12 +307,12 @@
rule lists.Cons,
fast,
assumption)+
- txt {* @{term Lambda} *}
+ txt {* Case @{term Lambda}: *}
apply (intro strip)
apply simp
apply (rule IT.Lambda)
apply fast
- txt {* @{term Beta} *}
+ txt {* Case @{term Beta}: *}
apply (intro strip)
apply (simp (no_asm_use) add: subst_subst [symmetric])
apply (rule IT.Beta)
@@ -319,7 +326,7 @@
apply (rule lists.Nil)
done
-lemma app_Var_IT: "t : IT ==> t $ Var i : IT"
+lemma app_Var_IT: "t \<in> IT ==> t $ Var i \<in> IT"
apply (erule IT.induct)
apply (subst app_last)
apply (rule IT.Var)
@@ -338,22 +345,22 @@
done
-text {* Well-typed substitution preserves termination. *}
+subsection {* Well-typed substitution preserves termination *}
lemma subst_type_IT [rulify]:
- "\<forall>t. t : IT --> (\<forall>e T u i.
+ "\<forall>t. t \<in> IT --> (\<forall>e T u i.
(\<lambda>j. if j < i then e j
else if j = i then U
else e (j - 1)) |- t : T -->
- u : IT --> e |- u : U --> t[u/i] : IT)"
+ u \<in> IT --> e |- u : U --> t[u/i] \<in> IT)"
apply (rule_tac f = size and a = U in measure_induct)
apply (rule allI)
apply (rule impI)
apply (erule IT.induct)
- txt {* @{term Var} *}
+ txt {* Case @{term Var}: *}
apply (intro strip)
apply (case_tac "n = i")
- txt {* @{term "n = i"} *}
+ txt {* Case @{term "n = i"}: *}
apply (case_tac rs)
apply simp
apply simp
@@ -363,14 +370,14 @@
apply (ind_cases "e |- Var i : T")
apply (drule_tac s = "(?T::type) => ?U" in sym)
apply simp
- apply (subgoal_tac "lift u 0 $ Var 0 : IT")
+ apply (subgoal_tac "lift u 0 $ Var 0 \<in> IT")
prefer 2
apply (rule app_Var_IT)
apply (erule lift_IT)
- apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT")
+ apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] \<in> IT")
apply (simp (no_asm_use))
apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0)
- (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] : IT")
+ (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] \<in> IT")
apply (simp (no_asm_use) del: map_compose
add: map_compose [symmetric] o_def)
apply (erule_tac x = "Ts =>> T" in allE)
@@ -383,7 +390,7 @@
apply (rule lifts_IT)
apply (drule lists_types)
apply
- (ind_cases "x # xs : lists (Collect P)",
+ (ind_cases "x # xs \<in> lists (Collect P)",
erule lists_IntI [THEN lists.induct],
assumption)
apply fastsimp
@@ -409,21 +416,21 @@
apply (rule typing.Var)
apply simp
apply (fast intro!: subst_lemma)
- txt {* @{term "n ~= i"} *}
+ txt {* Case @{term "n ~= i"}: *}
apply (drule list_app_typeD)
apply (erule exE)
apply (erule conjE)
apply (drule lists_types)
- apply (subgoal_tac "map (\<lambda>x. x[u/i]) rs : lists IT")
+ apply (subgoal_tac "map (\<lambda>x. x[u/i]) rs \<in> lists IT")
apply (simp add: subst_Var)
apply fast
apply (erule lists_IntI [THEN lists.induct])
apply assumption
apply fastsimp
apply fastsimp
- txt {* @{term Lambda} *}
+ txt {* Case @{term Lambda}: *}
apply fastsimp
- txt {* @{term Beta} *}
+ txt {* Case @{term Beta}: *}
apply (intro strip)
apply (simp (no_asm))
apply (rule IT.Beta)
@@ -437,13 +444,13 @@
done
-text {* main theorem: well-typed terms are strongly normalizing *}
+subsection {* Main theorem: well-typed terms are strongly normalizing *}
-lemma type_implies_IT: "e |- t : T ==> t : IT"
+lemma type_implies_IT: "e |- t : T ==> t \<in> IT"
apply (erule typing.induct)
apply (rule Var_IT)
apply (erule IT.Lambda)
- apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT")
+ apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] \<in> IT")
apply simp
apply (rule subst_type_IT)
apply (rule lists.Nil
@@ -458,9 +465,9 @@
apply assumption
done
-theorem type_implies_termi: "e |- t : T ==> t : termi beta"
+theorem type_implies_termi: "e |- t : T ==> t \<in> termi beta"
apply (rule IT_implies_termi)
apply (erule type_implies_IT)
done
-end
+end
\ No newline at end of file
--- a/src/HOL/README.html Sat Sep 02 21:53:03 2000 +0200
+++ b/src/HOL/README.html Sat Sep 02 21:56:24 2000 +0200
@@ -54,7 +54,7 @@
<DD>several introductory Isabelle/Isar examples
<DT>Lambda
-<DD>a proof of the Church-Rosser theorem for lambda-calculus
+<DD>fundamental properties of lambda-calculus (Church-Rosser and termination)
<DT>Lex
<DD>verification of a simple lexical analyzer generator