# HG changeset patch # User wenzelm # Date 967503444 -7200 # Node ID 9be481b4bc852eab8c0edaa4f11d0412efce5483 # Parent 5705a04d24eaa8162c9b26d2f325d11b6f620540 Lambda/InductTermi made new-style theory; tuned; diff -r 5705a04d24ea -r 9be481b4bc85 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Aug 29 00:56:22 2000 +0200 +++ b/src/HOL/IsaMakefile Tue Aug 29 00:57:24 2000 +0200 @@ -8,10 +8,10 @@ default: HOL images: HOL HOL-Real TLA -test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \ +test: HOL-Isar_examples HOL-Induct HOL-Lambda HOL-ex HOL-Subst HOL-IMP HOL-IMPP \ HOL-NumberTheory HOL-Hoare HOL-Lex HOL-Algebra \ HOL-Auth HOL-UNITY HOL-Modelcheck \ - HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \ + HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \ HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \ HOL-AxClasses-Tutorial HOL-Real-ex \ HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory @@ -304,7 +304,7 @@ 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.ML \ + Lambda/Commutation.thy Lambda/Eta.ML Lambda/Eta.thy \ Lambda/InductTermi.thy Lambda/Lambda.ML Lambda/Lambda.thy \ Lambda/ListApplication.ML Lambda/ListApplication.thy Lambda/ListBeta.ML \ Lambda/ListBeta.thy Lambda/ListOrder.ML Lambda/ListOrder.thy \ diff -r 5705a04d24ea -r 9be481b4bc85 src/HOL/Lambda/InductTermi.ML --- a/src/HOL/Lambda/InductTermi.ML Tue Aug 29 00:56:22 2000 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,102 +0,0 @@ -(* Title: HOL/Lambda/InductTermi.ML - ID: $Id$ - Author: Tobias Nipkow - Copyright 1998 TU Muenchen -*) - -(*** Every term in IT terminates ***) - -Goal "s : termi beta ==> !t. t : termi beta --> \ -\ (!r ss. t = r[s/0]$$ss --> Abs r $ s $$ ss : termi beta)"; -by (etac acc_induct 1); -by (etac thin_rl 1); -by (rtac allI 1); -by (rtac impI 1); -by (etac acc_induct 1); -by (Clarify_tac 1); -by (rtac accI 1); -by (safe_tac (claset() addSEs [apps_betasE])); - by (assume_tac 1); - by (blast_tac (claset() addIs [subst_preserves_beta,apps_preserves_beta]) 1); - by (blast_tac (claset() - addIs [apps_preserves_beta2,subst_preserves_beta2,rtrancl_converseI] - addDs [acc_downwards]) 1); -(* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) -by (blast_tac (claset() addDs [apps_preserves_betas]) 1); -qed_spec_mp "double_induction_lemma"; - -Goal "t : IT ==> t : termi(beta)"; -by (etac IT.induct 1); - by (dtac rev_subsetD 1); - by (rtac lists_mono 1); - by (rtac Int_lower2 1); - by (Asm_full_simp_tac 1); - by (dtac lists_accD 1); - by (etac acc_induct 1); - by (rtac accI 1); - by (blast_tac (claset() addSDs [head_Var_reduction]) 1); - by (etac acc_induct 1); - by (rtac accI 1); - by (Blast_tac 1); -by (blast_tac (claset() addIs [double_induction_lemma]) 1); -qed "IT_implies_termi"; - -(*** Every terminating term is in IT ***) - -Addsimps [Var_apps_neq_Abs_apps RS not_sym]; - -Goal "Var n $$ ss ~= Abs r $ s $$ ts"; -by (simp_tac (simpset() addsimps [foldl_Cons RS sym] - delsimps [foldl_Cons]) 1); -qed "Var_apps_neq_Abs_app_apps"; -Addsimps [Var_apps_neq_Abs_app_apps, - Var_apps_neq_Abs_app_apps RS not_sym]; - - -Goal "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' & s=s' & ss=ss')"; -by (simp_tac (simpset() addsimps [foldl_Cons RS sym] - delsimps [foldl_Cons]) 1); -qed "Abs_apps_eq_Abs_app_apps"; -Addsimps [Abs_apps_eq_Abs_app_apps]; - -val IT_cases = - map IT.mk_cases - ["Var n $$ ss : IT", "Abs t : IT", "Abs r $ s $$ ts : IT"]; -AddSEs IT_cases; - - -Goal "r : termi beta ==> r : IT"; -by (etac acc_induct 1); -by (rename_tac "r" 1); -by (etac thin_rl 1); -by (etac rev_mp 1); -by (Simp_tac 1); -by (res_inst_tac [("t","r")] Apps_dB_induct 1); - by (rename_tac "n ts" 1); - by (Clarify_tac 1); - by (resolve_tac IT.intrs 1); - by (Clarify_tac 1); - by (EVERY1[dtac bspec, atac]); - by (etac mp 1); - by (Clarify_tac 1); - by (dtac converseI 1); - by (EVERY1[dtac ex_step1I, atac]); - by (Clarify_tac 1); - by (rename_tac "us" 1); - by (eres_inst_tac [("x","Var n $$ us")] allE 1); - by (Force_tac 1); -by (rename_tac "u ts" 1); -by (case_tac "ts" 1); - by (Asm_full_simp_tac 1); - by (blast_tac (claset() addIs IT.intrs) 1); -by (rename_tac "s ss" 1); -by (Asm_full_simp_tac 1); -by (Clarify_tac 1); -by (resolve_tac IT.intrs 1); - by (blast_tac (claset() addIs [apps_preserves_beta]) 1); -by (etac mp 1); - by (Clarify_tac 1); - by (rename_tac "t" 1); - by (eres_inst_tac [("x","Abs u $ t $$ ss")] allE 1); - by (Force_tac 1); -qed "termi_implies_IT"; diff -r 5705a04d24ea -r 9be481b4bc85 src/HOL/Lambda/InductTermi.thy --- a/src/HOL/Lambda/InductTermi.thy Tue Aug 29 00:56:22 2000 +0200 +++ b/src/HOL/Lambda/InductTermi.thy Tue Aug 29 00:57:24 2000 +0200 @@ -9,14 +9,108 @@ Also rediscovered by Matthes and Joachimski. *) -InductTermi = ListBeta + +theory InductTermi = ListBeta: -consts IT :: dB set +consts + IT :: "dB set" + inductive IT -intrs -VarI "rs : lists IT ==> (Var n)$$rs : IT" -LambdaI "r : IT ==> Abs r : IT" -BetaI "[| (r[s/0])$$ss : IT; s : IT |] ==> (Abs r $ s)$$ss : IT" -monos lists_mono + 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" + monos lists_mono (* FIXME move to HOL!? *) + + +text {* Every term in IT terminates. *} + +lemma double_induction_lemma [rulify]: + "s : termi beta ==> \t. t : termi beta --> + (\r ss. t = r[s/0] $$ ss --> Abs r $ s $$ ss : termi beta)" + apply (erule acc_induct) + apply (erule thin_rl) + apply (rule allI) + apply (rule impI) + apply (erule acc_induct) + apply clarify + apply (rule accI) + apply (tactic {* safe_tac (claset () addSEs [apps_betasE]) *}) -- FIXME + apply assumption + apply (blast intro: subst_preserves_beta apps_preserves_beta) + apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI + dest: acc_downwards) (* FIXME: acc_downwards can be replaced by acc(R ^* ) = acc(r) *) + apply (blast dest: apps_preserves_betas) + done + +lemma IT_implies_termi: "t : IT ==> t : termi beta" + apply (erule IT.induct) + apply (drule rev_subsetD) + apply (rule lists_mono) + apply (rule Int_lower2) + apply simp + apply (drule lists_accD) + apply (erule acc_induct) + apply (rule accI) + apply (blast dest: head_Var_reduction) + apply (erule acc_induct) + apply (rule accI) + apply blast + apply (blast intro: double_induction_lemma) + done + + +text {* Every terminating term is in IT *} + +declare Var_apps_neq_Abs_apps [THEN not_sym, simp] + +lemma [simp, THEN not_sym, simp]: "Var n $$ ss ~= Abs r $ s $$ ts" + apply (simp add: foldl_Cons [symmetric] del: foldl_Cons) + done + +lemma [simp]: + "(Abs r $ s $$ ss = Abs r' $ s' $$ ss') = (r=r' \ s=s' \ ss=ss')" + apply (simp add: foldl_Cons [symmetric] del: foldl_Cons) + done + +inductive_cases [elim!]: + "Var n $$ ss : IT" + "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) + apply (erule thin_rl) + apply (erule rev_mp) + apply simp + apply (rule_tac t = r in Apps_dB_induct) + apply clarify + apply (rule IT.intros) + apply clarify + apply (drule bspec, assumption) + apply (erule mp) + apply clarify + apply (drule converseI) + apply (drule ex_step1I, assumption) + apply clarify + apply (rename_tac us) + apply (erule_tac x = "Var n $$ us" in allE) + apply force + apply (rename_tac u ts) + apply (case_tac ts) + apply simp + apply (blast intro: IT.intros) + apply (rename_tac s ss) + apply simp + apply clarify + apply (rule IT.intros) + apply (blast intro: apps_preserves_beta) + apply (erule mp) + apply clarify + apply (rename_tac t) + apply (erule_tac x = "Abs u $ t $$ ss" in allE) + apply force + done end diff -r 5705a04d24ea -r 9be481b4bc85 src/HOL/Lambda/Type.thy --- a/src/HOL/Lambda/Type.thy Tue Aug 29 00:56:22 2000 +0200 +++ b/src/HOL/Lambda/Type.thy Tue Aug 29 00:57:24 2000 +0200 @@ -143,7 +143,7 @@ apply (rule conjI) apply (rule impI, - rule IT.VarI, + rule IT.Var, erule lists.induct, simp (no_asm), rule lists.Nil, @@ -290,7 +290,7 @@ apply (simp (no_asm) add: subst_Var) apply ((rule conjI impI)+, - rule IT.VarI, + rule IT.Var, erule lists.induct, simp (no_asm), rule lists.Nil, @@ -303,35 +303,35 @@ txt {* @{term Lambda} *} apply (intro strip) apply simp - apply (rule IT.LambdaI) + apply (rule IT.Lambda) apply fast txt {* @{term Beta} *} apply (intro strip) apply (simp (no_asm_use) add: subst_subst [symmetric]) - apply (rule IT.BetaI) + apply (rule IT.Beta) apply auto done lemma Var_IT: "Var n \ IT" apply (subgoal_tac "Var n $$ [] \ IT") apply simp - apply (rule IT.VarI) + apply (rule IT.Var) apply (rule lists.Nil) done lemma app_Var_IT: "t : IT ==> t $ Var i : IT" apply (erule IT.induct) apply (subst app_last) - apply (rule IT.VarI) + apply (rule IT.Var) apply simp apply (rule lists.Cons) apply (rule Var_IT) apply (rule lists.Nil) - apply (rule IT.BetaI [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]]) + apply (rule IT.Beta [where ?ss = "[]", unfold foldl_Nil [THEN eq_reflection]]) apply (erule subst_Var_IT) apply (rule Var_IT) apply (subst app_last) - apply (rule IT.BetaI) + apply (rule IT.Beta) apply (subst app_last [symmetric]) apply assumption apply assumption @@ -378,7 +378,7 @@ apply (erule_tac x = "Var 0 $$ map (\t. lift t 0) (map (\t. t[u/i]) list)" in allE) apply (erule impE) - apply (rule IT.VarI) + apply (rule IT.Var) apply (rule lifts_IT) apply (drule lists_types) apply @@ -425,7 +425,7 @@ txt {* @{term Beta} *} apply (intro strip) apply (simp (no_asm)) - apply (rule IT.BetaI) + apply (rule IT.Beta) apply (simp (no_asm) del: subst_map add: subst_subst subst_map [symmetric]) apply (drule subject_reduction) apply (rule apps_preserves_beta) @@ -441,11 +441,11 @@ lemma type_implies_IT: "e |- t : T ==> t : IT" apply (erule typing.induct) apply (rule Var_IT) - apply (erule IT.LambdaI) + apply (erule IT.Lambda) apply (subgoal_tac "(Var 0 $ lift t 0)[s/0] : IT") apply simp apply (rule subst_type_IT) - apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.VarI], unfold foldl_Nil [THEN eq_reflection] + apply (rule lists.Nil [THEN 2 lists.Cons [THEN IT.Var], unfold foldl_Nil [THEN eq_reflection] foldl_Cons [THEN eq_reflection]]) apply (erule lift_IT) apply (rule typing.App)