use Tactic.prove;
authorwenzelm
Sat Nov 10 16:25:17 2001 +0100 (2001-11-10)
changeset 121347049eead7a50
parent 12133 f314630235a4
child 12135 e370e5d469c2
use Tactic.prove;
src/ZF/Datatype.ML
src/ZF/arith_data.ML
     1.1 --- a/src/ZF/Datatype.ML	Fri Nov 09 23:44:48 2001 +0100
     1.2 +++ b/src/ZF/Datatype.ML	Sat Nov 10 16:25:17 2001 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5  
     1.6    val elims = [make_elim InlD, make_elim InrD,   (*for mutual recursion*)
     1.7 -	       SigmaE, sumE];			 (*allows * and + in spec*)
     1.8 +               SigmaE, sumE];                    (*allows * and + in spec*)
     1.9    end;
    1.10  
    1.11  
    1.12 @@ -38,35 +38,32 @@
    1.13         zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
    1.14  
    1.15    val elims = [make_elim QInlD, make_elim QInrD,   (*for mutual recursion*)
    1.16 -	       QSigmaE, qsumE];			   (*allows * and + in spec*)
    1.17 +               QSigmaE, qsumE];                    (*allows * and + in spec*)
    1.18    end;
    1.19  
    1.20  structure CoData_Package = 
    1.21      Add_datatype_def_Fun(structure Fp=Gfp and Pr=Quine_Prod and CP=Quine_CP
    1.22                            and Su=Quine_Sum
    1.23 -			  and Ind_Package = CoInd_Package
    1.24 -			  and Datatype_Arg = CoData_Arg);
    1.25 +                          and Ind_Package = CoInd_Package
    1.26 +                          and Datatype_Arg = CoData_Arg);
    1.27  
    1.28  
    1.29  
    1.30  (*Simproc for freeness reasoning: compare datatype constructors for equality*)
    1.31  structure DataFree =
    1.32  struct
    1.33 -  (*prove while suppressing timing information*)
    1.34 -  fun prove ct = setmp Library.timing false (prove_goalw_cterm [] ct);
    1.35 -
    1.36    val trace = ref false;
    1.37  
    1.38    fun mk_new ([],[]) = Const("True",FOLogic.oT)
    1.39      | mk_new (largs,rargs) =
    1.40 -	fold_bal FOLogic.mk_conj
    1.41 -		 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    1.42 +        fold_bal FOLogic.mk_conj
    1.43 +                 (map FOLogic.mk_eq (ListPair.zip (largs,rargs)));
    1.44  
    1.45  
    1.46   fun proc sg _ old =
    1.47     let val _ = if !trace then writeln ("data_free: OLD = " ^ 
    1.48 -				       string_of_cterm (cterm_of sg old))
    1.49 -	       else ()
    1.50 +                                       string_of_cterm (cterm_of sg old))
    1.51 +               else ()
    1.52         val (lhs,rhs) = FOLogic.dest_eq old
    1.53         val (lhead, largs) = strip_comb lhs
    1.54         and (rhead, rargs) = strip_comb rhs
    1.55 @@ -75,22 +72,19 @@
    1.56         val lcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, lname))
    1.57         and rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
    1.58         val new = 
    1.59 -	   if #big_rec_name lcon_info = #big_rec_name rcon_info 
    1.60 -	       andalso not (null (#free_iffs lcon_info)) then
    1.61 -	       if lname = rname then mk_new (largs, rargs)
    1.62 -	       else Const("False",FOLogic.oT)
    1.63 -	   else raise Match
    1.64 +           if #big_rec_name lcon_info = #big_rec_name rcon_info 
    1.65 +               andalso not (null (#free_iffs lcon_info)) then
    1.66 +               if lname = rname then mk_new (largs, rargs)
    1.67 +               else Const("False",FOLogic.oT)
    1.68 +           else raise Match
    1.69         val _ = if !trace then 
    1.70 -		 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
    1.71 -	       else ()
    1.72 -       val ct = Thm.cterm_of sg (Logic.mk_equals (old, new))
    1.73 -       val thm = prove ct 
    1.74 -		   (fn _ => [rtac iff_reflection 1,
    1.75 -			     simp_tac (simpset_of Datatype.thy
    1.76 -  				          addsimps #free_iffs lcon_info) 1])
    1.77 -	 handle ERROR =>
    1.78 -	 error("data_free simproc:\nfailed to prove " ^
    1.79 -	       string_of_cterm ct)
    1.80 +                 writeln ("NEW = " ^ string_of_cterm (Thm.cterm_of sg new))
    1.81 +               else ();
    1.82 +       val goal = Logic.mk_equals (old, new)
    1.83 +       val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
    1.84 +           simp_tac (simpset_of Datatype.thy addsimps #free_iffs lcon_info) 1)
    1.85 +         handle ERROR =>
    1.86 +         error ("data_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal)
    1.87     in Some thm end
    1.88     handle _ => None;
    1.89  
     2.1 --- a/src/ZF/arith_data.ML	Fri Nov 09 23:44:48 2001 +0100
     2.2 +++ b/src/ZF/arith_data.ML	Sat Nov 10 16:25:17 2001 +0100
     2.3 @@ -72,16 +72,11 @@
     2.4    if t aconv u then None
     2.5    else
     2.6    let val hyps' = filter (not o is_eq_thm) hyps
     2.7 -      val ct = add_chyps hyps'
     2.8 -                  (cterm_of sg (FOLogic.mk_Trueprop (mk_eq_iff(t, u))))
     2.9 -  in Some
    2.10 -      (hyps' MRS 
    2.11 -       (prove_goalw_cterm [] ct 
    2.12 -	(fn prems => cut_facts_tac prems 1 :: tacs)))
    2.13 +      val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    2.14 +        FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    2.15 +  in Some (hyps' MRS Tactic.prove sg [] [] goal (K (EVERY tacs)))
    2.16        handle ERROR => 
    2.17 -	(warning 
    2.18 -	 ("Cancellation failed: no typing information? (" ^ name ^ ")"); 
    2.19 -	 None)
    2.20 +	(warning ("Cancellation failed: no typing information? (" ^ name ^ ")"); None)
    2.21    end;
    2.22  
    2.23  fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;