author  wenzelm 
Tue, 04 Dec 2001 02:01:31 +0100  
changeset 12355  c8d3c3d09080 
parent 11753  02b257ef0ee2 
child 15570  8d8c70b41bab 
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 

12355  33 
(*prevent substitution on bool*) 
34 
fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso 

35 
Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", [])  _ => false) 

36 
(Library.nth_elem (i  1, Thm.prems_of thm)) then hyp_subst_tac i thm else no_tac thm; 

37 

38 

9158  39 

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

9846  41 
structure Make_Elim = Make_Elim_Fun (val classical = classical); 
9158  42 

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

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

45 
val cla_make_elim = Make_Elim.make_elim; 

46 

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

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

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

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

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

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

53 
val classical = classical 
9158  54 
val sizef = size_of_thm 
4206  55 
val hyp_subst_tacs=[hyp_subst_tac] 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

57 

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

58 
structure Classical = ClassicalFun(Classical_Data); 
10197  59 

60 
structure BasicClassical: BASIC_CLASSICAL = Classical; 

61 
open BasicClassical; 

62 

10231  63 
bind_thm ("contrapos_np", inst "Pa" "?Q" swap); 
10197  64 

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

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

66 
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

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

68 

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

69 
(*Quantifier rules*) 
11451
8abfb4f7bd02
partial restructuring to reduce dependence on Axiom of Choice
paulson
parents:
11440
diff
changeset

70 
val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality] 
3004  71 
addSEs [exE] addEs [allE]; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

72 

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