# HG changeset patch
# User blanchet
# Date 1392582808 -3600
# Node ID f41ef840f09d50ca320ecd300ab093b60b9611db
# Parent  9429e7b5b8273d4d491ab93da5154e0a8e724177
folded 'list_all2' with the relator generated by 'datatype_new'

diff -r 9429e7b5b827 -r f41ef840f09d NEWS
--- a/NEWS	Sun Feb 16 21:33:28 2014 +0100
+++ b/NEWS	Sun Feb 16 21:33:28 2014 +0100
@@ -129,14 +129,16 @@
     and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
     INCOMPATIBILITY.
 
-* The types "'a list" and "'a option", their set and map functions, and their
-  selectors are now produced using the new BNF-based datatype package.
+* The types "'a list" and "'a option", their set and map functions, their
+  relators, and their selectors are now produced using the new BNF-based datatype
+  package.
   Renamed constants:
     Option.set ~> set_option
     Option.map ~> map_option
   Renamed theorems:
     map_def ~> map_rec[abs_def]
     Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
+    list_all2_def ~> list_all2_iff
     map.simps ~> list.map
     hd.simps ~> list.sel(1)
     tl.simps ~> list.sel(2-3)
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/Bali/AxSound.thy
--- a/src/HOL/Bali/AxSound.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/Bali/AxSound.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -1543,10 +1543,10 @@
               proof -
                 from normal_s2 conf_args
                 have "length vs = length pTs"
-                  by (simp add: list_all2_def)
+                  by (simp add: list_all2_iff)
                 also from pTs_widen
                 have "\<dots> = length pTs'"
-                  by (simp add: widens_def list_all2_def)
+                  by (simp add: widens_def list_all2_iff)
                 also from wf_dynM
                 have "\<dots> = length (pars (mthd dynM))"
                   by (simp add: wf_mdecl_def wf_mhead_def)
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/Bali/TypeSafe.thy
--- a/src/HOL/Bali/TypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/Bali/TypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -3240,10 +3240,10 @@
               proof -
                 from normal_s2 conf_args
                 have "length vs = length pTs"
-                  by (simp add: list_all2_def)
+                  by (simp add: list_all2_iff)
                 also from pTs_widen
                 have "\<dots> = length pTs'"
-                  by (simp add: widens_def list_all2_def)
+                  by (simp add: widens_def list_all2_iff)
                 also from wf_dynM
                 have "\<dots> = length (pars (mthd dynM))"
                   by (simp add: wf_mdecl_def wf_mhead_def)
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/Import/HOL_Light_Maps.thy
--- a/src/HOL/Import/HOL_Light_Maps.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/Import/HOL_Light_Maps.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -290,7 +290,7 @@
   foldr f (h # t) b = f h (foldr f t b)"
   by simp
 
-lemma ALL2_DEF[import_const ALL2 : List.list_all2]:
+lemma ALL2_DEF[import_const ALL2 : List.list.list_all2]:
   "list_all2 (P\<Colon>'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2\<Colon>'t18502 list) = (l2 = []) \<and>
   list_all2 P ((h1\<Colon>'t18495) # (t1\<Colon>'t18495 list)) l2 =
   (if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/List.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -8,7 +8,7 @@
 imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
 begin
 
-datatype_new 'a list (map: map rel: rel) =
+datatype_new 'a list (map: map rel: list_all2) =
     =: Nil (defaults tl: "[]")  ("[]")
   | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
 
@@ -34,8 +34,6 @@
 
 setup {* Sign.parent_path *}
 
-hide_const (open) rel
-
 syntax
   -- {* list Enumeration *}
   "_list" :: "args => 'a list"    ("[(_)]")
@@ -228,10 +226,6 @@
 definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
 "rotate n = rotate1 ^^ n"
 
-definition list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" where
-"list_all2 P xs ys =
-  (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
-
 definition sublist :: "'a list => nat set => 'a list" where
 "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
 
@@ -852,6 +846,10 @@
  \<Longrightarrow> P xs ys"
 by (induct xs arbitrary: ys) (case_tac x, auto)+
 
+lemma list_all2_iff:
+  "list_all2 P xs ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
+by (induct xs ys rule: list_induct2') auto
+
 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
 by (rule Eq_FalseI) auto
 
@@ -2534,17 +2532,17 @@
 
 lemma list_all2_lengthD [intro?]: 
   "list_all2 P xs ys ==> length xs = length ys"
-by (simp add: list_all2_def)
+by (simp add: list_all2_iff)
 
 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
-by (simp add: list_all2_def)
+by (simp add: list_all2_iff)
 
 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
-by (simp add: list_all2_def)
+by (simp add: list_all2_iff)
 
 lemma list_all2_Cons [iff, code]:
   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
-by (auto simp add: list_all2_def)
+by (auto simp add: list_all2_iff)
 
 lemma list_all2_Cons1:
 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
@@ -2566,7 +2564,7 @@
 
 lemma list_all2_rev [iff]:
 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
-by (simp add: list_all2_def zip_rev cong: conj_cong)
+by (simp add: list_all2_iff zip_rev cong: conj_cong)
 
 lemma list_all2_rev1:
 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
@@ -2576,7 +2574,7 @@
 "list_all2 P (xs @ ys) zs =
 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
 list_all2 P xs us \<and> list_all2 P ys vs)"
-apply (simp add: list_all2_def zip_append1)
+apply (simp add: list_all2_iff zip_append1)
 apply (rule iffI)
  apply (rule_tac x = "take (length xs) zs" in exI)
  apply (rule_tac x = "drop (length xs) zs" in exI)
@@ -2588,7 +2586,7 @@
 "list_all2 P xs (ys @ zs) =
 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
 list_all2 P us ys \<and> list_all2 P vs zs)"
-apply (simp add: list_all2_def zip_append2)
+apply (simp add: list_all2_iff zip_append2)
 apply (rule iffI)
  apply (rule_tac x = "take (length ys) xs" in exI)
  apply (rule_tac x = "drop (length ys) xs" in exI)
@@ -2608,7 +2606,7 @@
 lemma list_all2_conv_all_nth:
 "list_all2 P xs ys =
 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
-by (force simp add: list_all2_def set_zip)
+by (force simp add: list_all2_iff set_zip)
 
 lemma list_all2_trans:
   assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
@@ -2630,7 +2628,7 @@
 
 lemma list_all2I:
   "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
-by (simp add: list_all2_def)
+by (simp add: list_all2_iff)
 
 lemma list_all2_nthD:
   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
@@ -6643,7 +6641,7 @@
 
 lemma list_invariant_commute [invariant_commute]:
   "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
-  apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) 
+  apply (simp add: fun_eq_iff list_all2_iff list_all_iff Lifting.invariant_def Ball_def) 
   apply (intro allI) 
   apply (induct_tac rule: list_induct2') 
   apply simp_all 
@@ -6829,8 +6827,8 @@
 lemma list_all2_transfer [transfer_rule]:
   "((A ===> B ===> op =) ===> list_all2 A ===> list_all2 B ===> op =)
     list_all2 list_all2"
-  apply (subst (4) list_all2_def [abs_def])
-  apply (subst (3) list_all2_def [abs_def])
+  apply (subst (4) list_all2_iff [abs_def])
+  apply (subst (3) list_all2_iff [abs_def])
   apply transfer_prover
   done
 
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/BV/BVNoTypeError.thy
--- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -147,7 +147,7 @@
   method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
   (is "?app ST LT = ?P ST LT")
 proof
-  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_def)
+  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_iff)
 next  
   assume app: "?app ST LT"
   hence l: "length fpTs < length ST" by simp
@@ -170,7 +170,7 @@
   have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
   with app
   show "?P ST LT"
-    apply (clarsimp simp add: list_all2_def)
+    apply (clarsimp simp add: list_all2_iff)
     apply (intro exI conjI)
     apply auto
     done
@@ -178,7 +178,7 @@
 
 lemma approx_loc_len [simp]:
   "approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
-  by (simp add: approx_loc_def list_all2_def)
+  by (simp add: approx_loc_def list_all2_iff)
 
 lemma approx_stk_len [simp]:
   "approx_stk G hp stk ST \<Longrightarrow> length stk = length ST"
@@ -341,7 +341,7 @@
       have [simp]: "take (length ps) stk = aps" by simp
       from w ps
       have widen: "list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs ps"
-        by (simp add: list_all2_def) 
+        by (simp add: list_all2_iff) 
 
       from stk' l ps have "length ps < length stk" by simp
       moreover
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -947,7 +947,7 @@
       by (simp add: wt_start_def sup_state_conv)
 
     have r: "approx_loc G hp (replicate mxl' undefined) (replicate mxl' Err)"
-      by (simp add: approx_loc_def list_all2_def set_replicate_conv_if)
+      by (simp add: approx_loc_def list_all2_iff set_replicate_conv_if)
     
     from wfprog mD is_class_D
     have "G \<turnstile> Class D \<preceq> Class D''"
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/BV/Correct.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -157,7 +157,7 @@
 lemma approx_loc_subst:
   "\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
   \<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
-apply (unfold approx_loc_def list_all2_def)
+apply (unfold approx_loc_def list_all2_iff)
 apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
 done
 
@@ -165,7 +165,7 @@
   "length l1=length L1 \<Longrightarrow>
   approx_loc G hp (l1@l2) (L1@L2) = 
   (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
-  apply (unfold approx_loc_def list_all2_def)
+  apply (unfold approx_loc_def list_all2_iff)
   apply (simp cong: conj_cong)
   apply blast
   done
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/BV/Effect.thy
--- a/src/HOL/MicroJava/BV/Effect.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/BV/Effect.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -114,7 +114,7 @@
 
 
 lemma "list_all2 P a b \<Longrightarrow> \<forall>(x,y) \<in> set (zip a b). P x y"
-  by (simp add: list_all2_def) 
+  by (simp add: list_all2_iff) 
 
 
 text "Conditions under which eff is applicable:"
@@ -352,7 +352,7 @@
   method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> 
   (\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s")
 proof (cases s)
-  note list_all2_def [simp]
+  note list_all2_iff [simp]
   case (Pair a b)
   have "?app (a,b) \<Longrightarrow> ?P (a,b)"
   proof -
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/BV/JVMType.thy
--- a/src/HOL/MicroJava/BV/JVMType.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -118,7 +118,7 @@
       by (auto simp add: zip_map)
     with le
     have "subtype G x y"
-      by (simp add: list_all2_def Ball_def)
+      by (simp add: list_all2_iff Ball_def)
     with OK
     have "G \<turnstile> x' <=o y'"
       by (simp add: sup_ty_opt_def)
@@ -126,12 +126,12 @@
   
   with le
   show "G \<turnstile> map OK a <=l map OK b"
-    by (unfold sup_loc_def Listn.le_def lesub_def list_all2_def) auto
+    by (unfold sup_loc_def Listn.le_def lesub_def list_all2_iff) auto
 next
   assume "G \<turnstile> map OK a <=l map OK b"
 
   thus "Listn.le (subtype G) a b"
-    apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def)
+    apply (unfold sup_loc_def list_all2_iff Listn.le_def lesub_def)
     apply (clarsimp simp add: zip_map)
     apply (drule bspec, assumption)
     apply (auto simp add: sup_ty_opt_def subtype_def)
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -1264,7 +1264,7 @@
   apply (rule_tac x="Class cname" in exI)
   apply (simp add: max_spec_preserves_length comp_is_class)
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
-  apply (simp add: split_paired_all comp_widen list_all2_def)
+  apply (simp add: split_paired_all comp_widen list_all2_iff)
   apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   apply (rule exI)+
   apply (simp add: wf_prog_ws_prog [THEN comp_method])
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/MicroJava/Comp/LemmasComp.thy
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -392,7 +392,7 @@
   \<Longrightarrow> length pTs = length pTs'"
 apply (frule max_spec2mheads)
 apply (erule exE)+
-apply (simp add: list_all2_def)
+apply (simp add: list_all2_iff)
 done
 
 
diff -r 9429e7b5b827 -r f41ef840f09d src/HOL/Quotient_Examples/Lift_DList.thy
--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Sun Feb 16 21:33:28 2014 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Sun Feb 16 21:33:28 2014 +0100
@@ -55,7 +55,7 @@
   {
     fix x y
     have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
-      unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
+      unfolding list_all2_iff cr_dlist_def by (induction x y rule: list_induct2') auto
   }
   note cr = this
   fix x :: "'a list list" and y :: "'a list list"