Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
authorchaieb
Sun Jul 08 19:01:30 2007 +0200 (2007-07-08)
changeset 236494d865f3e4405
parent 23648 bccbf6138c30
child 23650 0a6a719d24d5
Changed syntax for the reflection method (reify unchanged). reflection takes an optional set of theorems for reification then several correctness theorems are specified by rules:'' then the optional term is specified by only:
src/HOL/ex/Reflection.thy
     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