author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 10429  8820f787e61e 
child 10906  de95ba2760fe 
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!*) 
4466
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4305
diff
changeset

17 
fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4305
diff
changeset

18 
val dest_Trueprop = HOLogic.dest_Trueprop 
305390f23734
Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
paulson
parents:
4305
diff
changeset

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

20 
val eq_reflection = eq_reflection 
9531  21 
val rev_eq_reflection = def_imp_eq 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

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

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

25 
val sym = sym 
7357  26 
val thin_refl = prove_goal (the_context ()) 
4223  27 
"!!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

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

29 

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

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

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

32 

9158  33 

34 
(*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***) 

9846  35 
structure Make_Elim = Make_Elim_Fun (val classical = classical); 
9158  36 

37 
(*we don't redeclare the original make_elim (Tactic.make_elim) for 

38 
compatibliity with strange things done in many existing proofs *) 

39 
val cla_make_elim = Make_Elim.make_elim; 

40 

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

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

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

43 
struct 
9158  44 
val make_elim = cla_make_elim 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

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

47 
val classical = classical 
9158  48 
val sizef = size_of_thm 
4206  49 
val hyp_subst_tacs=[hyp_subst_tac] 
10429  50 
val atomize = thms "atomize'" 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

52 

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

53 
structure Classical = ClassicalFun(Classical_Data); 
10197  54 

55 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

56 
open BasicClassical; 

57 

10231  58 
bind_thm ("contrapos_np", inst "Pa" "?Q" swap); 
10197  59 

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

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

61 
val prop_cs = empty_cs addSIs [refl,TrueI,conjI,disjCI,impI,notI,iffI] 
4305
03d7de40ee4f
The change from iffE to iffCE means fewer case splits in most cases. Very few
paulson
parents:
4240
diff
changeset

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

63 

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

64 
(*Quantifier rules*) 
9969  65 
val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, some_equality] 
3004  66 
addSEs [exE] addEs [allE]; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

67 

7357  68 
val clasetup = [fn thy => (claset_ref_of thy := HOL_cs; thy)]; 