author  oheimb 
Sat, 15 Feb 1997 17:44:10 +0100  
changeset 2634  b85c77b64c7a 
parent 1954  4b5b2d04782c 
child 3835  9a5a4e123859 
permissions  rwrr 
1459  1 
(* Title: FOL/ex/mini 
663  2 
ID: $Id$ 
1459  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
663  4 
Copyright 1994 University of Cambridge 
5 

6 
Classical FirstOrder Logic 

7 

8 
Conversion to nnf/miniscope format: pushing quantifiers in 

9 

10 
Demonstration of formula rewriting by proof 

11 
*) 

12 

13 
val ccontr = FalseE RS classical; 

14 

15 
(**** Negation Normal Form ****) 

16 

17 
(*** de Morgan laws ***) 

18 

743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

19 
fun prove_fun s = 
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

20 
(writeln s; 
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

21 
prove_goal FOL.thy s 
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

22 
(fn prems => [ (cut_facts_tac prems 1), 
1459  23 
(Cla.fast_tac FOL_cs 1) ])); 
663  24 

743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

25 
val demorgans = map prove_fun 
1459  26 
["~(P&Q) <> ~P  ~Q", 
27 
"~(PQ) <> ~P & ~Q", 

28 
"~~P <> P", 

29 
"~(ALL x.P(x)) <> (EX x. ~P(x))", 

30 
"~(EX x.P(x)) <> (ALL x. ~P(x))"]; 

663  31 

32 
(*** Removal of > and <> (positive and negative occurrences) ***) 

743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

33 
(*Last one is important for computing a compact CNF*) 
1954  34 
val nnf_simps = map prove_fun 
1459  35 
["(P>Q) <> (~P  Q)", 
36 
"~(P>Q) <> (P & ~Q)", 

37 
"(P<>Q) <> (~P  Q) & (~Q  P)", 

38 
"~(P<>Q) <> (P  Q) & (~P  ~Q)"]; 

663  39 

743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

40 
(* BEWARE: rewrite rules for <> can confuse the simplifier!! *) 
663  41 

42 
(*** Pushing in the existential quantifiers ***) 

43 

1954  44 
val ex_simps = map prove_fun 
1459  45 
["(EX x. P) <> P", 
46 
"(EX x. P(x) & Q) <> (EX x.P(x)) & Q", 

47 
"(EX x. P & Q(x)) <> P & (EX x.Q(x))", 

48 
"(EX x. P(x)  Q(x)) <> (EX x.P(x))  (EX x.Q(x))", 

49 
"(EX x. P(x)  Q) <> (EX x.P(x))  Q", 

50 
"(EX x. P  Q(x)) <> P  (EX x.Q(x))"]; 

663  51 

52 
(*** Pushing in the universal quantifiers ***) 

53 

1954  54 
val all_simps = map prove_fun 
1459  55 
["(ALL x. P) <> P", 
56 
"(ALL x. P(x) & Q(x)) <> (ALL x.P(x)) & (ALL x.Q(x))", 

57 
"(ALL x. P(x) & Q) <> (ALL x.P(x)) & Q", 

58 
"(ALL x. P & Q(x)) <> P & (ALL x.Q(x))", 

59 
"(ALL x. P(x)  Q) <> (ALL x.P(x))  Q", 

60 
"(ALL x. P  Q(x)) <> P  (ALL x.Q(x))"]; 

663  61 

62 

2634  63 
val mini_ss=FOL_basic_ss addsimps (demorgans @ nnf_simps @ ex_simps @ all_simps); 
663  64 

743
9dcce140bdfc
prove_fun: new; no longer depends upon the version in simpdata.ML
lcp
parents:
663
diff
changeset

65 
val mini_tac = rtac ccontr THEN' asm_full_simp_tac mini_ss; 
663  66 