Re-structured some proofs in order to get rid of rule_format attribute.
authorberghofe
Tue Mar 25 09:58:51 2003 +0100 (2003-03-25)
changeset 138830451e0fb3f22
parent 13882 2266550ab316
child 13884 5affbaee6b18
Re-structured some proofs in order to get rid of rule_format attribute.
src/HOL/List.thy
     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.6  
     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.15  
    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.21  
    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.41  
    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.62  
    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.82  
    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 *}