home *** CD-ROM | disk | FTP | other *** search
/ Celestin Apprentice 4 / Apprentice-Release4.iso / Source Code / C / Applications / SML⁄NJ 93+ / Documentation / examples / textbooks / working / Hal.ML < prev    next >
Encoding:
Text File  |  1995-12-30  |  23.5 KB  |  162 lines  |  [TEXT/R*ch]
  1. c ORELSE all_tac) st;
  2.  
  3.   (*Repeats again and again until "pred" reports proof tree as satisfied*)
  4.   fun DEPTH_FIRST pred tac st =
  5.      (if pred st  then  all_tac 
  6.           else  tac THEN DEPTH_FIRST pred tac) st;
  7.  
  8.   (*For combining int->tactic functions with ORELSE*)
  9.   fun (f1 ORI f2) i = f1 i ORELSE f2 i;
  10.   end;
  11.  
  12.  
  13. (*** An automatic tactic for first-order logic ***)
  14.  
  15. signature FOLTAC =
  16.   sig
  17.   structure Seq: SEQUENCE
  18.   type state
  19.   val safe_step_tac: int -> state -> state Seq.T
  20.   val quant_tac: int -> state -> state Seq.T
  21.   val step_tac: int -> state -> state Seq.T
  22.   val depth_tac: state -> state Seq.T
  23.   end;
  24.  
  25.  
  26. functor FolTacFUN (structure Proof: PROOF and Tactical: TACTICAL
  27.      sharing Proof.Seq = Tactical.Seq) : FOLTAC  =
  28.   struct
  29.   local  open Proof  Tactical  in
  30.   structure Seq = Seq;
  31.   type state = state;
  32.  
  33.   (*Deterministic; applies one rule to the goal; no unification or variable
  34.     instantiation; cannot render the goal unprovable.*)
  35.   val safe_step_tac =
  36.       (*1 subgoal*)
  37.       conj_left_tac ORI disj_right_tac ORI imp_right_tac ORI 
  38.       neg_left_tac ORI neg_right_tac ORI   
  39.       ex_left_tac ORI all_right_tac ORI 
  40.       (*2 subgoals*)
  41.       conj_right_tac ORI disj_left_tac ORI imp_left_tac ORI 
  42.       iff_left_tac ORI iff_right_tac;
  43.  
  44.   (*expand a quantifier on the left and the right (if possible!) *)
  45.   fun quant_tac i = TRY (all_left_tac i) THEN TRY (ex_right_tac i);
  46.  
  47.   val step_tac = unify_tac ORI safe_step_tac ORI quant_tac;
  48.  
  49.   val depth_tac = DEPTH_FIRST final (step_tac 1);
  50.   end
  51.   end;
  52.  
  53.  
  54. (******** SHORT DEMONSTRATIONS ********)
  55.  
  56. structure Basic = BasicFUN();
  57. structure FolKey = 
  58.     struct val alphas = ["ALL","EX"]
  59.            and symbols = ["(", ")", ".", ",", "?", "~", "&", "|", 
  60.                           "<->", "-->", "|-"]
  61.     end;
  62. structure FolLex = LexicalFUN (structure Basic=Basic and Keyword=FolKey);
  63. structure Parse = ParseFUN(FolLex);
  64. structure Pretty = PrettyFUN();
  65. structure Fol = FolFUN(Basic);
  66. structure ParseFol = ParseFolFUN(structure Parse=Parse and Fol=Fol);
  67. structure DispFol = DispFolFUN 
  68.     (structure Basic=Basic and Pretty=Pretty and Fol=Fol);
  69. structure Unify = UnifyFUN(structure Basic=Basic and Fol=Fol);
  70. structure Proof = ProofFUN(structure Basic=Basic 
  71.                          and Unify=Unify and Seq=Seq and Fol=Fol);
  72. structure Command = CommandFUN(structure Basic=Basic 
  73.             and Fol=Fol and ParseFol=ParseFol
  74.             and DispFol=DispFol and Proof=Proof);
  75. structure Tactical = TacticalFUN(Proof);
  76. structure FolTac = FolTacFUN (structure Proof=Proof and Tactical=Tactical);
  77. open Fol Proof Command Tactical FolTac;
  78.  
  79. (* the second quantifier proof, section 10.4 *)
  80. goal "EX z. P(z) --> (ALL x. P(x))";
  81. by (ex_right_tac 1);
  82. by (imp_right_tac 1);
  83. by (all_right_tac 1);
  84. by (unify_tac 1);  (*FAILS!*)
  85. by (ex_right_tac 1);
  86. by (imp_right_tac 1);
  87. by (unify_tac 1);
  88.  
  89.  
  90. (** Problems by Pelletier (1986). **)
  91.  
  92. (*3*)
  93. goal "~(P-->Q) --> (Q-->P)";
  94. by depth_tac;
  95.  
  96. (*5*)
  97. goal "((P|Q)-->(P|R)) --> (P|(Q-->R))";
  98. by depth_tac;
  99.  
  100. (*8.  Peirce's law*)
  101. goal "((P-->Q) --> P)  -->  P";
  102. by depth_tac;
  103.  
  104. (*12.  "Dijkstra's law"*)
  105. goal "((P <-> Q) <-> R)  -->  (P <-> (Q <-> R))";
  106. by depth_tac;
  107.  
  108. (*13.  Distributive law*)
  109. goal "P | (Q & R)  <-> (P | Q) & (P | R)";
  110. by depth_tac;
  111.  
  112. (*17*)
  113. goal "((P & (Q-->R))-->S)  <->  ((~P | Q | S) & (~P | ~R | S))";
  114. by depth_tac;
  115.  
  116. (*19*)
  117. goal "EX x. ALL y. ALL z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
  118. by depth_tac;
  119.  
  120. (*20*)
  121. goal "(ALL x. ALL y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))    \
  122. \   --> (EX x. EX y. P(x) & Q(y)) --> (EX z. R(z))";
  123. by depth_tac; 
  124.  
  125. (*21*)
  126. goal "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))";
  127. by depth_tac; 
  128.  
  129. (*22*)
  130. goal "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &    \
  131. \    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))    \
  132. \   --> (EX x. P(x)&R(x))";
  133. by depth_tac; 
  134.  
  135. (*27*)
  136. goal "(EX x. P(x) & ~Q(x)) &    \
  137. \       (ALL x. P(x) --> R(x)) &    \
  138. \       (ALL x. M(x) & L(x) --> P(x)) &    \
  139. \       ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))    \
  140. \   --> (ALL x. M(x) --> ~L(x))";
  141. by depth_tac; 
  142.  
  143. (*32*)
  144. goal "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &    \
  145. \       (ALL x. S(x) & R(x) --> L(x)) &        \
  146. \       (ALL x. M(x) --> R(x))    \
  147. \   --> (ALL x. P(x) & M(x) --> L(x))";
  148. by depth_tac;
  149.  
  150. (*37*)
  151. goal "(ALL z. EX w. ALL x. EX y.                    \
  152. \          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) &    \
  153. \       (ALL x. ALL z. ~P(x,z) --> (EX y. Q(y,z))) &            \
  154. \       ((EX x. EX y. Q(x,y)) --> (ALL x. R(x,x)))            \
  155. \   --> (ALL x. EX y. R(x,y))";
  156. by depth_tac;
  157.  
  158. (*40*)
  159. goal "(EX y. ALL x. J(y,x) <-> ~J(x,x))      \
  160. \       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
  161. by depth_tac;
  162.