src/HOL/ex/Reflection.thy
changeset 23649 4d865f3e4405
parent 23607 6a8fb529b542
     1.1 --- a/src/HOL/ex/Reflection.thy	Sun Jul 08 19:01:28 2007 +0200
     1.2 +++ b/src/HOL/ex/Reflection.thy	Sun Jul 08 19:01:30 2007 +0200
     1.3 @@ -21,15 +21,28 @@
     1.4  method_setup reify = {*
     1.5    fn src =>
     1.6      Method.syntax (Attrib.thms --
     1.7 -      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
     1.8 -  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ Reify_Data.get ctxt) to))
     1.9 +      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")") )) src #>
    1.10 +  (fn ((eqs, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.genreify_tac ctxt (eqs @ (fst (Reify_Data.get ctxt))) to))
    1.11  *} "partial automatic reification"
    1.12  
    1.13 -method_setup reflection = {*
    1.14 -  fn src =>
    1.15 -    Method.syntax (Attrib.thms --
    1.16 -      Scan.option (Scan.lift (Args.$$$ "(") |-- Args.term --| Scan.lift (Args.$$$ ")"))) src #>
    1.17 -  (fn ((ths, to), ctxt) => Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt (ths @ Reify_Data.get ctxt) to))
    1.18 +method_setup reflection = {* 
    1.19 +let 
    1.20 +fun keyword k = Scan.lift (Args.$$$ k -- Args.colon) >> K ();
    1.21 +val onlyN = "only";
    1.22 +val rulesN = "rules";
    1.23 +val any_keyword = keyword onlyN || keyword rulesN;
    1.24 +val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
    1.25 +val terms = thms >> map (term_of o Drule.dest_term);
    1.26 +fun optional scan = Scan.optional scan [];
    1.27 +in
    1.28 +fn src =>
    1.29 +    Method.syntax (thms -- optional (keyword rulesN |-- thms) -- Scan.option (keyword onlyN |-- Args.term)) src #> 
    1.30 +  (fn (((eqs,ths),to), ctxt) => 
    1.31 +      let 
    1.32 +        val (ceqs,cths) = Reify_Data.get ctxt 
    1.33 +        val corr_thms = ths@cths
    1.34 +        val raw_eqs = eqs@ceqs
    1.35 +      in Method.SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) 
    1.36 +     end) end
    1.37  *} "reflection method"
    1.38 -
    1.39  end