added attributes, method modifiers, theory setup;
authorwenzelm
Wed Mar 15 18:38:52 2000 +0100 (2000-03-15 ago)
changeset 8468d99902232df8
parent 8467 58dbeea60bb8
child 8469 482c301041b4
added attributes, method modifiers, theory setup;
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Wed Mar 15 18:36:53 2000 +0100
     1.2 +++ b/src/Provers/splitter.ML	Wed Mar 15 18:38:52 2000 +0100
     1.3 @@ -32,12 +32,19 @@
     1.4    val delsplits       : simpset * thm list -> simpset
     1.5    val Addsplits       : thm list -> unit
     1.6    val Delsplits       : thm list -> unit
     1.7 +  val split_add_global: theory attribute
     1.8 +  val split_del_global: theory attribute
     1.9 +  val split_add_local: Proof.context attribute
    1.10 +  val split_del_local: Proof.context attribute
    1.11 +  val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
    1.12 +  val setup: (theory -> theory) list
    1.13  end;
    1.14  
    1.15  functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
    1.16  struct 
    1.17  
    1.18 -type simpset = Data.Simplifier.simpset;
    1.19 +structure Simplifier = Data.Simplifier;
    1.20 +type simpset = Simplifier.simpset;
    1.21  
    1.22  val Const ("==>", _) $ (Const ("Trueprop", _) $
    1.23           (Const (const_not, _) $ _    )) $ _ = #prop (rep_thm(Data.notnotD));
    1.24 @@ -361,24 +368,68 @@
    1.25    in SUBGOAL tac
    1.26    end;
    1.27  
    1.28 +
    1.29 +
    1.30 +(** declare split rules **)
    1.31 +
    1.32 +(* addsplits / delsplits *)
    1.33 +
    1.34  fun split_name name asm = "split " ^ name ^ (if asm then " asm" else "");
    1.35  
    1.36  fun ss addsplits splits =
    1.37    let fun addsplit (ss,split) =
    1.38          let val (name,asm) = split_thm_info split
    1.39 -        in Data.Simplifier.addloop(ss,(split_name name asm,
    1.40 +        in Simplifier.addloop(ss,(split_name name asm,
    1.41  		       (if asm then split_asm_tac else split_tac) [split])) end
    1.42    in foldl addsplit (ss,splits) end;
    1.43  
    1.44  fun ss delsplits splits =
    1.45    let fun delsplit(ss,split) =
    1.46          let val (name,asm) = split_thm_info split
    1.47 -        in Data.Simplifier.delloop(ss,split_name name asm)
    1.48 +        in Simplifier.delloop(ss,split_name name asm)
    1.49    end in foldl delsplit (ss,splits) end;
    1.50  
    1.51 -fun Addsplits splits = (Data.Simplifier.simpset_ref() := 
    1.52 -			Data.Simplifier.simpset() addsplits splits);
    1.53 -fun Delsplits splits = (Data.Simplifier.simpset_ref() := 
    1.54 -			Data.Simplifier.simpset() delsplits splits);
    1.55 +fun Addsplits splits = (Simplifier.simpset_ref() := 
    1.56 +			Simplifier.simpset() addsplits splits);
    1.57 +fun Delsplits splits = (Simplifier.simpset_ref() := 
    1.58 +			Simplifier.simpset() delsplits splits);
    1.59 +
    1.60 +
    1.61 +(* attributes *)
    1.62 +
    1.63 +val splitN = "split";
    1.64 +val addN = "add";
    1.65 +val delN = "del";
    1.66 +
    1.67 +fun split_att change =
    1.68 +  (Args.$$$ addN >> K (op addsplits) ||
    1.69 +    Args.$$$ delN >> K (op delsplits) ||
    1.70 +    Scan.succeed (op addsplits))
    1.71 +  >> change
    1.72 +  |> Scan.lift
    1.73 +  |> Attrib.syntax;
    1.74 +
    1.75 +val setup_attrs = Attrib.add_attributes
    1.76 + [(splitN, (split_att Simplifier.change_global_ss, split_att Simplifier.change_local_ss),
    1.77 +    "declare splitter rule")];
    1.78 +
    1.79 +val split_add_global = Simplifier.change_global_ss (op addsplits);
    1.80 +val split_del_global = Simplifier.change_global_ss (op delsplits);
    1.81 +val split_add_local = Simplifier.change_local_ss (op addsplits);
    1.82 +val split_del_local = Simplifier.change_local_ss (op delsplits);
    1.83 +
    1.84 +
    1.85 +(* method modifiers *)
    1.86 +
    1.87 +val split_modifiers =
    1.88 + [Args.$$$ splitN -- Args.$$$ ":" >> K (I, split_add_local),
    1.89 +  Args.$$$ splitN -- Args.$$$ addN -- Args.$$$ ":" >> K (I, split_add_local),
    1.90 +  Args.$$$ splitN -- Args.$$$ delN -- Args.$$$ ":" >> K (I, split_del_local)];
    1.91 +
    1.92 +
    1.93 +
    1.94 +(** theory setup **)
    1.95 +
    1.96 +val setup = [setup_attrs];
    1.97  
    1.98  end;