]> matita.cs.unibo.it Git - helm.git/commitdiff
- "linear" flag added to lapply (automatic clearing)
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 28 Jun 2006 17:24:38 +0000 (17:24 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 28 Jun 2006 17:24:38 +0000 (17:24 +0000)
- RELATIONAL-ARITHMETICS updated to use this flag

15 files changed:
helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/eliminationTactics.ml
helm/software/components/tactics/fwdSimplTactic.ml
helm/software/components/tactics/fwdSimplTactic.mli
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli
helm/software/components/tactics/tactics.mli
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_fwd.ma
helm/software/matita/contribs/RELATIONAL-ARITHMETICS/add_props.ma
helm/software/matita/help/C/sec_tactics.xml
helm/software/matita/help/C/tactic_quickref.xml

index c73657ae1b4f8c458e5d290e5a202b15db41f7c0..32625f39f108635b78f3790f5921abdb35738a61 100644 (file)
@@ -72,7 +72,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Injection of loc * 'term
   | Intros of loc * int option * 'ident list
   | Inversion of loc * 'term
-  | LApply of loc * int option * 'term list * 'term * 'ident option
+  | LApply of loc * bool * int option * 'term list * 'term * 'ident option
   | Left of loc
   | LetIn of loc * 'term * 'ident
   | Reduce of loc * 'reduction * ('term, 'lazy_term, 'ident) pattern 
index 910ad5204f5d427de157dab1996a274b4f2cff08..18f14c5ce99aefe1f96c1dcf3fc1e3339b9198d1 100644 (file)
@@ -130,9 +130,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       sprintf "intros%s%s"
         (match num with None -> "" | Some num -> " " ^ string_of_int num)
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
-  | LApply (_, level_opt, terms, term, ident_opt) -> 
-      sprintf "lapply %s%s%s%s" 
-        (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
+  | LApply (_, linear, level_opt, terms, term, ident_opt) -> 
+      sprintf "lapply %s%s%s%s%s" 
+        (if linear then " linear " else "")
+       (match level_opt with None -> "" | Some i -> " depth = " ^ string_of_int i ^ " ")  
         (term_pp term) 
         (match terms with [] -> "" | _ -> " to " ^ terms_pp ~term_pp terms)
         (match ident_opt with None -> "" | Some ident -> " as " ^ ident)
index 52dde8979f72381e0c7d0297dd8628bc69f29632..d7343c98c1447c5831ace4066798c6828e37fd09 100644 (file)
@@ -130,10 +130,10 @@ let tactic_of_ast ast =
         ~mk_fresh_name_callback:(namer_of names) ()
   | GrafiteAst.Inversion (_, term) ->
       Tactics.inversion term
-  | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+  | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
       let names = match ident with None -> [] | Some id -> [id] in
-      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
-        ~to_what what
+      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
+        ~linear ?how_many ~to_what what
   | GrafiteAst.Left _ -> Tactics.left
   | GrafiteAst.LetIn (loc,term,name) ->
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
index 16421efafb386df29236fe77b36e9a9ba05b0cfe..5babe3604b2478424cfc48c0ed27e5432a3ee0fb 100644 (file)
@@ -212,14 +212,14 @@ let disambiguate_tactic
     | GrafiteAst.Inversion (loc, term) ->
        let metasenv,term = disambiguate_term context metasenv term in
         metasenv,GrafiteAst.Inversion (loc, term)
-    | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+    | GrafiteAst.LApply (loc, linear, depth, to_what, what, ident) ->
        let f term to_what =
           let metasenv,term = disambiguate_term context metasenv term in
           term :: to_what
        in
        let to_what = List.fold_right f to_what [] in 
        let metasenv,what = disambiguate_term context metasenv what in
-       metasenv,GrafiteAst.LApply (loc, depth, to_what, what, ident)
+       metasenv,GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
     | GrafiteAst.Left loc ->
        metasenv,GrafiteAst.Left loc
     | GrafiteAst.LetIn (loc, term, name) ->
index e9f530f17f49df995ae551ad5f675aef0ec25556..ccff1fab1d3560cd46e2f2a4d3927259418ae747 100644 (file)
@@ -195,12 +195,14 @@ EXTEND
     | IDENT "inversion"; t = tactic_term ->
         GrafiteAst.Inversion (loc, t)
     | IDENT "lapply"; 
+      linear = OPT [ IDENT "linear" ];
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
       what = tactic_term; 
       to_what = OPT [ "to" ; t = tactic_term_list1 -> t ];
       ident = OPT [ "as" ; ident = IDENT -> ident ] ->
-        let to_what = match to_what with None -> [] | Some to_what -> to_what in
-        GrafiteAst.LApply (loc, depth, to_what, what, ident)
+        let linear = match linear with None -> false | Some _ -> true in 
+       let to_what = match to_what with None -> [] | Some to_what -> to_what in
+        GrafiteAst.LApply (loc, linear, depth, to_what, what, ident)
     | IDENT "left" -> GrafiteAst.Left loc
     | IDENT "letin"; where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         GrafiteAst.LetIn (loc, t, where)
index 22bdd0a4f5b78fac9d0146093bd70516b2ed3add..37a4f713688a21ac4bcbf65082466b190d10c2a9 100644 (file)
@@ -35,12 +35,6 @@ module H = ProofEngineHelpers
 
 (* unexported tactics *******************************************************)
 
-let get_name context index =
-   try match List.nth context (pred index) with
-      | Some (Cic.Name name, _)     -> Some name
-      | _                           -> None
-   with Invalid_argument "List.nth" -> None
-
 let rec scan_tac ~old_context_length ~index ~tactic =
    let scan_tac status =
       let (proof, goal) = status in
@@ -48,7 +42,7 @@ let rec scan_tac ~old_context_length ~index ~tactic =
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let context_length = List.length context in
       let rec aux index =
-         match get_name context index with 
+         match H.get_name context index with 
            | _ when index <= 0 -> (proof, [goal])
            | None              -> aux (pred index)
            | Some what         -> 
index 5d78a4ed6949ef4fc57567a2aff7ab8400587fcc..ffc90c1cc4948f44c99ee3a1852d20fbaa93aca5 100644 (file)
@@ -95,8 +95,16 @@ let strip_prods metasenv context ?how_many to_what term =
       | _, t                                  -> metasenv, metas, conts 
    in
    aux metasenv [] [] to_what (how_many, term)
-   
-let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+
+let get_clearables context terms =
+   let aux = function
+      | Cic.Rel i 
+      | Cic.Appl (Cic.Rel i :: _) -> PEH.get_name context i
+      | _                         -> None
+   in
+   PEH.list_rev_map_filter aux terms 
+
+let lapply_tac_aux ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
                (* ?(substs = []) *) ?how_many ?(to_what = []) what =
    let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in   
    let lapply_tac (proof, goal) =
@@ -104,12 +112,13 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
       let lemma = FNG.clean_dummy_dependent_types lemma in
-      let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in      
+      let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
       let conclusion =  
          match metas with [] -> what | _ -> Cic.Appl (what :: List.rev metas)
       in
-      let tac = T.then_ ~start:(letin_tac conclusion) 
-        ~continuation:(clearbody ~index:1)
+      let tac =
+        T.then_ ~start:(letin_tac conclusion) 
+                 ~continuation:(clearbody ~index:1)     
       in
       let proof = (xuri, metasenv, u, t) in
       let aux (proof, goals) (tac, goal) = 
@@ -119,7 +128,26 @@ let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~sub
       List.fold_left aux (proof, []) ((tac, goal) :: conts)
    in
    PET.mk_tactic lapply_tac
-        
+
+let lapply_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) 
+               (* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
+   let lapply_tac status =
+      let proof, goal = status in
+      let _, metasenv, _, _ = proof in
+      let _, context, _ = CicUtil.lookup_meta goal metasenv in
+      let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
+      let tac =  
+         if linear then 
+            let hyps = get_clearables context (what :: to_what) in
+           T.then_ ~start:lapply
+                   ~continuation:(PESR.clear ~hyps) (* T.try_tactic ~tactic: *)
+        else 
+           lapply    
+        in
+        PET.apply_tactic tac status
+   in
+   PET.mk_tactic lapply_tac
+
 (* fwd **********************************************************************)
 
 let fwd_simpl_tac
index d75b83320ce4d25914906c9f5e0b0913f613f1bb..3dbcf6c9c72f690ee84270266012fedcc5d9997b 100644 (file)
@@ -25,7 +25,8 @@
 
 val lapply_tac:
    ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
-   ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
+   ?linear:bool -> ?how_many:int -> ?to_what:Cic.term list -> Cic.term -> 
+   ProofEngineTypes.tactic
 
 val fwd_simpl_tac:
    ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
index cf7df2d58a197ca9895837e784aa0a94e4b47294..c3e6f04aa8286d56c8aa31bc5129eb99edbfd346 100644 (file)
@@ -686,3 +686,22 @@ let lookup_type metasenv context hyp =
       | [] -> raise (ProofEngineTypes.Fail (lazy "lookup_type: not premise in the current goal"))
    in
    aux 1 context
+
+(* FG: **********************************************************************)
+
+let list_rev_map_filter f l =
+   let rec aux a = function
+      | []       -> a
+      | hd :: tl -> 
+         begin match f hd with
+           | None   -> aux a tl
+           | Some b -> aux (b :: a) tl 
+         end
+   in 
+   aux [] l
+
+let get_name context index =
+   try match List.nth context (pred index) with
+      | Some (Cic.Name name, _)     -> Some name
+      | _                           -> None
+   with Invalid_argument "List.nth" -> None
index a7c0e5b543cb6fe23f51dd9be8b1f81c39779cab..0b5db790dce1aa66cf9c0c5edc877c355f83eefa 100644 (file)
@@ -116,3 +116,9 @@ val saturate_term:
 (* returns the index and the type of a premise in a context *)
 val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term
 
+(* FG: some helper functions ************************************************)
+
+val list_rev_map_filter: ('a -> 'b option) -> 'a list -> 'b list
+
+val get_name: Cic.context -> int -> string option
+
index 5bacca20cd706898e9e432efd8e4e3c831d36d31..73d864e1dd7cbbc02e6b2c74ea672b76ea9e9004 100644 (file)
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Tue Jun 27 17:58:26 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Jun 28 17:27:38 CEST 2006 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
@@ -55,6 +55,7 @@ val intros :
 val inversion : term:Cic.term -> ProofEngineTypes.tactic
 val lapply :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
+  ?linear:bool ->
   ?how_many:int ->
   ?to_what:Cic.term list -> Cic.term -> ProofEngineTypes.tactic
 val left : ProofEngineTypes.tactic
index 168cfbc2b7632936cd6b13fff9db052b45c5a1d5..c630d3dfedd4daeeb0e9b2b53805778d4e210ae8 100644 (file)
@@ -1,4 +1,4 @@
-clear(**************************************************************************)
+(**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
 (*      ||A||       A project by Andrea Asperti                           *)
@@ -49,7 +49,7 @@ theorem add_gen_S_2: \forall p,q,r. add p (S q) r \to
  intros. inversion H; clear H; intros;
  [ lapply eq_gen_S_O to H as H0. apply H0
  | clear H1 H3 r.
-   lapply eq_gen_S_S to H2 as H0. clear H2.
+   lapply linear eq_gen_S_S to H2 as H0.
    rewrite > H0. clear H0 q.
    apply ex_intro; [| auto ] (**)
  ].
@@ -70,7 +70,7 @@ theorem add_gen_S_3: \forall p,q,r. add p q (S r) \to
  intros. inversion H; clear H; intros;
  [ rewrite < H1. clear H1 p
  | clear H1.
-   lapply eq_gen_S_S to H3 as H0. clear H3.
+   lapply linear eq_gen_S_S to H3 as H0.
    rewrite > H0. clear H0 r.
  ]; apply ex_intro; [| auto || auto ] (**)
 qed.
@@ -79,13 +79,13 @@ qed.
 
 variant add_gen_O_3_alt: \forall p,q. add p q O \to p = O \land q = O.
  intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0. clear H0 p.
    auto
  | clear H.
-   lapply add_gen_S_2 to H1 as H0. clear H1.
+   lapply linear add_gen_S_2 to H1 as H0.
    decompose.
-   lapply eq_gen_O_S to H1 as H0. apply H0
+   lapply linear eq_gen_O_S to H1 as H0. apply H0
  ].
 qed.
 
@@ -93,12 +93,12 @@ variant add_gen_S_3_alt: \forall p,q,r. add p q (S r) \to
                          \exists s. p = S s \land add s q r \lor
                                     q = S s \land add p s r.
  intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0. clear H0 p
  | clear H.
-   lapply add_gen_S_2 to H1 as H0. clear H1.
+   lapply linear add_gen_S_2 to H1 as H0.
    decompose.
-   lapply eq_gen_S_S to H1 as H0. clear H1.
+   lapply linear eq_gen_S_S to H1 as H0.
    rewrite > H0. clear H0 r.
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
@@ -107,22 +107,22 @@ qed.
 
 theorem add_gen_eq_2_3: \forall p,q. add p q q \to p = O.
  intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
    decompose.
-   lapply eq_gen_S_S to H2 as H0. clear H2.
+   lapply linear eq_gen_S_S to H2 as H0.
    rewrite < H0 in H3. clear H0 a
  ]; auto.
 qed.
 
 theorem add_gen_eq_1_3: \forall p,q. add p q p \to q = O.
  intros 1. elim p; clear p; intros;
- [ lapply add_gen_O_1 to H as H0. clear H.
+ [ lapply linear add_gen_O_1 to H as H0.
    rewrite > H0. clear H0 q
- | lapply add_gen_S_1 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_1 to H1 as H0.
    decompose.
-   lapply eq_gen_S_S to H2 as H0. clear H2.
+   lapply linear eq_gen_S_S to H2 as H0.
    rewrite < H0 in H3. clear H0 a
  ]; auto.
 qed.
index ab59c3a516a7846272400b16194e4128511775d4..dd360676b6cb464b9f98c8758ffcdc72a93129e3 100644 (file)
@@ -22,9 +22,9 @@ qed.
 
 theorem add_S_1: \forall p,q,r. add p q r \to add (S p) q (S r).
  intros 2. elim q; clear q;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
    decompose.
    rewrite > H2. clear H2 r
  ]; auto.
@@ -32,9 +32,9 @@ qed.
 
 theorem add_sym: \forall p,q,r. add p q r \to add q p r.
  intros 2. elim q; clear q;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
    decompose.
    rewrite > H2. clear H2 r
  ]; auto.
@@ -42,7 +42,7 @@ qed.
 
 theorem add_shift_S_sx: \forall p,q,r. add p (S q) r \to add (S p) q r.
  intros.
- lapply add_gen_S_2 to H as H0. clear H.
+ lapply linear add_gen_S_2 to H as H0.
  decompose.
  rewrite > H1. clear H1 r.
  auto.
@@ -50,7 +50,7 @@ qed.
 
 theorem add_shift_S_dx: \forall p,q,r. add (S p) q r \to add p (S q) r.
  intros.
- lapply add_gen_S_1 to H as H0. clear H.
+ lapply linear add_gen_S_1 to H as H0.
  decompose.
  rewrite > H1. clear H1 r.
  auto.
@@ -60,15 +60,15 @@ theorem add_trans_1: \forall p,q1,r1. add p q1 r1 \to
                      \forall q2,r2. add r1 q2 r2 \to
                      \exists q. add q1 q2 q \land add p q r2.
  intros 2; elim q1; clear q1; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
    decompose.
    rewrite > H3. rewrite > H3 in H2. clear H3 r1.
-   lapply add_gen_S_1 to H2 as H0. clear H2.
+   lapply linear add_gen_S_1 to H2 as H0.
    decompose.
    rewrite > H2. clear H2 r2.
-   lapply H to H4, H3 as H0. clear H H4 H3.
+   lapply linear H to H4, H3 as H0.
    decompose.
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
@@ -77,15 +77,15 @@ theorem add_trans_2: \forall p1,q,r1. add p1 q r1 \to
                      \forall p2,r2. add p2 r1 r2 \to
                      \exists p. add p1 p2 p \land add p q r2.
  intros 2; elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0. clear H0 p1
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
    decompose.
    rewrite > H3. rewrite > H3 in H2. clear H3 r1.
-   lapply add_gen_S_2 to H2 as H0. clear H2.
+   lapply linear add_gen_S_2 to H2 as H0.
    decompose.
    rewrite > H2. clear H2 r2.
-   lapply H to H4, H3 as H0. clear H H4 H3. 
+   lapply linear H to H4, H3 as H0.
    decompose.
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
@@ -93,12 +93,12 @@ qed.
 theorem add_conf: \forall p,q,r1. add p q r1 \to 
                   \forall r2. add p q r2 \to r1 = r2.
  intros 2. elim q; clear q; intros;
- [ lapply add_gen_O_2 to H as H0. clear H.
+ [ lapply linear add_gen_O_2 to H as H0.
    rewrite > H0 in H1. clear H0 p
- | lapply add_gen_S_2 to H1 as H0. clear H1.
+ | lapply linear add_gen_S_2 to H1 as H0.
    decompose.
    rewrite > H3. clear H3 r1.
-   lapply add_gen_S_2 to H2 as H0. clear H2.
+   lapply linear add_gen_S_2 to H2 as H0.
    decompose.
    rewrite > H2. clear H2 r2.
  ]; auto.
index 56c2a66167b4e47c17f14cecb6ec5a7cde65a809..130c08e56749cf2f08e9eb607fc3999e19781f83 100644 (file)
@@ -1061,7 +1061,7 @@ its constructor takes no arguments.</para>
     <title>lapply</title>
     <titleabbrev>lapply</titleabbrev>
     <para><userinput>
-     lapply depth=d t 
+     lapply linear depth=d t 
      to t<subscript>1</subscript>, ..., t<subscript>n</subscript> as H
     </userinput></para>
     <para>
@@ -1071,6 +1071,7 @@ its constructor takes no arguments.</para>
           <listitem>
             <para>
             <emphasis role="bold">lapply</emphasis> 
+            [<emphasis role="bold">linear</emphasis>]
             [<emphasis role="bold">depth=</emphasis>&nat;] 
             &sterm; 
             [<emphasis role="bold">to</emphasis>
@@ -1108,6 +1109,10 @@ its constructor takes no arguments.</para>
             Usually the other <command>?</command>'s preceding the 
             <command>n</command>-th independent premise of
             <command>t</command> are istantiated as a consequence.
+            If the <command>linear</command> flag is specified and if 
+            <command>t, t<subscript>1</subscript>, ..., t<subscript>n</subscript></command>
+            are (applications of) premises in the current context, they are
+             <command>clear</command>ed. 
            </para>
           </listitem>
         </varlistentry>
index 45e097e1bd1691f7436da434bfd804aef3a7afa0..dd14d8a2685b15d99c9493b9bebeaf21a7de122a 100644 (file)
   <listitem>
     <para>
             <link linkend="tac_lapply"><emphasis role="bold">lapply</emphasis></link> 
+            [<emphasis role="bold">linear</emphasis>]
             [<emphasis role="bold">depth=</emphasis><emphasis><link linkend="grammar.nat">nat</link></emphasis>] 
             <emphasis><link linkend="grammar.sterm">sterm</link></emphasis> 
             [<emphasis role="bold">to</emphasis>