Module development 

A formal-development parser: the body of a ## Theory block — a sequence of Axiom and Theorem declarations in formal notation — into the axioms and LibraryTheorems the multi-theorem driver consumes.

This is the surface for an axiomatic development like Tarski geometry: a shared axiom base plus dependency-ordered theorems, each citing earlier ones, all discharged and kernel-certified by prove_library_with_axioms.

Axiom flip: for all a b, Cong(a, b, b, a).
Axiom inner_trans: for all a b c d e f,
    if Cong(a,b,c,d) and Cong(a,b,e,f) then Cong(c,d,e,f).
Theorem reflexivity: prove for all a b, Cong(a, b, a, b).
Theorem symmetry cites reflexivity:
    prove for all a b c d, if Cong(a,b,c,d) then Cong(c,d,a,b).
Theorem null_segment: given Cong(P, Q, R, R); prove P = Q.

Grammar (statements terminated by .):

• Axiom <name> : <formula>
• Theorem <name> [cites <n1>, <n2>, …] : [given <formula> ;]* prove <formula>

Clauses within a theorem are separated by ;; cited lemma names by ,. Formulas are handed to parse_formula.

Structs

Development

A parsed formal development: a shared axiom base and the theorems built on it.

Functions

parse_development

Parse a ## Theory body into a Development.

prove_development

Parse a ## Theory body and discharge every theorem against the development’s axioms (and cited lemmas), in citation order — each kernel-certified. Results are in source order, paired with the theorem name.