How to understand syntax and translation in Isabelle

user_14429373 0
Viewed 191

I am trying to understand the code of Rely Guarantee in Isabelle/HOL and feel confused about the syntax and translation keyword in https://isabelle.in.tum.de/library/HOL/HOL-Hoare_Parallel/RG_Syntax.html

syntax
  "_Assign"    :: "idt ⇒ 'b ⇒ 'a com"                     ("(´_ :=/ _)" [70, 65] 61)
  "_Cond"      :: "'a bexp ⇒ 'a com ⇒ 'a com ⇒ 'a com"   ("(0IF _/ THEN _/ ELSE _/FI)" [0, 0, 0] 61)
  "_Cond2"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0IF _ THEN _ FI)" [0,0] 56)
  "_While"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0WHILE _ /DO _ /OD)"  [0, 0] 61)
  "_Await"     :: "'a bexp ⇒ 'a com ⇒ 'a com"             ("(0AWAIT _ /THEN /_ /END)"  [0,0] 61)
  "_Atom"      :: "'a com ⇒ 'a com"                        ("(⟨_⟩)" 61)
  "_Wait"      :: "'a bexp ⇒ 'a com"                       ("(0WAIT _ END)" 61)
  "_PAR"       :: "prgs ⇒ 'a"                              ("COBEGIN//_//COEND" 60)

I am confused about three questions

(1) Why there always be an underscore _Assign before the name?

(2) What's the meaning of slash and single quote in(´_ :=/ _) and double slash in COBEGIN//_//COEND

(3) Why there is a zero before the mixfix symbol 0IF _ THEN _ FI

translations
  "´x := a" ⇀ "CONST Basic «´(_update_name x (λ_. a))»"
  "IF b THEN c1 ELSE c2 FI" ⇀ "CONST Cond ⦃b⦄ c1 c2"
  "IF b THEN c FI" ⇌ "IF b THEN c ELSE SKIP FI"
  "WHILE b DO c OD" ⇀ "CONST While ⦃b⦄ c"
  "AWAIT b THEN c END" ⇌ "CONST Await ⦃b⦄ c"
  "⟨c⟩" ⇌ "AWAIT CONST True THEN c END"
  "WAIT b END" ⇌ "AWAIT b THEN SKIP END"

print_translation ‹
  let
    fun quote_tr' f (t :: ts) =
          Term.list_comb (f $ Syntax_Trans.quote_tr' \<^syntax_const>‹_antiquote› t, ts)
      | quote_tr' _ _ = raise Match;

    val assert_tr' = quote_tr' (Syntax.const \<^syntax_const>‹_Assert›);

    fun bexp_tr' name ((Const (\<^const_syntax>‹Collect›, _) $ t) :: ts) =
          quote_tr' (Syntax.const name) (t :: ts)
      | bexp_tr' _ _ = raise Match;

    fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
          quote_tr' (Syntax.const \<^syntax_const>‹_Assign› $ Syntax_Trans.update_name_tr' f)
            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
      | assign_tr' _ = raise Match;
  in
   [(\<^const_syntax>‹Collect›, K assert_tr'),
    (\<^const_syntax>‹Basic›, K assign_tr'),
    (\<^const_syntax>‹Cond›, K (bexp_tr' \<^syntax_const>‹_Cond›)),
    (\<^const_syntax>‹While›, K (bexp_tr' \<^syntax_const>‹_While›))]
  end
›

And I can't understand the meaning of code above. Where can I find reference about the use of translations and print_translation

isabelle verification formal-methods formal-verification syntax
1 Answers

The information that you seek can be found in chapter 8 of the standard reference manual of Isabelle (Isar-ref or The Isabelle/Isar Reference Manual by Makarius Wenzel). More specifically, see subsections 8.2, 8.4 and 8.5 in the reference manual.

Personally, I am not familiar with the implementation details of the syntax transformations in Isabelle, so my answer will rely on what is already stated in the documentation. Thus, my advice is to use the reference manual as the primary source of information. If, having studied the reference manual, you still have further questions, you may wish to try the mailing list of Isabelle or Zulip chat.

  1. The command syntax is explained in subsection 8.5.2 of the reference manual. In your question, _Assign is a syntax constant of the syntax declaration, which is merely a name among the syntactic entities of the Isar language (see subsection 3.2 in the reference manual). Technically, the underscore should have no special meaning, but the use of an underscore at the beginning of the names of the syntax constants is a convention and it seems that only the names of the syntax constants can start with an underscore.
  2. Subsection 8.2 in the reference manual already contains a reasonably detailed answer to your second question. A single quote ´ in the mixfix template (´_ :=/ _) does not have any special meaning. However, / allows (but does not force) a line break and // forces a line break during pretty printing.
  3. In general, (n with n being a natural number, opens a pretty printing block in mixfix annotations. The number n specifies the block indentation (that is, the number of spaces that are added when a line break occurs in the block). However, if n is not specified, it should default to 0. So, I am not entirely certain why 0 was, indeed, needed in this instance. You may wish to investigate further.

The commands translations and print_translation are explained in subsections 8.5.2 and 8.5.3, respectively. Thus, translations can be used for the specification of the rewrite rules on ASTs, whereas print_translations allow arbitrary manipulations of inner syntax for printing (keep in mind the rough “term->AST->pretty printed text” sequence). In this instance, you can examine the effects of the invocation of the print_translation directly as follows

lemma "´a := b = c"
  (*Basic (a_update (λ_. b)) = c*)
  oops

print_translation ‹…›

lemma "´a := b = c"
  (*´a := b = c*)
  oops

Hope this helps, or, at least, points you in the direction of the relevant resources.

user_97168690
Related