tidied
authorpaulson
Tue Apr 20 14:32:48 1999 +0200 (1999-04-20)
changeset 6451bc943acc5fda
parent 6450 990e6e2dee26
child 6452 6a1b393ccdc0
tidied
src/HOL/List.ML
src/HOL/UNITY/PPROD.ML
src/HOL/ex/Recdefs.ML
src/Sequents/ILL.ML
     1.1 --- a/src/HOL/List.ML	Mon Apr 19 17:53:38 1999 +0200
     1.2 +++ b/src/HOL/List.ML	Tue Apr 20 14:32:48 1999 +0200
     1.3 @@ -333,13 +333,11 @@
     1.4  qed "rev_map";
     1.5  
     1.6  (* a congruence rule for map: *)
     1.7 -Goal "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
     1.8 -by (rtac impI 1);
     1.9 +Goal "xs=ys ==> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
    1.10  by (hyp_subst_tac 1);
    1.11  by (induct_tac "ys" 1);
    1.12  by Auto_tac;
    1.13 -val lemma = result();
    1.14 -bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
    1.15 +bind_thm("map_cong", impI RSN (2,allI RSN (2, result() RS mp)));
    1.16  
    1.17  Goal "(map f xs = []) = (xs = [])";
    1.18  by (induct_tac "xs" 1);
     2.1 --- a/src/HOL/UNITY/PPROD.ML	Mon Apr 19 17:53:38 1999 +0200
     2.2 +++ b/src/HOL/UNITY/PPROD.ML	Tue Apr 20 14:32:48 1999 +0200
     2.3 @@ -21,12 +21,6 @@
     2.4  qed "lift_act_Id";
     2.5  Addsimps [lift_act_Id];
     2.6  
     2.7 -(*NEEDED????????????????????????????????????????????????????????????????*)
     2.8 -Goal "Id : lift_act i `` Acts F";
     2.9 -by (auto_tac (claset() addSIs [lift_act_Id RS sym], 
    2.10 -	      simpset() addsimps [image_iff]));
    2.11 -qed "Id_mem_lift_act";
    2.12 -
    2.13  Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
    2.14  by Auto_tac;
    2.15  qed "Init_lift_prog";
    2.16 @@ -133,19 +127,12 @@
    2.17  
    2.18  (** invariant **)
    2.19  
    2.20 -(*????????????????*)
    2.21 -Goal "F : invariant A ==> lift_prog i F : invariant (lift_set i A)";
    2.22 +(*UNUSED*)
    2.23 +Goal "(lift_prog i F : invariant (lift_set i A)) = (F : invariant A)";
    2.24  by (auto_tac (claset(),
    2.25  	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
    2.26 -qed "invariant_imp_lift_prog_invariant";
    2.27 +qed "lift_prog_invariant_eq";
    2.28  
    2.29 -(*????????????????*)
    2.30 -Goal "[| lift_prog i F : invariant (lift_set i A) |] ==> F : invariant A";
    2.31 -by (auto_tac (claset(),
    2.32 -	      simpset() addsimps [invariant_def, lift_prog_stable_eq]));
    2.33 -qed "lift_prog_invariant_imp_invariant";
    2.34 -
    2.35 -(*NOT clear that the previous lemmas help in proving this one.*)
    2.36  Goal "[| F i : invariant A;  i : I |] \
    2.37  \     ==> PPROD I F : invariant (lift_set i A)";
    2.38  by (auto_tac (claset(),
     3.1 --- a/src/HOL/ex/Recdefs.ML	Mon Apr 19 17:53:38 1999 +0200
     3.2 +++ b/src/HOL/ex/Recdefs.ML	Tue Apr 20 14:32:48 1999 +0200
     3.3 @@ -11,8 +11,7 @@
     3.4  
     3.5  Goal "(x: set (qsort (ord,l))) = (x: set l)";
     3.6  by (res_inst_tac [("u","ord"),("v","l")] qsort.induct 1);
     3.7 -by (ALLGOALS Asm_simp_tac);
     3.8 -by (Blast_tac 1);
     3.9 +by Auto_tac;
    3.10  qed "qsort_mem_stable";
    3.11  
    3.12  
     4.1 --- a/src/Sequents/ILL.ML	Mon Apr 19 17:53:38 1999 +0200
     4.2 +++ b/src/Sequents/ILL.ML	Tue Apr 20 14:32:48 1999 +0200
     4.3 @@ -5,9 +5,6 @@
     4.4  
     4.5  *)
     4.6  
     4.7 -open ILL;
     4.8 -
     4.9 -
    4.10  val lazy_cs = empty_pack
    4.11   add_safes [tensl, conjr, disjl, promote0,
    4.12  	    context2,context3]