]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportprove/prova.v
rebuilt
[helm.git] / helm / EXPORT / exportprove / prova.v
1 Require Export Xml.
2
3 Section prova.
4
5 Inductive
6  tree : Set := node : forest -> tree
7 with
8  forest : Set := leaf : forest | cons : tree -> forest -> forest.
9
10 Fixpoint tree_size [t:tree] : nat :=
11  Cases t of (node f) => (S (forest_size f)) end
12 with forest_size [f:forest] : nat :=
13  Cases f of leaf => (S O) | (cons t f') => (plus (tree_size t) (forest_size f'))
14  end.
15
16 Theorem a_ab_b: (A,B:Prop)A->(A->B)->B.
17 Auto.
18 Qed.
19
20 Axiom dummy_axiom: (n,m:nat)(le n m)\/(gt n m).
21
22 End prova.
23
24 Print XML Section Disk "examples/prove" prova.
25
26 Theorem ab_ac_abc: (A,B,C:Prop)(A->B)->(A->C)->A->B/\C.
27 Intros A B C AB AC A1.
28 Split.
29
30 Show XML File "examples/ab_ac_abc.xml" Proof.
31
32 Auto.
33 Auto.
34 Qed.