-
Notifications
You must be signed in to change notification settings - Fork 0
/
HOLF.thy
63 lines (52 loc) · 1.7 KB
/
HOLF.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(* Title: HOLF.thy
Author: Manuel Eberl & Lars Hupel,
FU Dietersheim Fakultaet fuer Informatik
Copyright 2013 FU Dietersheim
An Isabelle/HOL adaptation of the Falso axiom system.
(see http://www.eleves.ens.fr/home/amarilli/falso/)
For documentation, see http://www.fu-dietersheim.de/logik/isabelle/holf/
*)
theory HOLF
imports HOL Num
begin
subsection {* HOLF Axioms *}
(* The Falso axiom.
TODO: investigate whether this renders any of the other HOL
axioms superfluous and fork a HOLF object logic.
*)
axiomatization where
FalseI: False
subsection {* ExFalso prover code and setup *}
ML {*
signature EXFALSO =
sig
val exfalso_tac: bool -> Proof.context -> int -> tactic
val setup: theory -> theory
end;
functor ExFalso(): EXFALSO =
struct
fun exfalso_tac timing _ n =
let val start = Timing.start ();
val tac = rtac ([@{thm FalseI}] MRS @{thm FalseE}) n
val _ = if timing then
Output.urgent_message (Timing.message (Timing.result start))
else
();
in tac
end
val setup =
Method.setup @{binding exfalso}
(Scan.option (Scan.lift (Args.parens (Args.$$$ "timing"))) >>
(fn x => SIMPLE_METHOD' o (exfalso_tac (x <> NONE))))
"Experimental ExFalso prover";
end;
structure ExFalso = ExFalso ()
*}
setup ExFalso.setup
(* Twin prime theorem, used as regression test *)
lemma "\<not>finite {(m::nat,n::nat)|m n. n = m + 2 \<and>
\<not>(\<exists>x<m. x > 1 \<and> x dvd m) \<and>
\<not>(\<exists>x<n. x > 1 \<and> x dvd n)}"
apply (exfalso (timing))
done
end