author | paulson |
Thu, 26 Oct 2006 10:48:35 +0200 | |
changeset 21102 | 7f2ebe5c5b72 |
parent 20869 | 5abf3cd34a35 |
child 21137 | 8a1d62375ff8 |
permissions | -rw-r--r-- |
15151 | 1 |
(* Title: HOL/Reconstruction.thy |
17603 | 2 |
ID: $Id$ |
15151 | 3 |
Author: Lawrence C Paulson |
4 |
Copyright 2004 University of Cambridge |
|
5 |
*) |
|
6 |
||
17462
47f7bddc3239
moved setup ResAxioms.clause_setup to Main.thy (it refers to all previous theories);
wenzelm
parents:
17421
diff
changeset
|
7 |
header{* Reconstructing external resolution proofs *} |
15151 | 8 |
|
9 |
theory Reconstruction |
|
20809 | 10 |
imports Hilbert_Choice Map Extraction |
18449 | 11 |
uses "Tools/polyhash.ML" |
17819 | 12 |
"Tools/ATP/AtpCommunication.ML" |
13 |
"Tools/ATP/watcher.ML" |
|
18794 | 14 |
"Tools/ATP/reduce_axiomsN.ML" |
20761 | 15 |
"Tools/res_clause.ML" |
16 |
("Tools/res_hol_clause.ML") |
|
17 |
("Tools/res_axioms.ML") |
|
18 |
("Tools/res_atp.ML") |
|
15151 | 19 |
|
20 |
begin |
|
21 |
||
20761 | 22 |
constdefs |
23 |
COMBI :: "'a => 'a" |
|
24 |
"COMBI P == P" |
|
25 |
||
26 |
COMBK :: "'a => 'b => 'a" |
|
27 |
"COMBK P Q == P" |
|
28 |
||
29 |
COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c" |
|
30 |
"COMBB P Q R == P (Q R)" |
|
31 |
||
32 |
COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c" |
|
33 |
"COMBC P Q R == P R Q" |
|
34 |
||
35 |
COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" |
|
36 |
"COMBS P Q R == P R (Q R)" |
|
37 |
||
38 |
COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c" |
|
39 |
"COMBB' M P Q R == M (P (Q R))" |
|
40 |
||
41 |
COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c" |
|
42 |
"COMBC' M P Q R == M (P R) Q" |
|
43 |
||
44 |
COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c" |
|
45 |
"COMBS' M P Q R == M (P R) (Q R)" |
|
46 |
||
47 |
fequal :: "'a => 'a => bool" |
|
48 |
"fequal X Y == (X=Y)" |
|
49 |
||
50 |
lemma fequal_imp_equal: "fequal X Y ==> X=Y" |
|
51 |
by (simp add: fequal_def) |
|
52 |
||
53 |
lemma equal_imp_fequal: "X=Y ==> fequal X Y" |
|
54 |
by (simp add: fequal_def) |
|
55 |
||
20869 | 56 |
lemma K_simp: "COMBK P == (%Q. P)" |
20862 | 57 |
apply (rule eq_reflection) |
58 |
apply (rule ext) |
|
59 |
apply (simp add: COMBK_def) |
|
60 |
done |
|
61 |
||
20869 | 62 |
lemma I_simp: "COMBI == (%P. P)" |
20862 | 63 |
apply (rule eq_reflection) |
64 |
apply (rule ext) |
|
65 |
apply (simp add: COMBI_def) |
|
66 |
done |
|
67 |
||
20869 | 68 |
lemma B_simp: "COMBB P Q == %R. P (Q R)" |
20862 | 69 |
apply (rule eq_reflection) |
70 |
apply (rule ext) |
|
71 |
apply (simp add: COMBB_def) |
|
72 |
done |
|
73 |
||
20788 | 74 |
use "Tools/res_axioms.ML" |
20761 | 75 |
use "Tools/res_hol_clause.ML" |
76 |
use "Tools/res_atp.ML" |
|
77 |
||
16563 | 78 |
setup ResAxioms.meson_method_setup |
15151 | 79 |
|
15653 | 80 |
end |