equal
deleted
inserted
replaced
5 |
5 |
6 header {* Classical First-Order Logic with Proofs *} |
6 header {* Classical First-Order Logic with Proofs *} |
7 |
7 |
8 theory FOLP |
8 theory FOLP |
9 imports IFOLP |
9 imports IFOLP |
10 uses |
|
11 ("classical.ML") ("simp.ML") ("simpdata.ML") |
|
12 begin |
10 begin |
13 |
11 |
14 axiomatization cla :: "[p=>p]=>p" |
12 axiomatization cla :: "[p=>p]=>p" |
15 where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P" |
13 where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P" |
16 |
14 |
97 apply (rule major [THEN notE]) |
95 apply (rule major [THEN notE]) |
98 apply (rule r) |
96 apply (rule r) |
99 apply assumption |
97 apply assumption |
100 done |
98 done |
101 |
99 |
102 use "classical.ML" (* Patched 'cos matching won't instantiate proof *) |
100 ML_file "classical.ML" (* Patched because matching won't instantiate proof *) |
103 use "simp.ML" (* Patched 'cos matching won't instantiate proof *) |
101 ML_file "simp.ML" (* Patched because matching won't instantiate proof *) |
104 |
102 |
105 ML {* |
103 ML {* |
106 structure Cla = Classical |
104 structure Cla = Classical |
107 ( |
105 ( |
108 val sizef = size_of_thm |
106 val sizef = size_of_thm |
137 "?p3 : ~ ~ P <-> P" |
135 "?p3 : ~ ~ P <-> P" |
138 "?p4 : (~P --> P) <-> P" |
136 "?p4 : (~P --> P) <-> P" |
139 apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *}) |
137 apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *}) |
140 done |
138 done |
141 |
139 |
142 use "simpdata.ML" |
140 ML_file "simpdata.ML" |
143 |
141 |
144 end |
142 end |