adapted to new PureThy.add_thms etc.;
authorwenzelm
Mon Mar 13 13:28:31 2000 +0100 (2000-03-13)
changeset 8438b8389b4fca9c
parent 8437 258281c43dea
child 8439 17e62ef34ec8
adapted to new PureThy.add_thms etc.;
TFL/tfl.sml
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/theorems.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/TFL/tfl.sml	Mon Mar 13 13:27:44 2000 +0100
     1.2 +++ b/TFL/tfl.sml	Mon Mar 13 13:28:31 2000 +0100
     1.3 @@ -381,7 +381,7 @@
     1.4  	                  (wfrec $ map_term_types poly_tvars R) 
     1.5  	              $ functional
     1.6       val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M)
     1.7 -  in  PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy  end
     1.8 +  in  #1 (PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy)  end
     1.9  end;
    1.10  
    1.11  
    1.12 @@ -534,11 +534,11 @@
    1.13       val (Name,Ty) = dest_atom c
    1.14       val defn = mk_const_def (Theory.sign_of thy) 
    1.15                   (Name, Ty, S.list_mk_abs (args,rhs)) 
    1.16 -     val theory =
    1.17 +     val (theory, [def0]) =
    1.18         thy
    1.19         |> PureThy.add_defs_i 
    1.20              [Thm.no_attributes (fid ^ "_def", defn)]
    1.21 -     val def = freezeT (get_thm theory (fid ^ "_def"))
    1.22 +     val def = freezeT def0;
    1.23       val dummy = if !trace then writeln ("DEF = " ^ string_of_thm def)
    1.24  	                   else ()
    1.25       (* val fconst = #lhs(S.dest_eq(concl def))  *)
     2.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Mar 13 13:27:44 2000 +0100
     2.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Mon Mar 13 13:28:31 2000 +0100
     2.3 @@ -360,7 +360,7 @@
     2.4  (automaton_name ^ "_trans",
     2.5   "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
     2.6  (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
     2.7 -|> (PureThy.add_defs o map Thm.no_attributes) (* old: Attributes.none *)
     2.8 +|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
     2.9  [(automaton_name ^ "_initial_def",
    2.10  automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
    2.11  (automaton_name ^ "_asig_def",
    2.12 @@ -401,7 +401,7 @@
    2.13    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    2.14     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
    2.15  ,NoSyn)]
    2.16 -|> (PureThy.add_defs o map Thm.no_attributes)
    2.17 +|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
    2.18  [(automaton_name ^ "_def",
    2.19  automaton_name ^ " == " ^ comp_list)]
    2.20  end)
    2.21 @@ -416,7 +416,7 @@
    2.22  thy
    2.23  |> ContConsts.add_consts_i
    2.24  [(automaton_name, auttyp,NoSyn)]
    2.25 -|> (PureThy.add_defs o map Thm.no_attributes)
    2.26 +|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
    2.27  [(automaton_name ^ "_def",
    2.28  automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] 
    2.29  end)
    2.30 @@ -430,7 +430,7 @@
    2.31  thy
    2.32  |> ContConsts.add_consts_i
    2.33  [(automaton_name, auttyp,NoSyn)]
    2.34 -|> (PureThy.add_defs o map Thm.no_attributes)
    2.35 +|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
    2.36  [(automaton_name ^ "_def",
    2.37  automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] 
    2.38  end)
    2.39 @@ -462,7 +462,7 @@
    2.40    Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
    2.41     Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
    2.42  ,NoSyn)]
    2.43 -|> (PureThy.add_defs o map Thm.no_attributes)
    2.44 +|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
    2.45  [(automaton_name ^ "_def",
    2.46  automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
    2.47  end)
     3.1 --- a/src/HOLCF/domain/axioms.ML	Mon Mar 13 13:27:44 2000 +0100
     3.2 +++ b/src/HOLCF/domain/axioms.ML	Mon Mar 13 13:28:31 2000 +0100
     3.3 @@ -86,7 +86,7 @@
     3.4      [take_def, finite_def])
     3.5  end; (* let *)
     3.6  
     3.7 -val add_axioms_i = PureThy.add_axioms_i o map Thm.no_attributes;
     3.8 +fun add_axioms_i x = #1 o PureThy.add_axioms_i (map Thm.no_attributes x);
     3.9  
    3.10  in (* local *)
    3.11  
     4.1 --- a/src/HOLCF/domain/theorems.ML	Mon Mar 13 13:27:44 2000 +0100
     4.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Mar 13 13:28:31 2000 +0100
     4.3 @@ -315,7 +315,7 @@
     4.4                          (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
     4.5  val copy_rews = copy_strict::copy_apps @ copy_stricts;
     4.6  in thy |> Theory.add_path (Sign.base_name dname)
     4.7 -       |> (PureThy.add_thmss o map Thm.no_attributes) [
     4.8 +       |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
     4.9  		("iso_rews" , iso_rews  ),
    4.10  		("exhaust"  , [exhaust] ),
    4.11  		("casedist" , [casedist]),
    4.12 @@ -327,7 +327,7 @@
    4.13  		("dist_eqs", dist_eqs),
    4.14  		("inverts" , inverts ),
    4.15  		("injects" , injects ),
    4.16 -		("copy_rews", copy_rews)]
    4.17 +		("copy_rews", copy_rews)])))
    4.18         |> Theory.parent_path
    4.19  end; (* let *)
    4.20  
    4.21 @@ -590,13 +590,13 @@
    4.22  
    4.23  
    4.24  in thy |> Theory.add_path comp_dnam
    4.25 -       |> (PureThy.add_thmss o map Thm.no_attributes) [
    4.26 +       |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
    4.27  		("take_rews"  , take_rews  ),
    4.28  		("take_lemmas", take_lemmas),
    4.29  		("finites"    , finites    ),
    4.30  		("finite_ind", [finite_ind]),
    4.31  		("ind"       , [ind       ]),
    4.32 -		("coind"     , [coind     ])]
    4.33 +		("coind"     , [coind     ])])))
    4.34         |> Theory.parent_path
    4.35  end; (* let *)
    4.36  end; (* local *)
     5.1 --- a/src/ZF/Tools/datatype_package.ML	Mon Mar 13 13:27:44 2000 +0100
     5.2 +++ b/src/ZF/Tools/datatype_package.ML	Mon Mar 13 13:28:31 2000 +0100
     5.3 @@ -245,10 +245,10 @@
     5.4        if need_recursor then
     5.5  	   thy |> Theory.add_consts_i 
     5.6  	            [(recursor_base_name, recursor_typ, NoSyn)]
     5.7 -	       |> PureThy.add_defs_i [Thm.no_attributes recursor_def]
     5.8 +	       |> (#1 o PureThy.add_defs_i [Thm.no_attributes recursor_def])
     5.9        else thy;
    5.10  
    5.11 -  val thy0 = thy_path
    5.12 +  val (thy0, con_defs) = thy_path
    5.13  	     |> Theory.add_consts_i 
    5.14  		 ((case_base_name, case_typ, NoSyn) ::
    5.15  		  map #1 (flat con_ty_lists))
    5.16 @@ -257,11 +257,8 @@
    5.17  		  (case_def :: 
    5.18  		   flat (ListPair.map mk_con_defs
    5.19  			 (1 upto npart, con_ty_lists))))
    5.20 -	     |> add_recursor
    5.21 -	     |> Theory.parent_path
    5.22 -
    5.23 -  val con_defs = get_def thy0 case_name :: 
    5.24 -		 map (get_def thy0 o #2) (flat con_ty_lists);
    5.25 +	     |>> add_recursor
    5.26 +	     |>> Theory.parent_path
    5.27  
    5.28    val (thy1, ind_result) = 
    5.29           thy0  |> Ind_Package.add_inductive_i
    5.30 @@ -390,12 +387,12 @@
    5.31   in
    5.32    (*Updating theory components: simprules and datatype info*)
    5.33    (thy1 |> Theory.add_path big_rec_base_name
    5.34 -        |> PureThy.add_thmss [(("simps", simps), 
    5.35 -			       [Simplifier.simp_add_global])]
    5.36 -        |> PureThy.add_thmss [(("", intrs),   
    5.37 +        |> (#1 o PureThy.add_thmss [(("simps", simps), 
    5.38 +			       [Simplifier.simp_add_global])])
    5.39 +        |> (#1 o PureThy.add_thmss [(("", intrs),   
    5.40                                  (*not "intrs" to avoid the warning that they
    5.41  				  are already stored by the inductive package*)
    5.42 -			       [Classical.safe_intro_global])]
    5.43 +			       [Classical.safe_intro_global])])
    5.44          |> DatatypesData.put 
    5.45  	    (Symtab.update
    5.46  	     ((big_rec_name, dt_info), DatatypesData.get thy1)) 
     6.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Mar 13 13:27:44 2000 +0100
     6.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Mar 13 13:28:31 2000 +0100
     6.3 @@ -175,7 +175,7 @@
     6.4  
     6.5    in
     6.6        thy |> Theory.add_path (Sign.base_name big_rec_name)
     6.7 -	  |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
     6.8 +	  |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
     6.9  	  |> DatatypesData.put 
    6.10  	      (Symtab.update
    6.11  	       ((big_rec_name, dt_info), DatatypesData.get thy)) 
     7.1 --- a/src/ZF/Tools/inductive_package.ML	Mon Mar 13 13:27:44 2000 +0100
     7.2 +++ b/src/ZF/Tools/inductive_package.ML	Mon Mar 13 13:28:31 2000 +0100
     7.3 @@ -182,7 +182,7 @@
     7.4  
     7.5    (*add definitions of the inductive sets*)
     7.6    val thy1 = thy |> Theory.add_path big_rec_base_name
     7.7 -                 |> PureThy.add_defs_i (map Thm.no_attributes axpairs)  
     7.8 +                 |> (#1 o PureThy.add_defs_i (map Thm.no_attributes axpairs))
     7.9  
    7.10  
    7.11    (*fetch fp definitions from the theory*)
    7.12 @@ -531,12 +531,10 @@
    7.13       val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0) 
    7.14  		  |> standard
    7.15       and mutual_induct = CP.remove_split mutual_induct_fsplit
    7.16 -    in
    7.17 -      (thy
    7.18 -	|> PureThy.add_thms 
    7.19 -	    [(("induct", induct), []),
    7.20 -	     (("mutual_induct", mutual_induct), [])],
    7.21 -       induct, mutual_induct)
    7.22 +
    7.23 +     val (thy', [induct', mutual_induct']) =
    7.24 +	thy |> PureThy.add_thms [(("induct", induct), []), (("mutual_induct", mutual_induct), [])];
    7.25 +    in (thy', induct', mutual_induct')
    7.26      end;  (*of induction_rules*)
    7.27  
    7.28    val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
    7.29 @@ -546,26 +544,28 @@
    7.30        else (thy1, raw_induct, TrueI)
    7.31    and defs = big_rec_def :: part_rec_defs
    7.32  
    7.33 - in
    7.34 -   (thy2
    7.35 -	 |> (PureThy.add_thms o map Thm.no_attributes)
    7.36 -	      [("bnd_mono", bnd_mono),
    7.37 -	       ("dom_subset", dom_subset),
    7.38 -	       ("elim", elim)]
    7.39 -	 |> (PureThy.add_thmss o map Thm.no_attributes)
    7.40 -	       [("defs", defs),
    7.41 -		("intrs", intrs)]
    7.42 -         |> Theory.parent_path,
    7.43 -    {defs = defs,
    7.44 -     bnd_mono = bnd_mono,
    7.45 -     dom_subset = dom_subset,
    7.46 -     intrs = intrs,
    7.47 -     elim = elim,
    7.48 -     mk_cases = mk_cases,
    7.49 -     induct = induct,
    7.50 -     mutual_induct = mutual_induct})
    7.51  
    7.52 - end;
    7.53 +  val (thy3, ([bnd_mono', dom_subset', elim'], [defs', intrs'])) =
    7.54 +    thy2
    7.55 +    |> (PureThy.add_thms o map Thm.no_attributes)
    7.56 +        [("bnd_mono", bnd_mono),
    7.57 +         ("dom_subset", dom_subset),
    7.58 +         ("elim", elim)]
    7.59 +    |>>> (PureThy.add_thmss o map Thm.no_attributes)
    7.60 +        [("defs", defs),
    7.61 +         ("intrs", intrs)]
    7.62 +    |>> Theory.parent_path;
    7.63 +  in
    7.64 +    (thy3,
    7.65 +      {defs = defs',
    7.66 +       bnd_mono = bnd_mono',
    7.67 +       dom_subset = dom_subset',
    7.68 +       intrs = intrs',
    7.69 +       elim = elim',
    7.70 +       mk_cases = mk_cases,
    7.71 +       induct = induct,
    7.72 +       mutual_induct = mutual_induct})
    7.73 +  end;
    7.74  
    7.75  
    7.76  (*external version, accepting strings*)
     8.1 --- a/src/ZF/Tools/primrec_package.ML	Mon Mar 13 13:27:44 2000 +0100
     8.2 +++ b/src/ZF/Tools/primrec_package.ML	Mon Mar 13 13:28:31 2000 +0100
     8.3 @@ -167,10 +167,9 @@
     8.4      val Some (fname, ftype, ls, rs, con_info, eqns) = 
     8.5  	foldr (process_eqn thy) (map snd recursion_eqns, None);
     8.6      val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns) 
     8.7 -    val thy' = thy |> Theory.add_path (Sign.base_name (#1 def))
     8.8 +    val (thy', [def_thm]) = thy |> Theory.add_path (Sign.base_name (#1 def))
     8.9                     |> (PureThy.add_defs_i o map Thm.no_attributes) [def]
    8.10 -    val rewrites = get_thm thy' (#1 def) ::
    8.11 -	           map mk_meta_eq (#rec_rewrites con_info)
    8.12 +    val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)
    8.13      val char_thms = 
    8.14  	(if !Ind_Syntax.trace then	(* FIXME message / quiet_mode (!?) *)
    8.15  	     writeln ("Proving equations for primrec function " ^ fname)
    8.16 @@ -183,9 +182,9 @@
    8.17  	 recursion_eqns);
    8.18      val simps = char_thms;
    8.19      val thy'' = thy' 
    8.20 -      |> PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])]
    8.21 -      |> PureThy.add_thms (map (rpair [])
    8.22 -         (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps)))
    8.23 +      |> (#1 o PureThy.add_thmss [(("simps", simps), [Simplifier.simp_add_global])])
    8.24 +      |> (#1 o PureThy.add_thms (map (rpair [])
    8.25 +         (filter_out (equal "_" o fst) (map fst recursion_eqns ~~ simps))))
    8.26        |> Theory.parent_path;
    8.27    in
    8.28      (thy'', char_thms)