src/HOL/Induct/LList.ML
changeset 4831 dae4d63a1318
parent 4818 90dab9f7d81e
child 5069 3ea049f7979d
     1.1 --- a/src/HOL/Induct/LList.ML	Mon Apr 27 16:45:11 1998 +0200
     1.2 +++ b/src/HOL/Induct/LList.ML	Mon Apr 27 16:45:27 1998 +0200
     1.3 @@ -6,13 +6,11 @@
     1.4  SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
     1.5  *)
     1.6  
     1.7 -open LList;
     1.8 -
     1.9  bind_thm ("UN1_I", UNIV_I RS UN_I);
    1.10  
    1.11  (** Simplification **)
    1.12  
    1.13 -simpset_ref() := simpset() addsplits [expand_split, expand_sum_case];
    1.14 +simpset_ref() := simpset() addsplits [split_split, split_sum_case];
    1.15  
    1.16  
    1.17  (*This justifies using llist in other recursive type definitions*)
    1.18 @@ -68,11 +66,11 @@
    1.19  
    1.20  (*UNUSED; obsolete?
    1.21  goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
    1.22 -by (simp_tac (simpset() addsplits [expand_split]) 1);
    1.23 +by (Simp_tac 1);
    1.24  qed "split_UN1";
    1.25  
    1.26  goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
    1.27 -by (simp_tac (simpset() addsplits [expand_sum_case]) 1);
    1.28 +by (Simp_tac 1);
    1.29  qed "sum_case2_UN1";
    1.30  *)
    1.31  
    1.32 @@ -318,7 +316,7 @@
    1.33  by (rename_tac "y" 1);
    1.34  by (stac prem1 1);
    1.35  by (stac prem2 1);
    1.36 -by (simp_tac (simpset() addsplits [expand_sum_case]) 1);
    1.37 +by (Simp_tac 1);
    1.38  by (strip_tac 1);
    1.39  by (res_inst_tac [("n", "n")] natE 1);
    1.40  by (rename_tac "m" 2);
    1.41 @@ -366,15 +364,15 @@
    1.42  by (rtac Rep_llist_inverse 1);
    1.43  qed "inj_Rep_llist";
    1.44  
    1.45 -goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
    1.46 -by (rtac inj_onto_inverseI 1);
    1.47 +goal LList.thy "inj_on Abs_llist (llist(range Leaf))";
    1.48 +by (rtac inj_on_inverseI 1);
    1.49  by (etac Abs_llist_inverse 1);
    1.50 -qed "inj_onto_Abs_llist";
    1.51 +qed "inj_on_Abs_llist";
    1.52  
    1.53  (** Distinctness of constructors **)
    1.54  
    1.55  goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil";
    1.56 -by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1);
    1.57 +by (rtac (CONS_not_NIL RS (inj_on_Abs_llist RS inj_on_contraD)) 1);
    1.58  by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
    1.59  qed "LCons_not_LNil";
    1.60  
    1.61 @@ -408,7 +406,7 @@
    1.62  (*For reasoning about abstract llist constructors*)
    1.63  
    1.64  AddIs ([Rep_llist]@llist.intrs);
    1.65 -AddSDs [inj_onto_Abs_llist RS inj_ontoD,
    1.66 +AddSDs [inj_on_Abs_llist RS inj_onD,
    1.67          inj_Rep_llist RS injD, Leaf_inject];
    1.68  
    1.69  goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";