Re: [isabelle] How do I do stone age interaction?
On Mon, 6 Dec 2010, Jeremy Dawson wrote:
The ML layer certainly helps you perform proofs effectively - just by
way of example here is something I wrote this afternoon, which I
understand cannot be done in Isar
fun in_tac sg st = (rtac insertI1 ORELSE' (rtac insertI2 THEN' in_tac))
sg st ;
val _ = qed_goalw "inv_rule_aidps" CI_Rls.thy
(rule_defs @ rule_lists) "inv_rule_set (PC ` aidps)"
(fn _ => [ Simp_tac 1, rewtac inv_rule_set_def, Safe_tac,
(TRYALL (EVERY' [rtac exI, rtac conjI, rtac refl])),
(TRYALL (EVERY' [rtac drl.singleI, in_tac])),
As a general rule of thumb, you can do always do more in Isar than in the
stone age -- in the same way, you can do more with a computer that runs
Linux or Mac OS X, compared to the bare metal. This does not mean that
Linus Torvalds or Apple will let you poke around in hardware registers,
See the "tactic" proof method in the isar-ref manual how to embed ML
tactic expressions into Isar source text.
BTW, old Simp_tac and Safe_tac refer to "the_context()" which is not
always the same as your goal context, i.e. CI_Rls.thy above. This is why
I have called it a running gag from many years ago.
The naked ML toplevel lacks the formal Isabelle context, which means
you can hardly do anything useful, e.g. being able to parse/print
expressions always requires a proper context.
If "proper context" means something of the type Proof.context, then this
isn't so - the "read" function implicitly uses an old style "theory
An old style "theory context" is not a proper context. You are also
subject to "the_context()" confusion here, i.e. you can never be quite
sure what you get. Good that we got rid of the "read" function long ago.
I'm not sure if I understand this right, but at the ML level I certainly
get all the HOL syntax and theorems - note, though, if you're using
"new-style" theory files, then to get theorems derived from the theory
file as ML identifiers you need to use the "use_legacy_bindings"
Hardly anybody on the mailing list will remember "old-style" theories.
This is just historical cruft, even in Isabelle2005. Gladly this has been
deleted long ago.
This archive was generated by a fusion of
Pipermail (Mailman edition) and