--- a/src/HOL/IsaMakefile Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/IsaMakefile Fri Sep 01 00:30:25 2000 +0200
@@ -306,8 +306,7 @@
$(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 \
- Lambda/ListApplication.ML Lambda/ListApplication.thy \
- Lambda/ListBeta.thy Lambda/ListOrder.ML Lambda/ListOrder.thy \
+ Lambda/ListApplication.thy Lambda/ListBeta.thy Lambda/ListOrder.thy \
Lambda/ParRed.ML Lambda/ParRed.thy Lambda/Type.thy Lambda/ROOT.ML
@$(ISATOOL) usedir $(OUT)/HOL Lambda
--- a/src/HOL/Lambda/InductTermi.thy Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/InductTermi.thy Fri Sep 01 00:30:25 2000 +0200
@@ -19,7 +19,6 @@
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. *}
@@ -34,7 +33,7 @@
apply (erule acc_induct)
apply clarify
apply (rule accI)
- apply (tactic {* safe_tac (claset () addSEs [thm "apps_betasE"]) *}) -- FIXME
+ apply (safe elim!: apps_betasE)
apply assumption
apply (blast intro: subst_preserves_beta apps_preserves_beta)
apply (blast intro: apps_preserves_beta2 subst_preserves_beta2 rtrancl_converseI
--- a/src/HOL/Lambda/ListApplication.thy Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Fri Sep 01 00:30:25 2000 +0200
@@ -6,9 +6,157 @@
Application of a term to a list of terms
*)
-ListApplication = Lambda +
+theory ListApplication = Lambda:
+
+syntax
+ "_list_application" :: "dB => dB list => dB" (infixl "$$" 150)
+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
+ done
+
+lemma Var_eq_apps_conv [rulify, iff]:
+ "\<forall>s. (Var m = s $$ ss) = (Var m = s \<and> ss = [])"
+ apply (induct_tac ss)
+ apply auto
+ done
+
+lemma Var_apps_eq_Var_apps_conv [rulify, iff]:
+ "\<forall>ss. (Var m $$ rs = Var n $$ ss) = (m = n \<and> rs = ss)"
+ apply (induct_tac rs rule: rev_induct)
+ apply simp
+ apply blast
+ apply (rule allI)
+ apply (induct_tac ss rule: rev_induct)
+ apply auto
+ done
+
+lemma App_eq_foldl_conv:
+ "(r $ s = t $$ ts) =
+ (if ts = [] then r $ s = t
+ else (\<exists>ss. ts = ss @ [s] \<and> r = t $$ ss))"
+ apply (rule_tac xs = ts in rev_exhaust)
+ apply auto
+ done
+
+lemma Abs_eq_apps_conv [iff]:
+ "(Abs r = s $$ ss) = (Abs r = s \<and> ss = [])"
+ apply (induct_tac ss rule: rev_induct)
+ apply auto
+ done
+
+lemma apps_eq_Abs_conv [iff]: "(s $$ ss = Abs r) = (s = Abs r \<and> ss = [])"
+ apply (induct_tac ss rule: rev_induct)
+ apply auto
+ done
+
+lemma Abs_apps_eq_Abs_apps_conv [iff]:
+ "\<forall>ss. (Abs r $$ rs = Abs s $$ ss) = (r = s \<and> rs = ss)"
+ apply (induct_tac rs rule: rev_induct)
+ apply simp
+ apply blast
+ apply (rule allI)
+ apply (induct_tac ss rule: rev_induct)
+ apply auto
+ done
+
+lemma Abs_App_neq_Var_apps [iff]:
+ "\<forall>s t. Abs s $ t ~= Var n $$ ss"
+ apply (induct_tac ss rule: rev_induct)
+ apply auto
+ done
+
+lemma Var_apps_neq_Abs_apps [rulify, iff]:
+ "\<forall>ts. Var n $$ ts ~= Abs r $$ ss"
+ apply (induct_tac ss rule: rev_induct)
+ apply simp
+ apply (rule allI)
+ apply (induct_tac ts rule: rev_induct)
+ apply auto
+ done
-syntax "$$" :: dB => dB list => dB (infixl 150)
-translations "t $$ ts" == "foldl op$ t ts"
+lemma ex_head_tail:
+ "\<exists>ts h. t = h $$ ts \<and> ((\<exists>n. h = Var n) \<or> (\<exists>u. h = Abs u))"
+ apply (induct_tac t)
+ apply (rule_tac x = "[]" in exI)
+ apply simp
+ apply clarify
+ apply (rename_tac ts1 ts2 h1 h2)
+ apply (rule_tac x = "ts1 @ [h2 $$ ts2]" in exI)
+ apply simp
+ apply simp
+ done
+
+lemma size_apps [simp]:
+ "size (r $$ rs) = size r + foldl (op +) 0 (map size rs) + length rs"
+ apply (induct_tac rs rule: rev_induct)
+ apply auto
+ done
+
+lemma lem0: "[| (0::nat) < k; m <= n |] ==> m < n + k"
+ apply simp
+ done
+
+text {* A customized induction schema for @{text "$$"} *}
+
+lemma lem [rulify]:
+ "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
+ !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+ |] ==> \<forall>t. size t = n --> P t"
+proof -
+ case antecedent
+ show ?thesis
+ apply (induct_tac n rule: less_induct)
+ apply (rule allI)
+ apply (cut_tac t = t in ex_head_tail)
+ apply clarify
+ apply (erule disjE)
+ apply clarify
+ apply (rule prems)
+ apply clarify
+ apply (erule allE, erule impE)
+ prefer 2
+ apply (erule allE, erule mp, rule refl)
+ apply simp
+ apply (rule lem0)
+ apply force
+ apply (rule elem_le_sum)
+ apply force
+ apply clarify
+ apply (rule prems)
+ apply (erule allE, erule impE)
+ prefer 2
+ apply (erule allE, erule mp, rule refl)
+ apply simp
+ apply clarify
+ apply (erule allE, erule impE)
+ prefer 2
+ apply (erule allE, erule mp, rule refl)
+ apply simp
+ apply (rule le_imp_less_Suc)
+ apply (rule trans_le_add1)
+ apply (rule trans_le_add2)
+ apply (rule elem_le_sum)
+ apply force
+ done
+qed
+
+lemma Apps_dB_induct:
+ "[| !!n ts. \<forall>t \<in> set ts. P t ==> P (Var n $$ ts);
+ !!u ts. [| P u; \<forall>t \<in> set ts. P t |] ==> P (Abs u $$ ts)
+ |] ==> P t"
+proof -
+ case antecedent
+ show ?thesis
+ apply (rule_tac t = t in lem)
+ prefer 3
+ apply (rule refl)
+ apply (assumption | rule prems)+
+ done
+qed
end
--- a/src/HOL/Lambda/ListBeta.thy Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Fri Sep 01 00:30:25 2000 +0200
@@ -24,8 +24,7 @@
apply (rule allI)
apply (rule_tac xs = rs in rev_exhaust)
apply simp
- apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I], simpset()) 0 3 *})
- -- FIXME
+ apply (auto 0 3 intro: disjI2 [THEN append_step1I])
done
@@ -37,9 +36,9 @@
lemma apps_betasE_aux:
"u -> u' ==> \<forall>r rs. u = r $$ rs -->
- ((\<exists>r'. r -> r' \<and> u' = r'$$rs) \<or>
- (\<exists>rs'. rs => rs' \<and> u' = r$$rs') \<or>
- (\<exists>s t ts. r = Abs s \<and> rs = t#ts \<and> u' = s[t/0]$$ts))"
+ ((\<exists>r'. r -> r' \<and> u' = r' $$ rs) \<or>
+ (\<exists>rs'. rs => rs' \<and> u' = r $$ rs') \<or>
+ (\<exists>s t ts. r = Abs s \<and> rs = t # ts \<and> u' = s[t/0] $$ ts))"
apply (erule beta.induct)
apply (clarify del: disjCI)
apply (case_tac r)
@@ -64,8 +63,7 @@
apply (simp only: split: split_if_asm)
apply simp
apply blast
- apply (tactic {* mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3 *})
- -- FIXME
+ apply (auto 0 3 intro: disjI2 [THEN append_step1I])
done
lemma apps_betasE [elim!]:
--- a/src/HOL/Lambda/ListOrder.thy Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/ListOrder.thy Fri Sep 01 00:30:25 2000 +0200
@@ -6,11 +6,111 @@
Lifting an order to lists of elements, relating exactly one element
*)
-ListOrder = Acc +
+theory ListOrder = Acc:
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}"
+ step1 :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
+ "step1 r ==
+ {(ys, xs). \<exists>us z z' vs. xs = us @ z # vs \<and> (z', z) \<in> r \<and> ys = us @ z' # vs}"
+
+
+lemma step1_converse [simp]: "step1 (r^-1) = (step1 r)^-1"
+ apply (unfold step1_def)
+ apply blast
+ done
+
+lemma in_step1_converse [iff]: "(p \<in> step1 (r^-1)) = (p \<in> (step1 r)^-1)"
+ apply auto
+ done
+
+lemma not_Nil_step1 [iff]: "([], xs) \<notin> step1 r"
+ apply (unfold step1_def)
+ apply blast
+ done
+
+lemma not_step1_Nil [iff]: "(xs, []) \<notin> step1 r"
+ apply (unfold step1_def)
+ apply blast
+ done
+
+lemma Cons_step1_Cons [iff]:
+ "((y # ys, x # xs) \<in> step1 r) = ((y, x) \<in> r \<and> xs = ys \<or> x = y \<and> (ys, xs) \<in> step1 r)"
+ apply (unfold step1_def)
+ apply simp
+ apply (rule iffI)
+ apply (erule exE)
+ apply (rename_tac ts)
+ apply (case_tac ts)
+ apply force
+ apply force
+ apply (erule disjE)
+ apply blast
+ apply (blast intro: Cons_eq_appendI)
+ done
+
+lemma append_step1I:
+ "(ys, xs) \<in> step1 r \<and> vs = us \<or> ys = xs \<and> (vs, us) \<in> step1 r
+ ==> (ys @ vs, xs @ us) : step1 r"
+ apply (unfold step1_def)
+ apply auto
+ apply blast
+ apply (blast intro: append_eq_appendI)
+ done
+
+lemma Cons_step1E [rulify_prems, elim!]:
+ "[| (ys, x # xs) \<in> step1 r;
+ \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
+ \<forall>zs. ys = x # zs --> (zs, xs) : step1 r --> R
+ |] ==> R"
+ apply (case_tac ys)
+ apply (simp add: step1_def)
+ apply blast
+ done
+
+lemma Snoc_step1_SnocD:
+ "(ys @ [y], xs @ [x]) \<in> step1 r
+ ==> ((ys, xs) \<in> step1 r \<and> y = x \<or> ys = xs \<and> (y, x) \<in> r)"
+ apply (unfold step1_def)
+ apply simp
+ apply (clarify del: disjCI)
+ apply (rename_tac vs)
+ apply (rule_tac xs = vs in rev_exhaust)
+ apply force
+ apply simp
+ apply blast
+ done
+
+lemma Cons_acc_step1I [rulify, intro!]:
+ "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
+ apply (erule acc_induct)
+ apply (erule thin_rl)
+ apply clarify
+ apply (erule acc_induct)
+ apply (rule accI)
+ apply blast
+ done
+
+lemma lists_accD: "xs \<in> lists (acc r) ==> xs \<in> acc (step1 r)"
+ apply (erule lists.induct)
+ apply (rule accI)
+ apply simp
+ apply (rule accI)
+ apply (fast dest: acc_downward)
+ done
+
+lemma ex_step1I: "[| x \<in> set xs; (y, x) \<in> r |]
+ ==> \<exists>ys. (ys, xs) \<in> step1 r \<and> y \<in> set ys"
+ apply (unfold step1_def)
+ apply (drule in_set_conv_decomp [THEN iffD1])
+ apply force
+ done
+
+lemma lists_accI: "xs \<in> acc (step1 r) ==> xs \<in> lists (acc r)"
+ apply (erule acc_induct)
+ apply clarify
+ apply (rule accI)
+ apply (drule ex_step1I, assumption)
+ apply blast
+ done
end
--- a/src/HOL/Lambda/Type.thy Fri Sep 01 00:29:12 2000 +0200
+++ b/src/HOL/Lambda/Type.thy Fri Sep 01 00:30:25 2000 +0200
@@ -371,7 +371,8 @@
apply (simp (no_asm_use))
apply (subgoal_tac "(Var 0 $$ map (\<lambda>t. lift t 0)
(map (\<lambda>t. t[u/i]) list))[(u $ a[u/i])/0] : IT")
- apply (simp (no_asm_use) del: map_compose add: map_compose [symmetric] o_def)
+ apply (simp (no_asm_use) del: map_compose
+ add: map_compose [symmetric] o_def)
apply (erule_tac x = "Ts =>> T" in allE)
apply (erule impE)
apply simp
@@ -445,8 +446,9 @@
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.Var], unfold foldl_Nil [THEN eq_reflection]
- foldl_Cons [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)
apply (rule typing.Var)