--- 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 \
--- 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";
--- 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 ==> \<forall>t. t : termi beta -->
+ (\<forall>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' \<and> s=s' \<and> 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
--- 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 \<in> IT"
apply (subgoal_tac "Var n $$ [] \<in> 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 (\<lambda>t. lift t 0) (map (\<lambda>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)