src/Sequents/ILL.thy

optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
saves 2 sec per Sledgehammer invocation on my laptop!

(*  Title:      Sequents/ILL.thy
    Author:     Sara Kalvala and Valeria de Paiva
    Copyright   1995  University of Cambridge
*)

theory ILL
imports Sequents
begin

consts
  Trueprop       :: "two_seqi"

  tens :: "[o, o] => o"        (infixr "><" 35)
  limp :: "[o, o] => o"        (infixr "-o" 45)
  liff :: "[o, o] => o"        (infixr "o-o" 45)
  FShriek :: "o => o"          ("! _" [100] 1000)
  lconj :: "[o, o] => o"       (infixr "&&" 35)
  ldisj :: "[o, o] => o"       (infixr "++" 35)
  zero :: "o"                  ("0")
  top :: "o"                   ("1")
  eye :: "o"                   ("I")
  aneg :: "o=>o"               ("~_")


  (* context manipulation *)

 Context      :: "two_seqi"

  (* promotion rule *)

  PromAux :: "three_seqi"

syntax
  "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
  "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
  "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")

parse_translation {*
  [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
   (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
   (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
*}

print_translation {*
  [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
   (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
   (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
*}

defs

liff_def:        "P o-o Q == (P -o Q) >< (Q -o P)"

aneg_def:        "~A == A -o 0"


axioms

identity:        "P |- P"

zerol:           "$G, 0, $H |- A"

  (* RULES THAT DO NOT DIVIDE CONTEXT *)

derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C"
  (* unfortunately, this one removes !A  *)

contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"

weaken:     "$F, $G |- C ==> $G, !A, $F |- C"
  (* weak form of weakening, in practice just to clean context *)
  (* weaken and contract not needed (CHECK)  *)

promote2:        "promaux{ || $H || B} ==> $H |- !B"
promote1:        "promaux{!A, $G || $H || B}
                  ==> promaux {$G || $H, !A || B}"
promote0:        "$G |- A ==> promaux {$G || || A}"



tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"

impr:      "A, $F |- B ==> $F |- A -o B"

conjr:           "[| $F |- A ;
                 $F |- B |]
                ==> $F |- (A && B)"

conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C"

conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C"

disjrl:          "$G |- A ==> $G |- A ++ B"
disjrr:          "$G |- B ==> $G |- A ++ B"
disjl:           "[| $G, A, $H |- C ;
                     $G, B, $H |- C |]
                 ==> $G, A ++ B, $H |- C"


      (* RULES THAT DIVIDE CONTEXT *)

tensr:           "[| $F, $J :=: $G;
                     $F |- A ;
                     $J |- B     |]
                     ==> $G |- A >< B"

impl:            "[| $G, $F :=: $J, $H ;
                     B, $F |- C ;
                        $G |- A |]
                     ==> $J, A -o B, $H |- C"


cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
          $H1, $H2, $H3, $H4 |- A ;
          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B"


  (* CONTEXT RULES *)

context1:     "$G :=: $G"
context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G"
context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G"
context5:     "$F, $G :=: $H ==> $G, $F :=: $H"


ML {*

val lazy_cs = empty_pack
  add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0",
    thm "context2", thm "context3"]
  add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr",
    thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl",
    thm "derelict", thm "weaken", thm "promote1", thm "promote2",
    thm "context1", thm "context4a", thm "context4b"];

local
  val promote0 = thm "promote0"
  val promote1 = thm "promote1"
  val promote2 = thm "promote2"
in

fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)

end
*}

method_setup best_lazy =
  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
  "lazy classical reasoning"

lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
  apply (rule derelict)
  apply (rule impl)
  apply (rule_tac [2] identity)
  apply (rule context1)
  apply assumption
  done

lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
  apply (rule contract)
  apply (rule_tac A = " (!A) >< (!B) " in cut)
  apply (rule_tac [2] tensr)
  prefer 3
  apply (subgoal_tac "! (A && B) |- !A")
  apply assumption
  apply best_lazy
  prefer 3
  apply (subgoal_tac "! (A && B) |- !B")
  apply assumption
  apply best_lazy
  apply (rule_tac [2] context1)
  apply (rule_tac [2] tensl)
  prefer 2 apply (assumption)
  apply (rule context3)
  apply (rule context3)
  apply (rule context1)
  done

lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"
  apply (rule impr)
  apply (rule contract)
  apply assumption
  done

lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"
  apply (rule impr)
  apply (rule contract)
  apply (rule derelict)
  apply assumption
  done

lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
  apply (rule impl)
  apply (rule_tac [3] identity)
  apply (rule context3)
  apply (rule context1)
  apply (rule zerol)
  done


lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
  apply (rule impl)
  apply (rule_tac [3] identity)
  apply (rule context3)
  apply (rule context1)
  apply (rule zerol)
  done

lemma ll_mp: "A -o B, A |- B"
  apply (rule impl)
  apply (rule_tac [2] identity)
  apply (rule_tac [2] identity)
  apply (rule context1)
  done

lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
  apply (rule_tac A = "B" in cut)
  apply (rule_tac [2] ll_mp)
  prefer 2 apply (assumption)
  apply (rule context3)
  apply (rule context3)
  apply (rule context1)
  done

lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
  apply (rule_tac A = "B" in cut)
  apply (rule_tac [2] ll_mp)
  prefer 2 apply (assumption)
  apply (rule context3)
  apply (rule context3)
  apply (rule context1)
  done

lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
  by best_lazy

lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>  
          $F, !((!(A ++ B)) -o 0), $G |- C"
  apply (rule cut)
  apply (rule_tac [2] or_to_and)
  prefer 2 apply (assumption)
  apply (rule context3)
  apply (rule context1)
  done

lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
  apply (rule impr)
  apply (rule conj_lemma)
  apply (rule disjl)
  apply (rule mp_rule1, best_lazy)+
  done

lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
  by best_lazy

lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
  apply (rule impr)
  apply (rule contract)
  apply (rule impl)
  apply (rule_tac [3] identity)
  apply (rule context1)
  apply best_lazy
  done

lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
  apply (rule_tac A = "!A -o 0" in cut)
  apply (rule_tac [2] a_not_a)
  prefer 2 apply (assumption)
  apply best_lazy
  done

ML {*

val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",
                                 thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",
                                 thm "a_not_a_rule"]
                      add_unsafes [thm "aux_impl"];

val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
*}


method_setup best_safe =
  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""

method_setup best_power =
  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""


(* Some examples from Troelstra and van Dalen *)

lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
  by best_safe

lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
  by best_safe

lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
        (!A) -o ( (!  ((!B) -o 0)) -o 0)"
  by best_safe

lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |-
          (!((! ((!A) -o B) ) -o 0)) -o 0"
  by best_power

end