(* now in C8cases.thy
use "orC8.ML" ;
use "rsC8.ML" ;
use "andC8.ML" ;
use "compC8.ML" ;
use "unC8.ML" ;
use "conC8.ML" ;
*)
(* now we have theorems showing that a tree with a single left-right-principal
cut on a particular formula can be replaced by a tree with cuts on
the subformulae of that formula (this is Belnap's condition C8);
these theorems are converted to the theorems (map mkthC8E thsC8') e.g.
"canElimAll (cutOnFmls {?B, ?A}) ==> canElim (cutIsLRP (?B oo ?A))"
Using the previous results we get thC8Es, e.g.
"canElimAll (cutOnFmls {?B, ?A}) ==> canElim (cutOnFmls {?B oo ?A})"
We then use the result elimFmls with twoElim and trivElim to get
the theorems elimFmlRecs, e.g.
"[| canElim (cutOnFmls {?A}); canElim (cutOnFmls {?B}) |]
==> canElim (cutOnFmls {?B oo ?A})"
The theorems elimFmlRecs are then used in a proof by induction on the
structure of a formula to prove
canElimFml = "canElim (cutOnFmls {?fml})", then
canElimAny = "canElim (cutOnFmls UNIV)", and then, using elimFmls,
canElimAll = "canElimAll (cutOnFmls UNIV)"
Finally we convert canElimAll into
cutElim =
"IsDerivableR rls {} ?concl ==> IsDerivableR (rls - {cutr}) {} ?concl"
*)
val thsC8' = [orC8', rsC8', andC8', compC8', notC8', convC8'] ;
(* thsC8 theorems are a simplified version of the thsC8' theorems,
where the premise allNextDTs (cutOnFmls {?B, ?A}) ?dt is
replaced by allNextDTs (cutOnFmls {}) ?dt, which is all we actually need *)
val[orC8, rsC8, andC8, compC8, notC8, convC8] = [andcfem] RLN (4, thsC8') ;
val thsC8 = [orC8, rsC8, andC8, compC8, notC8, convC8,
tC8, fC8, r0C8, r1C8, FVC8, PPC8] ;
fun mkthC8E thC8 = prove_goalw HOL_ElimC8.thy
[canElim_def, canElimAll_def]
"canElimAll (cutOnFmls ?sAB) --> canElim (cutIsLRP ?AcB)"
(tacCE thC8) RS mp ;
val thC8Es' = map mkthC8E thsC8 ;
val thC8Es = thC8Es' RL [th8] ;
val fmlths = [twoElim RS elimFmls, trivElim RS elimFmls] ;
val tac = (resolve_tac fmlths 1) ORELSE rtac elimFmls 1 ;
val elimFmlRecs = map (tacthm tac) thC8Es ;
val canElimFml = prove_goal HOL_ElimC8.thy
"canElim (cutOnFmls {fml})"
(fn _ => [ (induct_tac "fml" 1),
(REPEAT ((resolve_tac elimFmlRecs THEN_ALL_NEW atac) 1))]) ;
val canElimAny = prove_goalw HOL_ElimC8.thy [mk_meta_eq cutOnFmls_UNIV]
"canElim (cutOnFmls UNIV)"
(fn _ => [ (fold_goals_tac [mk_meta_eq canElim_ex]),
rtac allI 1, rtac canElimFml 1]) ;
val canElimAll = canElimAny RS elimFmls ;
val cutElim' = meta_std (prove_goal HOL_ElimC8.thy
"premsDT dt = [] & allDT wfb dt & allDT (frb rls) dt --> \
\ (EX dt'. conclDT dt' = conclDT dt & \
\ premsDT dt' = [] & allDT wfb dt' & allDT (frb (rls - {cutr})) dt')"
(fn _ => [ (cut_facts_tac [rewrite_rule [canElimAll_def] canElimAll] 1),
rtac impI 1, etac allE 1, etac impE 1,
(fast_tac (claset () addSEs [noPremsD]) 1),
(fast_tac (claset () addSEs [cfpt, ex_match, noPremsI]) 1)] )) ;
val cutElim = prove_goalw HOL_ElimC8.thy [IsDerivableR_def]
"IsDerivableR rls {} concl --> IsDerivableR (rls - {cutr}) {} concl"
(fn _ => [ Safe_tac, Full_simp_tac 1,
(datac cutElim' 2 1), Fast_tac 1]) RS mp ;
(*
; val prems = it ;
*)