val convC8_2 = prove_goal HOL_C8.thy "[| dt = Der ($Z |- $Y) cutr [Der za convs [dtza], Der ay conva [dtay]] ; \ \ cutOnFmls {A^} dt ; allDT wfb dt |] ==> \ \ allDT wfb dtay & allDT wfb dtza & \ \ conclDT dtza = ($Z |- @A) & conclDT dtay = (@A |- $Y)" (tacC8_2 [conva, convs]) ; val convC8_3 = prove_goal HOL_C8.thy "allDT wfb dtay & allDT wfb dtza & \ \ conclDT dtza = ($Z |- @A) & conclDT dtay = (@A |- $Y) ==> \ \ EX dtn. dtn = Der ($Z |- $Y) rblobs [ Der ?zy cutr [ \ \ Der ?za (invert mblob) [dtza], Der ?ay mblob [dtay]]] & \ \ allDT wfb dtn" tacC8_3 ; val convC8'' = prove_goal HOL_C8.thy "[| dt = Der ($Z |- $Y) cutr [Der za convs [dtza], Der ay conva [dtay]] ; \ \ cutOnFmls {A^} dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {A}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {A}) dtn" (fn prems => [ tacC8'' (convC8_2 RS convC8_3) convC8_2 prems ]) ; val convC8_1 = prove_goal HOL_C8.thy "[| dt = Der seq cutr dtl ; cutIsLRP (A^) dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq) | \ \ (EX Y Z ay za dtay dtza. \ \ dt = Der ($Z |- $Y) cutr [Der za convs [dtza], Der ay conva [dtay]])" (fn prems => [ tacC8_1_1 prems, (tacC8_1_2 [conva, convs] 3), tacidf 1, tacidf 1]) ; val convC8' = prove_goal HOL_C8.thy "[| cutIsLRP (A^) dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {A}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {A}) dtn" (tacC8' convC8_1 (SOME convC8'')) ; val thC8_1 = convC8_1 ; val thC8'' = convC8'' ; val rules = [conva, convs] ; (* ; val prems = it ; *) val notC8_2 = prove_goal HOL_C8.thy "[| dt = Der ($Z |- $Y) cutr [Der za nots [dtza], Der ay nota [dtay]] ; \ \ cutOnFmls {--A} dt ; allDT wfb dt |] ==> \ \ allDT wfb dtay & allDT wfb dtza & \ \ conclDT dtza = ($Z |- *A) & conclDT dtay = ( *A |- $Y)" (tacC8_2 [nota, nots]) ; val notC8_3 = prove_goal HOL_C8.thy "allDT wfb dtay & allDT wfb dtza & \ \ conclDT dtza = ($Z |- *A) & conclDT dtay = ( *A |- $Y) ==> \ \ EX dtn. dtn = Der ($Z |- $Y) rstars [ Der ?zy cutr [ \ \ Der ?ya sA [dtay], Der ?az sS [dtza]]] & \ \ allDT wfb dtn" tacC8_3 ; val notC8'' = prove_goal HOL_C8.thy "[| dt = Der ($Z |- $Y) cutr [Der za nots [dtza], Der ay nota [dtay]] ; \ \ cutOnFmls {--A} dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {A}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {A}) dtn" (fn prems => [ tacC8'' (notC8_2 RS notC8_3) notC8_2 prems ]) ; val notC8_1 = prove_goal HOL_C8.thy "[| dt = Der seq cutr dtl ; cutIsLRP (--A) dt ; \ \ allDT wfb dt ; allDT (frb rls) dt |] ==> \ \ (EX dt':set dtl. conclDT dt' = seq) | \ \ (EX Y Z ay za dtay dtza. \ \ dt = Der ($Z |- $Y) cutr [Der za nots [dtza], Der ay nota [dtay]])" (fn prems => [ tacC8_1_1 prems, (tacC8_1_2 [nota, nots] 3), tacidf 1, tacidf 1]) ; val notC8' = prove_goal HOL_C8.thy "[| cutIsLRP (--A) dt ; allDT wfb dt ; allDT (frb rls) dt ; \ \ allNextDTs (cutOnFmls {A}) dt |] ==> \ \ EX dtn. conclDT dtn = conclDT dt & \ \ allDT wfb dtn & allDT (frb rls) dtn & allDT (cutOnFmls {A}) dtn" (tacC8' notC8_1 (SOME notC8'')) ; val thC8_1 = notC8_1 ; val thC8'' = notC8'' ; val rules = [nota, nots] ; (* ; val prems = it ; *)