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, though.


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
context" only

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" function.

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.