--- 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)
--- 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)
--- 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)
--- 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))"
--- 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
--- 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
--- 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''"
--- 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
--- 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 -
--- 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)
--- 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])
--- 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
--- 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"