# HG changeset patch # User wenzelm # Date 967924584 -7200 # Node ID 39ffdb8cab03266e8ea9afda2dccb66ee136805a # Parent 7e785df2b76ac7f2e8815c970e1849e9295b9217 HOL/Lambda: converted into new-style theory and document; diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/IsaMakefile --- 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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/Commutation.ML --- 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"; diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/Commutation.thy --- 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 \ 'a) set, ('a \ 'a) set, ('a \ 'a) set, ('a \ 'a) set] => bool" + "square R S T U == + \x y. (x, y) \ R --> (\z. (x, z) \ S --> (\u. (y, u) \ T \ (z, u) \ U))" + + commute :: "[('a \ 'a) set, ('a \ 'a) set] => bool" + "commute R S == square R S S R" + + diamond :: "('a \ 'a) set => bool" + "diamond R == commute R R" + + Church_Rosser :: "('a \ 'a) set => bool" + "Church_Rosser R == + \x y. (x, y) \ (R \ R^-1)^* --> (\z. (x, z) \ R^* \ (y, z) \ R^*)" + +syntax + confluent :: "('a \ '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 \ T' |] ==> square R S T' U" + apply (unfold square_def) + apply blast + done + +lemma square_reflcl: + "[| square R S T (R^=); S \ 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 \ 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 \ 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 \ 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 \ R; R \ 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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/Eta.ML --- 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 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"; diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/Eta.thy --- 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 \ free t i)" + "free (Abs s) i = free s (i + 1)" +consts + eta :: "(dB \ 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) \ eta" + "s -e>> t" == "(s,t) \ eta^*" + "s -e>= t" == "(s,t) \ 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: "\ 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]: + "\i t u. \ free s i --> s[t/i] = s[u/i]" + apply (induct_tac s) + apply (simp_all add: subst_Var) + done + +lemma free_lift [simp]: + "\i k. free (lift t k) i = + (i < k \ free t i \ k < i \ free t (i - 1))" + apply (induct_tac t) + apply (auto cong: conj_cong) + apply arith + done + +lemma free_subst [simp]: + "\i k t. free (s[t/k]) i = + (free s k \ free t i \ 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 ==> \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; \ free s i |] ==> \ free t i" + apply (simp add: free_eta) + done + +lemma eta_subst [rulify, simp]: + "s -e> t ==> \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 ==> \i. free t i --> free s i" + apply (erule beta.induct) + apply simp_all + done + +lemma beta_subst [rulify, intro]: + "s -> t ==> \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]: "\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 ==> \i. lift s i -e> lift t i" + apply (erule eta.induct) + apply simp_all + done + +lemma rtrancl_eta_subst [rulify]: + "\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 \ 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]: + "\i. (\ free s i) = (\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: + "(\s u. (\ free s 0) --> R (Abs (s $ Var 0)) (s[u/0])) = + (\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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/InductTermi.thy --- 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 ==> \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' \ s=s' \ ss=ss')" + "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r = r' \ s = s' \ 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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/Lambda.ML --- 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 (Var j)[u/i] = Var(j-1)"; -by (asm_full_simp_tac(addsplit(simpset())) 1); -qed "subst_gt"; - -Goal "j (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]; diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/Lambda.thy --- 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 \ 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) \ beta" + "s ->> t" == "(s,t) \ 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]: + "\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]: + "\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: + "\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]: + "\k s. (lift t k)[s/k] = t" + apply (induct_tac t) + apply simp_all + done + +lemma subst_subst [rulify]: + "\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]: "\k. liftn 0 t k = t" + apply (induct_tac t) + apply (simp_all add: subst_Var) + done + +lemma liftn_lift [simp]: + "\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]: + "\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 ==> \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 ==> \i. lift r i -> lift s i" + apply (erule beta.induct) + apply auto + done + +theorem subst_preserves_beta2 [rulify, simp]: + "\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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/ListApplication.ML --- 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"; diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/ListApplication.thy --- 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. \t \ set ts. P t ==> P (Var n $$ ts); - !!u ts. [| P u; \t \ set ts. P t |] ==> P (Abs u $$ ts) + !!u ts. [| P u; \t \ set ts. P t |] ==> P (Abs u $$ ts) |] ==> \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. \t \ set ts. P t ==> P (Var n $$ ts); - !!u ts. [| P u; \t \ set ts. P t |] ==> P (Abs u $$ ts) + !!u ts. [| P u; \t \ 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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/ListBeta.thy --- 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 ==> (\ss. rs => ss \ 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]: - "\ss. rs => ss --> r $$ rs -> r $$ ss" + "\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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/ListOrder.thy --- 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 \ 'a) set => ('a list \ 'a list) set" "step1 r == - {(ys, xs). \us z z' vs. xs = us @ z # vs \ (z', z) \ r \ ys = us @ z' # vs}" + {(ys, xs). \us z z' vs. xs = us @ z # vs \ (z', z) \ r \ 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) \ step1 r) = ((y, x) \ r \ xs = ys \ x = y \ (ys, xs) \ step1 r)" + "((y # ys, x # xs) \ step1 r) = + ((y, x) \ r \ xs = ys \ x = y \ (ys, xs) \ step1 r)" apply (unfold step1_def) apply simp apply (rule iffI) @@ -59,8 +66,8 @@ lemma Cons_step1E [rulify_prems, elim!]: "[| (ys, x # xs) \ step1 r; - \y. ys = y # xs --> (y, x) \ r --> R; - \zs. ys = x # zs --> (zs, xs) : step1 r --> R + \y. ys = y # xs --> (y, x) \ r --> R; + \zs. ys = x # zs --> (zs, xs) \ 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 \ set xs; (y, x) \ r |] +lemma ex_step1I: + "[| x \ set xs; (y, x) \ r |] ==> \ys. (ys, xs) \ step1 r \ y \ 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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/ParRed.ML --- 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"; diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/ParRed.thy --- 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 \ dB) set" +syntax + par_beta :: "[dB, dB] => bool" (infixl "=>" 50) translations - "s => t" == "(s,t) : par_beta" + "s => t" == "(s, t) \ 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 \ par_beta \ 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]: + "\t' n. t => t' --> lift t n => lift t' n" + apply (induct_tac t) + apply fastsimp+ + done + +lemma par_beta_subst [rulify]: + "\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]: + "\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 diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/Lambda/Type.thy --- 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) \ dB \ 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) \ 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 \ types e ts Ts)" inductive_cases [elim!]: - "x # xs : lists S" + "x # xs \ lists S" declare IT.intros [intro!] -text {* Some tests. *} +subsection {* Some examples *} lemma "\T U. e |- Abs (Abs (Abs (Var 1 $ (Var 2 $ Var 1 $ Var 0)))) : T \ 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]: "\t T. e |- t $$ ts : T --> (\Ts. e |- t : Ts =>> T \ types e ts Ts)" @@ -85,7 +91,7 @@ done lemma list_app_typeI [rulify]: - "\t T Ts. e |- t : Ts =>> T --> types e ts Ts --> e |- t $$ ts : T" + "\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]: - "\Ts. types e ts Ts --> ts : lists {t. \T. e |- t : T}" + "\Ts. types e ts Ts --> ts \ lists {t. \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]: "\t. lift (t $$ ts) i = lift t i $$ map (\t. lift t i) ts" @@ -136,7 +142,7 @@ done lemma lift_IT [rulify, intro!]: - "t : IT ==> \i. lift t i : IT" + "t \ IT ==> \i. lift t i \ 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 (\t. lift t 0) ts : lists IT" + "ts \ lists IT --> map (\t. lift t 0) ts \ lists IT" apply (induct_tac ts) apply auto done lemma shift_env [simp]: - "nat_case T + "nat_case T (\j. if j < i then e j else if j = i then Ua else e (j - 1)) = (\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 = (\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 ==> \e' i U u. + "e |- t : T ==> \e' i U u. e = (\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 ==> \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 ==> \i j. r[Var i/j] : IT" +lemma subst_Var_IT [rulify]: "r \ IT ==> \i j. r[Var i/j] \ 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 \ IT ==> t $ Var i \ 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]: - "\t. t : IT --> (\e T u i. + "\t. t \ IT --> (\e T u i. (\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 \ IT --> e |- u : U --> t[u/i] \ 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 \ 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] \ IT") apply (simp (no_asm_use)) apply (subgoal_tac "(Var 0 $$ map (\t. lift t 0) - (map (\t. t[u/i]) list))[(u $ a[u/i])/0] : IT") + (map (\t. t[u/i]) list))[(u $ a[u/i])/0] \ 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 \ 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 (\x. x[u/i]) rs : lists IT") + apply (subgoal_tac "map (\x. x[u/i]) rs \ 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 \ 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] \ 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 \ termi beta" apply (rule IT_implies_termi) apply (erule type_implies_IT) done -end +end \ No newline at end of file diff -r 7e785df2b76a -r 39ffdb8cab03 src/HOL/README.html --- 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 @@
several introductory Isabelle/Isar examples
Lambda -
a proof of the Church-Rosser theorem for lambda-calculus +
fundamental properties of lambda-calculus (Church-Rosser and termination)
Lex
verification of a simple lexical analyzer generator