An embedded Isabelle proof script in a Specware spec consists of an introductory line beginning with proof Isa, the actual Isabelle script on subsequent lines terminated by the string end-proof. For example, the simple proof script apply(auto) can be embedded as follows:
proof Isa
apply(auto)
end-proof |
The proof script should occur immediately after the theorem or definition that it applies to. If the script applies to a proof obligation that is not explicit in the spec, then the name of the obligation should appear after proof Isa, on the same line. There are rare cases where an obligation is inserted between a definition and an immediately following proof script, which causes the proof script to be ignored. If this happen, then the name of the op should be explicitly given.
If the user does not supply a proof script for a theorem then the translator will supply the script by auto which may be all that is required to prove simple theorems.
Annotations for theorems may be included on the proof Isa line. For example,
theorem Simplify_valif_normif is
fa(b,env,t,e) valif (normif b t e) env = valif (IF(b, t, e)) env
proof Isa [simp]
apply(induct_tac b)
apply(auto)
end-proof |
theorem Simplify_valif_normif [simp]:
"valif (normif b t e) env = valif (IF b t e) env"
apply(induct_tac b)
apply(auto)
done |
In this example we see that universal quantification in Specware becomes, by default, implicit quantification in Isabelle. This is normally what the user wants, but not always. The user may specify the variables that should be explicitly quantified by adding a clause like fa t e. to the proof Isa line. For example,
theorem Simplify_valif_normif is
fa(b,env,t,e) valif (normif b t e) env = valif (IF(b, t, e)) env
proof Isa [simp] fa t e.
apply(induct_tac b)
apply(auto)
end-proof |
theorem Simplify_valif_normif [simp]:
"\<forall>t e. valif (normif b t e) env = valif (IF b t e) env"
apply(induct_tac b)
apply(auto)
done |
The \<forall> will be displayed as a universal quantification symbol using X-Symbol mode in Isabelle. Note that instead of fa in the proof Isa line the user may use the X-Symbol for universal quantification.
Recursive functions that are translated to recdefs can have a measure function specified on the proof Isa line, by including it between double-quotes. For example:
proof Isa "measure (\<lambda>(wrd,sym). length wrd)" end-proof |