theory ctr imports seq gstep begin consts ctr_adm_prop :: "'a sequent set => 'a => 'a sequent => bool" ctr_adm_step1 :: "'a sequent set => 'a sequent psc => 'a sequent => bool" ctr_adm_step :: "('a * 'a) set => 'a sequent set => 'a sequent psc => 'a => bool" ctr_adm_seq :: "'a sequent set => 'a sequent => 'a sequent => bool" ctr_adm :: "'a sequent psc set => 'a => bool" ctr_admd :: "'a sequent set => 'a => bool" ctr_adm_antec :: "'a sequent psc set => 'a => bool" ctr_admd_antec :: "'a sequent set => 'a => bool" wk_adm :: "'a sequent psc set => bool" wk_adm_antec :: "'a sequent psc set => bool" wk_adm_succ :: "'a sequent psc set => bool" wk_adm_single_antec :: "'a sequent psc set => bool" wk_adm_single_succ :: "'a sequent psc set => bool" id_adm :: "'a sequent psc set => bool" id_decomp :: "'a sequent psc set => bool" id_decompi :: "'a sequent psc set => 'a sequent psc set => bool" inv_step :: "'a set => 'a psc set => 'a psc => bool" inv_stepm :: "'a psc set => 'a psc set => 'a psc => bool" invs_of :: "'a psc set => 'a => 'a set" mod_inv_rl :: "'a sequent psc set => ('a => bool) => 'a sequent psc => bool" mod_inv_rlg :: "'a sequent set => ('a => bool) => 'a sequent psc => bool" mod_inv_prop :: "'a set => 'a psc set => ('a => 'a) => 'a => bool" mod_inv_step :: "'a sequent set => 'a sequent psc set => ('a => bool) => 'a sequent psc => bool" inv_rl :: "'a psc set => 'a psc => bool" inv_rlg :: "'a set => 'a psc => bool" (* unlike inv_rl, do this as an inductively defined set *) mul_inv_rl :: "'a :: comm_monoid_add psc set => 'a psc set" multiples :: "'a :: comm_monoid_add psc set => 'a psc set" subfml_prop :: "('a * 'a) set => 'a sequent psc => bool" subfml_cp_prop :: "('a * 'a) set => 'a sequent psc => bool" ext_concl :: "'a sequent psc set => bool" ext_concl_rl :: "'a sequent psc set => 'a sequent psc => bool" comm_rules :: "'a psc => 'a psc => 'a psc set => 'a psc set => bool" commg_rules :: "'a psc => 'a psc => 'a psc set => 'a psc set => bool" etr :: "'a sequent => 'a sequent => 'a sequent => 'a sequent" trf_rls :: "('a => 'a) => 'a psc set" defs (* rules commuting, generalised form *) commg_rules_def : "commg_rules srl irl srls irls == ALL c ps ips xc. (ps, c) = srl --> (ips, c) = irl --> xc : set ips --> (EX xps. xc : derrec srls xps & (ALL xp : xps. (EX (yps, yc) : irls. xp : set yps & yc : set ps)))" comm_rules_def : "comm_rules srl irl srls irls == ALL c ps ips xc. (ps, c) = srl --> (ips, c) = irl --> xc : set ips --> (EX xps. (xps, xc) : srls & (ALL xp : set xps. (EX (yps, yc) : irls. xp : set yps & yc : set ps)))" (* contraction admissibility for a particular sequent *) ctr_adm_seq_def : "ctr_adm_seq derivs seq As == seq : derivs --> As + As <= seq --> seq - As : derivs" (* contraction admissibility for formula A ; if A,A,X |- Y is derivable, then so is A,X |- Y, and similarly *) ctr_admd_def : "ctr_admd derivs A == ALL As. ms_of_seq As = {#A#} --> (ALL XY. ctr_adm_seq derivs XY As)" ctr_adm_def' : "ctr_adm rls A == ctr_admd (derrec rls {}) A" (* ctr_adm_def : "ctr_adm rls A == ALL As. ms_of_seq As = {#A#} --> (ALL XY. XY : derrec rls {} --> As + As <= XY --> XY - As : derrec rls {})" *) (* contraction admissibility on the left for formula A ; if A,A,X |- Y is derivable, then so is A,X |- Y, and similarly *) ctr_admd_antec_def : "ctr_admd_antec derivs A == (ALL XY. ctr_adm_seq derivs XY ({#A#} |- 0))" ctr_adm_antec_def' : "ctr_adm_antec rls A == ctr_admd_antec (derrec rls {}) A" (* ctr_adm_antec_def : "ctr_adm_antec rls A == (ALL XY. XY : derrec rls {} --> ({#A#} + {#A#} |- 0) <= XY --> XY - ({#A#} |- 0) : derrec rls {})" *) (* can extend conclusions : suffices for admissibility of weakening *) primrec "ext_concl_rl rls (ps, c) = (ALL A. EX ps'. (ps', c + A) : rls & (ps, ps') : allrel {(p, p'). p' >= p})" defs ext_concl_def' : "ext_concl rls == ALL (ps, c) : rls. ext_concl_rl rls (ps, c)" (* admissibility of weakened axiom *) id_adm_def : "id_adm rls == ALL A X Y. A :# X --> A :# Y --> (X |- Y) : derrec rls {}" (* admissibility of weakening *) wk_adm_def : "wk_adm rls == ALL XY. XY : derrec rls {} --> (ALL As. XY + As : derrec rls {})" (* weakening only on the left/right *) wk_adm_antec_def : "wk_adm_antec rls == ALL XY. XY : derrec rls {} --> (ALL As. succ As = {#} --> XY + As : derrec rls {})" wk_adm_succ_def : "wk_adm_succ rls == ALL XY. XY : derrec rls {} --> (ALL As. antec As = {#} --> XY + As : derrec rls {})" wk_adm_single_antec_def : "wk_adm_single_antec rls == ALL XY. XY : derrec rls {} --> (ALL A. XY + ({#A#} |- {#}) : derrec rls {})" wk_adm_single_succ_def : "wk_adm_single_succ rls == ALL XY. XY : derrec rls {} --> (ALL A. XY + ({#} |- {#A#}) : derrec rls {})" (* identity decomposition property, key property for invertibility : any rule whose conclusion is the identity axiom has derivable premises *) id_decomp_def : "id_decomp rls == ALL A ps. (ps, {#A#} |- {#A#}) : rls --> set ps <= derrec rls {}" (* variant where we don't want to invert all rules, just those in irls *) id_decompi_def : "id_decompi irls rls == ALL A ps. (ps, {#A#} |- {#A#}) : irls --> set ps <= derrec rls {}" primrec (* version of subformula property: principal formula allowed in premise, on the same side only, and all other formulae must be smaller *) subfml_prop_def : "subfml_prop sub (ps, c) = (ALL p : set ps. (ALL fp. ms_mem fp (p - c) --> (EX fc. ms_mem fc c & (fp, fc) : sub)))" primrec (* first branch: the principal formula(e) is copied into the premise; second branch is subformula property of a rule, ie every formula in a premise is a subformula of a formula in the conclusion ; first branch is exceptional (premise containing conclusion) *) subfml_cp_prop_def : "subfml_cp_prop sub (ps, c) = (ALL p : set ps. c <= p | (ALL fp. ms_mem fp p --> (EX fc. ms_mem fc c & (fp, fc) : sub)))" primrec (* invertibility of a rule, in a set of rules *) defn : "inv_rl rls (ps, c) = (c : derrec rls {} --> ps : dersrec rls {})" inductive "mul_inv_rl rls" intros (* invertibility of a rule, multiple times, in a set of rules *) I : "!n. times n c : derrec rls {} --> map (times n) ps : dersrec rls {} ==> (ps, c) : mul_inv_rl rls" inductive "multiples rls" intros (* multiples of a rule *) I : "psc : rls ==> pscmap (times n) psc : multiples rls" primrec (* invertibility of a rule, more generalised *) defn : "inv_rlg derivs (ps, c) = (c : derivs --> set ps <= derivs)" primrec (* modified version of invertibility of a rule, in a set of rules *) defn : "mod_inv_rlg derivs p (ps, c) = (c : derivs --> set ps <= derivs | seq_filter p c : derivs)" primrec (* modified version of invertibility of a rule, in a set of rules *) defn : "mod_inv_rl rls p (ps, c) = mod_inv_rlg (derrec rls {}) p (ps, c)" inductive "invs_of irls seq" intros I : "p : set ps ==> (ps, seq) : irls ==> p : invs_of irls seq" primrec (* step in invertibility ; means that, if premises (ps) derivable, and can apply (invs_of irls) to premises, then can apply (invs_of irls) to conclusion (concl) *) "inv_step derivs irls (ps, concl) = (set ps <= derivs --> (ALL p : set ps. invs_of irls p <= derivs) --> invs_of irls concl <= derivs)" primrec (* variation on inv_step which will often be true and monotonic, whereby the inversions of the conclusion are derivable from the inversions of the premises *) "inv_stepm drls irls (ps, concl) = (invs_of irls concl <= derrec drls (set ps Un UNION (set ps) (invs_of irls)))" defs (* step in modified invertibility *) mod_inv_prop_def : "mod_inv_prop derivs irls f seq == invs_of irls seq <= derivs | f seq : derivs" primrec (* step in modified invertibility *) "mod_inv_step derivs irls f (ps, concl) = (set ps <= derivs --> (ALL p : set ps. mod_inv_prop derivs irls (seq_filter f) p) --> mod_inv_prop derivs irls (seq_filter f) concl)" defs etr_def : "etr M D XY == M + seq_delete D XY" inductive "trf_rls f" intros I : "([p], f p) : trf_rls f" constdefs gsf :: "'a sequent psc set => ('a sequent => 'a sequent) => 'a => 'a sequent psc => bool" "gsf rls cf A == gen_step (%A x. cf x : derrec rls {}) A {} (derrec rls {})" constdefs gsfg :: "'a sequent psc set => 'a sequent psc set => ('a sequent => 'a sequent) => 'a => 'a sequent psc => bool" "gsfg prls drls cf A == gen_step (%A x. cf x : derrec prls {}) A {} (derrec drls {})" constdefs gsfg_ps :: "'a sequent set => 'a sequent psc set => 'a sequent psc set => ('a sequent => 'a sequent) => 'a => 'a sequent psc => bool" "gsfg_ps ps prls drls cf A == gen_step (%A x. cf x : derrec prls (cf ` ps)) A {} (derrec drls ps)" (* step in contraction admissibility *) primrec "ctr_adm_step1 derivs (ps, concl) As = ((ALL p : set ps. p : derivs & (As + As <= p --> p - As : derivs)) --> As + As <= concl --> concl - As : derivs)" (* primrec "ctr_adm_step sub derivs (ps, concl) A = (ALL As. ms_of_seq As = {#A#} --> (ALL A'. (A', A) : sub --> ctr_admd derivs A') --> (ALL p : set ps. p : derivs & (As + As <= p --> p - As : derivs)) --> As + As <= concl --> concl - As : derivs)" *) defs ctr_adm_step_def : "ctr_adm_step sub derivs rl A == ALL As. ms_of_seq As = {#A#} --> (ALL A'. (A', A) : sub --> ctr_admd derivs A') --> ctr_adm_step1 derivs rl As" defs (* suitable for P in gen_step_def *) ctr_adm_prop_def : "ctr_adm_prop derivs A seq == ALL As. ms_of_seq As = {#A#} --> As + As <= seq --> seq - As : derivs" end