(* A formalisation for sequents.  This is NOT polymorphic, like Sequent.thy
   The lack of an atomic thing causes problems when we come to prove invertibility.
   Having all identity sequents as being derivable is not helpful. *) 
theory SequentDepth2
imports "/usr/local/Isabelle2007/src/HOL/Library/Multiset"
begin

datatype form = At "nat"
              | Compound "string" "form list"

datatype sequent = Sequent "form multiset" "form multiset" (" (_) \<Rightarrow>* (_)" [6,6] 5)

(* We have that any step in a rule, be it a primitive rule or an instance of a rule in a derivation
   can be represented as a list of premisses and a conclusion.  We need a list since a list is finite
   by definition *)
types rule = "sequent list * sequent"

types deriv = "sequent * nat"

abbreviation
multiset_plus (infixl "\<oplus>" 80) where
   "(\<Gamma> :: form multiset) \<oplus> (A :: form) \<equiv> \<Gamma> + {#A#}"
abbreviation
multiset_minus (infixl "\<ominus>" 80) where
   "(\<Gamma> :: form multiset) \<ominus>  (A :: form) \<equiv> \<Gamma> - {#A#}" 

consts
  (* extend a sequent by adding another one.  A form of weakening.  Is this overkill by adding a sequent? *)
  extend :: "sequent \<Rightarrow> sequent \<Rightarrow> sequent"
  extendRule :: "sequent \<Rightarrow> rule \<Rightarrow> rule"

  (* functions to get at components of sequents *)
  antec :: "sequent \<Rightarrow> form multiset"
  succ :: "sequent \<Rightarrow> form multiset"
  mset :: "sequent \<Rightarrow> form multiset"
  seq_size :: "sequent \<Rightarrow> nat"

  (* Unique conclusion Property *)
  uniqueConclusion :: "rule set \<Rightarrow> bool"

primrec antec_def : "antec (Sequent ant suc) = ant"
primrec succ_def : "succ (Sequent ant suc) = suc"
primrec mset_def : "mset (Sequent ant suc) = ant + suc"
primrec seq_size_def : "seq_size (Sequent ant suc) = size ant + size suc"

(* Extend a sequent, and then a rule by adding seq to all premisses and the conclusion *)
defs extend_def : "extend forms seq \<equiv> (antec forms + antec seq) \<Rightarrow>* (succ forms + succ seq)"
defs extendRule_def : "extendRule forms R \<equiv> (map (extend forms) (fst R), extend forms (snd R))"

(* The unique conclusion property.  A set of rules has unique conclusion property if for any pair of rules,
   the conclusions being the same means the rules are the same*)
defs uniqueConclusion_def : "uniqueConclusion R \<equiv> \<forall> r1 \<in> R. \<forall> r2 \<in> R. (snd r1 = snd r2) \<longrightarrow> (r1 =r2)"


(* The formulation of various rule sets *)

(* idRules is the set containing all identity RULES *)
inductive_set "idRules" where
   I[intro]: "([], {# At i #} \<Rightarrow>* {# At i #}) \<in> idRules"

(* scRules is the set of all rules which have a single conclusion.  This is akin to each rule having a 
   single principal formula.  We don't want rules to have no premisses, hence the restriction
   that ps \<noteq> [] *)
inductive_set "scRules" where
   I[intro]: "\<lbrakk> mset c \<equiv> {# Compound R Fs #} ; ps \<noteq> [] \<rbrakk> \<Longrightarrow> (ps,c) \<in> scRules"

(* Lemma which says these two sets are disjoint *)
lemma disjointRules:
assumes "r \<in> idRules" and "r \<in> scRules"
shows "False"
proof-
obtain Ps C where "r = (Ps,C)" by (cases r) auto
then have id:"(Ps,C) \<in> idRules" and sc:"(Ps,C) \<in> scRules" using assms by auto
from id have "Ps = []" by (cases) auto
moreover from sc have "Ps \<noteq> []" by (cases) auto
ultimately show ?thesis by auto
qed

inductive_set extRules :: "rule set \<Rightarrow> rule set"
  for R :: "rule set" 
  where
   I[intro]: "r \<in> R \<Longrightarrow> extendRule seq r \<in> extRules R"

(* A formulation of what it means to be a principal formula for a rule.  Note that we have to build up from
   single conclusion rules.   *)

inductive leftPrincipal :: "rule \<Rightarrow> form \<Rightarrow> bool"
  where
  sc[intro]: "C = ({#Compound F Fs#} \<Rightarrow>* {#})  \<Longrightarrow> 
                   leftPrincipal (Ps,C) (Compound F Fs)"


inductive rightPrincipal :: "rule \<Rightarrow> form \<Rightarrow> bool"
  where
  sc[intro]: "C = ({#} \<Rightarrow>* {#Compound F Fs#}) \<Longrightarrow> rightPrincipal (Ps,C) (Compound F Fs)"


(* What it means to be a derivable sequent.  Can have this as a predicate or as a set.
   The two formation rules say that the supplied premisses are derivable, and the second says
   that if all the premisses of some rule are derivable, then so is the conclusion. *)

inductive_set derivable :: "rule set \<Rightarrow> deriv set"
  for R :: "rule set"
  where
   base[intro]: "\<lbrakk>([],C) \<in> R\<rbrakk> \<Longrightarrow> (C,0) \<in> derivable R"
|  step[intro]: "\<lbrakk> r \<in> R ; (fst r)\<noteq>[] ; \<forall> p \<in> set (fst r). \<exists> n \<le> m. (p,n) \<in> derivable R \<rbrakk> 
                       \<Longrightarrow> (snd r,m + 1) \<in> derivable R"


(* Characterisation of a sequent *)
lemma characteriseSeq:
shows "\<exists> A B. (C :: sequent) = (A \<Rightarrow>* B)"
apply (rule_tac x="antec C" in exI, rule_tac x="succ C" in exI) by (cases C) (auto)


(* Helper function for later *)
lemma nonEmptySet:
shows "A \<noteq> [] \<longrightarrow> (\<exists> a. a \<in> set A)"
by (auto simp add:neq_Nil_conv)


(* Lemma which says that if we have extended an identity rule, then the propositional variable is
   contained in the extended multisets *)
lemma extendID:
assumes "extend S ({# At i #} \<Rightarrow>* {# At i #}) = (\<Gamma> \<Rightarrow>* \<Delta>)"
shows "At i :# \<Gamma> \<and> At i :# \<Delta>"
using assms
proof-
  from assms have "\<exists> \<Gamma>' \<Delta>'. \<Gamma> = \<Gamma>' \<oplus> At i \<and> \<Delta> = \<Delta>' \<oplus> At i" 
     using extend_def[where forms=S and seq="{# At i #} \<Rightarrow>* {# At i #}"]
     by (rule_tac x="antec S" in exI,rule_tac x="succ S" in exI) auto
  then show ?thesis by auto
qed


(* Lemma that says if a propositional variable is in both the antecedent and succedent of a sequent,
   then it is derivable from idscRules *)
lemma containID:
assumes a:"At i :# \<Gamma> \<and> At i :# \<Delta>"
    and b:"idRules \<subseteq> R"
shows "(\<Gamma> \<Rightarrow>* \<Delta>,0) \<in> derivable (extRules R)"
proof-
from a have "\<Gamma> = \<Gamma> \<ominus> At i \<oplus> At i \<and> \<Delta> = \<Delta> \<ominus> At i \<oplus> At i" using elem_imp_eq_diff_union by auto
then have "extend ((\<Gamma> \<ominus> At i) \<Rightarrow>* (\<Delta> \<ominus> At i)) ({# At i #} \<Rightarrow>* {# At i #}) = (\<Gamma> \<Rightarrow>* \<Delta>)" 
     using extend_def[where forms="\<Gamma> \<ominus> At i \<Rightarrow>* \<Delta> \<ominus> At i" and seq="{#At i#} \<Rightarrow>* {#At i#}"] by auto
moreover
have "([],{# At i #} \<Rightarrow>* {# At i #}) \<in> R" using b by auto
ultimately
have "([],\<Gamma> \<Rightarrow>* \<Delta>) \<in> extRules R" 
     using extRules.I[where R=R and r="([],  {#At i#} \<Rightarrow>* {#At i#})" and seq="\<Gamma> \<ominus> At i \<Rightarrow>* \<Delta> \<ominus> At i"] 
       and extendRule_def[where forms="\<Gamma> \<ominus> At i \<Rightarrow>* \<Delta> \<ominus> At i" and R="([],  {#At i#} \<Rightarrow>* {#At i#})"] by auto
then show ?thesis using derivable.base[where R="extRules R" and C="\<Gamma> \<Rightarrow>* \<Delta>"] by auto
qed


(* Lemma which says that if r is an identity rule, then r is of the form
   ([], P \<Rightarrow>* P) *)
lemma characteriseID:
assumes "r \<in> idRules"
shows "\<exists> i. r = ([], {# At i #} \<Rightarrow>* {# At i #})"
proof-
    obtain x y where "r = (x,y)" by (cases r)
    with `r \<in> idRules` have "(x,y) \<in> idRules" by simp
    then obtain i where "x=[]" and "y = ({# At i #} \<Rightarrow>* {# At i #})" by cases
    with `r= (x,y)` have "r = ([],{# At i #} \<Rightarrow>* {# At i #})" by simp
    then show "\<exists> i. r = ([],{# At i #} \<Rightarrow>* {# At i #})" by auto
qed


(* A lemma about the last rule used in a derivation, i.e. that one exists *)
lemma characteriseLast:
assumes "(C,m+1) \<in> derivable R"
shows "\<exists> Ps. Ps \<noteq> [] \<and>
             (Ps,C) \<in> R \<and> 
             (\<forall> p \<in> set Ps. \<exists> n\<le>m. (p,n) \<in> derivable R)"
using assms
proof (cases)
    case (base D)
    then show "\<exists> Ps. Ps \<noteq> [] \<and>
                     (Ps,C) \<in> R \<and> 
                     (\<forall> p \<in> set Ps. \<exists> n\<le>m. (p,n) \<in> derivable R)" using assms by simp
next
    case (step r n)
    then obtain Ps where "r = (Ps,C)" and "m=n" by (cases r) (auto)
    then have "fst r = Ps" and "snd r = C" by auto
    then show "\<exists> Ps. Ps \<noteq> [] \<and>
                     (Ps,C) \<in> R \<and> 
                     (\<forall> p \<in> set Ps. \<exists> n\<le>m. (p,n) \<in> derivable R)" 
         using `r \<in> R` and `m=n` and prems(5,6)
         by (rule_tac x=Ps in exI) (auto)
qed

(* Lemma which says that if rule is an scRule, then the succedent is either empty, or a single formula *)
lemma succ_scRule:
assumes "(Ps,\<Phi> \<Rightarrow>* \<Psi>) \<in> scRules"
shows "\<Psi> = {#} \<or> (\<exists> A. \<Psi> = {#A#})"
using assms 
proof (cases)
    case (I d R Rs ts)    
    then show "\<Psi> = {#} \<or> (\<exists> A. \<Psi> = {#A#})" using mset_def[where ant=\<Phi> and suc=\<Psi>] 
         and union_is_single[where M=\<Phi> and N=\<Psi> and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

(* Equivalent, but the antecedent *)
lemma antec_scRule:
assumes "(Ps,\<Phi> \<Rightarrow>* \<Psi>) \<in> scRules"
shows "\<Phi> = {#} \<or> (\<exists> A. \<Phi> = {#A#})"
using assms 
proof (cases)
    case (I d R Rs ts)    
    then show "\<Phi> = {#} \<or> (\<exists> A. \<Phi> = {#A#})" using mset_def[where ant=\<Phi> and suc=\<Psi>] 
         and union_is_single[where M=\<Phi> and N=\<Psi> and a="Compound R Rs"] by (simp,elim disjE) (auto)
qed

lemma scRule_Size:
assumes "r \<in> scRules"
shows "seq_size (snd r) = 1"
using assms
proof-
    obtain Ps C where "r = (Ps,C)" by (cases r)
    then have "(Ps,C) \<in> scRules" using assms by simp
    then show ?thesis
       proof (cases)
          case (I D R Rs Ts)
          obtain G H where "D = (G \<Rightarrow>* H)" by (cases D) (auto)
          then have "G + H = {#Compound R Rs#}" using mset_def and `mset D \<equiv> {#Compound R Rs#}` by auto
          then have "size (G+H) = 1" by auto 
          then have "size G + size H = 1" by auto
          then have "seq_size D = 1" using seq_size_def[where ant=G and suc=H] and `D = (G \<Rightarrow>* H)` by auto
          moreover have "snd r = D" using `r = (Ps,C)` and `C=D` by simp
          ultimately show "seq_size (snd r) = 1" by simp
       qed
qed

lemma scRuleCharacterise:
assumes "(Ps,C) \<in> scRules"
shows "\<exists> F Fs. C = ({#} \<Rightarrow>* {#Compound F Fs#}) \<or> C = ({#Compound F Fs#} \<Rightarrow>* {#})"
using assms
proof (cases)
case (I c F Fs Ps)
then obtain \<Gamma> \<Delta> where "c = (\<Gamma> \<Rightarrow>* \<Delta>)" using characteriseSeq[where C=c] by auto
then have "(Ps,\<Gamma> \<Rightarrow>* \<Delta>) \<in> scRules" using prems by simp
then have "\<exists> F Fs. c = ({#} \<Rightarrow>* {#Compound F Fs#}) \<or> c = ({#Compound F Fs#} \<Rightarrow>* {#})" 
     using `mset c \<equiv> {#Compound F Fs#}` and `c= (\<Gamma> \<Rightarrow>* \<Delta>)`
     and mset_def[where ant=\<Gamma> and suc=\<Delta>] and union_is_single[where M=\<Gamma> and N=\<Delta> and a="Compound F Fs"]
     by auto
thus ?thesis using `C=c` by simp
qed

lemma scExtend:
assumes "r \<in> scRules"
   and "extendRule S r \<in> scRules"
shows "S = ({#} \<Rightarrow>* {#})"
using assms
proof-
obtain \<Gamma> \<Delta> where "S = (\<Gamma> \<Rightarrow>* \<Delta>)" using characteriseSeq[where C=S] by auto
obtain Ps C where "r = (Ps,C)" by (cases r) (auto)
then have "extendRule S r = (map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps, extend S C)"
     using `S = (\<Gamma> \<Rightarrow>* \<Delta>)` and extendRule_def[where forms=S and R="(Ps,C)"] by auto
then have "(map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps, extend S C) \<in> scRules" using `extendRule S r \<in> scRules` by auto
from `r = (Ps,C)` obtain F Fs where "C = ({#} \<Rightarrow>* {#Compound F Fs#}) \<or> C = ({#Compound F Fs#} \<Rightarrow>* {#})" using `r \<in> scRules`
     and scRuleCharacterise[where Ps=Ps and C=C] by auto
moreover
     {assume "C = ({#} \<Rightarrow>* {#Compound F Fs#})"
      then have "extend S C = (\<Gamma> \<Rightarrow>* \<Delta> \<oplus> Compound F Fs)"
           using `S = (\<Gamma> \<Rightarrow>* \<Delta>)` and extend_def[where forms=S and seq=C] by auto
      then have "(map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps, \<Gamma> \<Rightarrow>* \<Delta> \<oplus> Compound F Fs) \<in> scRules"
           using `(map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps, extend S C) \<in> scRules` by auto
      then obtain T Ts where "(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> Compound F Fs) = ({#} \<Rightarrow>* {#Compound T Ts#})
                           \<or>  (\<Gamma> \<Rightarrow>* \<Delta> \<oplus> Compound F Fs) = ({#Compound T Ts#} \<Rightarrow>* {#})"
           using scRuleCharacterise[where Ps="map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps" and C="\<Gamma> \<Rightarrow>* \<Delta> \<oplus> Compound F Fs"] by auto
           moreover
           {assume eq:"(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> Compound F Fs) = ({#} \<Rightarrow>* {#Compound T Ts#})"
            then have "\<Delta> \<oplus> Compound F Fs = {#Compound T Ts#}" by auto
            then have "F=T" and "Fs = Ts" and "\<Delta> = {#}" by (auto simp add:union_is_single)
            moreover from eq have "\<Gamma> = {#}" by auto
            ultimately have "S = ({#} \<Rightarrow>* {#})" using `S = (\<Gamma> \<Rightarrow>* \<Delta>)` by simp
           }
           moreover
           {assume eq:"(\<Gamma> \<Rightarrow>* \<Delta> \<oplus> Compound F Fs) = ({#Compound T Ts#} \<Rightarrow>* {#})"
            then have "\<Delta> \<oplus> Compound F Fs = {#}" by auto
            then have "S = ({#} \<Rightarrow>* {#})" by auto
           }
           ultimately have "S = ({#} \<Rightarrow>* {#})" by blast
     }
moreover
     {assume "C = ({#Compound F Fs#} \<Rightarrow>* {#})"
      then have "extend S C = (\<Gamma> \<oplus> Compound F Fs \<Rightarrow>* \<Delta>)"
           using `S = (\<Gamma> \<Rightarrow>* \<Delta>)` and extend_def[where forms=S and seq=C] by auto
      then have "(map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps, \<Gamma> \<oplus> Compound F Fs \<Rightarrow>* \<Delta>) \<in> scRules"
           using `(map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps, extend S C) \<in> scRules` by auto
      then obtain T Ts where "(\<Gamma> \<oplus> Compound F Fs \<Rightarrow>* \<Delta>) = ({#} \<Rightarrow>* {#Compound T Ts#})
                           \<or>  (\<Gamma> \<oplus> Compound F Fs \<Rightarrow>* \<Delta>) = ({#Compound T Ts#} \<Rightarrow>* {#})"
           using scRuleCharacterise[where Ps="map (extend (\<Gamma> \<Rightarrow>* \<Delta>)) Ps" and C="\<Gamma> \<oplus> Compound F Fs \<Rightarrow>* \<Delta>"] by auto
           moreover
           {assume eq:"(\<Gamma> \<oplus> Compound F Fs \<Rightarrow>* \<Delta>) = ({#} \<Rightarrow>* {#Compound T Ts#})"
            then have "S = ({#} \<Rightarrow>* {#})" by auto
           }
           moreover
           {assume eq:"(\<Gamma> \<oplus> Compound F Fs \<Rightarrow>* \<Delta>) = ({#Compound T Ts#} \<Rightarrow>* {#})"
            then have "\<Gamma> \<oplus> Compound F Fs = {#Compound T Ts#}" by auto
            then have "\<Gamma> = {#}" by (auto simp add:union_is_single)
            moreover from eq have "\<Delta> = {#}" by auto
            ultimately have "S = ({#} \<Rightarrow>* {#})" using `S = (\<Gamma> \<Rightarrow>* \<Delta>)` by auto
           }
           ultimately have "S = ({#} \<Rightarrow>* {#})" by blast
     }
ultimately show "S = ({#} \<Rightarrow>* {#})" by blast
qed

lemma extendEmpty:
shows "extend ({#} \<Rightarrow>* {#}) C = C"
apply (auto simp add:extend_def) by (cases C) auto



lemma extendContain:
assumes "r = (ps,c)"
    and "(Ps,C) = extendRule S r"
    and "p \<in> set ps"
shows "extend S p \<in> set Ps"
proof-
from `p \<in> set ps` have "extend S p \<in> set (map (extend S) ps)" by auto
moreover from `(Ps,C) = extendRule S r` and `r = (ps,c)` have "map (extend S) ps = Ps" by (simp add:extendRule_def) 
ultimately show ?thesis by auto
qed

end