author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37310  96e2b9a6f074 
child 59058  a78612c67ec0 
permissions  rwrr 
13404  1 
(* Title: HOL/Tools/rewrite_hol_proof.ML 
2 
Author: Stefan Berghofer, TU Muenchen 

3 

4 
Rewrite rules for HOL proofs 

5 
*) 

6 

7 
signature REWRITE_HOL_PROOF = 

8 
sig 

9 
val rews: (Proofterm.proof * Proofterm.proof) list 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

10 
val elim_cong: typ list > term option list > Proofterm.proof > (Proofterm.proof * Proofterm.proof) option 
13404  11 
end; 
12 

13 
structure RewriteHOLProof : REWRITE_HOL_PROOF = 

14 
struct 

15 

33388  16 
val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

17 
Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT) 
13404  18 

19 
(** eliminate metaequality rules **) 

20 

21 
["(equal_elim % x1 % x2 %% \ 

22 
\ (combination % TYPE('T1) % TYPE('T2) % Trueprop % x3 % A % B %% \ 

28712
4f2954d995f0
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents:
28262
diff
changeset

23 
\ (axm.reflexive % TYPE('T3) % x4) %% prf1)) == \ 
13404  24 
\ (iffD1 % A % B %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

25 
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))", 
13404  26 

27 
"(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \ 

28 
\ (combination % TYPE('T2) % TYPE('T3) % Trueprop % x5 % A % B %% \ 

28712
4f2954d995f0
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
berghofe
parents:
28262
diff
changeset

29 
\ (axm.reflexive % TYPE('T4) % x6) %% prf1))) == \ 
13404  30 
\ (iffD2 % A % B %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

31 
\ (meta_eq_to_obj_eq % TYPE(bool) % A % B %% arity_type_bool %% prf1))", 
13404  32 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

33 
"(meta_eq_to_obj_eq % TYPE('U) % x1 % x2 %% prfU %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

34 
\ (combination % TYPE('T) % TYPE('U) % f % g % x % y %% prf1 %% prf2)) == \ 
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

35 
\ (cong % TYPE('T) % TYPE('U) % f % g % x % y %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

36 
\ (OfClass type_class % TYPE('T)) %% prfU %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

37 
\ (meta_eq_to_obj_eq % TYPE('T => 'U) % f % g %% (OfClass type_class % TYPE('T => 'U)) %% prf1) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

38 
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% (OfClass type_class % TYPE('T)) %% prf2))", 
13404  39 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

40 
"(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

41 
\ (axm.transitive % TYPE('T) % x % y % z %% prf1 %% prf2)) == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

42 
\ (HOL.trans % TYPE('T) % x % y % z %% prfT %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

43 
\ (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf1) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

44 
\ (meta_eq_to_obj_eq % TYPE('T) % y % z %% prfT %% prf2))", 
13404  45 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

46 
"(meta_eq_to_obj_eq % TYPE('T) % x % x %% prfT %% (axm.reflexive % TYPE('T) % x)) == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

47 
\ (HOL.refl % TYPE('T) % x %% prfT)", 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

48 

b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

49 
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \ 
13404  50 
\ (axm.symmetric % TYPE('T) % x % y %% prf)) == \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

51 
\ (sym % TYPE('T) % x % y %% prfT %% (meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% prf))", 
13404  52 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

53 
"(meta_eq_to_obj_eq % TYPE('T => 'U) % x1 % x2 %% prfTU %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

54 
\ (abstract_rule % TYPE('T) % TYPE('U) % f % g %% prf)) == \ 
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

55 
\ (ext % TYPE('T) % TYPE('U) % f % g %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

56 
\ (OfClass type_class % TYPE('T)) %% (OfClass type_class % TYPE('U)) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

57 
\ (Lam (x::'T). meta_eq_to_obj_eq % TYPE('U) % f x % g x %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

58 
\ (OfClass type_class % TYPE('U)) %% (prf % x)))", 
13404  59 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

60 
"(meta_eq_to_obj_eq % TYPE('T) % x % y %% prfT %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

61 
\ (eq_reflection % TYPE('T) % x % y %% prfT %% prf)) == prf", 
13404  62 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

63 
"(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

64 
\ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \ 
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

65 
\ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \ 
13404  66 
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \ 
67 
\ (iffD1 % A = C % B = D %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

68 
\ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

69 
\ prfT %% arity_type_bool %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

70 
\ (cong % TYPE('T) % TYPE('T=>bool) % \ 
13404  71 
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

72 
\ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

73 
\ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

74 
\ (OfClass type_class % TYPE('T=>'T=>bool))) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

75 
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

76 
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

77 
\ (meta_eq_to_obj_eq % TYPE('T) % A % C %% prfT %% prf3))", 
13404  78 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

79 
"(meta_eq_to_obj_eq % TYPE('T) % x1 % x2 %% prfT %% (equal_elim % x3 % x4 %% \ 
13404  80 
\ (axm.symmetric % TYPE('T2) % x5 % x6 %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

81 
\ (combination % TYPE('T) % TYPE(prop) % x7 % x8 % C % D %% \ 
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

82 
\ (combination % TYPE('T) % TYPE('T3) % op == % op == % A % B %% \ 
13404  83 
\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \ 
84 
\ (iffD2 % A = C % B = D %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

85 
\ (cong % TYPE('T) % TYPE(bool) % op = A % op = B % C % D %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

86 
\ prfT %% arity_type_bool %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

87 
\ (cong % TYPE('T) % TYPE('T=>bool) % \ 
13404  88 
\ (op = :: 'T=>'T=>bool) % (op = :: 'T=>'T=>bool) % A % B %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

89 
\ prfT %% (OfClass type_class % TYPE('T=>bool)) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

90 
\ (HOL.refl % TYPE('T=>'T=>bool) % (op = :: 'T=>'T=>bool) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

91 
\ (OfClass type_class % TYPE('T=>'T=>bool))) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

92 
\ (meta_eq_to_obj_eq % TYPE('T) % A % B %% prfT %% prf1)) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

93 
\ (meta_eq_to_obj_eq % TYPE('T) % C % D %% prfT %% prf2)) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

94 
\ (meta_eq_to_obj_eq % TYPE('T) % B % D %% prfT %% prf3))", 
13404  95 

96 
(** rewriting on bool: insert proper congruence rules for logical connectives **) 

97 

98 
(* All *) 

99 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

100 
"(iffD1 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

101 
\ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

102 
\ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

103 
\ (allI % TYPE('a) % Q %% prfa %% \ 
13404  104 
\ (Lam x. \ 
105 
\ iffD1 % P x % Q x %% (prf % x) %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

106 
\ (spec % TYPE('a) % P % x %% prfa %% prf')))", 
13404  107 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

108 
"(iffD2 % All P % All Q %% (cong % TYPE('T1) % TYPE('T2) % All % All % P % Q %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

109 
\ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

110 
\ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

111 
\ (allI % TYPE('a) % P %% prfa %% \ 
13404  112 
\ (Lam x. \ 
113 
\ iffD2 % P x % Q x %% (prf % x) %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

114 
\ (spec % TYPE('a) % Q % x %% prfa %% prf')))", 
13404  115 

116 
(* Ex *) 

117 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

118 
"(iffD1 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

119 
\ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

120 
\ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

121 
\ (exE % TYPE('a) % P % EX x. Q x %% prfa %% prf' %% \ 
13404  122 
\ (Lam x H : P x. \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

123 
\ exI % TYPE('a) % Q % x %% prfa %% \ 
13404  124 
\ (iffD1 % P x % Q x %% (prf % x) %% H)))", 
125 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

126 
"(iffD2 % Ex P % Ex Q %% (cong % TYPE('T1) % TYPE('T2) % Ex % Ex % P % Q %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

127 
\ (HOL.refl % TYPE('T3) % x1 %% prfT3) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

128 
\ (ext % TYPE('a) % TYPE(bool) % x2 % x3 %% prfa %% prfb %% prf)) %% prf') == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

129 
\ (exE % TYPE('a) % Q % EX x. P x %% prfa %% prf' %% \ 
13404  130 
\ (Lam x H : Q x. \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

131 
\ exI % TYPE('a) % P % x %% prfa %% \ 
13404  132 
\ (iffD2 % P x % Q x %% (prf % x) %% H)))", 
133 

134 
(* & *) 

135 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

136 
"(iffD1 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

137 
\ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

138 
\ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \ 
13404  139 
\ (conjI % B % D %% \ 
140 
\ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \ 

141 
\ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))", 

142 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

143 
"(iffD2 % A & C % B & D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

144 
\ (cong % TYPE('T3) % TYPE('T4) % op & % op & % A % B %% prfT3 %% prfT4 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

145 
\ (HOL.refl % TYPE('T5) % op & %% prfT5) %% prf1) %% prf2) %% prf3) == \ 
13404  146 
\ (conjI % A % C %% \ 
147 
\ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \ 

148 
\ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))", 

149 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

150 
"(cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

151 
\ (HOL.refl % TYPE(bool=>bool) % op & A %% prfbb)) == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

152 
\ (cong % TYPE(bool) % TYPE(bool) % op & A % op & A % B % C %% prfb %% prfb %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

153 
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \ 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

154 
\ (op & :: bool=>bool=>bool) % (op & :: bool=>bool=>bool) % A % A %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

155 
\ prfb %% prfbb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

156 
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op & :: bool=>bool=>bool) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

157 
\ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

158 
\ (HOL.refl % TYPE(bool) % A %% prfb)))", 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

159 

13404  160 
(*  *) 
161 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

162 
"(iffD1 % A  C % B  D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

163 
\ (cong % TYPE('T3) % TYPE('T4) % op  % op  % A % B %% prfT3 %% prfT4 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

164 
\ (HOL.refl % TYPE('T5) % op  %% prfT5) %% prf1) %% prf2) %% prf3) == \ 
13404  165 
\ (disjE % A % C % B  D %% prf3 %% \ 
166 
\ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \ 

167 
\ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))", 

168 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

169 
"(iffD2 % A  C % B  D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

170 
\ (cong % TYPE('T3) % TYPE('T4) % op  % op  % A % B %% prfT3 %% prfT4 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

171 
\ (HOL.refl % TYPE('T5) % op  %% prfT5) %% prf1) %% prf2) %% prf3) == \ 
13404  172 
\ (disjE % B % D % A  C %% prf3 %% \ 
173 
\ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \ 

174 
\ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))", 

175 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

176 
"(cong % TYPE(bool) % TYPE(bool) % op  A % op  A % B % C %% prfb %% prfb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

177 
\ (HOL.refl % TYPE(bool=>bool) % op  A %% prfbb)) == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

178 
\ (cong % TYPE(bool) % TYPE(bool) % op  A % op  A % B % C %% prfb %% prfb %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

179 
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \ 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

180 
\ (op  :: bool=>bool=>bool) % (op  :: bool=>bool=>bool) % A % A %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

181 
\ prfb %% prfbb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

182 
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op  :: bool=>bool=>bool) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

183 
\ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

184 
\ (HOL.refl % TYPE(bool) % A %% prfb)))", 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

185 

13404  186 
(* > *) 
187 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

188 
"(iffD1 % A > C % B > D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

189 
\ (cong % TYPE('T3) % TYPE('T4) % op > % op > % A % B %% prfT3 %% prfT4 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

190 
\ (HOL.refl % TYPE('T5) % op > %% prfT5) %% prf1) %% prf2) %% prf3) == \ 
13404  191 
\ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \ 
192 
\ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))", 

193 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

194 
"(iffD2 % A > C % B > D %% (cong % TYPE('T1) % TYPE('T2) % x1 % x2 % C % D %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

195 
\ (cong % TYPE('T3) % TYPE('T4) % op > % op > % A % B %% prfT3 %% prfT4 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

196 
\ (HOL.refl % TYPE('T5) % op > %% prfT5) %% prf1) %% prf2) %% prf3) == \ 
13404  197 
\ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \ 
198 
\ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))", 

199 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

200 
"(cong % TYPE(bool) % TYPE(bool) % op > A % op > A % B % C %% prfb %% prfb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

201 
\ (HOL.refl % TYPE(bool=>bool) % op > A %% prfbb)) == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

202 
\ (cong % TYPE(bool) % TYPE(bool) % op > A % op > A % B % C %% prfb %% prfb %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

203 
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \ 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

204 
\ (op > :: bool=>bool=>bool) % (op > :: bool=>bool=>bool) % A % A %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

205 
\ prfb %% prfbb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

206 
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op > :: bool=>bool=>bool) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

207 
\ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

208 
\ (HOL.refl % TYPE(bool) % A %% prfb)))", 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

209 

13404  210 
(* ~ *) 
211 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

212 
"(iffD1 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

213 
\ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \ 
13404  214 
\ (notI % Q %% (Lam H: Q. \ 
215 
\ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))", 

216 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

217 
"(iffD2 % ~ P % ~ Q %% (cong % TYPE('T1) % TYPE('T2) % Not % Not % P % Q %% prfT1 %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

218 
\ (HOL.refl % TYPE('T3) % Not %% prfT3) %% prf1) %% prf2) == \ 
13404  219 
\ (notI % P %% (Lam H: P. \ 
220 
\ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))", 

221 

222 
(* = *) 

223 

224 
"(iffD1 % B % D %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

225 
\ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

226 
\ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

227 
\ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \ 
13404  228 
\ (iffD1 % C % D %% prf2 %% \ 
229 
\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))", 

230 

231 
"(iffD2 % B % D %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

232 
\ (iffD1 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

233 
\ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

234 
\ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \ 
13404  235 
\ (iffD1 % A % B %% prf1 %% \ 
236 
\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))", 

237 

238 
"(iffD1 % A % C %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

239 
\ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

240 
\ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

241 
\ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4)== \ 
13404  242 
\ (iffD2 % C % D %% prf2 %% \ 
243 
\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))", 

244 

245 
"(iffD2 % A % C %% \ 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

246 
\ (iffD2 % A = C % B = D %% (cong % TYPE(bool) % TYPE('T1) % x1 % x2 % C % D %% prfb %% prfT1 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

247 
\ (cong % TYPE(bool) % TYPE('T2) % op = % op = % A % B %% prfb %% prfT2 %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

248 
\ (HOL.refl % TYPE('T3) % op = %% prfT3) %% prf1) %% prf2) %% prf3) %% prf4) == \ 
13404  249 
\ (iffD2 % A % B %% prf1 %% \ 
250 
\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))", 

251 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

252 
"(cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

253 
\ (HOL.refl % TYPE(bool=>bool) % op = A %% prfbb)) == \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

254 
\ (cong % TYPE(bool) % TYPE(bool) % op = A % op = A % B % C %% prfb %% prfb %% \ 
36042
85efdadee8ae
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
krauss
parents:
35845
diff
changeset

255 
\ (cong % TYPE(bool) % TYPE(bool=>bool) % \ 
13404  256 
\ (op = :: bool=>bool=>bool) % (op = :: bool=>bool=>bool) % A % A %% \ 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

257 
\ prfb %% prfbb %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

258 
\ (HOL.refl % TYPE(bool=>bool=>bool) % (op = :: bool=>bool=>bool) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

259 
\ (OfClass type_class % TYPE(bool=>bool=>bool))) %% \ 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

260 
\ (HOL.refl % TYPE(bool) % A %% prfb)))", 
13404  261 

13916
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

262 
(** transitivity, reflexivity, and symmetry **) 
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

263 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

264 
"(iffD1 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \ 
13404  265 
\ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))", 
266 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

267 
"(iffD2 % A % C %% (HOL.trans % TYPE(bool) % A % B % C %% prfb %% prf1 %% prf2) %% prf3) == \ 
13404  268 
\ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))", 
269 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

270 
"(iffD1 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf", 
13404  271 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

272 
"(iffD2 % A % A %% (HOL.refl % TYPE(bool) % A %% prfb) %% prf) == prf", 
13404  273 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

274 
"(iffD1 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD2 % B % A %% prf)", 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

275 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

276 
"(iffD2 % A % B %% (sym % TYPE(bool) % B % A %% prfb %% prf)) == (iffD1 % B % A %% prf)", 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

277 

13404  278 
(** normalization of HOL proofs **) 
279 

280 
"(mp % A % B %% (impI % A % B %% prf)) == prf", 

281 

282 
"(impI % A % B %% (mp % A % B %% prf)) == prf", 

283 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

284 
"(spec % TYPE('a) % P % x %% prfa %% (allI % TYPE('a) % P %% prfa %% prf)) == prf % x", 
13404  285 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

286 
"(allI % TYPE('a) % P %% prfa %% (Lam x::'a. spec % TYPE('a) % P % x %% prfa %% prf)) == prf", 
13404  287 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

288 
"(exE % TYPE('a) % P % Q %% prfa %% (exI % TYPE('a) % P % x %% prfa %% prf1) %% prf2) == (prf2 % x %% prf1)", 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

289 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

290 
"(exE % TYPE('a) % P % Q %% prfa %% prf %% (exI % TYPE('a) % P %% prfa)) == prf", 
13602
4cecd1e0f4a9
 additional congruence rules for boolean operators
berghofe
parents:
13404
diff
changeset

291 

13404  292 
"(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)", 
293 

294 
"(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)", 

295 

296 
"(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1", 

297 

298 
"(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2", 

299 

300 
"(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1", 

301 

302 
"(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"]; 

303 

304 

305 
(** Replace congruence rules by substitution rules **) 

306 

28801
fc45401bdf6f
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
wenzelm
parents:
28712
diff
changeset

307 
fun strip_cong ps (PThm (_, (("HOL.cong", _, _), _)) % _ % _ % SOME x % SOME y %% 
37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

308 
prfa %% prfT %% prf1 %% prf2) = strip_cong (((x, y), (prf2, prfa)) :: ps) prf1 
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

309 
 strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps) 
15531  310 
 strip_cong _ _ = NONE; 
13404  311 

37310  312 
val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst)))); 
313 
val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym)))); 

13404  314 

315 
fun make_subst Ts prf xs (_, []) = prf 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

316 
 make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) = 
13404  317 
let val T = fastype_of1 (Ts, x) 
318 
in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps) 

37310  319 
else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %> 
13404  320 
Abs ("z", T, list_comb (incr_boundvars 1 f, 
321 
map (incr_boundvars 1) xs @ Bound 0 :: 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

322 
map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %% 
13404  323 
make_subst Ts prf (xs @ [x]) (f, ps) 
324 
end; 

325 

37233
b78f31ca4675
Adapted to new format of proof terms containing explicit proofs of class membership.
berghofe
parents:
36042
diff
changeset

326 
fun make_sym Ts ((x, y), (prf, clprf)) = 
37310  327 
((y, x), 
328 
(Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf)); 

13404  329 

22277  330 
fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t); 
13916
f078a758e5d8
elim_cong now etaexpands proofs on the fly if required.
berghofe
parents:
13602
diff
changeset

331 

33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33388
diff
changeset

332 
fun elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % _ % _ %% prf1 %% prf2) = 
15570  333 
Option.map (make_subst Ts prf2 []) (strip_cong [] prf1) 
33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33388
diff
changeset

334 
 elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) = 
15570  335 
Option.map (mk_AbsP P o make_subst Ts (PBound 0) []) 
37310  336 
(strip_cong [] (Proofterm.incr_pboundvars 1 0 prf)) 
33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33388
diff
changeset

337 
 elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) = 
15570  338 
Option.map (make_subst Ts prf2 [] o 
13404  339 
apsnd (map (make_sym Ts))) (strip_cong [] prf1) 
33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33388
diff
changeset

340 
 elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) = 
15570  341 
Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o 
37310  342 
apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf)) 
33722
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33388
diff
changeset

343 
 elim_cong_aux _ _ = NONE; 
e588744f14da
generalized procs for rewrite_proof: allow skeleton;
wenzelm
parents:
33388
diff
changeset

344 

37310  345 
fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf); 
13404  346 

347 
end; 