author | paulson |
Thu, 05 Oct 2006 10:41:27 +0200 | |
changeset 20862 | 1059f2316f88 |
parent 20809 | 6c4fd0b4b63a |
child 20869 | 5abf3cd34a35 |
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") |
|
19 |
("Tools/reconstruction.ML") |
|
15151 | 20 |
|
21 |
begin |
|
22 |
||
20761 | 23 |
constdefs |
24 |
COMBI :: "'a => 'a" |
|
25 |
"COMBI P == P" |
|
26 |
||
27 |
COMBK :: "'a => 'b => 'a" |
|
28 |
"COMBK P Q == P" |
|
29 |
||
30 |
COMBB :: "('b => 'c) => ('a => 'b) => 'a => 'c" |
|
31 |
"COMBB P Q R == P (Q R)" |
|
32 |
||
33 |
COMBC :: "('a => 'b => 'c) => 'b => 'a => 'c" |
|
34 |
"COMBC P Q R == P R Q" |
|
35 |
||
36 |
COMBS :: "('a => 'b => 'c) => ('a => 'b) => 'a => 'c" |
|
37 |
"COMBS P Q R == P R (Q R)" |
|
38 |
||
39 |
COMBB' :: "('a => 'c) => ('b => 'a) => ('d => 'b) => 'd => 'c" |
|
40 |
"COMBB' M P Q R == M (P (Q R))" |
|
41 |
||
42 |
COMBC' :: "('a => 'b => 'c) => ('d => 'a) => 'b => 'd => 'c" |
|
43 |
"COMBC' M P Q R == M (P R) Q" |
|
44 |
||
45 |
COMBS' :: "('a => 'b => 'c) => ('d => 'a) => ('d => 'b) => 'd => 'c" |
|
46 |
"COMBS' M P Q R == M (P R) (Q R)" |
|
47 |
||
48 |
fequal :: "'a => 'a => bool" |
|
49 |
"fequal X Y == (X=Y)" |
|
50 |
||
51 |
lemma fequal_imp_equal: "fequal X Y ==> X=Y" |
|
52 |
by (simp add: fequal_def) |
|
53 |
||
54 |
lemma equal_imp_fequal: "X=Y ==> fequal X Y" |
|
55 |
by (simp add: fequal_def) |
|
56 |
||
20862 | 57 |
lemma COMBK1: "COMBK P == (%Q. P)" |
58 |
apply (rule eq_reflection) |
|
59 |
apply (rule ext) |
|
60 |
apply (simp add: COMBK_def) |
|
61 |
done |
|
62 |
||
63 |
lemma COMBI1: "COMBI == (%P. P)" |
|
64 |
apply (rule eq_reflection) |
|
65 |
apply (rule ext) |
|
66 |
apply (simp add: COMBI_def) |
|
67 |
done |
|
68 |
||
69 |
lemma COMBB1: "COMBB P Q == %R. P (Q R)" |
|
70 |
apply (rule eq_reflection) |
|
71 |
apply (rule ext) |
|
72 |
apply (simp add: COMBB_def) |
|
73 |
done |
|
74 |
||
75 |
||
20788 | 76 |
use "Tools/res_axioms.ML" |
20761 | 77 |
use "Tools/res_hol_clause.ML" |
78 |
use "Tools/res_atp.ML" |
|
79 |
use "Tools/reconstruction.ML" |
|
80 |
||
16563 | 81 |
setup ResAxioms.meson_method_setup |
15151 | 82 |
setup Reconstruction.setup |
83 |
||
15653 | 84 |
end |