# HG changeset patch
# User paulson
# Date 881142496 -3600
# Node ID 50403e5a44c058d1006e7b62ac32f8550c3708c1
# Parent  c7f6b4256964c2439708cc7c403ef2fd841ba1ff
Instantiated the one-point-rule quantifier simpprocs for FOL

New file fologic.ML holds abstract syntax operations

Also, miniscoping provided for intuitionistic logic

diff -r c7f6b4256964 -r 50403e5a44c0 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Wed Dec 03 10:47:13 1997 +0100
+++ b/src/FOL/IsaMakefile	Wed Dec 03 10:48:16 1997 +0100
@@ -10,7 +10,7 @@
 	simplifier.ML splitter.ML ind.ML 
 
 FILES =	ROOT.ML IFOL.thy IFOL.ML FOL.thy FOL.ML intprover.ML simpdata.ML \
-	cladata.ML $(PROVERS:%=../Provers/%)
+	fologic.ML cladata.ML $(PROVERS:%=../Provers/%)
 
 EX_NAMES = If List Nat Nat2 Prolog IffOracle
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/foundn.ML ex/int.ML ex/intro.ML \
diff -r c7f6b4256964 -r 50403e5a44c0 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Dec 03 10:47:13 1997 +0100
+++ b/src/FOL/ROOT.ML	Wed Dec 03 10:48:16 1997 +0100
@@ -19,8 +19,10 @@
 use "$ISABELLE_HOME/src/Provers/hypsubst.ML";
 use "$ISABELLE_HOME/src/Provers/classical.ML";
 use "$ISABELLE_HOME/src/Provers/blast.ML";
+use "$ISABELLE_HOME/src/Provers/quantifier1.ML";
 
 use_thy "IFOL";
+use "fologic.ML";
 
 (** Applying HypsubstFun to generate hyp_subst_tac **)
 structure Hypsubst_Data =
diff -r c7f6b4256964 -r 50403e5a44c0 src/FOL/fologic.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/fologic.ML	Wed Dec 03 10:48:16 1997 +0100
@@ -0,0 +1,52 @@
+(*  Title:      FOL/fologic.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+
+Abstract syntax operations for FOL.
+*)
+
+signature FOLOGIC =
+sig
+  val oT: typ
+  val mk_Trueprop: term -> term
+  val dest_Trueprop: term -> term
+  val conj: term
+  val disj: term
+  val imp: term
+  val eq_const: typ -> term
+  val all_const: typ -> term
+  val exists_const: typ -> term
+  val mk_eq: term * term -> term
+  val mk_all: term * term -> term
+  val mk_exists: term * term -> term
+end;
+
+
+structure FOLogic: FOLOGIC =
+struct
+
+val oT = Type("o",[]);
+
+val Trueprop = Const("Trueprop", oT-->propT);
+
+fun mk_Trueprop P = Trueprop $ P;
+
+fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
+  | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
+
+(** Logical constants **)
+
+val conj = Const("op &", [oT,oT]--->oT)
+and disj = Const("op |", [oT,oT]--->oT)
+and imp = Const("op -->", [oT,oT]--->oT);
+
+fun eq_const T = Const ("op =", [T, T] ---> oT);
+fun mk_eq (t, u) = eq_const (fastype_of t) $ t $ u;
+
+fun all_const T = Const ("All", [T --> oT] ---> oT);
+fun mk_all (Free(x,T),P) = all_const T $ (absfree (x,T,P));
+
+fun exists_const T = Const ("Ex", [T --> oT] ---> oT);
+fun mk_exists (Free(x,T),P) = exists_const T $ (absfree (x,T,P));
+
+end;
diff -r c7f6b4256964 -r 50403e5a44c0 src/FOL/simpdata.ML
--- a/src/FOL/simpdata.ML	Wed Dec 03 10:47:13 1997 +0100
+++ b/src/FOL/simpdata.ML	Wed Dec 03 10:48:16 1997 +0100
@@ -41,8 +41,14 @@
   "(P <-> P) <-> True",
   "(False <-> P) <-> ~P",       "(P <-> False) <-> ~P"];
 
+(*The x=t versions are needed for the simplification procedures*)
 val quant_simps = map int_prove_fun
- ["(ALL x. P) <-> P",    "(EX x. P) <-> P"];
+ ["(ALL x. P) <-> P",   
+  "(ALL x. x=t --> P(x)) <-> P(t)",
+  "(ALL x. t=x --> P(x)) <-> P(t)",
+  "(EX x. P) <-> P",
+  "(EX x. x=t & P(x)) <-> P(t)", 
+  "(EX x. t=x & P(x)) <-> P(t)"];
 
 (*These are NOT supplied by default!*)
 val distrib_simps  = map int_prove_fun
@@ -96,30 +102,43 @@
   cases boil down to the same thing.*) 
 val cases_simp = prove_fun "(P --> Q) & (~P --> Q) <-> Q";
 
-(*At present, miniscoping is for classical logic only.  We do NOT include
-  distribution of ALL over &, or dually that of EX over |.*)
+
+(*** Miniscoping: pushing quantifiers in
+     We do NOT distribute of ALL over &, or dually that of EX over |
+     Baaz and Leitsch, On Skolemization and Proof Complexity (1994) 
+     show that this step can increase proof length!
+***)
+
+(*existential miniscoping*)
+val int_ex_simps = map int_prove_fun 
+		     ["(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
+		      "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
+		      "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
+		      "(EX x. P | Q(x)) <-> P | (EX x. Q(x))"];
+
+(*classical rules*)
+val cla_ex_simps = map prove_fun 
+                     ["(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
+		      "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
 
-(*Miniscoping: pushing in existential quantifiers*)
-val ex_simps = map prove_fun 
-                ["(EX x. x=t & P(x)) <-> P(t)",
-                 "(EX x. t=x & P(x)) <-> P(t)",
-                 "(EX x. P(x) & Q) <-> (EX x. P(x)) & Q",
-                 "(EX x. P & Q(x)) <-> P & (EX x. Q(x))",
-                 "(EX x. P(x) | Q) <-> (EX x. P(x)) | Q",
-                 "(EX x. P | Q(x)) <-> P | (EX x. Q(x))",
-                 "(EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q",
-                 "(EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"];
+val ex_simps = int_ex_simps @ cla_ex_simps;
+
+(*universal miniscoping*)
+val int_all_simps = map int_prove_fun
+		      ["(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
+		       "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
+		       "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
+		       "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
 
-(*Miniscoping: pushing in universal quantifiers*)
-val all_simps = map prove_fun
-                ["(ALL x. x=t --> P(x)) <-> P(t)",
-                 "(ALL x. t=x --> P(x)) <-> P(t)",
-                 "(ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q",
-                 "(ALL x. P & Q(x)) <-> P & (ALL x. Q(x))",
-                 "(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
-                 "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))",
-                 "(ALL x. P(x) --> Q) <-> (EX x. P(x)) --> Q",
-                 "(ALL x. P --> Q(x)) <-> P --> (ALL x. Q(x))"];
+(*classical rules*)
+val cla_all_simps = map prove_fun
+                      ["(ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q",
+		       "(ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"];
+
+val all_simps = int_all_simps @ cla_all_simps;
+
+
+(*** Named rewrite rules proved for IFOL ***)
 
 fun int_prove nm thm  = qed_goal nm IFOL.thy thm
     (fn prems => [ (cut_facts_tac prems 1), 
@@ -168,7 +187,50 @@
 val meta_eq_to_obj_eq = prove_goal IFOL.thy "x==y ==> x=y"
   (fn [prem] => [rewtac prem, rtac refl 1]);
 
-(*** case splitting ***)
+
+open Simplifier;
+
+(** make simplification procedures for quantifier elimination **)
+structure Quantifier1 = Quantifier1Fun(
+struct
+  (*abstract syntax*)
+  fun dest_eq((c as Const("op =",_)) $ s $ t) = Some(c,s,t)
+    | dest_eq _ = None;
+  fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
+    | dest_conj _ = None;
+  val conj = FOLogic.conj
+  val imp  = FOLogic.imp
+  (*rules*)
+  val iff_reflection = iff_reflection
+  val iffI = iffI
+  val sym  = sym
+  val conjI= conjI
+  val conjE= conjE
+  val impI = impI
+  val impE = impE
+  val mp   = mp
+  val exI  = exI
+  val exE  = exE
+  val allI = allI
+  val allE = allE
+end);
+
+local
+val ex_pattern =
+  read_cterm (sign_of FOL.thy) ("EX x. P(x) & Q(x)", FOLogic.oT)
+
+val all_pattern =
+  read_cterm (sign_of FOL.thy) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
+
+in
+val defEX_regroup =
+  mk_simproc "defined EX" [ex_pattern] Quantifier1.rearrange_ex;
+val defALL_regroup =
+  mk_simproc "defined ALL" [all_pattern] Quantifier1.rearrange_all;
+end;
+
+
+(*** Case splitting ***)
 
 qed_goal "meta_iffD" IFOL.thy "[| P==Q; Q |] ==> P"
         (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]);
@@ -192,7 +254,7 @@
 
 structure Induction = InductionFun(struct val spec=IFOL.spec end);
 
-open Simplifier Induction;
+open Induction;
 
 (*Add congruence rules for = or <-> (instead of ==) *)
 infix 4 addcongs delcongs;
@@ -222,12 +284,13 @@
 
 (*No simprules, but basic infastructure for simplification*)
 val FOL_basic_ss = empty_ss setsubgoaler asm_simp_tac
+                            addsimprocs [defALL_regroup,defEX_regroup]
 			    setSSolver   safe_solver
 			    setSolver  unsafe_solver
 			    setmksimps (map mk_meta_eq o atomize o gen_all);
 
 (*intuitionistic simprules only*)
-val IFOL_ss = FOL_basic_ss addsimps IFOL_simps
+val IFOL_ss = FOL_basic_ss addsimps (IFOL_simps @ int_ex_simps @ int_all_simps)
 			   addcongs [imp_cong];
 
 val cla_simps = 
@@ -240,7 +303,7 @@
       "(~P <-> ~Q) <-> (P<->Q)"];
 
 (*classical simprules too*)
-val FOL_ss = IFOL_ss addsimps (cla_simps @ ex_simps @ all_simps);
+val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
 
 simpset_ref() := FOL_ss;