# HG changeset patch
# User wenzelm
# Date 1573139006 -3600
# Node ID 995fe5877d53550f8bd74c906746d7c129ccefd3
# Parent  45a1fcee14a0c8cc882306beada737b8f4b982d5
tuned declarations for more compact proof terms;

diff -r 45a1fcee14a0 -r 995fe5877d53 src/ZF/Bin.thy
--- a/src/ZF/Bin.thy	Thu Nov 07 15:30:48 2019 +0100
+++ b/src/ZF/Bin.thy	Thu Nov 07 16:03:26 2019 +0100
@@ -162,7 +162,7 @@
 by (induct_tac "w", auto)
 
 (*This proof is complicated by the mutual recursion*)
-lemma bin_add_type [rule_format,TC]:
+lemma bin_add_type [rule_format]:
      "v \<in> bin ==> \<forall>w\<in>bin. bin_add(v,w) \<in> bin"
 apply (unfold bin_add_def)
 apply (induct_tac "v")
@@ -172,6 +172,8 @@
 apply (simp_all add: NCons_type)
 done
 
+declare bin_add_type [TC]
+
 lemma bin_mult_type [TC]: "[| v \<in> bin; w \<in> bin |] ==> bin_mult(v,w) \<in> bin"
 by (induct_tac "v", auto)
 
diff -r 45a1fcee14a0 -r 995fe5877d53 src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Nov 07 15:30:48 2019 +0100
+++ b/src/ZF/List.thy	Thu Nov 07 16:03:26 2019 +0100
@@ -567,7 +567,7 @@
 apply (auto simp add: length_app)
 done
 
-lemma append_eq_append_iff [rule_format,simp]:
+lemma append_eq_append_iff [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(A).
       length(xs)=length(ys) \<longrightarrow> (xs@us = ys@vs) \<longleftrightarrow> (xs=ys & us=vs)"
 apply (erule list.induct)
@@ -575,6 +575,7 @@
 apply clarify
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare append_eq_append_iff [simp]
 
 lemma append_eq_append [rule_format]:
   "xs:list(A) ==>
@@ -604,7 +605,7 @@
 
 (* Can also be proved from append_eq_append_iff2,
 but the proof requires two more hypotheses: x \<in> A and y \<in> A *)
-lemma append1_eq_iff [rule_format,simp]:
+lemma append1_eq_iff [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] \<longleftrightarrow> (xs = ys & x=y)"
 apply (erule list.induct)
  apply clarify
@@ -614,7 +615,7 @@
 apply clarify
 apply (erule_tac a=ys in list.cases, simp_all)
 done
-
+declare append1_eq_iff [simp]
 
 lemma append_right_is_self_iff [simp]:
      "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) \<longleftrightarrow> (xs=Nil)"
@@ -626,13 +627,15 @@
 apply (drule sym, auto)
 done
 
-lemma hd_append [rule_format,simp]:
+lemma hd_append [rule_format]:
      "xs:list(A) ==> xs \<noteq> Nil \<longrightarrow> hd(xs @ ys) = hd(xs)"
 by (induct_tac "xs", auto)
+declare hd_append [simp]
 
-lemma tl_append [rule_format,simp]:
+lemma tl_append [rule_format]:
      "xs:list(A) ==> xs\<noteq>Nil \<longrightarrow> tl(xs @ ys) = tl(xs)@ys"
 by (induct_tac "xs", auto)
+declare tl_append [simp]
 
 (** rev **)
 lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil \<longleftrightarrow> xs = Nil)"
@@ -641,11 +644,12 @@
 lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) \<longleftrightarrow> xs = Nil)"
 by (erule list.induct, auto)
 
-lemma rev_is_rev_iff [rule_format,simp]:
+lemma rev_is_rev_iff [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) \<longleftrightarrow> xs=ys"
 apply (erule list.induct, force, clarify)
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare rev_is_rev_iff [simp]
 
 lemma rev_list_elim [rule_format]:
      "xs:list(A) ==>
@@ -655,17 +659,19 @@
 
 (** more theorems about drop **)
 
-lemma length_drop [rule_format,simp]:
+lemma length_drop [rule_format]:
      "n \<in> nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
 apply (erule nat_induct)
 apply (auto elim: list.cases)
 done
+declare length_drop [simp]
 
-lemma drop_all [rule_format,simp]:
+lemma drop_all [rule_format]:
      "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n \<longrightarrow> drop(n, xs)=Nil"
 apply (erule nat_induct)
 apply (auto elim: list.cases)
 done
+declare drop_all [simp]
 
 lemma drop_append [rule_format]:
      "n \<in> nat ==>
@@ -695,25 +701,28 @@
 lemma take_Nil [simp]: "n \<in> nat ==> take(n, Nil) = Nil"
 by (unfold take_def, auto)
 
-lemma take_all [rule_format,simp]:
+lemma take_all [rule_format]:
      "n \<in> nat ==> \<forall>xs \<in> list(A). length(xs) \<le> n  \<longrightarrow> take(n, xs) = xs"
 apply (erule nat_induct)
 apply (auto elim: list.cases)
 done
+declare take_all [simp]
 
-lemma take_type [rule_format,simp,TC]:
+lemma take_type [rule_format]:
      "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
 apply (erule list.induct, simp, clarify)
 apply (erule natE, auto)
 done
+declare take_type [simp,TC]
 
-lemma take_append [rule_format,simp]:
+lemma take_append [rule_format]:
  "xs:list(A) ==>
   \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
                             take(n, xs) @ take(n #- length(xs), ys)"
 apply (erule list.induct, simp, clarify)
 apply (erule natE, auto)
 done
+declare take_append [simp]
 
 lemma take_take [rule_format]:
    "m \<in> nat ==>
@@ -736,12 +745,13 @@
 lemma nth_empty [simp]: "nth(n, Nil) = 0"
 by (simp add: nth_def)
 
-lemma nth_type [rule_format,simp,TC]:
+lemma nth_type [rule_format]:
      "xs:list(A) ==> \<forall>n. n < length(xs) \<longrightarrow> nth(n,xs) \<in> A"
 apply (erule list.induct, simp, clarify)
 apply (subgoal_tac "n \<in> nat")
  apply (erule natE, auto dest!: le_in_nat)
 done
+declare nth_type [simp,TC]
 
 lemma nth_eq_0 [rule_format]:
      "xs:list(A) ==> \<forall>n \<in> nat. length(xs) \<le> n \<longrightarrow> nth(n,xs) = 0"
@@ -894,22 +904,24 @@
 apply (blast intro: list_on_set_of_list list_mono [THEN subsetD])
 done
 
-lemma zip_type [rule_format,simp,TC]:
+lemma zip_type [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply clarify
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare zip_type [simp,TC]
 
 (* zip length *)
-lemma length_zip [rule_format,simp]:
+lemma length_zip [rule_format]:
      "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
                                      min(length(xs), length(ys))"
 apply (unfold min_def)
 apply (induct_tac "xs", simp_all, clarify)
 apply (erule_tac a = ys in list.cases, auto)
 done
+declare length_zip [simp]
 
 lemma zip_append1 [rule_format]:
  "[| ys:list(A); zs:list(B) |] ==>
@@ -933,15 +945,16 @@
 by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
 
 
-lemma zip_rev [rule_format,simp]:
+lemma zip_rev [rule_format]:
  "ys:list(B) ==> \<forall>xs \<in> list(A).
     length(xs) = length(ys) \<longrightarrow> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
 apply (induct_tac "ys", force, clarify)
 apply (erule_tac a = xs in list.cases)
 apply (auto simp add: length_rev)
 done
+declare zip_rev [simp]
 
-lemma nth_zip [rule_format,simp]:
+lemma nth_zip [rule_format]:
    "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
                     i < length(xs) \<longrightarrow> i < length(ys) \<longrightarrow>
                     nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
@@ -949,6 +962,7 @@
 apply (erule_tac a = xs in list.cases, simp)
 apply (auto elim: natE)
 done
+declare nth_zip [simp]
 
 lemma set_of_list_zip [rule_format]:
      "[| xs:list(A); ys:list(B); i \<in> nat |]
@@ -971,21 +985,23 @@
 apply (unfold list_update_def, auto)
 done
 
-lemma list_update_type [rule_format,simp,TC]:
+lemma list_update_type [rule_format]:
      "[| xs:list(A); v \<in> A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply clarify
 apply (erule natE, auto)
 done
+declare list_update_type [simp,TC]
 
-lemma length_list_update [rule_format,simp]:
+lemma length_list_update [rule_format]:
      "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
 apply (induct_tac "xs")
 apply (simp (no_asm))
 apply clarify
 apply (erule natE, auto)
 done
+declare length_list_update [simp]
 
 lemma nth_list_update [rule_format]:
      "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs)  \<longrightarrow>
@@ -1004,7 +1020,7 @@
 by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
 
 
-lemma nth_list_update_neq [rule_format,simp]:
+lemma nth_list_update_neq [rule_format]:
   "xs:list(A) ==>
      \<forall>i \<in> nat. \<forall>j \<in> nat. i \<noteq> j \<longrightarrow> nth(j, list_update(xs,i,x)) = nth(j,xs)"
 apply (induct_tac "xs")
@@ -1014,8 +1030,9 @@
 apply (erule_tac [2] natE, simp_all)
 apply (erule natE, simp_all)
 done
+declare nth_list_update_neq [simp]
 
-lemma list_update_overwrite [rule_format,simp]:
+lemma list_update_overwrite [rule_format]:
      "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
    \<longrightarrow> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
 apply (induct_tac "xs")
@@ -1023,6 +1040,7 @@
 apply clarify
 apply (erule natE, auto)
 done
+declare list_update_overwrite [simp]
 
 lemma list_update_same_conv [rule_format]:
      "xs:list(A) ==>
@@ -1105,15 +1123,16 @@
 apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
 done
 
-lemma nth_upt [rule_format,simp]:
+lemma nth_upt [rule_format]:
      "[| i \<in> nat; j \<in> nat; k \<in> nat |] ==> i #+ k < j \<longrightarrow> nth(k, upt(i,j)) = i #+ k"
 apply (induct_tac "j", simp)
 apply (simp add: nth_append le_iff)
 apply (auto dest!: not_lt_imp_le
             simp add: nth_append less_diff_conv add_commute)
 done
+declare nth_upt [simp]
 
-lemma take_upt [rule_format,simp]:
+lemma take_upt [rule_format]:
      "[| m \<in> nat; n \<in> nat |] ==>
          \<forall>i \<in> nat. i #+ m \<le> n \<longrightarrow> take(m, upt(i,n)) = upt(i,i#+m)"
 apply (induct_tac "m")
@@ -1126,6 +1145,7 @@
 apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
 apply auto
 done
+declare take_upt [simp]
 
 lemma map_succ_upt:
      "[| m \<in> nat; n \<in> nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
@@ -1133,13 +1153,14 @@
 apply (auto simp add: map_app_distrib)
 done
 
-lemma nth_map [rule_format,simp]:
+lemma nth_map [rule_format]:
      "xs:list(A) ==>
       \<forall>n \<in> nat. n < length(xs) \<longrightarrow> nth(n, map(f, xs)) = f(nth(n, xs))"
 apply (induct_tac "xs", simp)
 apply (rule ballI)
 apply (induct_tac "n", auto)
 done
+declare nth_map [simp]
 
 lemma nth_map_upt [rule_format]:
      "[| m \<in> nat; n \<in> nat |] ==>
@@ -1213,13 +1234,14 @@
      "sublist([x], A) = (if 0 \<in> A then [x] else [])"
 by (simp add: sublist_Cons)
 
-lemma sublist_upt_eq_take [rule_format, simp]:
+lemma sublist_upt_eq_take [rule_format]:
     "xs:list(A) ==> \<forall>n\<in>nat. sublist(xs,n) = take(n,xs)"
 apply (erule list.induct, simp)
 apply (clarify )
 apply (erule natE)
 apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
 done
+declare sublist_upt_eq_take [simp]
 
 lemma sublist_Int_eq:
      "xs \<in> list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"