author berghofe Tue Mar 25 09:58:51 2003 +0100 (2003-03-25) changeset 13883 0451e0fb3f22 parent 13882 2266550ab316 child 13884 5affbaee6b18
Re-structured some proofs in order to get rid of rule_format attribute.
 src/HOL/List.thy file | annotate | diff | revisions
1.1 --- a/src/HOL/List.thy	Tue Mar 25 09:56:01 2003 +0100
1.2 +++ b/src/HOL/List.thy	Tue Mar 25 09:58:51 2003 +0100
1.3 @@ -225,11 +225,9 @@
1.4  lemma lists_mono [mono]: "A \<subseteq> B ==> lists A \<subseteq> lists B"
1.5  by (unfold lists.defs) (blast intro!: lfp_mono)
1.7 -lemma lists_IntI [rule_format]:
1.8 -"l: lists A ==> l: lists B --> l: lists (A Int B)"
1.9 -apply (erule lists.induct)
1.10 -apply blast+
1.11 -done
1.12 +lemma lists_IntI:
1.13 +  assumes l: "l: lists A" shows "l: lists B ==> l: lists (A Int B)" using l
1.14 +  by induct blast+
1.16  lemma lists_Int_eq [simp]: "lists (A \<inter> B) = lists A \<inter> lists B"
1.17  apply (rule mono_Int [THEN equalityI])
1.18 @@ -292,15 +290,13 @@
1.19  lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
1.20  by (induct xs) auto
1.22 -lemma append_eq_append_conv [rule_format, simp]:
1.23 - "\<forall>ys. length xs = length ys \<or> length us = length vs
1.24 - --> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
1.25 -apply (induct_tac xs)
1.26 - apply(rule allI)
1.27 +lemma append_eq_append_conv [simp]:
1.28 + "!!ys. length xs = length ys \<or> length us = length vs
1.29 + ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
1.30 +apply (induct xs)
1.31   apply (case_tac ys)
1.32  apply simp
1.33   apply force
1.34 -apply (rule allI)
1.35  apply (case_tac ys)
1.36   apply force
1.37  apply simp
1.38 @@ -1041,6 +1037,20 @@
1.39  (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
1.40  by (force simp add: list_all2_def set_zip)
1.42 +lemma list_all2_trans:
1.43 +  assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
1.44 +  shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
1.45 +        (is "!!bs cs. PROP ?Q as bs cs")
1.46 +proof (induct as)
1.47 +  fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
1.48 +  show "!!cs. PROP ?Q (x # xs) bs cs"
1.49 +  proof (induct bs)
1.50 +    fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
1.51 +    show "PROP ?Q (x # xs) (y # ys) cs"
1.52 +      by (induct cs) (auto intro: tr I1 I2)
1.53 +  qed simp
1.54 +qed simp
1.55 +
1.56  lemma list_all2_all_nthI [intro?]:
1.57    "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
1.58    by (simp add: list_all2_conv_all_nth)
1.59 @@ -1057,19 +1067,6 @@
1.60    "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
1.61    by (auto simp add: list_all2_conv_all_nth)
1.63 -lemma list_all2_trans[rule_format]:
1.64 -"\<forall>a b c. P1 a b --> P2 b c --> P3 a c ==>
1.65 -\<forall>bs cs. list_all2 P1 as bs --> list_all2 P2 bs cs --> list_all2 P3 as cs"
1.66 -apply(induct_tac as)
1.67 - apply simp
1.68 -apply(rule allI)
1.69 -apply(induct_tac bs)
1.70 - apply simp
1.71 -apply(rule allI)
1.72 -apply(induct_tac cs)
1.73 - apply auto
1.74 -done
1.75 -
1.76  lemma list_all2_refl:
1.77    "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
1.78    by (simp add: list_all2_conv_all_nth)
1.79 @@ -1173,11 +1170,10 @@
1.80  apply (auto simp add: less_diff_conv nth_upt)
1.81  done
1.83 -lemma nth_take_lemma [rule_format]:
1.84 -"ALL xs ys. k <= length xs --> k <= length ys
1.85 ---> (ALL i. i < k --> xs!i = ys!i)
1.86 ---> take k xs = take k ys"
1.87 -apply (induct k)
1.88 +lemma nth_take_lemma:
1.89 +  "!!xs ys. k <= length xs ==> k <= length ys ==>
1.90 +     (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
1.91 +apply (atomize, induct k)
1.92  apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib)
1.93  apply clarify
1.94  txt {* Both lists must be non-empty *}