removal of the legacy ML structure List
authorpaulson
Thu Feb 19 18:24:08 2004 +0100 (2004-02-19)
changeset 14401477380c74c1d
parent 14400 6069098854b9
child 14402 4201e1916482
removal of the legacy ML structure List
NEWS
src/HOL/Lex/MaxChop.ML
src/HOL/Lex/RegExp2NA.ML
src/HOL/Lex/RegExp2NAe.ML
src/HOL/Lex/RegSet_of_nat_DA.ML
src/HOL/List.ML
src/HOL/MiniML/Type.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/ABP/Lemmas.thy
     1.1 --- a/NEWS	Thu Feb 19 17:57:54 2004 +0100
     1.2 +++ b/NEWS	Thu Feb 19 18:24:08 2004 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4    - INCOMPATIBILITY: many type-specific instances of laws proved in 
     1.5      Ring_and_Field are no longer available.
     1.6  
     1.7 -* Type "rat" of the rational numbers is now availabe in HOL-Complex.
     1.8 +* Type "rat" of the rational numbers is now available in HOL-Complex.
     1.9  
    1.10  * Records:
    1.11    - Record types are now by default printed with their type abbreviation
    1.12 @@ -119,8 +119,6 @@
    1.13  
    1.14  * HOL-Algebra: new locale "ring" for non-commutative rings.
    1.15  
    1.16 -* SET-Protocol: formalization and verification of the SET protocol suite;
    1.17 -
    1.18  * HOL-ex: InductiveInvariant_examples illustrates advanced recursive function
    1.19   defintions, thanks to Sava Krsti\'{c} and John Matthews.
    1.20  
    1.21 @@ -131,6 +129,8 @@
    1.22    Similarly for "\<Union>x. B", and for \<Inter> instead of \<Union>.
    1.23    The subscript version is also accepted as input syntax.
    1.24  
    1.25 +* ML: the legacy theory structures Int and List have been removed. They had
    1.26 +  conflicted with ML Basis Library structures having the same names.
    1.27  
    1.28  New in Isabelle2003 (May 2003)
    1.29  --------------------------------
     2.1 --- a/src/HOL/Lex/MaxChop.ML	Thu Feb 19 17:57:54 2004 +0100
     2.2 +++ b/src/HOL/Lex/MaxChop.ML	Thu Feb 19 18:24:08 2004 +0100
     2.3 @@ -80,7 +80,7 @@
     2.4                          addsplits [split_split]) 1);
     2.5  by (Clarify_tac 1);
     2.6  by (rename_tac "xs1 ys1 xss1 ys" 1);
     2.7 -by (split_asm_tac [list.split_asm] 1);
     2.8 +by (split_asm_tac [thm "list.split_asm"] 1);
     2.9   by (Asm_full_simp_tac 1);
    2.10   by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
    2.11   by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
     3.1 --- a/src/HOL/Lex/RegExp2NA.ML	Thu Feb 19 17:57:54 2004 +0100
     3.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Thu Feb 19 18:24:08 2004 +0100
     3.3 @@ -249,7 +249,7 @@
     3.4  Goalw [conc_def]
     3.5   "!L R. fin(conc L R) p = ((fin R (start R) & (? s. p = True#s & fin L s)) | \
     3.6  \                          (? s. p = False#s & fin R s))";
     3.7 -by (simp_tac (simpset() addsplits [list.split]) 1);
     3.8 +by (simp_tac (simpset() addsplits [thm"list.split"]) 1);
     3.9  by (Blast_tac 1);
    3.10  qed_spec_mp "final_conc";
    3.11  
     4.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Thu Feb 19 17:57:54 2004 +0100
     4.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Feb 19 18:24:08 2004 +0100
     4.3 @@ -408,7 +408,7 @@
     4.4  
     4.5  Goalw [conc_def]
     4.6   "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
     4.7 -by (simp_tac (simpset() addsplits [list.split]) 1);
     4.8 +by (simp_tac (simpset() addsplits [thm"list.split"]) 1);
     4.9  qed_spec_mp "final_conc";
    4.10  
    4.11  Goal
     5.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Feb 19 17:57:54 2004 +0100
     5.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Thu Feb 19 18:24:08 2004 +0100
     5.3 @@ -135,7 +135,7 @@
     5.4   "!i j xs. xs : regset d i j k = \
     5.5  \          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
     5.6  by (induct_tac "k" 1);
     5.7 - by (simp_tac (simpset() addcongs [conj_cong] addsplits [list.split]) 1);
     5.8 + by (simp_tac (simpset() addcongs [conj_cong] addsplits [thm"list.split"]) 1);
     5.9  by (strip_tac 1);
    5.10  by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
    5.11  by (rtac iffI 1);
     6.1 --- a/src/HOL/List.ML	Thu Feb 19 17:57:54 2004 +0100
     6.2 +++ b/src/HOL/List.ML	Thu Feb 19 18:24:08 2004 +0100
     6.3 @@ -1,40 +1,6 @@
     6.4  
     6.5  (** legacy ML bindings **)
     6.6  
     6.7 -structure List =
     6.8 -struct
     6.9 -
    6.10 -val thy = the_context ();
    6.11 -
    6.12 -structure list =
    6.13 -struct
    6.14 -  val distinct = thms "list.distinct";
    6.15 -  val inject = thms "list.inject";
    6.16 -  val exhaust = thm "list.exhaust";
    6.17 -  val cases = thms "list.cases";
    6.18 -  val split = thm "list.split";
    6.19 -  val split_asm = thm "list.split_asm";
    6.20 -  val induct = thm "list.induct";
    6.21 -  val recs = thms "list.recs";
    6.22 -  val simps = thms "list.simps";
    6.23 -  val size = thms "list.size";
    6.24 -end;
    6.25 -
    6.26 -structure lists =
    6.27 -struct
    6.28 -  val intrs = thms "lists.intros";
    6.29 -  val elims = thms "lists.cases";
    6.30 -  val elim = thm "lists.cases";
    6.31 -  val induct = thm "lists.induct";
    6.32 -  val mk_cases = InductivePackage.the_mk_cases (the_context ()) "List.lists";
    6.33 -  val [Nil, Cons] = intrs;
    6.34 -end;
    6.35 -
    6.36 -end;
    6.37 -
    6.38 -open List;
    6.39 -
    6.40 -
    6.41  val Cons_eq_appendI = thm "Cons_eq_appendI";
    6.42  val Cons_in_lex = thm "Cons_in_lex";
    6.43  val Nil2_notin_lex = thm "Nil2_notin_lex";
     7.1 --- a/src/HOL/MiniML/Type.ML	Thu Feb 19 17:57:54 2004 +0100
     7.2 +++ b/src/HOL/MiniML/Type.ML	Thu Feb 19 18:24:08 2004 +0100
     7.3 @@ -373,7 +373,7 @@
     7.4  Addsimps [bound_tv_subst_scheme];
     7.5  
     7.6  Goal "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A";
     7.7 -by (rtac list.induct 1);
     7.8 +by (rtac (thm"list.induct") 1);
     7.9  by (Simp_tac 1);
    7.10  by (Asm_simp_tac 1);
    7.11  qed "bound_tv_subst_scheme_list";
    7.12 @@ -627,7 +627,7 @@
    7.13  Addsimps [subst_TVar_scheme];
    7.14  
    7.15  Goal "!!A::type_scheme list. $ TVar A = A";
    7.16 -by (rtac list.induct 1);
    7.17 +by (rtac (thm"list.induct") 1);
    7.18  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [app_subst_list])));
    7.19  qed "subst_TVar_scheme_list";
    7.20  
     8.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Thu Feb 19 17:57:54 2004 +0100
     8.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Thu Feb 19 18:24:08 2004 +0100
     8.3 @@ -41,26 +41,26 @@
     8.4  
     8.5  Goal "(reduce(l)=[]) = (l=[])";  
     8.6  by (induct_tac "l" 1);
     8.7 -by (auto_tac (claset(), simpset() addsplits [list.split]));
     8.8 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
     8.9  val l_iff_red_nil = result();
    8.10  
    8.11  Goal "s~=[] --> hd(s)=hd(reduce(s))";
    8.12  by (induct_tac "s" 1);
    8.13 -by (auto_tac (claset(), simpset() addsplits [list.split]));
    8.14 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    8.15  qed"hd_is_reduce_hd";
    8.16  
    8.17  (* to be used in the following Lemma *)
    8.18  Goal "l~=[] --> reverse(reduce(l))~=[]";
    8.19  by (induct_tac "l" 1);
    8.20 -by (auto_tac (claset(), simpset() addsplits [list.split]));
    8.21 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    8.22  qed_spec_mp "rev_red_not_nil";
    8.23  
    8.24  (* shows applicability of the induction hypothesis of the following Lemma 1 *)
    8.25  Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
    8.26   by (Simp_tac 1);
    8.27 - by (asm_full_simp_tac (list_ss addsplits [list.split]
    8.28 + by (auto_tac (claset(), HOL_ss addsplits [thm"list.split"]
    8.29                                  addsimps [reverse_Cons,hd_append,
    8.30 -					  rev_red_not_nil])  1);
    8.31 +					  rev_red_not_nil]));
    8.32  qed"last_ind_on_first";
    8.33  
    8.34  val impl_ss = simpset() delsimps [reduce_Cons];
    8.35 @@ -106,7 +106,7 @@
    8.36  by (cut_inst_tac [("l","s")] cons_not_nil 1);
    8.37  by (Asm_full_simp_tac 1);
    8.38  by (REPEAT (etac exE 1));
    8.39 -by (auto_tac (claset(), simpset() addsplits [list.split]));
    8.40 +by (auto_tac (claset(), simpset() addsplits [thm"list.split"]));
    8.41  val reduce_tl =result();
    8.42  
    8.43  
    8.44 @@ -145,12 +145,12 @@
    8.45  Addsplits [split_if]; 
    8.46  
    8.47  Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
    8.48 -by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    8.49 +by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    8.50   srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
    8.51  qed"sender_abstraction";
    8.52  
    8.53  Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
    8.54 -by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    8.55 +by (simp_tac (HOL_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
    8.56   srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
    8.57  qed"receiver_abstraction";
    8.58  
     9.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Feb 19 17:57:54 2004 +0100
     9.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Thu Feb 19 18:24:08 2004 +0100
     9.3 @@ -37,16 +37,14 @@
     9.4  
     9.5  (* Lists *)
     9.6  
     9.7 -val list_ss = simpset_of List.thy;
     9.8 -
     9.9 -goal List.thy "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
    9.10 +Goal "hd(l@m) = (if l~=[] then hd(l) else hd(m))";
    9.11  by (induct_tac "l" 1);
    9.12 -by (simp_tac list_ss 1);
    9.13 -by (simp_tac list_ss 1);
    9.14 +by (Simp_tac 1);
    9.15 +by (Simp_tac 1);
    9.16  val hd_append =result();
    9.17  
    9.18 -goal List.thy "l ~= [] --> (? x xs. l = (x#xs))";
    9.19 +Goal "l ~= [] --> (? x xs. l = (x#xs))";
    9.20   by (induct_tac "l" 1);
    9.21 - by (simp_tac list_ss 1);
    9.22 + by (Simp_tac 1);
    9.23   by (Fast_tac 1);
    9.24  qed"cons_not_nil";
    10.1 --- a/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Feb 19 17:57:54 2004 +0100
    10.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.thy	Thu Feb 19 18:24:08 2004 +0100
    10.3 @@ -6,4 +6,4 @@
    10.4  Arithmetic lemmas.
    10.5  *)
    10.6  
    10.7 -Lemmas = NatArith
    10.8 +Lemmas = Main