src/Pure/Isar/method.ML
changeset 5884 113badd4dae5
parent 5824 91113aa09371
child 5916 4039395e29ce
     1.1 --- a/src/Pure/Isar/method.ML	Mon Nov 16 11:06:31 1998 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Nov 16 11:07:12 1998 +0100
     1.3 @@ -27,6 +27,19 @@
     1.4    val method: theory -> Args.src -> Proof.context -> Proof.method
     1.5    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
     1.6      -> theory -> theory
     1.7 +  val syntax: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
     1.8 +    Proof.context -> Args.src -> Proof.context * 'a
     1.9 +  val no_args: Proof.method -> Args.src -> Proof.context -> Proof.method
    1.10 +  val sectioned_args: ((Args.T list -> Proof.context attribute * Args.T list) list ->
    1.11 +      Proof.context * Args.T list -> 'a * (Proof.context * Args.T list)) ->
    1.12 +    (Args.T list -> Proof.context attribute * Args.T list) list ->
    1.13 +    ('a -> Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.14 +  val default_sectioned_args: Proof.context attribute ->
    1.15 +    (Args.T list -> Proof.context attribute * Args.T list) list ->
    1.16 +    (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.17 +  val only_sectioned_args: (Args.T list -> Proof.context attribute * Args.T list) list ->
    1.18 +    (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.19 +  val thms_args: (tthm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    1.20    datatype text =
    1.21      Basic of (Proof.context -> Proof.method) |
    1.22      Source of Args.src |
    1.23 @@ -38,7 +51,7 @@
    1.24    val dynamic_method: string -> (Proof.context -> Proof.method)
    1.25    val refine: text -> Proof.state -> Proof.state Seq.seq
    1.26    val tac: text -> Proof.state -> Proof.state Seq.seq
    1.27 -  val etac: text -> Proof.state -> Proof.state Seq.seq
    1.28 +  val then_tac: text -> Proof.state -> Proof.state Seq.seq
    1.29    val proof: text option -> Proof.state -> Proof.state Seq.seq
    1.30    val end_block: Proof.state -> Proof.state Seq.seq
    1.31    val terminal_proof: text -> Proof.state -> Proof.state Seq.seq
    1.32 @@ -46,11 +59,6 @@
    1.33    val default_proof: Proof.state -> Proof.state Seq.seq
    1.34    val qed: bstring option -> theory attribute list option -> Proof.state
    1.35      -> theory * (string * string * tthm)
    1.36 -  val syntax: (Args.T list -> 'a * Args.T list) -> ('a -> 'b) -> Args.src -> 'b
    1.37 -  val no_args: 'a -> Args.src -> Proof.context -> 'a
    1.38 -  val thm_args: (tthm list -> 'a) -> Args.src -> Proof.context -> 'a
    1.39 -  val sectioned_args: (Proof.context -> 'a) -> ('a * tthm list -> 'b) ->
    1.40 -    (string * ('b * tthm list -> 'b)) list -> ('b -> 'c) -> Args.src -> Proof.context -> 'c
    1.41    val setup: (theory -> theory) list
    1.42  end;
    1.43  
    1.44 @@ -78,7 +86,7 @@
    1.45  fun trivial_tac [] = K all_tac
    1.46    | trivial_tac facts =
    1.47        let
    1.48 -        val thms = map Attribute.thm_of facts;
    1.49 +        val thms = Attribute.thms_of facts;
    1.50          val r = ~ (length facts);
    1.51        in metacuts_tac thms THEN' rotate_tac r end;
    1.52  
    1.53 @@ -100,10 +108,10 @@
    1.54  
    1.55  fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
    1.56  
    1.57 -fun rule_tac rules [] = resolve_tac (map Attribute.thm_of rules)
    1.58 +fun rule_tac rules [] = resolve_tac (Attribute.thms_of rules)
    1.59    | rule_tac erules facts =
    1.60        let
    1.61 -        val rules = forward_chain (map Attribute.thm_of facts) (map Attribute.thm_of erules);
    1.62 +        val rules = forward_chain (Attribute.thms_of facts) (Attribute.thms_of erules);
    1.63          fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules);
    1.64        in tac end;
    1.65  
    1.66 @@ -149,11 +157,14 @@
    1.67    let
    1.68      val {space, meths} = MethodsData.get thy;
    1.69  
    1.70 -    fun meth ((raw_name, args), pos) =
    1.71 -      let val name = NameSpace.intern space raw_name in
    1.72 +    fun meth src =
    1.73 +      let
    1.74 +        val ((raw_name, _), pos) = Args.dest_src src;
    1.75 +        val name = NameSpace.intern space raw_name;
    1.76 +      in
    1.77          (case Symtab.lookup (meths, name) of
    1.78            None => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
    1.79 -        | Some ((mth, _), _) => mth ((name, args), pos))
    1.80 +        | Some ((mth, _), _) => mth src)
    1.81        end;
    1.82    in meth end;
    1.83  
    1.84 @@ -178,30 +189,43 @@
    1.85  fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);
    1.86  
    1.87  
    1.88 -(* argument syntax *)
    1.89 +
    1.90 +(** method syntax **)
    1.91  
    1.92 -val methodN = "method";
    1.93 -fun syntax scan = Args.syntax methodN scan;
    1.94 +(* basic *)
    1.95 +
    1.96 +fun syntax (scan: (Proof.context * Args.T list -> 'a * (Proof.context * Args.T list))) =
    1.97 +  Args.syntax "method" scan;
    1.98  
    1.99 -fun no_args x = syntax (Scan.succeed (fn (_: Proof.context) => x)) I;
   1.100 +fun no_args (x: Proof.method) src ctxt = #2 (syntax (Scan.succeed x) ctxt src);
   1.101 +
   1.102 +
   1.103 +(* sections *)
   1.104  
   1.105 -(* FIXME move? *)
   1.106 -fun thm_args f = syntax (Scan.repeat Args.name)
   1.107 -  (fn names => fn ctxt => f (ProofContext.get_tthmss ctxt names));
   1.108 +fun sect ss = Scan.first (map (fn s => Scan.lift (s --| Args.$$$ ":")) ss);
   1.109 +fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
   1.110 +fun thmss ss = Scan.repeat (thms ss) >> flat;
   1.111 +
   1.112 +fun apply att (ctxt, ths) = Attribute.applys ((ctxt, ths), [att]);
   1.113  
   1.114 -fun sectioned_args get_data def_sect sects f =
   1.115 -  syntax (Args.sectioned (map fst sects))
   1.116 -    (fn (names, sect_names) => fn ctxt =>
   1.117 -      let
   1.118 -        val get_thms = ProofContext.get_tthmss ctxt;
   1.119 -        val thms = get_thms names;
   1.120 -        val sect_thms = map (apsnd get_thms) sect_names;
   1.121 +fun section ss = (sect ss -- thmss ss) :-- (fn (att, ths) => Scan.depend (fn ctxt =>
   1.122 +  Scan.succeed (apply att (ctxt, ths)))) >> #2;
   1.123 +
   1.124 +fun sectioned args ss = args ss -- Scan.repeat (section ss);
   1.125 +
   1.126  
   1.127 -        fun apply_sect (data, (s, ths)) =
   1.128 -          (case assoc (sects, s) of
   1.129 -            Some add => add (data, ths)
   1.130 -          | None => error ("Unknown argument section " ^ quote s));
   1.131 -       in f (foldl apply_sect (def_sect (get_data ctxt, thms), sect_thms)) end);
   1.132 +fun sectioned_args args ss f src ctxt =
   1.133 +  let val (ctxt', (x, thss)) = syntax (sectioned args ss) ctxt src
   1.134 +  in
   1.135 +    warning "TRACE thms:"; seq Attribute.print_tthm (flat thss);             (* FIXME *)
   1.136 +    f x ctxt'
   1.137 +  end;
   1.138 +
   1.139 +fun default_sectioned_args att ss f src ctxt =
   1.140 +  sectioned_args thmss ss (fn ths => fn ctxt' => f (#1 (apply att (ctxt', ths)))) src ctxt;
   1.141 +
   1.142 +fun only_sectioned_args ss f = sectioned_args (K (Scan.succeed ())) ss (fn () => f);
   1.143 +fun thms_args f = sectioned_args thmss [] (fn ths => fn _ => f ths);
   1.144  
   1.145  
   1.146  
   1.147 @@ -222,7 +246,7 @@
   1.148  (* dynamic methods *)
   1.149  
   1.150  fun dynamic_method name = (fn ctxt =>
   1.151 -  method (ProofContext.theory_of ctxt) ((name, []), Position.none) ctxt);
   1.152 +  method (ProofContext.theory_of ctxt) (Args.src ((name, []), Position.none)) ctxt);
   1.153  
   1.154  
   1.155  (* refine *)
   1.156 @@ -248,7 +272,7 @@
   1.157    |> Proof.goal_facts (K [])
   1.158    |> refine text;
   1.159  
   1.160 -fun etac text state =
   1.161 +fun then_tac text state =
   1.162    state
   1.163    |> Proof.goal_facts Proof.the_facts
   1.164    |> refine text;
   1.165 @@ -256,7 +280,7 @@
   1.166  
   1.167  (* proof steps *)
   1.168  
   1.169 -val default_txt = Source (("default", []), Position.none);
   1.170 +val default_txt = Source (Args.src (("default", []), Position.none));
   1.171  val finishN = "finish";
   1.172  
   1.173  fun proof opt_text state =
   1.174 @@ -288,7 +312,7 @@
   1.175    ("trivial", no_args trivial, "proof all goals trivially"),
   1.176    ("assumption", no_args assumption, "proof by assumption"),
   1.177    ("finish", no_args asm_finish, "finish proof by assumption"),
   1.178 -  ("rule", thm_args rule, "apply primitive rule")];
   1.179 +  ("rule", thms_args rule, "apply primitive rule")];
   1.180  
   1.181  
   1.182  (* setup *)