author  oheimb 
Wed, 12 Nov 1997 18:58:50 +0100  
changeset 4223  f60e3d2c81d3 
parent 4206  688050e83d89 
child 4240  8ba60a4cd380 
permissions  rwrr 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

1 
(* Title: HOL/cladata.ML 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

2 
ID: $Id$ 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

3 
Author: Tobias Nipkow 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

5 

4085  6 
Setting up the classical reasoner. 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

7 
*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

8 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

9 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

10 
(** Applying HypsubstFun to generate hyp_subst_tac **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

11 
section "Classical Reasoner"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

12 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

13 
structure Hypsubst_Data = 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

14 
struct 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

15 
structure Simplifier = Simplifier 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

16 
(*Take apart an equality judgement; otherwise raise Match!*) 
4179
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
4085
diff
changeset

17 
fun dest_eq (Const("Trueprop",_) $ (Const("op =",T) $ t $ u)) = 
cc4b6791d5dc
hyp_subst_tac checks if the equality has type variables and uses a suitable
paulson
parents:
4085
diff
changeset

18 
(t, u, domain_type T) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

19 
val eq_reflection = eq_reflection 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

20 
val imp_intr = impI 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

21 
val rev_mp = rev_mp 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

22 
val subst = subst 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

23 
val sym = sym 
4223  24 
val thin_refl = prove_goal HOL.thy 
25 
"!!X. [x=x; PROP W] ==> PROP W" (K [atac 1]); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

26 
end; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

27 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

28 
structure Hypsubst = HypsubstFun(Hypsubst_Data); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

29 
open Hypsubst; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

30 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

31 
(*** Applying ClassicalFun to create a classical prover ***) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

32 
structure Classical_Data = 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

33 
struct 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

34 
val sizef = size_of_thm 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

35 
val mp = mp 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

36 
val not_elim = notE 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

37 
val classical = classical 
4206  38 
val hyp_subst_tacs=[hyp_subst_tac] 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

39 
end; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

40 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

41 
structure Classical = ClassicalFun(Classical_Data); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

42 
open Classical; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

43 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

44 
(*Propositional rules*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

45 
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

46 
addSEs [conjE,disjE,impCE,FalseE,iffE]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

47 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

48 
(*Quantifier rules*) 
3004  49 
val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
50 
addSEs [exE] addEs [allE]; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

51 

4085  52 
claset_ref() := HOL_cs; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

53 

3004  54 
(*Better then ex1E for classical reasoner: needs no quantifier duplication!*) 
55 
qed_goal "alt_ex1E" thy 

3842  56 
"[ ?! x. P(x); \ 
3004  57 
\ !!x. [ P(x); ALL y y'. P(y) & P(y') > y=y' ] ==> R \ 
58 
\ ] ==> R" 

59 
(fn major::prems => 

60 
[ (rtac (major RS ex1E) 1), 

61 
(REPEAT (ares_tac (allI::prems) 1)), 

62 
(etac (dup_elim allE) 1), 

63 
(Fast_tac 1)]); 

64 

65 
AddSEs [alt_ex1E]; 

2860  66 

67 
(*** Applying BlastFun to create Blast_tac ***) 

68 
structure Blast_Data = 

69 
struct 

70 
type claset = Classical.claset 

71 
val notE = notE 

72 
val ccontr = ccontr 

73 
val contr_tac = Classical.contr_tac 

74 
val dup_intr = Classical.dup_intr 

75 
val vars_gen_hyp_subst_tac = Hypsubst.vars_gen_hyp_subst_tac 

76 
val claset = Classical.claset 

77 
val rep_claset = Classical.rep_claset 

78 
end; 

79 

80 
structure Blast = BlastFun(Blast_Data); 

4059  81 
Blast.overload ("op =", domain_type); (*overloading of equality as iff*) 
2860  82 

83 
val Blast_tac = Blast.Blast_tac 

84 
and blast_tac = Blast.blast_tac; 