allow theorem attributes on fixpat declarations
authorhuffman
Wed Jun 15 21:48:35 2005 +0200 (2005-06-15)
changeset 1640236f41d5e3b3e
parent 16401 57c35ede00b9
child 16403 294a7864063e
allow theorem attributes on fixpat declarations
src/HOLCF/fixrec_package.ML
     1.1 --- a/src/HOLCF/fixrec_package.ML	Wed Jun 15 20:50:38 2005 +0200
     1.2 +++ b/src/HOLCF/fixrec_package.ML	Wed Jun 15 21:48:35 2005 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  signature FIXREC_PACKAGE =
     1.5  sig
     1.6    val add_fixrec: string list list -> theory -> theory
     1.7 -  val add_fixpat: string * string -> theory -> theory
     1.8 +  val add_fixpat: ((string * Attrib.src list) * string) list -> theory -> theory
     1.9  end;
    1.10  
    1.11  structure FixrecPackage: FIXREC_PACKAGE =
    1.12 @@ -42,13 +42,11 @@
    1.13  infix 9 `  ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x;
    1.14  
    1.15  (* infers the type of a term *)
    1.16 -(* similar to Theory.inferT_axm, but allows any type *)
    1.17 +(* similar to Theory.inferT_axm, but allows any type, not just propT *)
    1.18  fun infer sg t =
    1.19    fst (Sign.infer_types (Sign.pp sg) sg (K NONE) (K NONE) [] true ([t],dummyT));
    1.20  
    1.21 -(* The next few functions build continuous lambda abstractions *)
    1.22 -
    1.23 -(* Similar to Term.lambda, but allows abstraction over constants *)
    1.24 +(* Similar to Term.lambda, but also allows abstraction over constants *)
    1.25  fun lambda' (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
    1.26    | lambda' (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
    1.27    | lambda' (v as Const (x, T)) t = Abs (Sign.base_name x, T, abstract_over (v, t))
    1.28 @@ -73,7 +71,7 @@
    1.29  |   mk_ctuple (t::ts) = %%:"Cprod.cpair"`t`(mk_ctuple ts);
    1.30  
    1.31  (*************************************************************************)
    1.32 -(************************ fixed-point definitions ************************)
    1.33 +(************* fixed-point definitions and unfolding theorems ************)
    1.34  (*************************************************************************)
    1.35  
    1.36  fun add_fixdefs eqs thy =
    1.37 @@ -224,22 +222,6 @@
    1.38      (#1 o PureThy.add_thmss (map Thm.no_attributes thmss)) thy
    1.39    end;
    1.40  
    1.41 -(* this proves the def without fix is a theorem, this uses the fixpoint def *)
    1.42 -(*
    1.43 -fun make_simp name eqs ct fixdef_thm thy' = 
    1.44 -  let
    1.45 -    val ss = simpset_of thy';
    1.46 -    val eq_thm = fixdef_thm RS fix_eq2;
    1.47 -    val ind_thm = fixdef_thm RS def_fix_ind;
    1.48 -    val rew_thms = prove_list thy' unfold_thm eqs;
    1.49 -    val thmss =
    1.50 -      [ (basename^"_unfold", [unfold_thm])
    1.51 -      , (basename^"_ind", [ind_thm])
    1.52 -      , (basename^"_rews", rew_thms) ]
    1.53 -  in
    1.54 -    (#1 o PureThy.add_thmss (map Thm.no_attributes thmss)) thy'
    1.55 -  end;
    1.56 -*)
    1.57  (*************************************************************************)
    1.58  (************************* Main fixrec function **************************)
    1.59  (*************************************************************************)
    1.60 @@ -260,10 +242,10 @@
    1.61  (******************************** Fixpat *********************************)
    1.62  (*************************************************************************)
    1.63  
    1.64 -fun fix_pat name pat thy = 
    1.65 +fun fix_pat thy pat = 
    1.66    let
    1.67 -    val sign = sign_of thy;
    1.68 -    val t = term_of (Thm.read_cterm sign (pat, dummyT));
    1.69 +    val sg = sign_of thy;
    1.70 +    val t = term_of (Thm.read_cterm sg (pat, dummyT));
    1.71      val T = fastype_of t;
    1.72      val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
    1.73      fun head_const (Const ("Cfun.Rep_CFun",_) $ f $ t) = head_const f
    1.74 @@ -271,14 +253,17 @@
    1.75        | head_const _ = sys_error "FIXPAT: function is not declared as constant in theory";
    1.76      val c = head_const t;
    1.77      val unfold_thm = Goals.get_thm thy (c^"_unfold");
    1.78 -    val thm = prove_goalw_cterm [] (cterm_of sign eq)
    1.79 +    val rew = prove_goalw_cterm [] (cterm_of sg eq)
    1.80            (fn _ => [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
    1.81 -    val _ = print_thm thm;
    1.82 -  in
    1.83 -    (#1 o PureThy.add_thmss [Thm.no_attributes (name, [thm])]) thy
    1.84 -  end;
    1.85 +  in rew end;
    1.86  
    1.87 -fun add_fixpat (name,pat) = fix_pat name pat;
    1.88 +fun add_fixpat pats thy = 
    1.89 +  let
    1.90 +    val ((names, srcss), strings) = apfst ListPair.unzip (ListPair.unzip pats);
    1.91 +    val atts = map (map (Attrib.global_attribute thy)) srcss;
    1.92 +    val rews = map (fix_pat thy) strings;
    1.93 +    val (thy', _) = PureThy.add_thms ((names ~~ rews) ~~ atts) thy;
    1.94 +  in thy' end;
    1.95  
    1.96  (*************************************************************************)
    1.97  (******************************** Parsers ********************************)
    1.98 @@ -291,17 +276,18 @@
    1.99  (* this builds a parser for a new keyword, fixrec, whose functionality 
   1.100  is defined by add_fixrec *)
   1.101  val fixrecP =
   1.102 -  OuterSyntax.command "fixrec" "parser for fixrec functions" K.thy_decl
   1.103 +  OuterSyntax.command "fixrec" "define recursive functions (HOLCF)" K.thy_decl
   1.104      (fixrec_decl >> (Toplevel.theory o add_fixrec));
   1.105  
   1.106  (* this adds the parser for fixrec to the syntax *)
   1.107  val _ = OuterSyntax.add_parsers [fixrecP];
   1.108  
   1.109  (* fixpat parser *)
   1.110 -val fixpat_decl = P.name -- P.prop;
   1.111 +(*val fixpat_decl = P.name -- P.prop;*)
   1.112 +val fixpat_decl = Scan.repeat1 (P.thm_name ":" -- P.prop);
   1.113  
   1.114  val fixpatP =
   1.115 -  OuterSyntax.command "fixpat" "testing out this parser" K.thy_decl
   1.116 +  OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl
   1.117      (fixpat_decl >> (Toplevel.theory o add_fixpat));
   1.118  
   1.119  val _ = OuterSyntax.add_parsers [fixpatP];