CTT.ML/SumE_fst,SumE_snd: tidied
authorlcp
Wed May 04 18:00:14 1994 +0200 (1994-05-04)
changeset 3610aeff597d4b1
parent 360 2b74eebdbdb8
child 362 6bea8fdc0e70
CTT.ML/SumE_fst,SumE_snd: tidied
src/CTT/CTT.ML
     1.1 --- a/src/CTT/CTT.ML	Wed May 04 17:47:30 1994 +0200
     1.2 +++ b/src/CTT/CTT.ML	Wed May 04 18:00:14 1994 +0200
     1.3 @@ -222,27 +222,20 @@
     1.4  
     1.5  (** The elimination rules for fst/snd **)
     1.6  
     1.7 -val SumE_fst = prove_goal CTT.thy 
     1.8 +val SumE_fst = prove_goalw CTT.thy basic_defs
     1.9      "p : Sum(A,B) ==> fst(p) : A"
    1.10 - (fn prems=>
    1.11 -  [ (rewrite_goals_tac basic_defs),
    1.12 -    (resolve_tac elim_rls 1),
    1.13 -    (REPEAT (pc_tac prems 1)),
    1.14 -    (fold_tac basic_defs) ]);
    1.15 + (fn [major] =>
    1.16 +  [ (rtac (major RS SumE) 1),
    1.17 +    (assume_tac 1) ]);
    1.18  
    1.19  (*The first premise must be p:Sum(A,B) !!*)
    1.20 -val SumE_snd = prove_goal CTT.thy 
    1.21 +val SumE_snd = prove_goalw CTT.thy basic_defs
    1.22      "[| p: Sum(A,B);  A type;  !!x. x:A ==> B(x) type \
    1.23  \    |] ==> snd(p) : B(fst(p))"
    1.24 - (fn prems=>
    1.25 -  [ (rewrite_goals_tac basic_defs),
    1.26 -    (resolve_tac elim_rls 1),
    1.27 -    (resolve_tac prems 1),
    1.28 -    (resolve_tac [replace_type] 1),
    1.29 -    (resolve_tac [subst_eqtyparg] 1),   (*like B(x) equality formation?*)
    1.30 -    (resolve_tac comp_rls 1),
    1.31 -    (typechk_tac prems),
    1.32 -    (fold_tac basic_defs) ]);
    1.33 + (fn major::prems=>
    1.34 +  [ (rtac (major RS SumE) 1),
    1.35 +    (resolve_tac [SumC RS subst_eqtyparg RS replace_type] 1),
    1.36 +    (typechk_tac prems) ]);
    1.37  
    1.38  end;
    1.39