isabelle: src/HOL/Tools/rewrite_hol_proof.ML@0b217404522a (annotated)

13404 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	1	(* Title: HOL/Tools/rewrite_hol_proof.ML
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	2	Author: Stefan Berghofer, TU Muenchen
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	3
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	4	Rewrite rules for HOL proofs
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	5	*)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	6
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	7	signature REWRITE_HOL_PROOF =
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	8	sig
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	11	end;
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	12
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	13	structure RewriteHOLProof : REWRITE_HOL_PROOF =
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	14	struct
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	15
33388 d64545e6cba5 modernized structure Proof_Syntax; wenzelm parents: 32010 diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	18
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	19	( eliminate meta-equality rules )
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	20
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	21	["(equal_elim % x1 % x2 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	26
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	27	"(equal_elim % x1 % x2 %% (axm.symmetric % TYPE('T1) % x3 % x4 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	66	\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2) %% prf3)) == \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	83	\ (axm.reflexive % TYPE('T4) % op ==) %% prf1) %% prf2)) %% prf3)) == \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	95
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	96	( rewriting on bool: insert proper congruence rules for logical connectives )
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	97
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	98	(* All *)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	104	\ (Lam x. \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	112	\ (Lam x. \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	115
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	116	(* Ex *)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	124	\ (iffD1 % P x % Q x %% (prf % x) %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	132	\ (iffD2 % P x % Q x %% (prf % x) %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	133
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	134	(* & *)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	139	\ (conjI % B % D %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	140	\ (iffD1 % A % B %% prf1 %% (conjunct1 % A % C %% prf3)) %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	141	\ (iffD1 % C % D %% prf2 %% (conjunct2 % A % C %% prf3)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	146	\ (conjI % A % C %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	147	\ (iffD2 % A % B %% prf1 %% (conjunct1 % B % D %% prf3)) %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	148	\ (iffD2 % C % D %% prf2 %% (conjunct2 % B % D %% prf3)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	160	(* \| *)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	165	\ (disjE % A % C % B \| D %% prf3 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	166	\ (Lam H : A. disjI1 % B % D %% (iffD1 % A % B %% prf1 %% H)) %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	167	\ (Lam H : C. disjI2 % D % B %% (iffD1 % C % D %% prf2 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	172	\ (disjE % B % D % A \| C %% prf3 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	173	\ (Lam H : B. disjI1 % A % C %% (iffD2 % A % B %% prf1 %% H)) %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	174	\ (Lam H : D. disjI2 % C % A %% (iffD2 % C % D %% prf2 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	186	(* --> *)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	191	\ (impI % B % D %% (Lam H: B. iffD1 % C % D %% prf2 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	192	\ (mp % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% H))))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	197	\ (impI % A % C %% (Lam H: A. iffD2 % C % D %% prf2 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	198	\ (mp % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% H))))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	210	(* ~ *)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	214	\ (notI % Q %% (Lam H: Q. \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	215	\ notE % P % False %% prf2 %% (iffD2 % P % Q %% prf1 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	219	\ (notI % P %% (Lam H: P. \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	220	\ notE % Q % False %% prf2 %% (iffD1 % P % Q %% prf1 %% H)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	221
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	222	(* = *)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	223
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	228	\ (iffD1 % C % D %% prf2 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	229	\ (iffD1 % A % C %% prf3 %% (iffD2 % A % B %% prf1 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	230
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	235	\ (iffD1 % A % B %% prf1 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	236	\ (iffD2 % A % C %% prf3 %% (iffD2 % C % D %% prf2 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	237
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	242	\ (iffD2 % C % D %% prf2 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	243	\ (iffD1 % B % D %% prf3 %% (iffD1 % A % B %% prf1 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	244
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	249	\ (iffD2 % A % B %% prf1 %% \
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	250	\ (iffD2 % B % D %% prf3 %% (iffD1 % C % D %% prf2 %% prf4)))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	261
13916 f078a758e5d8 elim_cong now eta-expands proofs on the fly if required. berghofe parents: 13602 diff changeset	262	( transitivity, reflexivity, and symmetry )
f078a758e5d8 elim_cong now eta-expands 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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	265	\ (iffD1 % B % C %% prf2 %% (iffD1 % A % B %% prf1 %% prf3))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	268	\ (iffD2 % A % B %% prf1 %% (iffD2 % B % C %% prf2 %% prf3))",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	278	( normalization of HOL proofs )
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	279
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	280	"(mp % A % B %% (impI % A % B %% prf)) == prf",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	281
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	282	"(impI % A % B %% (mp % A % B %% prf)) == prf",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	292	"(disjE % P % Q % R %% (disjI1 % P % Q %% prf1) %% prf2 %% prf3) == (prf2 %% prf1)",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	293
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	294	"(disjE % P % Q % R %% (disjI2 % Q % P %% prf1) %% prf2 %% prf3) == (prf3 %% prf1)",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	295
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	296	"(conjunct1 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf1",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	297
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	298	"(conjunct2 % P % Q %% (conjI % P % Q %% prf1 %% prf2)) == prf2",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	299
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	300	"(iffD1 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf1",
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	301
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	302	"(iffD2 % A % B %% (iffI % A % B %% prf1 %% prf2)) == prf2"];
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	303
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	304
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	305	( Replace congruence rules by substitution rules )
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 08c8dad8e399 Deleted Library.option type. skalberg parents: 15530 diff changeset	310	\| strip_cong _ _ = NONE;
13404 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	311
37310 96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	312	val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst))));
96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	313	val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym))));
13404 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	314
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	317	let val T = fastype_of1 (Ts, x)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	318	in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
37310 96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	319	else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %>
13404 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	320	Abs ("z", T, list_comb (incr_boundvars 1 f,
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	323	make_subst Ts prf (xs @ [x]) (f, ps)
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	324	end;
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	327	((y, x),
96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	328	(Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
13404 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	329
22277 b89dc456dbc6 Fixed bug in mk_AbsP. berghofe parents: 21646 diff changeset	330	fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
13916 f078a758e5d8 elim_cong now eta-expands 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 8d8c70b41bab Move towards standard functions. skalberg parents: 15531 diff changeset	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 8d8c70b41bab Move towards standard functions. skalberg parents: 15531 diff changeset	335	Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
37310 96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	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 8d8c70b41bab Move towards standard functions. skalberg parents: 15531 diff changeset	338	Option.map (make_subst Ts prf2 [] o
13404 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	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 8d8c70b41bab Move towards standard functions. skalberg parents: 15531 diff changeset	341	Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
37310 96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	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 96e2b9a6f074 do not open Proofterm, which is very ould style; wenzelm parents: 37233 diff changeset	345	fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf);
13404 eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	346
eeac2bbfe958 Rules for rewriting HOL proofs. berghofe parents: diff changeset	347	end;

author	krauss
	Sun, 21 Aug 2011 22:13:04 +0200
changeset 44374	0b217404522a
parent 37310	96e2b9a6f074
child 59058	a78612c67ec0
permissions	-rw-r--r--