HOL/Lambda: converted into new-style theory and document;
authorwenzelm
Sat Sep 02 21:56:24 2000 +0200 (2000-09-02)
changeset 981139ffdb8cab03
parent 9810 7e785df2b76a
child 9812 87ba969d069c
HOL/Lambda: converted into new-style theory and document;
src/HOL/IsaMakefile
src/HOL/Lambda/Commutation.ML
src/HOL/Lambda/Commutation.thy
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Eta.thy
src/HOL/Lambda/InductTermi.thy
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/Lambda.thy
src/HOL/Lambda/ListApplication.ML
src/HOL/Lambda/ListApplication.thy
src/HOL/Lambda/ListBeta.thy
src/HOL/Lambda/ListOrder.thy
src/HOL/Lambda/ParRed.ML
src/HOL/Lambda/ParRed.thy
src/HOL/Lambda/Type.thy
src/HOL/README.html
     1.1 --- a/src/HOL/IsaMakefile	Sat Sep 02 21:53:03 2000 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Sat Sep 02 21:56:24 2000 +0200
     1.3 @@ -303,11 +303,10 @@
     1.4  
     1.5  HOL-Lambda: HOL $(LOG)/HOL-Lambda.gz
     1.6  
     1.7 -$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Lambda/Commutation.ML \
     1.8 -  Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy \
     1.9 -  Lambda/InductTermi.thy Lambda/Lambda.ML Lambda/Lambda.thy \
    1.10 +$(LOG)/HOL-Lambda.gz: $(OUT)/HOL Induct/Acc.thy Lambda/Commutation.thy \
    1.11 +  Lambda/Eta.thy Lambda/InductTermi.thy Lambda/Lambda.thy \
    1.12    Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
    1.13 -  Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
    1.14 +  Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
    1.15  	@$(ISATOOL) usedir $(OUT)/HOL Lambda
    1.16  
    1.17  
     2.1 --- a/src/HOL/Lambda/Commutation.ML	Sat Sep 02 21:53:03 2000 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,97 +0,0 @@
     2.4 -(*  Title:      HOL/Lambda/Commutation.thy
     2.5 -    ID:         $Id$
     2.6 -    Author:     Tobias Nipkow
     2.7 -    Copyright   1995 TU Muenchen
     2.8 -
     2.9 -Basic commutation lemmas.
    2.10 -*)
    2.11 -
    2.12 -open Commutation;
    2.13 -
    2.14 -(*** square ***)
    2.15 -
    2.16 -Goalw [square_def] "square R S T U ==> square S R U T";
    2.17 -by (Blast_tac 1);
    2.18 -qed "square_sym";
    2.19 -
    2.20 -Goalw [square_def]
    2.21 -  "[| square R S T U; T <= T' |] ==> square R S T' U";
    2.22 -by (Blast_tac 1);
    2.23 -qed "square_subset";
    2.24 -
    2.25 -Goalw [square_def]
    2.26 -  "[| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
    2.27 -by (Blast_tac 1);
    2.28 -qed "square_reflcl";
    2.29 -
    2.30 -Goalw [square_def]
    2.31 -  "square R S S T ==> square (R^*) S S (T^*)";
    2.32 -by (strip_tac 1);
    2.33 -by (etac rtrancl_induct 1);
    2.34 -by (Blast_tac 1);
    2.35 -by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
    2.36 -qed "square_rtrancl";
    2.37 -
    2.38 -Goalw [commute_def]
    2.39 - "square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
    2.40 -by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl]
    2.41 -                       addEs [r_into_rtrancl]
    2.42 -                       addss simpset()) 1);
    2.43 -qed "square_rtrancl_reflcl_commute";
    2.44 -
    2.45 -(*** commute ***)
    2.46 -
    2.47 -Goalw [commute_def] "commute R S ==> commute S R";
    2.48 -by (blast_tac (claset() addIs [square_sym]) 1);
    2.49 -qed "commute_sym";
    2.50 -
    2.51 -Goalw [commute_def] "commute R S ==> commute (R^*) (S^*)";
    2.52 -by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1);
    2.53 -qed "commute_rtrancl";
    2.54 -
    2.55 -Goalw [commute_def,square_def]
    2.56 -  "[| commute R T; commute S T |] ==> commute (R Un S) T";
    2.57 -by (Blast_tac 1);
    2.58 -qed "commute_Un";
    2.59 -
    2.60 -(*** diamond, confluence and union ***)
    2.61 -
    2.62 -Goalw [diamond_def]
    2.63 -  "[| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
    2.64 -by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
    2.65 -qed "diamond_Un";
    2.66 -
    2.67 -Goalw [diamond_def] "diamond R ==> confluent (R)";
    2.68 -by (etac commute_rtrancl 1);
    2.69 -qed "diamond_confluent";
    2.70 -
    2.71 -Goalw [diamond_def]
    2.72 -  "square R R (R^=) (R^=) ==> confluent R";
    2.73 -by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
    2.74 -                       addEs [square_subset]) 1);
    2.75 -qed "square_reflcl_confluent";
    2.76 -
    2.77 -Goal
    2.78 - "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent(R Un S)";
    2.79 -by (rtac (rtrancl_Un_rtrancl RS subst) 1);
    2.80 -by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1);
    2.81 -qed "confluent_Un";
    2.82 -
    2.83 -Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
    2.84 -by (force_tac (claset() addIs [diamond_confluent] 
    2.85 -                        addDs [rtrancl_subset RS sym], simpset()) 1);
    2.86 -qed "diamond_to_confluence";
    2.87 -
    2.88 -(*** Church_Rosser ***)
    2.89 -
    2.90 -Goalw [square_def,commute_def,diamond_def,Church_Rosser_def]
    2.91 -  "Church_Rosser(R) = confluent(R)";
    2.92 -by (safe_tac HOL_cs);
    2.93 - by (blast_tac (HOL_cs addIs
    2.94 -      [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
    2.95 -       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD])1);
    2.96 -by (etac rtrancl_induct 1);
    2.97 - by (Blast_tac 1);
    2.98 -by (blast_tac (claset() delrules [rtrancl_refl] 
    2.99 -                        addIs [r_into_rtrancl, rtrancl_trans]) 1);
   2.100 -qed "Church_Rosser_confluent";
     3.1 --- a/src/HOL/Lambda/Commutation.thy	Sat Sep 02 21:53:03 2000 +0200
     3.2 +++ b/src/HOL/Lambda/Commutation.thy	Sat Sep 02 21:56:24 2000 +0200
     3.3 @@ -2,28 +2,137 @@
     3.4      ID:         $Id$
     3.5      Author:     Tobias Nipkow
     3.6      Copyright   1995  TU Muenchen
     3.7 -
     3.8 -Abstract commutation and confluence notions.
     3.9  *)
    3.10  
    3.11 -Commutation = Main +
    3.12 +header {* Abstract commutation and confluence notions *}
    3.13 +
    3.14 +theory Commutation = Main:
    3.15 +
    3.16 +subsection {* Basic definitions *}
    3.17 +
    3.18 +constdefs
    3.19 +  square :: "[('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
    3.20 +  "square R S T U ==
    3.21 +    \<forall>x y. (x, y) \<in> R --> (\<forall>z. (x, z) \<in> S --> (\<exists>u. (y, u) \<in> T \<and> (z, u) \<in> U))"
    3.22 +
    3.23 +  commute :: "[('a \<times> 'a) set, ('a \<times> 'a) set] => bool"
    3.24 +  "commute R S == square R S S R"
    3.25 +
    3.26 +  diamond :: "('a \<times> 'a) set => bool"
    3.27 +  "diamond R == commute R R"
    3.28 +
    3.29 +  Church_Rosser :: "('a \<times> 'a) set => bool"
    3.30 +  "Church_Rosser R ==
    3.31 +    \<forall>x y. (x, y) \<in> (R \<union> R^-1)^* --> (\<exists>z. (x, z) \<in> R^* \<and> (y, z) \<in> R^*)"
    3.32 +
    3.33 +syntax
    3.34 +  confluent :: "('a \<times> 'a) set => bool"
    3.35 +translations
    3.36 +  "confluent R" == "diamond (R^*)"
    3.37 +
    3.38 +
    3.39 +subsection {* Basic lemmas *}
    3.40 +
    3.41 +subsubsection {* square *}
    3.42  
    3.43 -consts
    3.44 -  square  :: "[('a*'a)set,('a*'a)set,('a*'a)set,('a*'a)set] => bool"
    3.45 -  commute :: "[('a*'a)set,('a*'a)set] => bool"
    3.46 -  confluent, diamond, Church_Rosser :: "('a*'a)set => bool"
    3.47 +lemma square_sym: "square R S T U ==> square S R U T"
    3.48 +  apply (unfold square_def)
    3.49 +  apply blast
    3.50 +  done
    3.51 +
    3.52 +lemma square_subset:
    3.53 +    "[| square R S T U; T \<subseteq> T' |] ==> square R S T' U"
    3.54 +  apply (unfold square_def)
    3.55 +  apply blast
    3.56 +  done
    3.57 +
    3.58 +lemma square_reflcl:
    3.59 +    "[| square R S T (R^=); S \<subseteq> T |] ==> square (R^=) S T (R^=)"
    3.60 +  apply (unfold square_def)
    3.61 +  apply blast
    3.62 +  done
    3.63  
    3.64 -defs
    3.65 -  square_def
    3.66 - "square R S T U == !x y.(x,y):R --> (!z.(x,z):S --> (? u. (y,u):T & (z,u):U))"
    3.67 +lemma square_rtrancl:
    3.68 +    "square R S S T ==> square (R^*) S S (T^*)"
    3.69 +  apply (unfold square_def)
    3.70 +  apply (intro strip)
    3.71 +  apply (erule rtrancl_induct)
    3.72 +   apply blast
    3.73 +  apply (blast intro: rtrancl_into_rtrancl)
    3.74 +  done
    3.75 +
    3.76 +lemma square_rtrancl_reflcl_commute:
    3.77 +    "square R S (S^*) (R^=) ==> commute (R^*) (S^*)"
    3.78 +  apply (unfold commute_def)
    3.79 +  apply (fastsimp dest: square_reflcl square_sym [THEN square_rtrancl]
    3.80 +    elim: r_into_rtrancl)
    3.81 +  done
    3.82 +
    3.83  
    3.84 -  commute_def "commute R S == square R S S R"
    3.85 -  diamond_def "diamond R   == commute R R"
    3.86 +subsubsection {* commute *}
    3.87 +
    3.88 +lemma commute_sym: "commute R S ==> commute S R"
    3.89 +  apply (unfold commute_def)
    3.90 +  apply (blast intro: square_sym)
    3.91 +  done
    3.92 +
    3.93 +lemma commute_rtrancl: "commute R S ==> commute (R^*) (S^*)"
    3.94 +  apply (unfold commute_def)
    3.95 +  apply (blast intro: square_rtrancl square_sym)
    3.96 +  done
    3.97 +
    3.98 +lemma commute_Un:
    3.99 +    "[| commute R T; commute S T |] ==> commute (R \<union> S) T"
   3.100 +  apply (unfold commute_def square_def)
   3.101 +  apply blast
   3.102 +  done
   3.103 +
   3.104 +
   3.105 +subsubsection {* diamond, confluence, and union *}
   3.106 +
   3.107 +lemma diamond_Un:
   3.108 +    "[| diamond R; diamond S; commute R S |] ==> diamond (R \<union> S)"
   3.109 +  apply (unfold diamond_def)
   3.110 +  apply (assumption | rule commute_Un commute_sym)+
   3.111 +  done
   3.112 +
   3.113 +lemma diamond_confluent: "diamond R ==> confluent R"
   3.114 +  apply (unfold diamond_def)
   3.115 +  apply (erule commute_rtrancl)
   3.116 +  done
   3.117  
   3.118 -  Church_Rosser_def "Church_Rosser(R) ==   
   3.119 -  !x y. (x,y) : (R Un R^-1)^* --> (? z. (x,z) : R^* & (y,z) : R^*)"
   3.120 +lemma square_reflcl_confluent:
   3.121 +    "square R R (R^=) (R^=) ==> confluent R"
   3.122 +  apply (unfold diamond_def)
   3.123 +  apply (fast intro: square_rtrancl_reflcl_commute r_into_rtrancl
   3.124 +    elim: square_subset)
   3.125 +  done
   3.126 +
   3.127 +lemma confluent_Un:
   3.128 +    "[| confluent R; confluent S; commute (R^*) (S^*) |] ==> confluent (R \<union> S)"
   3.129 +  apply (rule rtrancl_Un_rtrancl [THEN subst])
   3.130 +  apply (blast dest: diamond_Un intro: diamond_confluent)
   3.131 +  done
   3.132  
   3.133 -translations
   3.134 -  "confluent R" == "diamond(R^*)"
   3.135 +lemma diamond_to_confluence:
   3.136 +    "[| diamond R; T \<subseteq> R; R \<subseteq> T^* |] ==> confluent T"
   3.137 +  apply (force intro: diamond_confluent
   3.138 +    dest: rtrancl_subset [symmetric])
   3.139 +  done
   3.140 +
   3.141 +
   3.142 +subsection {* Church-Rosser *}
   3.143  
   3.144 -end
   3.145 +lemma Church_Rosser_confluent: "Church_Rosser R = confluent R"
   3.146 +  apply (unfold square_def commute_def diamond_def Church_Rosser_def)
   3.147 +  apply (tactic {* safe_tac HOL_cs *})
   3.148 +   apply (tactic {*
   3.149 +     blast_tac (HOL_cs addIs
   3.150 +       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
   3.151 +       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
   3.152 +  apply (erule rtrancl_induct)
   3.153 +   apply blast
   3.154 +  apply (blast del: rtrancl_refl intro: r_into_rtrancl rtrancl_trans)
   3.155 +  done
   3.156 +
   3.157 +end
   3.158 \ No newline at end of file
     4.1 --- a/src/HOL/Lambda/Eta.ML	Sat Sep 02 21:53:03 2000 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,208 +0,0 @@
     4.4 -(*  Title:      HOL/Lambda/Eta.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Tobias Nipkow
     4.7 -    Copyright   1995 TU Muenchen
     4.8 -
     4.9 -Eta reduction,
    4.10 -confluence of eta,
    4.11 -commutation of beta/eta,
    4.12 -confluence of beta+eta
    4.13 -*)
    4.14 -
    4.15 -Addsimps eta.intrs;
    4.16 -AddIs eta.intrs;
    4.17 -
    4.18 -val eta_cases = map eta.mk_cases ["Abs s -e> z", "s $ t -e> u", "Var i -e> t"];
    4.19 -AddSEs eta_cases;
    4.20 -
    4.21 -section "eta, subst and free";
    4.22 -
    4.23 -Goal "!i t u. ~free s i --> s[t/i] = s[u/i]";
    4.24 -by (induct_tac "s" 1);
    4.25 -by (ALLGOALS(simp_tac (addsplit (simpset()))));
    4.26 -by (Blast_tac 1);
    4.27 -by (Blast_tac 1);
    4.28 -qed_spec_mp "subst_not_free";
    4.29 -Addsimps [subst_not_free RS eqTrueI];
    4.30 -
    4.31 -Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
    4.32 -by (induct_tac "t" 1);
    4.33 -  by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
    4.34 - by (arith_tac 1);
    4.35 -by (Auto_tac);
    4.36 -qed "free_lift";
    4.37 -Addsimps [free_lift];
    4.38 -
    4.39 -Goal "!i k t. free (s[t/k]) i = \
    4.40 -\              (free s k & free t i | free s (if i<k then i else i+1))";
    4.41 -by (induct_tac "s" 1);
    4.42 -by (Asm_simp_tac 2);
    4.43 -by (Blast_tac 2);
    4.44 -by (asm_full_simp_tac (addsplit (simpset())) 2);
    4.45 -by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
    4.46 -                      addsplits [nat.split]) 1);
    4.47 -by (safe_tac (HOL_cs addSEs [linorder_neqE]));
    4.48 -by (ALLGOALS Simp_tac);
    4.49 -qed "free_subst";
    4.50 -Addsimps [free_subst];
    4.51 -
    4.52 -Goal "s -e> t ==> !i. free t i = free s i";
    4.53 -by (etac eta.induct 1);
    4.54 -by (ALLGOALS(asm_simp_tac (simpset() addcongs [conj_cong])));
    4.55 -qed_spec_mp "free_eta";
    4.56 -
    4.57 -Goal "[| s -e> t; ~free s i |] ==> ~free t i";
    4.58 -by (asm_simp_tac (simpset() addsimps [free_eta]) 1);
    4.59 -qed "not_free_eta";
    4.60 -
    4.61 -Goal "s -e> t ==> !u i. s[u/i] -e> t[u/i]";
    4.62 -by (etac eta.induct 1);
    4.63 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
    4.64 -qed_spec_mp "eta_subst";
    4.65 -Addsimps [eta_subst];
    4.66 -
    4.67 -section "Confluence of -e>";
    4.68 -
    4.69 -Goalw [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
    4.70 -by (rtac (impI RS allI RS allI) 1);
    4.71 -by (Simp_tac 1);
    4.72 -by (etac eta.induct 1);
    4.73 -by (slow_tac (claset() addIs [subst_not_free,eta_subst]
    4.74 -                      addIs [free_eta RS iffD1] addss simpset()) 1);
    4.75 -by Safe_tac;
    4.76 -by (blast_tac (claset() addSIs [eta_subst] addIs [free_eta RS iffD1]) 5);
    4.77 -by (ALLGOALS Blast_tac);
    4.78 -qed "square_eta";
    4.79 -
    4.80 -Goal "confluent(eta)";
    4.81 -by (rtac (square_eta RS square_reflcl_confluent) 1);
    4.82 -qed "eta_confluent";
    4.83 -
    4.84 -section "Congruence rules for -e>>";
    4.85 -
    4.86 -Goal "s -e>> s' ==> Abs s -e>> Abs s'";
    4.87 -by (etac rtrancl_induct 1);
    4.88 -by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.89 -qed "rtrancl_eta_Abs";
    4.90 -
    4.91 -Goal "s -e>> s' ==> s $ t -e>> s' $ t";
    4.92 -by (etac rtrancl_induct 1);
    4.93 -by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.94 -qed "rtrancl_eta_AppL";
    4.95 -
    4.96 -Goal "t -e>> t' ==> s $ t -e>> s $ t'";
    4.97 -by (etac rtrancl_induct 1);
    4.98 -by (ALLGOALS(blast_tac (claset() addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.99 -qed "rtrancl_eta_AppR";
   4.100 -
   4.101 -Goal "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'";
   4.102 -by (blast_tac (claset() addSIs [rtrancl_eta_AppL, rtrancl_eta_AppR]
   4.103 -                       addIs [rtrancl_trans]) 1);
   4.104 -qed "rtrancl_eta_App";
   4.105 -
   4.106 -section "Commutation of -> and -e>";
   4.107 -
   4.108 -Goal "s -> t ==> (!i. free t i --> free s i)";
   4.109 -by (etac beta.induct 1);
   4.110 -by (ALLGOALS(Asm_full_simp_tac));
   4.111 -qed_spec_mp "free_beta";
   4.112 -
   4.113 -Goal "s -> t ==> !u i. s[u/i] -> t[u/i]";
   4.114 -by (etac beta.induct 1);
   4.115 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [subst_subst RS sym])));
   4.116 -qed_spec_mp "beta_subst";
   4.117 -AddIs [beta_subst];
   4.118 -
   4.119 -Goal "!i. t[Var i/i] = t[Var(i)/i+1]";
   4.120 -by (induct_tac "t" 1);
   4.121 -by (auto_tac (claset() addSEs [linorder_neqE], addsplit (simpset())));
   4.122 -qed_spec_mp "subst_Var_Suc";
   4.123 -Addsimps [subst_Var_Suc];
   4.124 -
   4.125 -Goal "s -e> t ==> (!i. lift s i -e> lift t i)";
   4.126 -by (etac eta.induct 1);
   4.127 -by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
   4.128 -qed_spec_mp "eta_lift";
   4.129 -Addsimps [eta_lift];
   4.130 -
   4.131 -Goal "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
   4.132 -by (induct_tac "u" 1);
   4.133 -by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
   4.134 -by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
   4.135 -by (blast_tac (claset() addSIs [rtrancl_eta_App]) 1);
   4.136 -by (blast_tac (claset() addSIs [rtrancl_eta_Abs,eta_lift]) 1);
   4.137 -qed_spec_mp "rtrancl_eta_subst";
   4.138 -
   4.139 -Goalw [square_def] "square beta eta (eta^*) (beta^=)";
   4.140 -by (rtac (impI RS allI RS allI) 1);
   4.141 -by (etac beta.induct 1);
   4.142 -by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_subst,eta_subst]
   4.143 -                      addss simpset()) 1);
   4.144 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppL]) 1);
   4.145 -by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_AppR]) 1);
   4.146 -(*23 seconds?*)
   4.147 -DelIffs dB.distinct;
   4.148 -Addsimps dB.distinct;
   4.149 -by (slow_tac (claset() addIs [r_into_rtrancl,rtrancl_eta_Abs,free_beta]
   4.150 -                      addss simpset()) 1);
   4.151 -qed "square_beta_eta";
   4.152 -
   4.153 -Goal "confluent(beta Un eta)";
   4.154 -by (REPEAT(ares_tac [square_rtrancl_reflcl_commute,confluent_Un,
   4.155 -                    beta_confluent,eta_confluent,square_beta_eta] 1));
   4.156 -qed "confluent_beta_eta";
   4.157 -
   4.158 -section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
   4.159 -
   4.160 -Goal "!i. (~free s i) = (? t. s = lift t i)";
   4.161 -by (induct_tac "s" 1);
   4.162 -  by (Simp_tac 1);
   4.163 -  by (SELECT_GOAL(safe_tac HOL_cs)1);
   4.164 -   by (etac linorder_neqE 1);
   4.165 -    by (res_inst_tac [("x","Var nat")] exI 1);
   4.166 -    by (Asm_simp_tac 1);
   4.167 -   by (res_inst_tac [("x","Var(nat-1)")] exI 1);
   4.168 -   by (Asm_simp_tac 1);
   4.169 -  by (rtac notE 1);
   4.170 -   by (assume_tac 2);
   4.171 -  by (etac thin_rl 1);
   4.172 -  by (case_tac "t" 1);
   4.173 -    by (Asm_simp_tac 1);
   4.174 -   by (Asm_simp_tac 1);
   4.175 -  by (Asm_simp_tac 1);
   4.176 - by (Asm_simp_tac 1);
   4.177 - by (etac thin_rl 1);
   4.178 - by (etac thin_rl 1);
   4.179 - by (rtac allI 1);
   4.180 - by (rtac iffI 1);
   4.181 -  by (REPEAT(eresolve_tac [conjE,exE] 1));
   4.182 -  by (rename_tac "u1 u2" 1);
   4.183 -  by (res_inst_tac [("x","u1$u2")] exI 1);
   4.184 -  by (Asm_simp_tac 1);
   4.185 - by (etac exE 1);
   4.186 - by (etac rev_mp 1);
   4.187 - by (case_tac "t" 1);
   4.188 -   by (Asm_simp_tac 1);
   4.189 -  by (Asm_simp_tac 1);
   4.190 -  by (Blast_tac 1);
   4.191 - by (Asm_simp_tac 1);
   4.192 -by (Asm_simp_tac 1);
   4.193 -by (etac thin_rl 1);
   4.194 -by (rtac allI 1);
   4.195 -by (rtac iffI 1);
   4.196 - by (etac exE 1);
   4.197 - by (res_inst_tac [("x","Abs t")] exI 1);
   4.198 - by (Asm_simp_tac 1);
   4.199 -by (etac exE 1);
   4.200 -by (etac rev_mp 1);
   4.201 -by (case_tac "t" 1);
   4.202 -  by (Asm_simp_tac 1);
   4.203 - by (Asm_simp_tac 1);
   4.204 -by (Asm_simp_tac 1);
   4.205 -by (Blast_tac 1);
   4.206 -qed_spec_mp "not_free_iff_lifted";
   4.207 -
   4.208 -Goal "(!s u. (~free s 0) --> R(Abs(s $ Var 0))(s[u/0])) = \
   4.209 -\     (!s. R(Abs(lift s 0 $ Var 0))(s))";
   4.210 -by (fast_tac (HOL_cs addss (simpset() addsimps [not_free_iff_lifted])) 1);
   4.211 -qed "explicit_is_implicit";
     5.1 --- a/src/HOL/Lambda/Eta.thy	Sat Sep 02 21:53:03 2000 +0200
     5.2 +++ b/src/HOL/Lambda/Eta.thy	Sat Sep 02 21:56:24 2000 +0200
     5.3 @@ -2,33 +2,250 @@
     5.4      ID:         $Id$
     5.5      Author:     Tobias Nipkow
     5.6      Copyright   1995 TU Muenchen
     5.7 -
     5.8 -Eta-reduction and relatives.
     5.9  *)
    5.10  
    5.11 -Eta = ParRed +
    5.12 -consts free :: dB => nat => bool
    5.13 -       decr :: dB => dB
    5.14 -       eta  :: "(dB * dB) set"
    5.15 +header {* Eta-reduction *}
    5.16 +
    5.17 +theory Eta = ParRed:
    5.18 +
    5.19 +
    5.20 +subsection {* Definition of eta-reduction and relatives *}
    5.21  
    5.22 -syntax  "-e>", "-e>>", "-e>=" , "->=" :: [dB,dB] => bool (infixl 50)
    5.23 +consts
    5.24 +  free :: "dB => nat => bool"
    5.25 +primrec
    5.26 +  "free (Var j) i = (j = i)"
    5.27 +  "free (s $ t) i = (free s i \<or> free t i)"
    5.28 +  "free (Abs s) i = free s (i + 1)"
    5.29  
    5.30 +consts
    5.31 +  eta :: "(dB \<times> dB) set"
    5.32 +
    5.33 +syntax 
    5.34 +  "_eta" :: "[dB, dB] => bool"   (infixl "-e>" 50)
    5.35 +  "_eta_rtrancl" :: "[dB, dB] => bool"   (infixl "-e>>" 50)
    5.36 +  "_eta_reflcl" :: "[dB, dB] => bool"   (infixl "-e>=" 50)
    5.37  translations
    5.38 -  "s -e>  t" == "(s,t) : eta"
    5.39 -  "s -e>> t" == "(s,t) : eta^*"
    5.40 -  "s -e>= t" == "(s,t) : eta^="
    5.41 -  "s ->=  t" == "(s,t) : beta^="
    5.42 -
    5.43 -primrec
    5.44 -  "free (Var j) i = (j=i)"
    5.45 -  "free (s $ t) i = (free s i | free t i)"
    5.46 -  "free (Abs s) i = free s (i+1)"
    5.47 +  "s -e> t" == "(s,t) \<in> eta"
    5.48 +  "s -e>> t" == "(s,t) \<in> eta^*"
    5.49 +  "s -e>= t" == "(s,t) \<in> eta^="
    5.50  
    5.51  inductive eta
    5.52 -intrs
    5.53 -   eta  "~free s 0 ==> Abs(s $ Var 0) -e> s[dummy/0]"
    5.54 -   appL  "s -e> t ==> s$u -e> t$u"
    5.55 -   appR  "s -e> t ==> u$s -e> u$t"
    5.56 -   abs   "s -e> t ==> Abs s -e> Abs t"
    5.57 -end
    5.58 +  intros [simp, intro]
    5.59 +    eta: "\<not> free s 0 ==> Abs (s $ Var 0) -e> s[dummy/0]"
    5.60 +    appL: "s -e> t ==> s $ u -e> t $ u"
    5.61 +    appR: "s -e> t ==> u $ s -e> u $ t"
    5.62 +    abs: "s -e> t ==> Abs s -e> Abs t"
    5.63 +
    5.64 +inductive_cases eta_cases [elim!]:
    5.65 +  "Abs s -e> z"
    5.66 +  "s $ t -e> u"
    5.67 +  "Var i -e> t"
    5.68 +
    5.69 +
    5.70 +subsection "Properties of eta, subst and free"
    5.71 +
    5.72 +lemma subst_not_free [rulify, simp]:
    5.73 +    "\<forall>i t u. \<not> free s i --> s[t/i] = s[u/i]"
    5.74 +  apply (induct_tac s)
    5.75 +    apply (simp_all add: subst_Var)
    5.76 +  done
    5.77 +
    5.78 +lemma free_lift [simp]:
    5.79 +    "\<forall>i k. free (lift t k) i =
    5.80 +      (i < k \<and> free t i \<or> k < i \<and> free t (i - 1))"
    5.81 +  apply (induct_tac t)
    5.82 +    apply (auto cong: conj_cong)
    5.83 +  apply arith
    5.84 +  done
    5.85 +
    5.86 +lemma free_subst [simp]:
    5.87 +    "\<forall>i k t. free (s[t/k]) i =
    5.88 +      (free s k \<and> free t i \<or> free s (if i < k then i else i + 1))"
    5.89 +  apply (induct_tac s)
    5.90 +    prefer 2
    5.91 +    apply simp
    5.92 +    apply blast
    5.93 +   prefer 2
    5.94 +   apply simp
    5.95 +  apply (simp add: diff_Suc subst_Var split: nat.split)
    5.96 +  apply clarify
    5.97 +  apply (erule linorder_neqE)
    5.98 +  apply simp_all
    5.99 +  done
   5.100 +
   5.101 +lemma free_eta [rulify]:
   5.102 +    "s -e> t ==> \<forall>i. free t i = free s i"
   5.103 +  apply (erule eta.induct)
   5.104 +     apply (simp_all cong: conj_cong)
   5.105 +  done
   5.106 +
   5.107 +lemma not_free_eta:
   5.108 +    "[| s -e> t; \<not> free s i |] ==> \<not> free t i"
   5.109 +  apply (simp add: free_eta)
   5.110 +  done
   5.111 +
   5.112 +lemma eta_subst [rulify, simp]:
   5.113 +    "s -e> t ==> \<forall>u i. s[u/i] -e> t[u/i]"
   5.114 +  apply (erule eta.induct)
   5.115 +  apply (simp_all add: subst_subst [symmetric])
   5.116 +  done
   5.117 +
   5.118 +
   5.119 +subsection "Confluence of eta"
   5.120 +
   5.121 +lemma square_eta: "square eta eta (eta^=) (eta^=)"
   5.122 +  apply (unfold square_def id_def)
   5.123 +  apply (rule impI [THEN allI [THEN allI]])
   5.124 +  apply simp
   5.125 +  apply (erule eta.induct)
   5.126 +     apply (slowsimp intro: subst_not_free eta_subst free_eta [THEN iffD1])
   5.127 +    apply safe
   5.128 +       prefer 5
   5.129 +       apply (blast intro!: eta_subst intro: free_eta [THEN iffD1])
   5.130 +      apply blast+
   5.131 +  done
   5.132 +
   5.133 +theorem eta_confluent: "confluent eta"
   5.134 +  apply (rule square_eta [THEN square_reflcl_confluent])
   5.135 +  done
   5.136 +
   5.137 +
   5.138 +subsection "Congruence rules for eta*"
   5.139 +
   5.140 +lemma rtrancl_eta_Abs: "s -e>> s' ==> Abs s -e>> Abs s'"
   5.141 +  apply (erule rtrancl_induct)
   5.142 +   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   5.143 +  done
   5.144 +
   5.145 +lemma rtrancl_eta_AppL: "s -e>> s' ==> s $ t -e>> s' $ t"
   5.146 +  apply (erule rtrancl_induct)
   5.147 +   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   5.148 +  done
   5.149 +
   5.150 +lemma rtrancl_eta_AppR: "t -e>> t' ==> s $ t -e>> s $ t'"
   5.151 +  apply (erule rtrancl_induct)
   5.152 +   apply (blast intro: rtrancl_refl rtrancl_into_rtrancl)+
   5.153 +  done
   5.154 +
   5.155 +lemma rtrancl_eta_App:
   5.156 +    "[| s -e>> s'; t -e>> t' |] ==> s $ t -e>> s' $ t'"
   5.157 +  apply (blast intro!: rtrancl_eta_AppL rtrancl_eta_AppR intro: rtrancl_trans)
   5.158 +  done
   5.159 +
   5.160 +
   5.161 +subsection "Commutation of beta and eta"
   5.162  
   5.163 +lemma free_beta [rulify]:
   5.164 +    "s -> t ==> \<forall>i. free t i --> free s i"
   5.165 +  apply (erule beta.induct)
   5.166 +     apply simp_all
   5.167 +  done
   5.168 +
   5.169 +lemma beta_subst [rulify, intro]:
   5.170 +    "s -> t ==> \<forall>u i. s[u/i] -> t[u/i]"
   5.171 +  apply (erule beta.induct)
   5.172 +     apply (simp_all add: subst_subst [symmetric])
   5.173 +  done
   5.174 +
   5.175 +lemma subst_Var_Suc [simp]: "\<forall>i. t[Var i/i] = t[Var(i)/i + 1]"
   5.176 +  apply (induct_tac t)
   5.177 +  apply (auto elim!: linorder_neqE simp: subst_Var)
   5.178 +  done
   5.179 +
   5.180 +lemma eta_lift [rulify, simp]:
   5.181 +    "s -e> t ==> \<forall>i. lift s i -e> lift t i"
   5.182 +  apply (erule eta.induct)
   5.183 +     apply simp_all
   5.184 +  done
   5.185 +
   5.186 +lemma rtrancl_eta_subst [rulify]:
   5.187 +    "\<forall>s t i. s -e> t --> u[s/i] -e>> u[t/i]"
   5.188 +  apply (induct_tac u)
   5.189 +    apply (simp_all add: subst_Var)
   5.190 +    apply (blast intro: r_into_rtrancl)
   5.191 +   apply (blast intro: rtrancl_eta_App)
   5.192 +  apply (blast intro!: rtrancl_eta_Abs eta_lift)
   5.193 +  done
   5.194 +
   5.195 +lemma square_beta_eta: "square beta eta (eta^*) (beta^=)"
   5.196 +  apply (unfold square_def)
   5.197 +  apply (rule impI [THEN allI [THEN allI]])
   5.198 +  apply (erule beta.induct)
   5.199 +     apply (slowsimp intro: r_into_rtrancl rtrancl_eta_subst eta_subst)
   5.200 +    apply (blast intro: r_into_rtrancl rtrancl_eta_AppL)
   5.201 +   apply (blast intro: r_into_rtrancl rtrancl_eta_AppR)
   5.202 +  apply (slowsimp intro: r_into_rtrancl rtrancl_eta_Abs free_beta
   5.203 +    other: dB.distinct [iff del, simp])    (*23 seconds?*)
   5.204 +  done
   5.205 +
   5.206 +lemma confluent_beta_eta: "confluent (beta \<union> eta)"
   5.207 +  apply (assumption |
   5.208 +    rule square_rtrancl_reflcl_commute confluent_Un
   5.209 +      beta_confluent eta_confluent square_beta_eta)+
   5.210 +  done
   5.211 +
   5.212 +
   5.213 +subsection "Implicit definition of eta"
   5.214 +
   5.215 +text {* @{term "Abs (lift s 0 $ Var 0) -e> s"} *}
   5.216 +
   5.217 +lemma not_free_iff_lifted [rulify]:
   5.218 +    "\<forall>i. (\<not> free s i) = (\<exists>t. s = lift t i)"
   5.219 +  apply (induct_tac s)
   5.220 +    apply simp
   5.221 +    apply clarify
   5.222 +    apply (rule iffI)
   5.223 +     apply (erule linorder_neqE)
   5.224 +      apply (rule_tac x = "Var nat" in exI)
   5.225 +      apply simp
   5.226 +     apply (rule_tac x = "Var (nat - 1)" in exI)
   5.227 +     apply simp
   5.228 +    apply clarify
   5.229 +    apply (rule notE)
   5.230 +     prefer 2
   5.231 +     apply assumption
   5.232 +    apply (erule thin_rl)
   5.233 +    apply (case_tac t)
   5.234 +      apply simp
   5.235 +     apply simp
   5.236 +    apply simp
   5.237 +   apply simp
   5.238 +   apply (erule thin_rl)
   5.239 +   apply (erule thin_rl)
   5.240 +   apply (rule allI)
   5.241 +   apply (rule iffI)
   5.242 +    apply (elim conjE exE)
   5.243 +    apply (rename_tac u1 u2)
   5.244 +    apply (rule_tac x = "u1 $ u2" in exI)
   5.245 +    apply simp
   5.246 +   apply (erule exE)
   5.247 +   apply (erule rev_mp)
   5.248 +   apply (case_tac t)
   5.249 +     apply simp
   5.250 +    apply simp
   5.251 +    apply blast
   5.252 +   apply simp
   5.253 +  apply simp
   5.254 +  apply (erule thin_rl)
   5.255 +  apply (rule allI)
   5.256 +  apply (rule iffI)
   5.257 +   apply (erule exE)
   5.258 +   apply (rule_tac x = "Abs t" in exI)
   5.259 +   apply simp
   5.260 +  apply (erule exE)
   5.261 +  apply (erule rev_mp)
   5.262 +  apply (case_tac t)
   5.263 +    apply simp
   5.264 +   apply simp
   5.265 +  apply simp
   5.266 +  apply blast
   5.267 +  done
   5.268 +
   5.269 +theorem explicit_is_implicit:
   5.270 +  "(\<forall>s u. (\<not> free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) =
   5.271 +    (\<forall>s. R (Abs (lift s 0 $ Var 0)) s)"
   5.272 +  apply (auto simp add: not_free_iff_lifted)
   5.273 +  done
   5.274 +
   5.275 +end
   5.276 \ No newline at end of file
     6.1 --- a/src/HOL/Lambda/InductTermi.thy	Sat Sep 02 21:53:03 2000 +0200
     6.2 +++ b/src/HOL/Lambda/InductTermi.thy	Sat Sep 02 21:56:24 2000 +0200
     6.3 @@ -3,14 +3,17 @@
     6.4      Author:     Tobias Nipkow
     6.5      Copyright   1998 TU Muenchen
     6.6  
     6.7 -Inductive characterization of terminating lambda terms.
     6.8 -Goes back to
     6.9 -Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.
    6.10 -Also rediscovered by Matthes and Joachimski.
    6.11 +Inductive characterization of terminating lambda terms.  Goes back to
    6.12 +Raamsdonk & Severi. On normalization. CWI TR CS-R9545, 1995.  Also
    6.13 +rediscovered by Matthes and Joachimski.
    6.14  *)
    6.15  
    6.16 +header {* Inductive characterization of terminating lambda terms *}
    6.17 +
    6.18  theory InductTermi = ListBeta:
    6.19  
    6.20 +subsection {* Terminating lambda terms *}
    6.21 +
    6.22  consts
    6.23    IT :: "dB set"
    6.24  
    6.25 @@ -18,10 +21,10 @@
    6.26    intros
    6.27      Var: "rs : lists IT ==> Var n $$ rs : IT"
    6.28      Lambda: "r : IT ==> Abs r : IT"
    6.29 -    Beta: "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT"
    6.30 +    Beta: "[| (r[s/0]) $$ ss : IT; s : IT |] ==> (Abs r $ s) $$ ss : IT"
    6.31  
    6.32  
    6.33 -text {* Every term in IT terminates. *}
    6.34 +subsection {* Every term in IT terminates *}
    6.35  
    6.36  lemma double_induction_lemma [rulify]:
    6.37    "s : termi beta ==> \<forall>t. t : termi beta -->
    6.38 @@ -58,7 +61,7 @@
    6.39    done
    6.40  
    6.41  
    6.42 -text {* Every terminating term is in IT *}
    6.43 +subsection {* Every terminating term is in IT *}
    6.44  
    6.45  declare Var_apps_neq_Abs_apps [THEN not_sym, simp]
    6.46  
    6.47 @@ -67,7 +70,7 @@
    6.48    done
    6.49  
    6.50  lemma [simp]:
    6.51 -  "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' \<and> s=s' \<and> ss=ss')"
    6.52 +  "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \<and> s = s' \<and> ss = ss')"
    6.53    apply (simp add: foldl_Cons [symmetric] del: foldl_Cons)
    6.54    done
    6.55  
    6.56 @@ -76,7 +79,6 @@
    6.57    "Abs t : IT"
    6.58    "Abs r $ s $$ ts : IT"
    6.59  
    6.60 -
    6.61  theorem termi_implies_IT: "r : termi beta ==> r : IT"
    6.62    apply (erule acc_induct)
    6.63    apply (rename_tac r)
    6.64 @@ -112,4 +114,4 @@
    6.65     apply force
    6.66     done
    6.67  
    6.68 -end
    6.69 +end
    6.70 \ No newline at end of file
     7.1 --- a/src/HOL/Lambda/Lambda.ML	Sat Sep 02 21:53:03 2000 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,146 +0,0 @@
     7.4 -(*  Title:      HOL/Lambda/Lambda.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Tobias Nipkow
     7.7 -    Copyright   1995 TU Muenchen
     7.8 -
     7.9 -Substitution-lemmas.
    7.10 -*)
    7.11 -
    7.12 -(*** Lambda ***)
    7.13 -
    7.14 -val beta_cases = map beta.mk_cases ["Var i -> t", "Abs r -> s", "s $ t -> u"];
    7.15 -AddSEs beta_cases;
    7.16 -
    7.17 -Delsimps [subst_Var];
    7.18 -Addsimps ([if_not_P, not_less_eq] @ beta.intrs);
    7.19 -
    7.20 -(* don't add r_into_rtrancl! *)
    7.21 -AddSIs beta.intrs;
    7.22 -
    7.23 -(*** Congruence rules for ->> ***)
    7.24 -
    7.25 -Goal "s ->> s' ==> Abs s ->> Abs s'";
    7.26 -by (etac rtrancl_induct 1);
    7.27 -by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    7.28 -qed "rtrancl_beta_Abs";
    7.29 -AddSIs [rtrancl_beta_Abs];
    7.30 -
    7.31 -Goal "s ->> s' ==> s $ t ->> s' $ t";
    7.32 -by (etac rtrancl_induct 1);
    7.33 -by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    7.34 -qed "rtrancl_beta_AppL";
    7.35 -
    7.36 -Goal "t ->> t' ==> s $ t ->> s $ t'";
    7.37 -by (etac rtrancl_induct 1);
    7.38 -by (ALLGOALS (blast_tac (claset() addIs [rtrancl_into_rtrancl])));
    7.39 -qed "rtrancl_beta_AppR";
    7.40 -
    7.41 -Goal "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'";
    7.42 -by (blast_tac (claset() addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
    7.43 -                       addIs  [rtrancl_trans]) 1);
    7.44 -qed "rtrancl_beta_App";
    7.45 -AddIs [rtrancl_beta_App];
    7.46 -
    7.47 -(*** subst and lift ***)
    7.48 -
    7.49 -fun addsplit ss = ss addsimps [subst_Var]
    7.50 -                     delsplits [split_if]
    7.51 -                     setloop (split_inside_tac [split_if]);
    7.52 -
    7.53 -Goal "(Var k)[u/k] = u";
    7.54 -by (asm_full_simp_tac(addsplit(simpset())) 1);
    7.55 -qed "subst_eq";
    7.56 -
    7.57 -Goal "i<j ==> (Var j)[u/i] = Var(j-1)";
    7.58 -by (asm_full_simp_tac(addsplit(simpset())) 1);
    7.59 -qed "subst_gt";
    7.60 -
    7.61 -Goal "j<i ==> (Var j)[u/i] = Var(j)";
    7.62 -by (asm_full_simp_tac (addsplit(simpset()) addsimps [less_not_refl3]) 1);
    7.63 -qed "subst_lt";
    7.64 -
    7.65 -Addsimps [subst_eq,subst_gt,subst_lt];
    7.66 -
    7.67 -Goal
    7.68 -  "!i k. i < k+1 --> lift (lift t i) (Suc k) = lift (lift t k) i";
    7.69 -by (induct_tac "t" 1);
    7.70 -by (Auto_tac);
    7.71 -qed_spec_mp "lift_lift";
    7.72 -
    7.73 -Goal "!i j s. j < i+1 --> lift (t[s/j]) i = (lift t (i+1)) [lift s i / j]";
    7.74 -by (induct_tac "t" 1);
    7.75 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
    7.76 -                                addsplits [nat.split])));
    7.77 -by (Auto_tac);
    7.78 -qed "lift_subst";
    7.79 -Addsimps [lift_subst];
    7.80 -
    7.81 -Goal
    7.82 -  "!i j s. i < j+1 --> lift (t[s/j]) i = (lift t i) [lift s i / j+1]";
    7.83 -by (induct_tac "t" 1);
    7.84 -by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift])));
    7.85 -qed "lift_subst_lt";
    7.86 -
    7.87 -Goal "!k s. (lift t k)[s/k] = t";
    7.88 -by (induct_tac "t" 1);
    7.89 -by (ALLGOALS Asm_full_simp_tac);
    7.90 -qed "subst_lift";
    7.91 -Addsimps [subst_lift];
    7.92 -
    7.93 -
    7.94 -Goal "!i j u v. i < j+1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
    7.95 -by (induct_tac "t" 1);
    7.96 -by (ALLGOALS(asm_simp_tac
    7.97 -      (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
    7.98 -                 addsplits [nat.split])));
    7.99 -by (safe_tac (HOL_cs addSEs [nat_neqE]));
   7.100 -by (ALLGOALS Simp_tac);
   7.101 -qed_spec_mp "subst_subst";
   7.102 -
   7.103 -
   7.104 -(*** Equivalence proof for optimized substitution ***)
   7.105 -
   7.106 -Goal "!k. liftn 0 t k = t";
   7.107 -by (induct_tac "t" 1);
   7.108 -by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
   7.109 -qed "liftn_0";
   7.110 -Addsimps [liftn_0];
   7.111 -
   7.112 -Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k";
   7.113 -by (induct_tac "t" 1);
   7.114 -by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
   7.115 -qed "liftn_lift";
   7.116 -Addsimps [liftn_lift];
   7.117 -
   7.118 -Goal "!n. substn t s n = t[liftn n s 0 / n]";
   7.119 -by (induct_tac "t" 1);
   7.120 -by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
   7.121 -qed "substn_subst_n";
   7.122 -Addsimps [substn_subst_n];
   7.123 -
   7.124 -Goal "substn t s 0 = t[s/0]";
   7.125 -by (Simp_tac 1);
   7.126 -qed "substn_subst_0";
   7.127 -
   7.128 -(*** Preservation thms ***)
   7.129 -(* Not used in CR-proof but in SN-proof *)
   7.130 -
   7.131 -Goal "r -> s ==> !t i. r[t/i] -> s[t/i]";
   7.132 -by (etac beta.induct 1);
   7.133 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [subst_subst RS sym])));
   7.134 -qed_spec_mp "subst_preserves_beta";
   7.135 -Addsimps [subst_preserves_beta];
   7.136 -
   7.137 -Goal "r -> s ==> !i. lift r i -> lift s i";
   7.138 -by (etac beta.induct 1);
   7.139 -by (Auto_tac);
   7.140 -qed_spec_mp "lift_preserves_beta";
   7.141 -Addsimps [lift_preserves_beta];
   7.142 -
   7.143 -Goal "!r s i. r -> s --> t[r/i] ->> t[s/i]";
   7.144 -by (induct_tac "t" 1);
   7.145 -by (asm_simp_tac (addsplit(simpset() addsimps [r_into_rtrancl])) 1);
   7.146 -by (asm_simp_tac (simpset() addsimps [rtrancl_beta_App]) 1);
   7.147 -by (asm_simp_tac (simpset() addsimps [rtrancl_beta_Abs]) 1);
   7.148 -qed_spec_mp "subst_preserves_beta2";
   7.149 -Addsimps [subst_preserves_beta2];
     8.1 --- a/src/HOL/Lambda/Lambda.thy	Sat Sep 02 21:53:03 2000 +0200
     8.2 +++ b/src/HOL/Lambda/Lambda.thy	Sat Sep 02 21:56:24 2000 +0200
     8.3 @@ -2,56 +2,205 @@
     8.4      ID:         $Id$
     8.5      Author:     Tobias Nipkow
     8.6      Copyright   1995 TU Muenchen
     8.7 -
     8.8 -Lambda-terms in de Bruijn notation,
     8.9 -substitution and beta-reduction.
    8.10  *)
    8.11  
    8.12 -Lambda = Main +
    8.13 +header {* Basic definitions of Lambda-calculus *}
    8.14 +
    8.15 +theory Lambda = Main:
    8.16 +
    8.17  
    8.18 -datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
    8.19 +subsection {* Lambda-terms in de Bruijn notation and substitution *}
    8.20 +
    8.21 +datatype dB =
    8.22 +    Var nat
    8.23 +  | App dB dB (infixl "$" 200)
    8.24 +  | Abs dB
    8.25  
    8.26  consts
    8.27 -  subst  :: [dB,dB,nat]=>dB ("_[_'/_]" [300,0,0] 300)
    8.28 -  lift   :: [dB,nat] => dB
    8.29 -  (* optimized versions *)
    8.30 -  substn :: [dB,dB,nat] => dB
    8.31 -  liftn  :: [nat,dB,nat] => dB
    8.32 +  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
    8.33 +  lift :: "[dB, nat] => dB"
    8.34  
    8.35  primrec
    8.36 -  "lift (Var i) k = (if i < k then Var i else Var(i+1))"
    8.37 -  "lift (s $ t) k = (lift s k) $ (lift t k)"
    8.38 -  "lift (Abs s) k = Abs(lift s (k+1))"
    8.39 +  "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
    8.40 +  "lift (s $ t) k = lift s k $ lift t k"
    8.41 +  "lift (Abs s) k = Abs (lift s (k + 1))"
    8.42 +
    8.43 +primrec  (* FIXME base names *)
    8.44 +  subst_Var: "(Var i)[s/k] =
    8.45 +    (if k < i then Var (i - 1) else if i = k then s else Var i)"
    8.46 +  subst_App: "(t $ u)[s/k] = t[s/k] $ u[s/k]"
    8.47 +  subst_Abs: "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
    8.48 +
    8.49 +declare subst_Var [simp del]
    8.50 +
    8.51 +text {* Optimized versions of @{term subst} and @{term lift}. *}
    8.52 +
    8.53 +consts
    8.54 +  substn :: "[dB, dB, nat] => dB"
    8.55 +  liftn :: "[nat, dB, nat] => dB"
    8.56 +
    8.57 +primrec
    8.58 +  "liftn n (Var i) k = (if i < k then Var i else Var (i + n))"
    8.59 +  "liftn n (s $ t) k = liftn n s k $ liftn n t k"
    8.60 +  "liftn n (Abs s) k = Abs (liftn n s (k + 1))"
    8.61  
    8.62  primrec
    8.63 -  subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
    8.64 -                            else if i = k then s else Var i)"
    8.65 -  subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
    8.66 -  subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / k+1])"
    8.67 +  "substn (Var i) s k =
    8.68 +    (if k < i then Var (i - 1) else if i = k then liftn k s 0 else Var i)"
    8.69 +  "substn (t $ u) s k = substn t s k $ substn u s k"
    8.70 +  "substn (Abs t) s k = Abs (substn t s (k + 1))"
    8.71  
    8.72 -primrec
    8.73 -  "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
    8.74 -  "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
    8.75 -  "liftn n (Abs s) k = Abs(liftn n s (k+1))"
    8.76 +
    8.77 +subsection {* Beta-reduction *}
    8.78  
    8.79 -primrec
    8.80 -  "substn (Var i) s k = (if k < i then Var(i-1)
    8.81 -                         else if i = k then liftn k s 0 else Var i)"
    8.82 -  "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
    8.83 -  "substn (Abs t) s k = Abs (substn t s (k+1))"
    8.84 +consts
    8.85 +  beta :: "(dB \<times> dB) set"
    8.86  
    8.87 -consts  beta :: "(dB * dB) set"
    8.88 -
    8.89 -syntax  "->", "->>" :: [dB,dB] => bool (infixl 50)
    8.90 -
    8.91 +syntax
    8.92 +  "_beta" :: "[dB, dB] => bool"  (infixl "->" 50)
    8.93 +  "_beta_rtrancl" :: "[dB, dB] => bool"  (infixl "->>" 50)
    8.94  translations
    8.95 -  "s -> t"  == "(s,t) : beta"
    8.96 -  "s ->> t" == "(s,t) : beta^*"
    8.97 +  "s -> t" == "(s,t) \<in> beta"
    8.98 +  "s ->> t" == "(s,t) \<in> beta^*"
    8.99  
   8.100  inductive beta
   8.101 -intrs
   8.102 -   beta  "(Abs s) $ t -> s[t/0]"
   8.103 -   appL  "s -> t ==> s$u -> t$u"
   8.104 -   appR  "s -> t ==> u$s -> u$t"
   8.105 -   abs   "s -> t ==> Abs s -> Abs t"
   8.106 -end
   8.107 +  intros [simp, intro!]
   8.108 +    beta: "Abs s $ t -> s[t/0]"
   8.109 +    appL: "s -> t ==> s $ u -> t $ u"
   8.110 +    appR: "s -> t ==> u $ s -> u $ t"
   8.111 +    abs: "s -> t ==> Abs s -> Abs t"
   8.112 +
   8.113 +inductive_cases beta_cases [elim!]:
   8.114 +  "Var i -> t"
   8.115 +  "Abs r -> s"
   8.116 +  "s $ t -> u"
   8.117 +
   8.118 +declare if_not_P [simp] not_less_eq [simp]
   8.119 +  -- {* don't add @{text "r_into_rtrancl[intro!]"} *}
   8.120 +
   8.121 +
   8.122 +subsection {* Congruence rules *}
   8.123 +
   8.124 +lemma rtrancl_beta_Abs [intro!]:
   8.125 +    "s ->> s' ==> Abs s ->> Abs s'"
   8.126 +  apply (erule rtrancl_induct)
   8.127 +   apply (blast intro: rtrancl_into_rtrancl)+
   8.128 +  done
   8.129 +
   8.130 +lemma rtrancl_beta_AppL:
   8.131 +    "s ->> s' ==> s $ t ->> s' $ t"
   8.132 +  apply (erule rtrancl_induct)
   8.133 +   apply (blast intro: rtrancl_into_rtrancl)+
   8.134 +  done
   8.135 +
   8.136 +lemma rtrancl_beta_AppR:
   8.137 +    "t ->> t' ==> s $ t ->> s $ t'"
   8.138 +  apply (erule rtrancl_induct)
   8.139 +   apply (blast intro: rtrancl_into_rtrancl)+
   8.140 +  done
   8.141 +
   8.142 +lemma rtrancl_beta_App [intro]:
   8.143 +    "[| s ->> s'; t ->> t' |] ==> s $ t ->> s' $ t'"
   8.144 +  apply (blast intro!: rtrancl_beta_AppL rtrancl_beta_AppR
   8.145 +    intro: rtrancl_trans)
   8.146 +  done
   8.147 +
   8.148 +
   8.149 +subsection {* Substitution-lemmas *}
   8.150 +
   8.151 +lemma subst_eq [simp]: "(Var k)[u/k] = u"
   8.152 +  apply (simp add: subst_Var)
   8.153 +  done
   8.154 +
   8.155 +lemma subst_gt [simp]: "i < j ==> (Var j)[u/i] = Var (j - 1)"
   8.156 +  apply (simp add: subst_Var)
   8.157 +  done
   8.158 +
   8.159 +lemma subst_lt [simp]: "j < i ==> (Var j)[u/i] = Var j"
   8.160 +  apply (simp add: subst_Var)
   8.161 +  done
   8.162 +
   8.163 +lemma lift_lift [rulify]:
   8.164 +    "\<forall>i k. i < k + 1 --> lift (lift t i) (Suc k) = lift (lift t k) i"
   8.165 +  apply (induct_tac t)
   8.166 +    apply auto
   8.167 +  done
   8.168 +
   8.169 +lemma lift_subst [simp]:
   8.170 +    "\<forall>i j s. j < i + 1 --> lift (t[s/j]) i = (lift t (i + 1)) [lift s i / j]"
   8.171 +  apply (induct_tac t)
   8.172 +    apply (simp_all add: diff_Suc subst_Var lift_lift split: nat.split)
   8.173 +  done
   8.174 +
   8.175 +lemma lift_subst_lt:
   8.176 +    "\<forall>i j s. i < j + 1 --> lift (t[s/j]) i = (lift t i) [lift s i / j + 1]"
   8.177 +  apply (induct_tac t)
   8.178 +    apply (simp_all add: subst_Var lift_lift)
   8.179 +  done
   8.180 +
   8.181 +lemma subst_lift [simp]:
   8.182 +    "\<forall>k s. (lift t k)[s/k] = t"
   8.183 +  apply (induct_tac t)
   8.184 +    apply simp_all
   8.185 +  done
   8.186 +
   8.187 +lemma subst_subst [rulify]:
   8.188 +    "\<forall>i j u v. i < j + 1 --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]"
   8.189 +  apply (induct_tac t)
   8.190 +    apply (simp_all
   8.191 +      add: diff_Suc subst_Var lift_lift [symmetric] lift_subst_lt
   8.192 +      split: nat.split)
   8.193 +  apply (auto elim: nat_neqE)
   8.194 +  done
   8.195 +
   8.196 +
   8.197 +subsection {* Equivalence proof for optimized substitution *}
   8.198 +
   8.199 +lemma liftn_0 [simp]: "\<forall>k. liftn 0 t k = t"
   8.200 +  apply (induct_tac t)
   8.201 +    apply (simp_all add: subst_Var)
   8.202 +  done
   8.203 +
   8.204 +lemma liftn_lift [simp]:
   8.205 +    "\<forall>k. liftn (Suc n) t k = lift (liftn n t k) k"
   8.206 +  apply (induct_tac t)
   8.207 +    apply (simp_all add: subst_Var)
   8.208 +  done
   8.209 +
   8.210 +lemma substn_subst_n [simp]:
   8.211 +    "\<forall>n. substn t s n = t[liftn n s 0 / n]"
   8.212 +  apply (induct_tac t)
   8.213 +    apply (simp_all add: subst_Var)
   8.214 +  done
   8.215 +
   8.216 +theorem substn_subst_0: "substn t s 0 = t[s/0]"
   8.217 +  apply simp
   8.218 +  done
   8.219 +
   8.220 +
   8.221 +subsection {* Preservation theorems *}
   8.222 +
   8.223 +text {* Not used in Church-Rosser proof, but in Strong
   8.224 +  Normalization. \medskip *}
   8.225 +
   8.226 +theorem subst_preserves_beta [rulify, simp]:
   8.227 +    "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
   8.228 +  apply (erule beta.induct)
   8.229 +     apply (simp_all add: subst_subst [symmetric])
   8.230 +  done
   8.231 +
   8.232 +theorem lift_preserves_beta [rulify, simp]:
   8.233 +    "r -> s ==> \<forall>i. lift r i -> lift s i"
   8.234 +  apply (erule beta.induct)
   8.235 +     apply auto
   8.236 +  done
   8.237 +
   8.238 +theorem subst_preserves_beta2 [rulify, simp]:
   8.239 +    "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
   8.240 +  apply (induct_tac t)
   8.241 +    apply (simp add: subst_Var r_into_rtrancl)
   8.242 +   apply (simp add: rtrancl_beta_App)
   8.243 +  apply (simp add: rtrancl_beta_Abs)
   8.244 +  done
   8.245 +
   8.246 +end
   8.247 \ No newline at end of file
     9.1 --- a/src/HOL/Lambda/ListApplication.ML	Sat Sep 02 21:53:03 2000 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,135 +0,0 @@
     9.4 -(*  Title:      HOL/Lambda/ListApplication.ML
     9.5 -    ID:         $Id$
     9.6 -    Author:     Tobias Nipkow
     9.7 -    Copyright   1998 TU Muenchen
     9.8 -*)
     9.9 -
    9.10 -Goal "(r$$ts = s$$ts) = (r = s)";
    9.11 -by (rev_induct_tac "ts" 1);
    9.12 -by (Auto_tac);
    9.13 -qed "apps_eq_tail_conv";
    9.14 -AddIffs [apps_eq_tail_conv];
    9.15 -
    9.16 -Goal "!s. (Var m = s$$ss) = (Var m = s & ss = [])";
    9.17 -by (induct_tac "ss" 1);
    9.18 -by (Auto_tac);
    9.19 -qed_spec_mp "Var_eq_apps_conv";
    9.20 -AddIffs [Var_eq_apps_conv];
    9.21 -
    9.22 -Goal "!ss. ((Var m)$$rs = (Var n)$$ss) = (m=n & rs=ss)";
    9.23 -by (rev_induct_tac "rs" 1);
    9.24 - by (Simp_tac 1);
    9.25 - by (Blast_tac 1);
    9.26 -by (rtac allI 1);
    9.27 -by (rev_induct_tac "ss" 1);
    9.28 -by (Auto_tac);
    9.29 -qed_spec_mp "Var_apps_eq_Var_apps_conv";
    9.30 -AddIffs [Var_apps_eq_Var_apps_conv];
    9.31 -
    9.32 -Goal "(r$s = t$$ts) = \
    9.33 -\     (if ts = [] then r$s = t \
    9.34 -\      else (? ss. ts = ss@[s] & r = t$$ss))";
    9.35 -by (res_inst_tac [("xs","ts")] rev_exhaust 1);
    9.36 -by (Auto_tac);
    9.37 -qed "App_eq_foldl_conv";
    9.38 -
    9.39 -Goal "(Abs r = s$$ss) = (Abs r = s & ss=[])";
    9.40 -by (rev_induct_tac "ss" 1);
    9.41 -by (Auto_tac);
    9.42 -qed "Abs_eq_apps_conv";
    9.43 -AddIffs [Abs_eq_apps_conv];
    9.44 -
    9.45 -Goal "(s$$ss = Abs r) = (s = Abs r & ss=[])";
    9.46 -by (rev_induct_tac "ss" 1);
    9.47 -by (Auto_tac);
    9.48 -qed "apps_eq_Abs_conv";
    9.49 -AddIffs [apps_eq_Abs_conv];
    9.50 -
    9.51 -Goal "!ss. ((Abs r)$$rs = (Abs s)$$ss) = (r=s & rs=ss)";
    9.52 -by (rev_induct_tac "rs" 1);
    9.53 - by (Simp_tac 1);
    9.54 - by (Blast_tac 1);
    9.55 -by (rtac allI 1);
    9.56 -by (rev_induct_tac "ss" 1);
    9.57 -by (Auto_tac);
    9.58 -qed_spec_mp "Abs_apps_eq_Abs_apps_conv";
    9.59 -AddIffs [Abs_apps_eq_Abs_apps_conv];
    9.60 -
    9.61 -Goal "!s t. Abs s $ t ~= (Var n)$$ss";
    9.62 -by (rev_induct_tac "ss" 1);
    9.63 -by (Auto_tac);
    9.64 -qed_spec_mp "Abs_App_neq_Var_apps";
    9.65 -AddIffs [Abs_App_neq_Var_apps];
    9.66 -
    9.67 -Goal "!ts. Var n $$ ts ~= (Abs r)$$ss";
    9.68 -by (rev_induct_tac "ss" 1);
    9.69 - by (Simp_tac 1);
    9.70 -by (rtac allI 1);
    9.71 -by (rev_induct_tac "ts" 1);
    9.72 -by (Auto_tac);
    9.73 -qed_spec_mp "Var_apps_neq_Abs_apps";
    9.74 -AddIffs [Var_apps_neq_Abs_apps];
    9.75 -
    9.76 -Goal "? ts h. t = h$$ts & ((? n. h = Var n) | (? u. h = Abs u))";
    9.77 -by (induct_tac "t" 1);
    9.78 -  by (res_inst_tac[("x","[]")] exI 1);
    9.79 -  by (Simp_tac 1);
    9.80 - by (Clarify_tac 1);
    9.81 - by (rename_tac "ts1 ts2 h1 h2" 1);
    9.82 - by (res_inst_tac[("x","ts1@[h2$$ts2]")] exI 1);
    9.83 - by (Simp_tac 1);
    9.84 -by (Simp_tac 1);
    9.85 -qed "ex_head_tail";
    9.86 -
    9.87 -Goal "size(r$$rs) = size r + foldl (op +) 0 (map size rs) + length rs";
    9.88 -by (rev_induct_tac "rs" 1);
    9.89 -by (Auto_tac);
    9.90 -qed "size_apps";
    9.91 -Addsimps [size_apps];
    9.92 -
    9.93 -Goal "[| (0::nat) < k; m <= n |] ==> m < n+k";
    9.94 -by (fast_arith_tac 1);
    9.95 -val lemma0 = result();
    9.96 -
    9.97 -(* a customized induction schema for $$ *)
    9.98 -
    9.99 -val prems = Goal
   9.100 -"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
   9.101 -\   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
   9.102 -\|] ==> !t. size t = n --> P t";
   9.103 -by (induct_thm_tac less_induct "n" 1);
   9.104 -by (rtac allI 1);
   9.105 -by (cut_inst_tac [("t","t")] ex_head_tail 1);
   9.106 -by (Clarify_tac 1);
   9.107 -by (etac disjE 1);
   9.108 - by (Clarify_tac 1);
   9.109 - by (resolve_tac prems 1);
   9.110 - by (Clarify_tac 1);
   9.111 - by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   9.112 - by (Simp_tac 1);
   9.113 - by (rtac lemma0 1);
   9.114 -  by (Force_tac 1);
   9.115 - by (rtac elem_le_sum 1);
   9.116 - by (Force_tac 1);
   9.117 -by (Clarify_tac 1);
   9.118 -by (resolve_tac prems 1);
   9.119 -by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   9.120 -by (Simp_tac 1);
   9.121 -by (Clarify_tac 1);
   9.122 -by (EVERY[etac allE 1, etac impE 1, etac allE 2, etac mp 2, rtac refl 2]);
   9.123 -by (Simp_tac 1);
   9.124 -by (rtac le_imp_less_Suc 1);
   9.125 -by (rtac trans_le_add1 1);
   9.126 -by (rtac trans_le_add2 1);
   9.127 -by (rtac elem_le_sum 1);
   9.128 -by (Force_tac 1);
   9.129 -val lemma = result() RS spec RS mp;
   9.130 -
   9.131 -val prems = Goal
   9.132 -"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
   9.133 -\   !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
   9.134 -\|] ==> P t";
   9.135 -by (res_inst_tac [("x1","t")] lemma 1);
   9.136 -by (rtac refl 3);
   9.137 -by (REPEAT(ares_tac prems 1));
   9.138 -qed "Apps_dB_induct";
    10.1 --- a/src/HOL/Lambda/ListApplication.thy	Sat Sep 02 21:53:03 2000 +0200
    10.2 +++ b/src/HOL/Lambda/ListApplication.thy	Sat Sep 02 21:56:24 2000 +0200
    10.3 @@ -2,9 +2,9 @@
    10.4      ID:         $Id$
    10.5      Author:     Tobias Nipkow
    10.6      Copyright   1998 TU Muenchen
    10.7 +*)
    10.8  
    10.9 -Application of a term to a list of terms
   10.10 -*)
   10.11 +header {* Application of a term to a list of terms *}
   10.12  
   10.13  theory ListApplication = Lambda:
   10.14  
   10.15 @@ -13,7 +13,6 @@
   10.16  translations
   10.17    "t $$ ts" == "foldl (op $) t ts"
   10.18  
   10.19 -
   10.20  lemma apps_eq_tail_conv [iff]: "(r $$ ts = s $$ ts) = (r = s)"
   10.21    apply (induct_tac ts rule: rev_induct)
   10.22     apply auto
   10.23 @@ -101,11 +100,12 @@
   10.24    apply simp
   10.25    done
   10.26  
   10.27 -text {* A customized induction schema for @{text "$$"} *}
   10.28 +
   10.29 +text {* \medskip A customized induction schema for @{text "$$"}. *}
   10.30  
   10.31  lemma lem [rulify]:
   10.32    "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   10.33 -      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   10.34 +    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   10.35    |] ==> \<forall>t. size t = n --> P t"
   10.36  proof -
   10.37    case antecedent
   10.38 @@ -145,9 +145,9 @@
   10.39      done
   10.40  qed
   10.41  
   10.42 -lemma Apps_dB_induct:
   10.43 +theorem Apps_dB_induct:
   10.44    "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
   10.45 -      !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   10.46 +    !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
   10.47    |] ==> P t"
   10.48  proof -
   10.49    case antecedent
   10.50 @@ -159,4 +159,4 @@
   10.51      done
   10.52  qed
   10.53  
   10.54 -end
   10.55 +end
   10.56 \ No newline at end of file
    11.1 --- a/src/HOL/Lambda/ListBeta.thy	Sat Sep 02 21:53:03 2000 +0200
    11.2 +++ b/src/HOL/Lambda/ListBeta.thy	Sat Sep 02 21:56:24 2000 +0200
    11.3 @@ -2,12 +2,16 @@
    11.4      ID:         $Id$
    11.5      Author:     Tobias Nipkow
    11.6      Copyright   1998 TU Muenchen
    11.7 -
    11.8 -Lifting beta-reduction to lists of terms, reducing exactly one element
    11.9  *)
   11.10  
   11.11 +header {* Lifting beta-reduction to lists *}
   11.12 +
   11.13  theory ListBeta = ListApplication + ListOrder:
   11.14  
   11.15 +text {*
   11.16 +  Lifting beta-reduction to lists of terms, reducing exactly one element.
   11.17 +*}
   11.18 +
   11.19  syntax
   11.20    "_list_beta" :: "dB => dB => bool"   (infixl "=>" 50)
   11.21  translations
   11.22 @@ -27,7 +31,6 @@
   11.23      apply (auto 0 3 intro: disjI2 [THEN append_step1I])
   11.24    done
   11.25  
   11.26 -
   11.27  lemma head_Var_reduction:
   11.28    "Var n $$ rs -> v ==> (\<exists>ss. rs => ss \<and> v = Var n $$ ss)"
   11.29    apply (drule head_Var_reduction_aux)
   11.30 @@ -44,33 +47,33 @@
   11.31       apply (case_tac r)
   11.32         apply simp
   11.33        apply (simp add: App_eq_foldl_conv)
   11.34 -      apply (simp only: split: split_if_asm)
   11.35 +      apply (split (asm) split_if_asm)
   11.36         apply simp
   11.37         apply blast
   11.38        apply simp
   11.39       apply (simp add: App_eq_foldl_conv)
   11.40 -     apply (simp only: split: split_if_asm)
   11.41 +     apply (split (asm) split_if_asm)
   11.42        apply simp
   11.43       apply simp
   11.44      apply (clarify del: disjCI)
   11.45      apply (drule App_eq_foldl_conv [THEN iffD1])
   11.46 -    apply (simp only: split: split_if_asm)
   11.47 +    apply (split (asm) split_if_asm)
   11.48       apply simp
   11.49       apply blast
   11.50      apply (force intro: disjI1 [THEN append_step1I])
   11.51     apply (clarify del: disjCI)
   11.52     apply (drule App_eq_foldl_conv [THEN iffD1])
   11.53 -   apply (simp only: split: split_if_asm)
   11.54 +   apply (split (asm) split_if_asm)
   11.55      apply simp
   11.56      apply blast
   11.57     apply (auto 0 3 intro: disjI2 [THEN append_step1I])
   11.58    done
   11.59  
   11.60  lemma apps_betasE [elim!]:
   11.61 -"[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
   11.62 -        !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
   11.63 -        !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
   11.64 -     ==> R"
   11.65 +  "[| r $$ rs -> s; !!r'. [| r -> r'; s = r' $$ rs |] ==> R;
   11.66 +    !!rs'. [| rs => rs'; s = r $$ rs' |] ==> R;
   11.67 +    !!t u us. [| r = Abs t; rs = u # us; s = t[u/0] $$ us |] ==> R |]
   11.68 +  ==> R"
   11.69  proof -
   11.70    assume major: "r $$ rs -> s"
   11.71    case antecedent
   11.72 @@ -94,7 +97,7 @@
   11.73    done
   11.74  
   11.75  lemma apps_preserves_betas [rulify, simp]:
   11.76 -  "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
   11.77 +    "\<forall>ss. rs => ss --> r $$ rs -> r $$ ss"
   11.78    apply (induct_tac rs rule: rev_induct)
   11.79     apply simp
   11.80    apply simp
   11.81 @@ -106,4 +109,4 @@
   11.82    apply blast
   11.83    done
   11.84  
   11.85 -end
   11.86 +end
   11.87 \ No newline at end of file
    12.1 --- a/src/HOL/Lambda/ListOrder.thy	Sat Sep 02 21:53:03 2000 +0200
    12.2 +++ b/src/HOL/Lambda/ListOrder.thy	Sat Sep 02 21:56:24 2000 +0200
    12.3 @@ -2,16 +2,22 @@
    12.4      ID:         $Id$
    12.5      Author:     Tobias Nipkow
    12.6      Copyright   1998 TU Muenchen
    12.7 -
    12.8 -Lifting an order to lists of elements, relating exactly one element
    12.9  *)
   12.10  
   12.11 +header {* Lifting an order to lists of elements *}
   12.12 +
   12.13  theory ListOrder = Acc:
   12.14  
   12.15 +text {*
   12.16 +  Lifting an order to lists of elements, relating exactly one
   12.17 +  element.
   12.18 +*}
   12.19 +
   12.20  constdefs
   12.21    step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
   12.22    "step1 r ==
   12.23 -    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = us @ z' # vs}"
   12.24 +    {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys =
   12.25 +      us @ z' # vs}"
   12.26  
   12.27  
   12.28  lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
   12.29 @@ -34,7 +40,8 @@
   12.30    done
   12.31  
   12.32  lemma Cons_step1_Cons [iff]:
   12.33 -  "((y # ys, x # xs) \<in> step1 r) = ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
   12.34 +    "((y # ys, x # xs) \<in> step1 r) =
   12.35 +      ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
   12.36    apply (unfold step1_def)
   12.37    apply simp
   12.38    apply (rule iffI)
   12.39 @@ -59,8 +66,8 @@
   12.40  
   12.41  lemma Cons_step1E [rulify_prems, elim!]:
   12.42    "[| (ys, x # xs) \<in> step1 r;
   12.43 -      \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
   12.44 -      \<forall>zs. ys = x # zs --> (zs, xs) : step1 r --> R
   12.45 +    \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
   12.46 +    \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
   12.47     |] ==> R"
   12.48    apply (case_tac ys)
   12.49     apply (simp add: step1_def)
   12.50 @@ -98,7 +105,8 @@
   12.51    apply (fast dest: acc_downward)
   12.52    done
   12.53  
   12.54 -lemma ex_step1I: "[| x \<in> set xs; (y, x) \<in> r |]
   12.55 +lemma ex_step1I:
   12.56 +  "[| x \<in> set xs; (y, x) \<in> r |]
   12.57      ==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
   12.58    apply (unfold step1_def)
   12.59    apply (drule in_set_conv_decomp [THEN iffD1])
   12.60 @@ -113,4 +121,4 @@
   12.61    apply blast
   12.62    done
   12.63  
   12.64 -end
   12.65 +end
   12.66 \ No newline at end of file
    13.1 --- a/src/HOL/Lambda/ParRed.ML	Sat Sep 02 21:53:03 2000 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,100 +0,0 @@
    13.4 -(*  Title:      HOL/Lambda/ParRed.ML
    13.5 -    ID:         $Id$
    13.6 -    Author:     Tobias Nipkow
    13.7 -    Copyright   1995 TU Muenchen
    13.8 -
    13.9 -Properties of => and cd, in particular the diamond property of => and
   13.10 -confluence of beta.
   13.11 -*)
   13.12 -
   13.13 -Addsimps par_beta.intrs;
   13.14 -
   13.15 -val par_beta_cases = 
   13.16 -    map par_beta.mk_cases
   13.17 -       ["Var n => t", 
   13.18 -	"Abs s => Abs t",
   13.19 -	"(Abs s) $ t => u", 
   13.20 -	"s $ t => u", 
   13.21 -	"Abs s => t"];
   13.22 -
   13.23 -AddSIs par_beta.intrs;
   13.24 -AddSEs par_beta_cases;
   13.25 -
   13.26 -(*** beta <= par_beta <= beta^* ***)
   13.27 -
   13.28 -Goal "(Var n => t) = (t = Var n)";
   13.29 -by (Blast_tac 1);
   13.30 -qed "par_beta_varL";
   13.31 -Addsimps [par_beta_varL];
   13.32 -
   13.33 -Goal "t => t";
   13.34 -by (induct_tac "t" 1);
   13.35 -by (ALLGOALS Asm_simp_tac);
   13.36 -qed"par_beta_refl";
   13.37 -Addsimps [par_beta_refl];
   13.38 -(* AddSIs [par_beta_refl]; causes search to blow up *)
   13.39 -
   13.40 -Goal "beta <= par_beta";
   13.41 -by (rtac subsetI 1);
   13.42 -by (split_all_tac 1);
   13.43 -by (etac beta.induct 1);
   13.44 -by (ALLGOALS(blast_tac (claset() addSIs [par_beta_refl])));
   13.45 -qed "beta_subset_par_beta";
   13.46 -
   13.47 -Goal "par_beta <= beta^*";
   13.48 -by (rtac subsetI 1);
   13.49 -by (split_all_tac 1);
   13.50 -by (etac par_beta.induct 1);
   13.51 -by (Blast_tac 1);
   13.52 -(* rtrancl_refl complicates the proof by increasing the branching factor*)
   13.53 -by (ALLGOALS (blast_tac (claset() delrules [rtrancl_refl]
   13.54 -				 addIs [rtrancl_into_rtrancl])));
   13.55 -qed "par_beta_subset_beta";
   13.56 -
   13.57 -(*** => ***)
   13.58 -
   13.59 -Goal "!t' n. t => t' --> lift t n => lift t' n";
   13.60 -by (induct_tac "t" 1);
   13.61 -by (ALLGOALS(fast_tac (claset() addss (simpset()))));
   13.62 -qed_spec_mp "par_beta_lift";
   13.63 -Addsimps [par_beta_lift];
   13.64 -
   13.65 -Goal
   13.66 -  "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
   13.67 -by (induct_tac "t" 1);
   13.68 -  by (asm_simp_tac (addsplit(simpset())) 1);
   13.69 - by (strip_tac 1);
   13.70 - by (eresolve_tac par_beta_cases 1);
   13.71 -  by (Asm_simp_tac 1);
   13.72 - by (asm_simp_tac (simpset() addsimps [subst_subst RS sym]) 1);
   13.73 - by (fast_tac (claset() addSIs [par_beta_lift] addss (simpset())) 1);
   13.74 -by (fast_tac (claset() addss (simpset())) 1);
   13.75 -qed_spec_mp "par_beta_subst";
   13.76 -
   13.77 -(*** Confluence (directly) ***)
   13.78 -
   13.79 -Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)";
   13.80 -by (rtac (impI RS allI RS allI) 1);
   13.81 -by (etac par_beta.induct 1);
   13.82 -by (ALLGOALS(blast_tac (claset() addSIs [par_beta_subst])));
   13.83 -qed "diamond_par_beta";
   13.84 -
   13.85 -
   13.86 -(*** cd ***)
   13.87 -
   13.88 -Goal "!t. s => t --> t => cd s";
   13.89 -by (induct_thm_tac cd.induct "s" 1);
   13.90 -by (Auto_tac);
   13.91 -by (fast_tac (claset() addSIs [par_beta_subst]) 1);
   13.92 -qed_spec_mp "par_beta_cd";
   13.93 -
   13.94 -(*** Confluence (via cd) ***)
   13.95 -
   13.96 -Goalw [diamond_def,commute_def,square_def] "diamond(par_beta)";
   13.97 -by (blast_tac (claset() addIs [par_beta_cd]) 1);
   13.98 -qed "diamond_par_beta2";
   13.99 -
  13.100 -Goal "confluent(beta)";
  13.101 -by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
  13.102 -			     par_beta_subset_beta, beta_subset_par_beta]) 1);
  13.103 -qed"beta_confluent";
    14.1 --- a/src/HOL/Lambda/ParRed.thy	Sat Sep 02 21:53:03 2000 +0200
    14.2 +++ b/src/HOL/Lambda/ParRed.thy	Sat Sep 02 21:56:24 2000 +0200
    14.3 @@ -3,32 +3,131 @@
    14.4      Author:     Tobias Nipkow
    14.5      Copyright   1995 TU Muenchen
    14.6  
    14.7 -Parallel reduction and a complete developments function "cd".
    14.8 +Properties of => and "cd", in particular the diamond property of => and
    14.9 +confluence of beta.
   14.10  *)
   14.11  
   14.12 -ParRed = Lambda + Commutation +
   14.13 +header {* Parallel reduction and a complete developments *}
   14.14  
   14.15 -consts  par_beta :: "(dB * dB) set"
   14.16 +theory ParRed = Lambda + Commutation:
   14.17 +
   14.18 +
   14.19 +subsection {* Parallel reduction *}
   14.20  
   14.21 -syntax  "=>" :: [dB,dB] => bool (infixl 50)
   14.22 +consts
   14.23 +  par_beta :: "(dB \<times> dB) set"
   14.24  
   14.25 +syntax
   14.26 +  par_beta :: "[dB, dB] => bool"  (infixl "=>" 50)
   14.27  translations
   14.28 -  "s => t" == "(s,t) : par_beta"
   14.29 +  "s => t" == "(s, t) \<in> par_beta"
   14.30  
   14.31  inductive par_beta
   14.32 -  intrs
   14.33 -    var   "Var n => Var n"
   14.34 -    abs   "s => t ==> Abs s => Abs t"
   14.35 -    app   "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
   14.36 -    beta  "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
   14.37 +  intros [simp, intro!]
   14.38 +    var: "Var n => Var n"
   14.39 +    abs: "s => t ==> Abs s => Abs t"
   14.40 +    app: "[| s => s'; t => t' |] ==> s $ t => s' $ t'"
   14.41 +    beta: "[| s => s'; t => t' |] ==> (Abs s) $ t => s'[t'/0]"
   14.42 +
   14.43 +inductive_cases par_beta_cases [elim!]:
   14.44 +  "Var n => t"
   14.45 +  "Abs s => Abs t"
   14.46 +  "(Abs s) $ t => u"
   14.47 +  "s $ t => u"
   14.48 +  "Abs s => t"
   14.49 +
   14.50 +
   14.51 +subsection {* Inclusions *}
   14.52 +
   14.53 +text {* @{text "beta \<subseteq> par_beta \<subseteq> beta^*"} \medskip *}
   14.54 +
   14.55 +lemma par_beta_varL [simp]:
   14.56 +    "(Var n => t) = (t = Var n)"
   14.57 +  apply blast
   14.58 +  done
   14.59 +
   14.60 +lemma par_beta_refl [simp]: "t => t"  (* par_beta_refl [intro!] causes search to blow up *)
   14.61 +  apply (induct_tac t)
   14.62 +    apply simp_all
   14.63 +  done
   14.64 +
   14.65 +lemma beta_subset_par_beta: "beta <= par_beta"
   14.66 +  apply (rule subsetI)
   14.67 +  apply clarify
   14.68 +  apply (erule beta.induct)
   14.69 +     apply (blast intro!: par_beta_refl)+
   14.70 +  done
   14.71 +
   14.72 +lemma par_beta_subset_beta: "par_beta <= beta^*"
   14.73 +  apply (rule subsetI)
   14.74 +  apply clarify
   14.75 +  apply (erule par_beta.induct)
   14.76 +     apply blast
   14.77 +    apply (blast del: rtrancl_refl intro: rtrancl_into_rtrancl)+
   14.78 +      -- {* @{thm[source] rtrancl_refl} complicates the proof by increasing the branching factor *}
   14.79 +  done
   14.80 +
   14.81 +
   14.82 +subsection {* Misc properties of par-beta *}
   14.83 +
   14.84 +lemma par_beta_lift [rulify, simp]:
   14.85 +    "\<forall>t' n. t => t' --> lift t n => lift t' n"
   14.86 +  apply (induct_tac t)
   14.87 +    apply fastsimp+
   14.88 +  done
   14.89 +
   14.90 +lemma par_beta_subst [rulify]:
   14.91 +    "\<forall>s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]"
   14.92 +  apply (induct_tac t)
   14.93 +    apply (simp add: subst_Var)
   14.94 +   apply (intro strip)
   14.95 +   apply (erule par_beta_cases)
   14.96 +    apply simp
   14.97 +   apply (simp add: subst_subst [symmetric])
   14.98 +   apply (fastsimp intro!: par_beta_lift)
   14.99 +  apply fastsimp
  14.100 +  done
  14.101 +
  14.102 +
  14.103 +subsection {* Confluence (directly) *}
  14.104 +
  14.105 +lemma diamond_par_beta: "diamond par_beta"
  14.106 +  apply (unfold diamond_def commute_def square_def)
  14.107 +  apply (rule impI [THEN allI [THEN allI]])
  14.108 +  apply (erule par_beta.induct)
  14.109 +     apply (blast intro!: par_beta_subst)+
  14.110 +  done
  14.111 +
  14.112 +
  14.113 +subsection {* Complete developments *}
  14.114  
  14.115  consts
  14.116 -  cd  :: dB => dB
  14.117 +  "cd" :: "dB => dB"
  14.118 +recdef "cd" "measure size"
  14.119 +  "cd (Var n) = Var n"
  14.120 +  "cd (Var n $ t) = Var n $ cd t"
  14.121 +  "cd ((s1 $ s2) $ t) = cd (s1 $ s2) $ cd t"
  14.122 +  "cd (Abs u $ t) = (cd u)[cd t/0]"
  14.123 +  "cd (Abs s) = Abs (cd s)"
  14.124 +
  14.125 +lemma par_beta_cd [rulify]:
  14.126 +    "\<forall>t. s => t --> t => cd s"
  14.127 +  apply (induct_tac s rule: cd.induct)
  14.128 +      apply auto
  14.129 +  apply (fast intro!: par_beta_subst)
  14.130 +  done
  14.131  
  14.132 -recdef cd "measure size"
  14.133 -  "cd(Var n) = Var n"
  14.134 -  "cd(Var n     $ t) = Var n $ cd t"
  14.135 -  "cd((s1 $ s2) $ t) = cd(s1 $ s2) $ cd t"
  14.136 -  "cd(Abs u     $ t) = (cd u)[cd t/0]"
  14.137 -  "cd(Abs s) = Abs(cd s)"
  14.138 -end
  14.139 +
  14.140 +subsection {* Confluence (via complete developments) *}
  14.141 +
  14.142 +lemma diamond_par_beta2: "diamond par_beta"
  14.143 +  apply (unfold diamond_def commute_def square_def)
  14.144 +  apply (blast intro: par_beta_cd)
  14.145 +  done
  14.146 +
  14.147 +theorem beta_confluent: "confluent beta"
  14.148 +  apply (rule diamond_par_beta2 diamond_to_confluence
  14.149 +    par_beta_subset_beta beta_subset_par_beta)+
  14.150 +  done
  14.151 +
  14.152 +end
  14.153 \ No newline at end of file
    15.1 --- a/src/HOL/Lambda/Type.thy	Sat Sep 02 21:53:03 2000 +0200
    15.2 +++ b/src/HOL/Lambda/Type.thy	Sat Sep 02 21:56:24 2000 +0200
    15.3 @@ -2,34 +2,40 @@
    15.4      ID:         $Id$
    15.5      Author:     Stefan Berghofer
    15.6      Copyright   2000 TU Muenchen
    15.7 +*)
    15.8  
    15.9 -Simply-typed lambda terms.  Subject reduction and strong normalization
   15.10 -of simply-typed lambda terms.  Partly based on a paper proof by Ralph
   15.11 -Matthes.
   15.12 -*)
   15.13 +header {* Simply-typed lambda terms: subject reduction and strong
   15.14 +  normalization *}
   15.15  
   15.16  theory Type = InductTermi:
   15.17  
   15.18 +text_raw {*
   15.19 +  \footnote{Formalization by Stefan Berghofer.  Partly based on a
   15.20 +  paper proof by Ralph Matthes.}
   15.21 +*}
   15.22 +
   15.23 +
   15.24 +subsection {* Types and typing rules *}
   15.25 +
   15.26  datatype type =
   15.27      Atom nat
   15.28 -  | Fun type type     (infixr "=>" 200)
   15.29 +  | Fun type type  (infixr "=>" 200)
   15.30  
   15.31  consts
   15.32    typing :: "((nat => type) \<times> dB \<times> type) set"
   15.33  
   15.34  syntax
   15.35 -  "_typing" :: "[nat => type, dB, type] => bool"   ("_ |- _ : _" [50,50,50] 50)
   15.36 -  "_funs"   :: "[type list, type] => type"         (infixl "=>>" 150)
   15.37 -
   15.38 +  "_typing" :: "[nat => type, dB, type] => bool"  ("_ |- _ : _" [50,50,50] 50)
   15.39 +  "_funs" :: "[type list, type] => type"  (infixl "=>>" 150)
   15.40  translations
   15.41 -  "env |- t : T" == "(env, t, T) : typing"
   15.42 +  "env |- t : T" == "(env, t, T) \<in> typing"
   15.43    "Ts =>> T" == "foldr Fun Ts T"
   15.44  
   15.45  inductive typing
   15.46 -intros [intro!]
   15.47 -  Var: "env x = T ==> env |- Var x : T"
   15.48 -  Abs: "(nat_case T env) |- t : U ==> env |- (Abs t) : (T => U)"
   15.49 -  App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
   15.50 +  intros [intro!]
   15.51 +    Var: "env x = T ==> env |- Var x : T"
   15.52 +    Abs: "(nat_case T env) |- t : U ==> env |- Abs t : (T => U)"
   15.53 +    App: "env |- s : T => U ==> env |- t : T ==> env |- (s $ t) : U"
   15.54  
   15.55  inductive_cases [elim!]:
   15.56    "e |- Var i : T"
   15.57 @@ -46,12 +52,12 @@
   15.58      | T # Ts => e |- t : T \<and> types e ts Ts)"
   15.59  
   15.60  inductive_cases [elim!]:
   15.61 -  "x # xs : lists S"
   15.62 +  "x # xs \<in> lists S"
   15.63  
   15.64  declare IT.intros [intro!]
   15.65  
   15.66  
   15.67 -text {* Some tests. *}
   15.68 +subsection {* Some examples *}
   15.69  
   15.70  lemma "\<exists>T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \<and> U = T"
   15.71    apply (intro exI conjI)
   15.72 @@ -66,7 +72,7 @@
   15.73    done
   15.74  
   15.75  
   15.76 -text {* n-ary function types *}
   15.77 +text {* Iterated function types *}
   15.78  
   15.79  lemma list_app_typeD [rulify]:
   15.80      "\<forall>t T. e |- t $$ ts : T --> (\<exists>Ts. e |- t : Ts =>> T \<and> types e ts Ts)"
   15.81 @@ -85,7 +91,7 @@
   15.82    done
   15.83  
   15.84  lemma list_app_typeI [rulify]:
   15.85 -  "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
   15.86 +    "\<forall>t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T"
   15.87    apply (induct_tac ts)
   15.88     apply (intro strip)
   15.89     apply simp
   15.90 @@ -104,7 +110,7 @@
   15.91    done
   15.92  
   15.93  lemma lists_types [rulify]:
   15.94 -    "\<forall>Ts. types e ts Ts --> ts : lists {t. \<exists>T. e |- t : T}"
   15.95 +    "\<forall>Ts. types e ts Ts --> ts \<in> lists {t. \<exists>T. e |- t : T}"
   15.96    apply (induct_tac ts)
   15.97     apply (intro strip)
   15.98     apply (case_tac Ts)
   15.99 @@ -121,7 +127,7 @@
  15.100    done
  15.101  
  15.102  
  15.103 -text {* lifting preserves termination and well-typedness *}
  15.104 +subsection {* Lifting preserves termination and well-typedness *}
  15.105  
  15.106  lemma lift_map [rulify, simp]:
  15.107      "\<forall>t. lift (t $$ ts) i = lift t i $$ map (\<lambda>t. lift t i) ts"
  15.108 @@ -136,7 +142,7 @@
  15.109    done
  15.110  
  15.111  lemma lift_IT [rulify, intro!]:
  15.112 -    "t : IT ==> \<forall>i. lift t i : IT"
  15.113 +    "t \<in> IT ==> \<forall>i. lift t i \<in> IT"
  15.114    apply (erule IT.induct)
  15.115      apply (rule allI)
  15.116      apply (simp (no_asm))
  15.117 @@ -156,14 +162,14 @@
  15.118     done
  15.119  
  15.120  lemma lifts_IT [rulify]:
  15.121 -    "ts : lists IT --> map (\<lambda>t. lift t 0) ts : lists IT"
  15.122 +    "ts \<in> lists IT --> map (\<lambda>t. lift t 0) ts \<in> lists IT"
  15.123    apply (induct_tac ts)
  15.124     apply auto
  15.125    done
  15.126  
  15.127  
  15.128  lemma shift_env [simp]:
  15.129 - "nat_case T
  15.130 +  "nat_case T
  15.131      (\<lambda>j. if j < i then e j else if j = i then Ua else e (j - 1)) =
  15.132      (\<lambda>j. if j < Suc i then nat_case T e j else if j = Suc i then Ua
  15.133            else nat_case T e (j - 1))"
  15.134 @@ -184,7 +190,7 @@
  15.135    done
  15.136  
  15.137  lemma lift_type [intro!]:
  15.138 -  "e |- t : T ==> nat_case U e |- lift t 0 : T"
  15.139 +    "e |- t : T ==> nat_case U e |- lift t 0 : T"
  15.140    apply (subgoal_tac
  15.141      "nat_case U e =
  15.142        (\<lambda>j. if j < 0 then e j
  15.143 @@ -211,10 +217,10 @@
  15.144    done
  15.145  
  15.146  
  15.147 -text {* substitution lemma *}
  15.148 +subsection {* Substitution lemmas *}
  15.149  
  15.150  lemma subst_lemma [rulify]:
  15.151 - "e |- t : T ==> \<forall>e' i U u.
  15.152 +  "e |- t : T ==> \<forall>e' i U u.
  15.153      e = (\<lambda>j. if j < i then e' j
  15.154                else if j = i then U
  15.155                else e' (j-1)) -->
  15.156 @@ -257,7 +263,7 @@
  15.157    done
  15.158  
  15.159  
  15.160 -text {* subject reduction *}
  15.161 +subsection {* Subject reduction *}
  15.162  
  15.163  lemma subject_reduction [rulify]:
  15.164      "e |- t : T ==> \<forall>t'. t -> t' --> e |- t' : T"
  15.165 @@ -277,15 +283,16 @@
  15.166       apply auto
  15.167    done
  15.168  
  15.169 -text {* additional lemmas *}
  15.170 +
  15.171 +subsection {* Additional lemmas *}
  15.172  
  15.173  lemma app_last: "(t $$ ts) $ u = t $$ (ts @ [u])"
  15.174    apply simp
  15.175    done
  15.176  
  15.177 -lemma subst_Var_IT [rulify]: "r : IT ==> \<forall>i j. r[Var i/j] : IT"
  15.178 +lemma subst_Var_IT [rulify]: "r \<in> IT ==> \<forall>i j. r[Var i/j] \<in> IT"
  15.179    apply (erule IT.induct)
  15.180 -    txt {* @{term Var} *}
  15.181 +    txt {* Case @{term Var}: *}
  15.182      apply (intro strip)
  15.183      apply (simp (no_asm) add: subst_Var)
  15.184      apply
  15.185 @@ -300,12 +307,12 @@
  15.186        rule lists.Cons,
  15.187        fast,
  15.188        assumption)+
  15.189 -   txt {* @{term Lambda} *}
  15.190 +   txt {* Case @{term Lambda}: *}
  15.191     apply (intro strip)
  15.192     apply simp
  15.193     apply (rule IT.Lambda)
  15.194     apply fast
  15.195 -  txt {* @{term Beta} *}
  15.196 +  txt {* Case @{term Beta}: *}
  15.197    apply (intro strip)
  15.198    apply (simp (no_asm_use) add: subst_subst [symmetric])
  15.199    apply (rule IT.Beta)
  15.200 @@ -319,7 +326,7 @@
  15.201    apply (rule lists.Nil)
  15.202    done
  15.203  
  15.204 -lemma app_Var_IT: "t : IT ==> t $ Var i : IT"
  15.205 +lemma app_Var_IT: "t \<in> IT ==> t $ Var i \<in> IT"
  15.206    apply (erule IT.induct)
  15.207      apply (subst app_last)
  15.208      apply (rule IT.Var)
  15.209 @@ -338,22 +345,22 @@
  15.210    done
  15.211  
  15.212  
  15.213 -text {* Well-typed substitution preserves termination. *}
  15.214 +subsection {* Well-typed substitution preserves termination *}
  15.215  
  15.216  lemma subst_type_IT [rulify]:
  15.217 -  "\<forall>t. t : IT --> (\<forall>e T u i.
  15.218 +  "\<forall>t. t \<in> IT --> (\<forall>e T u i.
  15.219      (\<lambda>j. if j < i then e j
  15.220            else if j = i then U
  15.221            else e (j - 1)) |- t : T -->
  15.222 -    u : IT --> e |- u : U --> t[u/i] : IT)"
  15.223 +    u \<in> IT --> e |- u : U --> t[u/i] \<in> IT)"
  15.224    apply (rule_tac f = size and a = U in measure_induct)
  15.225    apply (rule allI)
  15.226    apply (rule impI)
  15.227    apply (erule IT.induct)
  15.228 -    txt {* @{term Var} *}
  15.229 +    txt {* Case @{term Var}: *}
  15.230      apply (intro strip)
  15.231      apply (case_tac "n = i")
  15.232 -     txt {* @{term "n = i"} *}
  15.233 +     txt {* Case @{term "n = i"}: *}
  15.234       apply (case_tac rs)
  15.235        apply simp
  15.236       apply simp
  15.237 @@ -363,14 +370,14 @@
  15.238       apply (ind_cases "e |- Var i : T")
  15.239       apply (drule_tac s = "(?T::type) => ?U" in sym)
  15.240       apply simp
  15.241 -     apply (subgoal_tac "lift u 0 $ Var 0 : IT")
  15.242 +     apply (subgoal_tac "lift u 0 $ Var 0 \<in> IT")
  15.243        prefer 2
  15.244        apply (rule app_Var_IT)
  15.245        apply (erule lift_IT)
  15.246 -     apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] : IT")
  15.247 +     apply (subgoal_tac "(lift u 0 $ Var 0)[a[u/i]/0] \<in> IT")
  15.248        apply (simp (no_asm_use))
  15.249        apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0)
  15.250 -        (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] : IT")
  15.251 +        (map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] \<in> IT")
  15.252         apply (simp (no_asm_use) del: map_compose
  15.253  	 add: map_compose [symmetric] o_def)
  15.254        apply (erule_tac x = "Ts =>> T" in allE)
  15.255 @@ -383,7 +390,7 @@
  15.256         apply (rule lifts_IT)
  15.257         apply (drule lists_types)
  15.258         apply
  15.259 -        (ind_cases "x # xs : lists (Collect P)",
  15.260 +        (ind_cases "x # xs \<in> lists (Collect P)",
  15.261           erule lists_IntI [THEN lists.induct],
  15.262           assumption)
  15.263          apply fastsimp
  15.264 @@ -409,21 +416,21 @@
  15.265        apply (rule typing.Var)
  15.266        apply simp
  15.267       apply (fast intro!: subst_lemma)
  15.268 -    txt {* @{term "n ~= i"} *}
  15.269 +    txt {* Case @{term "n ~= i"}: *}
  15.270      apply (drule list_app_typeD)
  15.271      apply (erule exE)
  15.272      apply (erule conjE)
  15.273      apply (drule lists_types)
  15.274 -    apply (subgoal_tac "map (\<lambda>x. x[u/i]) rs : lists IT")
  15.275 +    apply (subgoal_tac "map (\<lambda>x. x[u/i]) rs \<in> lists IT")
  15.276       apply (simp add: subst_Var)
  15.277       apply fast
  15.278      apply (erule lists_IntI [THEN lists.induct])
  15.279        apply assumption
  15.280       apply fastsimp
  15.281      apply fastsimp
  15.282 -   txt {* @{term Lambda} *}
  15.283 +   txt {* Case @{term Lambda}: *}
  15.284     apply fastsimp
  15.285 -  txt {* @{term Beta} *}
  15.286 +  txt {* Case @{term Beta}: *}
  15.287    apply (intro strip)
  15.288    apply (simp (no_asm))
  15.289    apply (rule IT.Beta)
  15.290 @@ -437,13 +444,13 @@
  15.291    done
  15.292  
  15.293  
  15.294 -text {* main theorem: well-typed terms are strongly normalizing *}
  15.295 +subsection {* Main theorem: well-typed terms are strongly normalizing *}
  15.296  
  15.297 -lemma type_implies_IT: "e |- t : T ==> t : IT"
  15.298 +lemma type_implies_IT: "e |- t : T ==> t \<in> IT"
  15.299    apply (erule typing.induct)
  15.300      apply (rule Var_IT)
  15.301     apply (erule IT.Lambda)
  15.302 -  apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT")
  15.303 +  apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] \<in> IT")
  15.304     apply simp
  15.305    apply (rule subst_type_IT)
  15.306    apply (rule lists.Nil
  15.307 @@ -458,9 +465,9 @@
  15.308    apply assumption
  15.309    done
  15.310  
  15.311 -theorem type_implies_termi: "e |- t : T ==> t : termi beta"
  15.312 +theorem type_implies_termi: "e |- t : T ==> t \<in> termi beta"
  15.313    apply (rule IT_implies_termi)
  15.314    apply (erule type_implies_IT)
  15.315    done
  15.316  
  15.317 -end
  15.318 +end
  15.319 \ No newline at end of file
    16.1 --- a/src/HOL/README.html	Sat Sep 02 21:53:03 2000 +0200
    16.2 +++ b/src/HOL/README.html	Sat Sep 02 21:56:24 2000 +0200
    16.3 @@ -54,7 +54,7 @@
    16.4  <DD>several introductory Isabelle/Isar examples
    16.5  
    16.6  <DT>Lambda
    16.7 -<DD>a proof of the Church-Rosser theorem for lambda-calculus
    16.8 +<DD>fundamental properties of lambda-calculus (Church-Rosser and termination)
    16.9  
   16.10  <DT>Lex
   16.11  <DD>verification of a simple lexical analyzer generator