folded 'list_all2' with the relator generated by 'datatype_new'
authorblanchet
Sun Feb 16 21:33:28 2014 +0100 (2014-02-16)
changeset 55524f41ef840f09d
parent 55523 9429e7b5b827
child 55525 70b7e91fa1f9
folded 'list_all2' with the relator generated by 'datatype_new'
NEWS
src/HOL/Bali/AxSound.thy
src/HOL/Bali/TypeSafe.thy
src/HOL/Import/HOL_Light_Maps.thy
src/HOL/List.thy
src/HOL/MicroJava/BV/BVNoTypeError.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/Effect.thy
src/HOL/MicroJava/BV/JVMType.thy
src/HOL/MicroJava/Comp/CorrCompTp.thy
src/HOL/MicroJava/Comp/LemmasComp.thy
src/HOL/Quotient_Examples/Lift_DList.thy
     1.1 --- a/NEWS	Sun Feb 16 21:33:28 2014 +0100
     1.2 +++ b/NEWS	Sun Feb 16 21:33:28 2014 +0100
     1.3 @@ -129,14 +129,16 @@
     1.4      and "rec_xxx" (e.g., "prod_case" ~> "case_prod").
     1.5      INCOMPATIBILITY.
     1.6  
     1.7 -* The types "'a list" and "'a option", their set and map functions, and their
     1.8 -  selectors are now produced using the new BNF-based datatype package.
     1.9 +* The types "'a list" and "'a option", their set and map functions, their
    1.10 +  relators, and their selectors are now produced using the new BNF-based datatype
    1.11 +  package.
    1.12    Renamed constants:
    1.13      Option.set ~> set_option
    1.14      Option.map ~> map_option
    1.15    Renamed theorems:
    1.16      map_def ~> map_rec[abs_def]
    1.17      Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option")
    1.18 +    list_all2_def ~> list_all2_iff
    1.19      map.simps ~> list.map
    1.20      hd.simps ~> list.sel(1)
    1.21      tl.simps ~> list.sel(2-3)
     2.1 --- a/src/HOL/Bali/AxSound.thy	Sun Feb 16 21:33:28 2014 +0100
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Sun Feb 16 21:33:28 2014 +0100
     2.3 @@ -1543,10 +1543,10 @@
     2.4                proof -
     2.5                  from normal_s2 conf_args
     2.6                  have "length vs = length pTs"
     2.7 -                  by (simp add: list_all2_def)
     2.8 +                  by (simp add: list_all2_iff)
     2.9                  also from pTs_widen
    2.10                  have "\<dots> = length pTs'"
    2.11 -                  by (simp add: widens_def list_all2_def)
    2.12 +                  by (simp add: widens_def list_all2_iff)
    2.13                  also from wf_dynM
    2.14                  have "\<dots> = length (pars (mthd dynM))"
    2.15                    by (simp add: wf_mdecl_def wf_mhead_def)
     3.1 --- a/src/HOL/Bali/TypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
     3.2 +++ b/src/HOL/Bali/TypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
     3.3 @@ -3240,10 +3240,10 @@
     3.4                proof -
     3.5                  from normal_s2 conf_args
     3.6                  have "length vs = length pTs"
     3.7 -                  by (simp add: list_all2_def)
     3.8 +                  by (simp add: list_all2_iff)
     3.9                  also from pTs_widen
    3.10                  have "\<dots> = length pTs'"
    3.11 -                  by (simp add: widens_def list_all2_def)
    3.12 +                  by (simp add: widens_def list_all2_iff)
    3.13                  also from wf_dynM
    3.14                  have "\<dots> = length (pars (mthd dynM))"
    3.15                    by (simp add: wf_mdecl_def wf_mhead_def)
     4.1 --- a/src/HOL/Import/HOL_Light_Maps.thy	Sun Feb 16 21:33:28 2014 +0100
     4.2 +++ b/src/HOL/Import/HOL_Light_Maps.thy	Sun Feb 16 21:33:28 2014 +0100
     4.3 @@ -290,7 +290,7 @@
     4.4    foldr f (h # t) b = f h (foldr f t b)"
     4.5    by simp
     4.6  
     4.7 -lemma ALL2_DEF[import_const ALL2 : List.list_all2]:
     4.8 +lemma ALL2_DEF[import_const ALL2 : List.list.list_all2]:
     4.9    "list_all2 (P\<Colon>'t18495 \<Rightarrow> 't18502 \<Rightarrow> bool) [] (l2\<Colon>'t18502 list) = (l2 = []) \<and>
    4.10    list_all2 P ((h1\<Colon>'t18495) # (t1\<Colon>'t18495 list)) l2 =
    4.11    (if l2 = [] then False else P h1 (hd l2) \<and> list_all2 P t1 (tl l2))"
     5.1 --- a/src/HOL/List.thy	Sun Feb 16 21:33:28 2014 +0100
     5.2 +++ b/src/HOL/List.thy	Sun Feb 16 21:33:28 2014 +0100
     5.3 @@ -8,7 +8,7 @@
     5.4  imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product
     5.5  begin
     5.6  
     5.7 -datatype_new 'a list (map: map rel: rel) =
     5.8 +datatype_new 'a list (map: map rel: list_all2) =
     5.9      =: Nil (defaults tl: "[]")  ("[]")
    5.10    | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
    5.11  
    5.12 @@ -34,8 +34,6 @@
    5.13  
    5.14  setup {* Sign.parent_path *}
    5.15  
    5.16 -hide_const (open) rel
    5.17 -
    5.18  syntax
    5.19    -- {* list Enumeration *}
    5.20    "_list" :: "args => 'a list"    ("[(_)]")
    5.21 @@ -228,10 +226,6 @@
    5.22  definition rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    5.23  "rotate n = rotate1 ^^ n"
    5.24  
    5.25 -definition list_all2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool" where
    5.26 -"list_all2 P xs ys =
    5.27 -  (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
    5.28 -
    5.29  definition sublist :: "'a list => nat set => 'a list" where
    5.30  "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
    5.31  
    5.32 @@ -852,6 +846,10 @@
    5.33   \<Longrightarrow> P xs ys"
    5.34  by (induct xs arbitrary: ys) (case_tac x, auto)+
    5.35  
    5.36 +lemma list_all2_iff:
    5.37 +  "list_all2 P xs ys \<longleftrightarrow> length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y)"
    5.38 +by (induct xs ys rule: list_induct2') auto
    5.39 +
    5.40  lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
    5.41  by (rule Eq_FalseI) auto
    5.42  
    5.43 @@ -2534,17 +2532,17 @@
    5.44  
    5.45  lemma list_all2_lengthD [intro?]: 
    5.46    "list_all2 P xs ys ==> length xs = length ys"
    5.47 -by (simp add: list_all2_def)
    5.48 +by (simp add: list_all2_iff)
    5.49  
    5.50  lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
    5.51 -by (simp add: list_all2_def)
    5.52 +by (simp add: list_all2_iff)
    5.53  
    5.54  lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
    5.55 -by (simp add: list_all2_def)
    5.56 +by (simp add: list_all2_iff)
    5.57  
    5.58  lemma list_all2_Cons [iff, code]:
    5.59    "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
    5.60 -by (auto simp add: list_all2_def)
    5.61 +by (auto simp add: list_all2_iff)
    5.62  
    5.63  lemma list_all2_Cons1:
    5.64  "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
    5.65 @@ -2566,7 +2564,7 @@
    5.66  
    5.67  lemma list_all2_rev [iff]:
    5.68  "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
    5.69 -by (simp add: list_all2_def zip_rev cong: conj_cong)
    5.70 +by (simp add: list_all2_iff zip_rev cong: conj_cong)
    5.71  
    5.72  lemma list_all2_rev1:
    5.73  "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
    5.74 @@ -2576,7 +2574,7 @@
    5.75  "list_all2 P (xs @ ys) zs =
    5.76  (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
    5.77  list_all2 P xs us \<and> list_all2 P ys vs)"
    5.78 -apply (simp add: list_all2_def zip_append1)
    5.79 +apply (simp add: list_all2_iff zip_append1)
    5.80  apply (rule iffI)
    5.81   apply (rule_tac x = "take (length xs) zs" in exI)
    5.82   apply (rule_tac x = "drop (length xs) zs" in exI)
    5.83 @@ -2588,7 +2586,7 @@
    5.84  "list_all2 P xs (ys @ zs) =
    5.85  (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
    5.86  list_all2 P us ys \<and> list_all2 P vs zs)"
    5.87 -apply (simp add: list_all2_def zip_append2)
    5.88 +apply (simp add: list_all2_iff zip_append2)
    5.89  apply (rule iffI)
    5.90   apply (rule_tac x = "take (length ys) xs" in exI)
    5.91   apply (rule_tac x = "drop (length ys) xs" in exI)
    5.92 @@ -2608,7 +2606,7 @@
    5.93  lemma list_all2_conv_all_nth:
    5.94  "list_all2 P xs ys =
    5.95  (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
    5.96 -by (force simp add: list_all2_def set_zip)
    5.97 +by (force simp add: list_all2_iff set_zip)
    5.98  
    5.99  lemma list_all2_trans:
   5.100    assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
   5.101 @@ -2630,7 +2628,7 @@
   5.102  
   5.103  lemma list_all2I:
   5.104    "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
   5.105 -by (simp add: list_all2_def)
   5.106 +by (simp add: list_all2_iff)
   5.107  
   5.108  lemma list_all2_nthD:
   5.109    "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
   5.110 @@ -6643,7 +6641,7 @@
   5.111  
   5.112  lemma list_invariant_commute [invariant_commute]:
   5.113    "list_all2 (Lifting.invariant P) = Lifting.invariant (list_all P)"
   5.114 -  apply (simp add: fun_eq_iff list_all2_def list_all_iff Lifting.invariant_def Ball_def) 
   5.115 +  apply (simp add: fun_eq_iff list_all2_iff list_all_iff Lifting.invariant_def Ball_def) 
   5.116    apply (intro allI) 
   5.117    apply (induct_tac rule: list_induct2') 
   5.118    apply simp_all 
   5.119 @@ -6829,8 +6827,8 @@
   5.120  lemma list_all2_transfer [transfer_rule]:
   5.121    "((A ===> B ===> op =) ===> list_all2 A ===> list_all2 B ===> op =)
   5.122      list_all2 list_all2"
   5.123 -  apply (subst (4) list_all2_def [abs_def])
   5.124 -  apply (subst (3) list_all2_def [abs_def])
   5.125 +  apply (subst (4) list_all2_iff [abs_def])
   5.126 +  apply (subst (3) list_all2_iff [abs_def])
   5.127    apply transfer_prover
   5.128    done
   5.129  
     6.1 --- a/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Feb 16 21:33:28 2014 +0100
     6.2 +++ b/src/HOL/MicroJava/BV/BVNoTypeError.thy	Sun Feb 16 21:33:28 2014 +0100
     6.3 @@ -147,7 +147,7 @@
     6.4    method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
     6.5    (is "?app ST LT = ?P ST LT")
     6.6  proof
     6.7 -  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_def)
     6.8 +  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_iff)
     6.9  next  
    6.10    assume app: "?app ST LT"
    6.11    hence l: "length fpTs < length ST" by simp
    6.12 @@ -170,7 +170,7 @@
    6.13    have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
    6.14    with app
    6.15    show "?P ST LT"
    6.16 -    apply (clarsimp simp add: list_all2_def)
    6.17 +    apply (clarsimp simp add: list_all2_iff)
    6.18      apply (intro exI conjI)
    6.19      apply auto
    6.20      done
    6.21 @@ -178,7 +178,7 @@
    6.22  
    6.23  lemma approx_loc_len [simp]:
    6.24    "approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
    6.25 -  by (simp add: approx_loc_def list_all2_def)
    6.26 +  by (simp add: approx_loc_def list_all2_iff)
    6.27  
    6.28  lemma approx_stk_len [simp]:
    6.29    "approx_stk G hp stk ST \<Longrightarrow> length stk = length ST"
    6.30 @@ -341,7 +341,7 @@
    6.31        have [simp]: "take (length ps) stk = aps" by simp
    6.32        from w ps
    6.33        have widen: "list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs ps"
    6.34 -        by (simp add: list_all2_def) 
    6.35 +        by (simp add: list_all2_iff) 
    6.36  
    6.37        from stk' l ps have "length ps < length stk" by simp
    6.38        moreover
     7.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
     7.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sun Feb 16 21:33:28 2014 +0100
     7.3 @@ -947,7 +947,7 @@
     7.4        by (simp add: wt_start_def sup_state_conv)
     7.5  
     7.6      have r: "approx_loc G hp (replicate mxl' undefined) (replicate mxl' Err)"
     7.7 -      by (simp add: approx_loc_def list_all2_def set_replicate_conv_if)
     7.8 +      by (simp add: approx_loc_def list_all2_iff set_replicate_conv_if)
     7.9      
    7.10      from wfprog mD is_class_D
    7.11      have "G \<turnstile> Class D \<preceq> Class D''"
     8.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Sun Feb 16 21:33:28 2014 +0100
     8.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Sun Feb 16 21:33:28 2014 +0100
     8.3 @@ -157,7 +157,7 @@
     8.4  lemma approx_loc_subst:
     8.5    "\<lbrakk> approx_loc G hp loc LT; approx_val G hp x X \<rbrakk>
     8.6    \<Longrightarrow> approx_loc G hp (loc[idx:=x]) (LT[idx:=X])"
     8.7 -apply (unfold approx_loc_def list_all2_def)
     8.8 +apply (unfold approx_loc_def list_all2_iff)
     8.9  apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update)
    8.10  done
    8.11  
    8.12 @@ -165,7 +165,7 @@
    8.13    "length l1=length L1 \<Longrightarrow>
    8.14    approx_loc G hp (l1@l2) (L1@L2) = 
    8.15    (approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)"
    8.16 -  apply (unfold approx_loc_def list_all2_def)
    8.17 +  apply (unfold approx_loc_def list_all2_iff)
    8.18    apply (simp cong: conj_cong)
    8.19    apply blast
    8.20    done
     9.1 --- a/src/HOL/MicroJava/BV/Effect.thy	Sun Feb 16 21:33:28 2014 +0100
     9.2 +++ b/src/HOL/MicroJava/BV/Effect.thy	Sun Feb 16 21:33:28 2014 +0100
     9.3 @@ -114,7 +114,7 @@
     9.4  
     9.5  
     9.6  lemma "list_all2 P a b \<Longrightarrow> \<forall>(x,y) \<in> set (zip a b). P x y"
     9.7 -  by (simp add: list_all2_def) 
     9.8 +  by (simp add: list_all2_iff) 
     9.9  
    9.10  
    9.11  text "Conditions under which eff is applicable:"
    9.12 @@ -352,7 +352,7 @@
    9.13    method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> 
    9.14    (\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s")
    9.15  proof (cases s)
    9.16 -  note list_all2_def [simp]
    9.17 +  note list_all2_iff [simp]
    9.18    case (Pair a b)
    9.19    have "?app (a,b) \<Longrightarrow> ?P (a,b)"
    9.20    proof -
    10.1 --- a/src/HOL/MicroJava/BV/JVMType.thy	Sun Feb 16 21:33:28 2014 +0100
    10.2 +++ b/src/HOL/MicroJava/BV/JVMType.thy	Sun Feb 16 21:33:28 2014 +0100
    10.3 @@ -118,7 +118,7 @@
    10.4        by (auto simp add: zip_map)
    10.5      with le
    10.6      have "subtype G x y"
    10.7 -      by (simp add: list_all2_def Ball_def)
    10.8 +      by (simp add: list_all2_iff Ball_def)
    10.9      with OK
   10.10      have "G \<turnstile> x' <=o y'"
   10.11        by (simp add: sup_ty_opt_def)
   10.12 @@ -126,12 +126,12 @@
   10.13    
   10.14    with le
   10.15    show "G \<turnstile> map OK a <=l map OK b"
   10.16 -    by (unfold sup_loc_def Listn.le_def lesub_def list_all2_def) auto
   10.17 +    by (unfold sup_loc_def Listn.le_def lesub_def list_all2_iff) auto
   10.18  next
   10.19    assume "G \<turnstile> map OK a <=l map OK b"
   10.20  
   10.21    thus "Listn.le (subtype G) a b"
   10.22 -    apply (unfold sup_loc_def list_all2_def Listn.le_def lesub_def)
   10.23 +    apply (unfold sup_loc_def list_all2_iff Listn.le_def lesub_def)
   10.24      apply (clarsimp simp add: zip_map)
   10.25      apply (drule bspec, assumption)
   10.26      apply (auto simp add: sup_ty_opt_def subtype_def)
    11.1 --- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Feb 16 21:33:28 2014 +0100
    11.2 +++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Sun Feb 16 21:33:28 2014 +0100
    11.3 @@ -1264,7 +1264,7 @@
    11.4    apply (rule_tac x="Class cname" in exI)
    11.5    apply (simp add: max_spec_preserves_length comp_is_class)
    11.6    apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
    11.7 -  apply (simp add: split_paired_all comp_widen list_all2_def)
    11.8 +  apply (simp add: split_paired_all comp_widen list_all2_iff)
    11.9    apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
   11.10    apply (rule exI)+
   11.11    apply (simp add: wf_prog_ws_prog [THEN comp_method])
    12.1 --- a/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Feb 16 21:33:28 2014 +0100
    12.2 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy	Sun Feb 16 21:33:28 2014 +0100
    12.3 @@ -392,7 +392,7 @@
    12.4    \<Longrightarrow> length pTs = length pTs'"
    12.5  apply (frule max_spec2mheads)
    12.6  apply (erule exE)+
    12.7 -apply (simp add: list_all2_def)
    12.8 +apply (simp add: list_all2_iff)
    12.9  done
   12.10  
   12.11  
    13.1 --- a/src/HOL/Quotient_Examples/Lift_DList.thy	Sun Feb 16 21:33:28 2014 +0100
    13.2 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Sun Feb 16 21:33:28 2014 +0100
    13.3 @@ -55,7 +55,7 @@
    13.4    {
    13.5      fix x y
    13.6      have "list_all2 cr_dlist x y \<Longrightarrow> x = List.map list_of_dlist y"
    13.7 -      unfolding list_all2_def cr_dlist_def by (induction x y rule: list_induct2') auto
    13.8 +      unfolding list_all2_iff cr_dlist_def by (induction x y rule: list_induct2') auto
    13.9    }
   13.10    note cr = this
   13.11    fix x :: "'a list list" and y :: "'a list list"