(* A formalisation for sequents, First-Order *) 
theory SequentDepthNominal
imports "/usr/local/Isabelle2007/src/HOL/Library/Multiset" "/usr/local/Isabelle2007/src/HOL/Nominal/Nominal"
begin

atom_decl var


nominal_datatype form = At "nat" "var list" 
                      | Cpd0 "string" "form_list"
                      | Cpd1 "string" "\<guillemotleft>var\<guillemotright>form" ("_ (\<nabla> [_]._)" [100,100,100]100)
and form_list = FNil
              | FCons "form" "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"
  set_of_seq :: "sequent \<Rightarrow> form set"
  set_of_prem :: "sequent list \<Rightarrow> form set"
  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"
primrec set_of_seq_def: "set_of_seq (Sequent ant suc) = set_of (mset (Sequent ant suc))"
primrec (set_of_prem)
   "set_of_prem Nil = {}"
   "set_of_prem (p # ps) = set_of_seq p \<union> set_of_prem ps"

(* 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)"


consts sequentMinus :: "sequent \<Rightarrow> form \<Rightarrow> sequent" ("_ - _" [100,100]100)
primrec "(\<Gamma> \<Rightarrow>* \<Delta>) - A = (\<Gamma> \<ominus> A \<Rightarrow>* \<Delta> \<ominus> A)"

consts listMinus :: "sequent list \<Rightarrow> form \<Rightarrow> sequent list" (" _ - _ " [100,100]100)
primrec "[] - A = []"
        "(P # Ps) - A = (P - A) # (Ps - A)"


(* The formulation of various rule sets *)

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

(* propRules 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 "propRules" where
   I[intro]: "\<lbrakk> mset c \<equiv> {# Cpd0 R Fs #} ; ps \<noteq> [] \<rbrakk> \<Longrightarrow> (ps,c) \<in> propRules"

(* provRules is the set of rules where we have a freshness proviso *)
inductive_set "provRules" where
   I[intro]: "\<lbrakk> mset c = {# F \<nabla> [x].A #} ; ps \<noteq> [] ; x \<sharp> set_of_prem (ps - A)\<rbrakk>
                      \<Longrightarrow> (ps,c) \<in> provRules"

(* nprovRules is the set of rules where we do not have a freshness proviso, but we have
   a first order formula *)
inductive_set "nprovRules" where
   I[intro]: "\<lbrakk> mset c = {# F \<nabla> [x].A #} ; ps \<noteq> [] \<rbrakk>
                   \<Longrightarrow> (ps,c) \<in> nprovRules"

(* provRules are a subset of nprovRules *)
lemma nprovContain:
shows "provRules \<subseteq> nprovRules"
proof-
{fix ps c
 assume "(ps,c) \<in> provRules"
 then have "(ps,c) \<in> nprovRules" by (cases) auto
}
then show ?thesis by auto
qed

consts 
  subst :: "var \<Rightarrow> var \<Rightarrow> 'a \<Rightarrow> 'a" ("[_,_]_" [100,100,100] 100)

primrec (subst_list)
   Empt:"[z,y][] = []"
   NEmpt:"[z,y](x#ys) = (if x=y then (z#([z,y]ys)) else (x#([z,y]ys)))"

lemma subst_var_list_eqvt[eqvt]:
  fixes pi::"var prm"
  and   y::"var list"
  shows "pi\<bullet>([z,x]y) = [(pi\<bullet>z),(pi\<bullet>x)](pi\<bullet>y)"
by (induct y) (auto simp add: eqvts)

nominal_primrec (subst_form)
  "[z,y](At P xs) = At P ([z,y]xs)"
  "x\<sharp>(z,y) \<Longrightarrow> [z,y](F \<nabla> [x].A) = F \<nabla> [x].([z,y]A)"
  "[z,y](Cpd0 F Fs) = Cpd0 F ([z,y]Fs)"
  "[z,y]FNil = FNil"
  "[z,y](FCons f Fs) = FCons ([z,y]f) ([z,y]Fs)"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)+
apply(fresh_guess add: fresh_string)+
done

constdefs multSubst :: "form multiset \<Rightarrow> bool"
multSubst_def: "multSubst \<Gamma> \<equiv> (\<exists> A \<in> (set_of \<Gamma>). \<exists> x y B. [y,x]B = A \<and> y\<noteq>x)"

(* We need to be careful now about how to extend a rule, since we have binding *)
inductive_set extRules :: "rule set \<Rightarrow> rule set"   (" _*" )
   for R :: "rule set"
   where
     id[intro]: "\<lbrakk> r \<in> R ; r \<in> idRules \<rbrakk> \<Longrightarrow> extendRule S r \<in> R*"
|    sc[intro]: "\<lbrakk> r \<in> R ; r \<in> propRules \<rbrakk> \<Longrightarrow> extendRule S r \<in> R*"
|    np[intro]: "\<lbrakk> r \<in> R ; r \<in> nprovRules \<rbrakk> \<Longrightarrow> extendRule S r \<in> R*"
|     p[intro]: "\<lbrakk> (ps,c) \<in> R ; (ps,c) \<in> provRules ; mset c = {# F \<nabla> [x].A #} ; x \<sharp> set_of_seq S \<rbrakk>
                          \<Longrightarrow> extendRule S (ps,c) \<in> 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 = ({#A#} \<Rightarrow>* {#})  \<Longrightarrow> 
                   leftPrincipal (Ps,C) A"


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


(* 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 xs #} \<Rightarrow>* {# At i xs #}) = (\<Gamma> \<Rightarrow>* \<Delta>)"
shows "At i xs :# \<Gamma> \<and> At i xs :# \<Delta>"
using assms
proof-
  from assms have "\<exists> \<Gamma>' \<Delta>'. \<Gamma> = \<Gamma>' \<oplus> At i xs \<and> \<Delta> = \<Delta>' \<oplus> At i xs" 
     using extend_def[where forms=S and seq="{# At i xs #} \<Rightarrow>* {# At i xs #}"]
     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 xs :# \<Gamma> \<and> At i xs :# \<Delta>"
    and b:"idRules \<subseteq> R"
shows "(\<Gamma> \<Rightarrow>* \<Delta>,0) \<in> derivable R*"
proof-
from a have "\<Gamma> = \<Gamma> \<ominus> At i xs \<oplus> At i xs \<and> \<Delta> = \<Delta> \<ominus> At i xs \<oplus> At i xs" using elem_imp_eq_diff_union by auto
then have "extend ((\<Gamma> \<ominus> At i xs) \<Rightarrow>* (\<Delta> \<ominus> At i xs)) ({# At i xs #} \<Rightarrow>* {# At i xs #}) = (\<Gamma> \<Rightarrow>* \<Delta>)" 
     using extend_def[where forms="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs" and seq="{#At i xs#} \<Rightarrow>* {#At i xs#}"] by auto
moreover
have "([],{# At i xs #} \<Rightarrow>* {# At i xs #}) \<in> R" using b by auto
ultimately
have "([],\<Gamma> \<Rightarrow>* \<Delta>) \<in> extRules R" 
     using extRules.id[where R=R and r="([],  {#At i xs#} \<Rightarrow>* {#At i xs#})" and S="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs"] 
       and extendRule_def[where forms="\<Gamma> \<ominus> At i xs \<Rightarrow>* \<Delta> \<ominus> At i xs" and R="([],  {#At i xs#} \<Rightarrow>* {#At i xs#})"] by auto
then show ?thesis using derivable.base[where R="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 xs. r = ([], {# At i xs#} \<Rightarrow>* {# At i xs#})"
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 xs where "x=[]" and "y = ({# At i xs#} \<Rightarrow>* {# At i xs#})" by cases
    with `r= (x,y)` have "r = ([],{# At i xs#} \<Rightarrow>* {# At i xs#})" by simp
    then show "\<exists> i xs. r = ([],{# At i xs#} \<Rightarrow>* {# At i xs#})" 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 propRuleCharacterise:
assumes "(Ps,C) \<in> propRules"
shows "\<exists> F Fs. C = ({#} \<Rightarrow>* {#Cpd0 F Fs#}) \<or> C = ({#Cpd0 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> propRules" using prems by simp
then have "\<exists> F Fs. c = ({#} \<Rightarrow>* {#Cpd0 F Fs#}) \<or> c = ({#Cpd0 F Fs#} \<Rightarrow>* {#})" 
     using `mset c \<equiv> {#Cpd0 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="Cpd0 F Fs"]
     by auto
thus ?thesis using `C=c` by simp
qed

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

lemma nprovRuleCharacterise:
assumes "(Ps,C) \<in> nprovRules"
shows "\<exists> F x A. C = ({#} \<Rightarrow>* {# F \<nabla> [x].A #}) \<or> C = ({# F \<nabla> [x].A #} \<Rightarrow>* {#})"
using assms
proof (cases)
case (I c F x A Ps)
then obtain \<Gamma> \<Delta> where "c = (\<Gamma> \<Rightarrow>* \<Delta>)" using characteriseSeq[where C=c] by auto
then have "(Ps,\<Gamma> \<Rightarrow>* \<Delta>) \<in> nprovRules" using prems by simp
then have "\<exists> F x A. c = ({#} \<Rightarrow>* {# F \<nabla> [x].A #}) \<or> c = ({# F \<nabla> [x].A #} \<Rightarrow>* {#})" 
     using `mset c = {# F \<nabla> [x].A #}` 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="F \<nabla> [x].A"]
     by auto
thus ?thesis using `C=c` by simp
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

lemma finSeqSet:
fixes S :: "sequent"
shows "finite (set_of_seq S)"
proof-
obtain \<Gamma> \<Delta> where "S = (\<Gamma> \<Rightarrow>* \<Delta>)" by (cases S) auto
then show ?thesis by (auto simp add:finite_set_of)
qed

lemma finPremSet:
fixes Ps :: "sequent list"
shows "finite (set_of_prem Ps)"
by (induct Ps) (auto simp add:finSeqSet)


lemma finSupp:
fixes A :: "form" and As :: "form_list"
shows "finite ((supp A) :: var set)" and "finite ((supp As) :: var set)"
proof (nominal_induct A and As rule:form_form_list.inducts)
print_cases
case (At n xs)   
   have "finite (set xs :: var set)" by (induct xs) auto
   moreover have "set xs = (supp xs :: var set)" by (induct xs) (auto simp add:supp_list_nil supp_set_empty supp_list_cons supp_atm)
   ultimately have "finite (supp xs :: var set)" by auto
   moreover have "supp (At n xs) = supp n \<union> (supp xs :: var set)" using form.supp(1)[where ?x2.0=n and ?x1.0=xs] by auto
   then have "supp (At n xs) = (supp xs :: var set)" using supp_nat[where n=n] by force
   ultimately show ?case by auto
next
case FNil
   have "supp FNil = ({} :: var set)" using form_list.supp by auto
   then show ?case by auto
next
case (FCons F Fs)
   then show ?case using form_list.supp by auto
next
case (Cpd0 Str Fs)
   then show ?case using form.supp(2)[where ?x2.0="Str" and ?x1.0=Fs] and supp_string[where s=Str] by auto
next
case (Cpd1 F x B)
   from `finite (supp B)` have "supp ([x].B) = supp B - {x}" using abs_fun_supp[OF pt_var_inst, OF at_var_inst] by auto
   then show ?case using form.supp(3)[where ?x3.0=F and ?x1.0=x and ?x2.0=B] and supp_string[where s=F]
                   and `finite (supp B)` by force
qed

lemma getFresh:
fixes x :: "var" and A :: "form" and S :: "sequent" and Ps :: "sequent list"
shows "\<exists> (y :: var). y \<sharp> x \<and> y \<sharp> A \<and> y \<sharp> set_of_seq S \<and> y \<sharp> set_of_prem Ps"
proof-
have "finite ({A} \<union> set_of_seq S \<union> set_of_prem Ps)" using finSeqSet and finPremSet by auto
then have "finite (supp ({A} \<union> set_of_seq S \<union> set_of_prem Ps) :: var set)"
     using finSupp(1) and supp_of_fin_sets[OF pt_var_inst, OF at_var_inst, OF fs_var_inst,
                                           where X="({A} \<union> set_of_seq S \<union> set_of_prem Ps)"] 
     by auto
then have "finite (supp ({A} \<union> set_of_seq S \<union> set_of_prem Ps) \<union> supp x :: var set)" using supp_atm by auto
then obtain y where "y \<notin> (supp ({A} \<union> set_of_seq S \<union> set_of_prem Ps) \<union> supp x :: var set)" 
     using ex_in_inf[OF at_var_inst,where A="supp ({A} \<union> set_of_seq S \<union> set_of_prem Ps) \<union> supp x"] by auto
then have "y \<notin> supp x \<and> y \<notin> supp ({A} \<union> set_of_seq S \<union> set_of_prem Ps)" by auto
then have "y \<sharp> ({A} \<union> set_of_seq S \<union> set_of_prem Ps) \<and> y \<sharp> x" using fresh_def[where a=y and x=x]
     and fresh_def[where a=y and x="{A} \<union> set_of_seq S \<union> set_of_prem Ps"] by auto
then have "y \<sharp> A \<and> y \<sharp> (set_of_seq S \<union> set_of_prem Ps) \<and> y \<sharp> x" 
     using fresh_fin_insert[OF pt_var_inst, OF at_var_inst, OF fs_var_inst,where X="set_of_seq S \<union> set_of_prem Ps" and x=A]
       and finSeqSet and finPremSet by auto
then have "y \<sharp> A \<and> y \<sharp> set_of_seq S \<and> y \<sharp> set_of_prem Ps \<and> y \<sharp> x"
     using fresh_fin_union[OF pt_var_inst,OF at_var_inst, OF fs_var_inst, where X="set_of_seq S" and Y="set_of_prem Ps"]
       and finSeqSet and finPremSet by auto
then show ?thesis by auto
qed

lemma switchAux:
fixes Xs :: "var list"
assumes "y \<sharp> Xs"
shows "[y,x]Xs = [(y,x)]\<bullet>Xs"
using assms
proof (induct Xs)
print_cases
case Nil
   then show ?case using nil_eqvt by auto
next
case (Cons a As)
   then have "y \<sharp> a \<and> y \<sharp> As" and "[y,x]As = [(y,x)]\<bullet>As" 
        using fresh_list_cons[where a=y and x=a and xs=As] by auto
   then show ?case using NEmpt[where z=y and y=x and x=a and ys= As] 
                 and cons_eqvt[where pi="[(y,x)]" and x=a and xs=As] by (perm_simp add:fresh_atm)
qed

lemma switch:
fixes A :: "form" and As :: "form_list"
shows "y \<sharp> A \<Longrightarrow> [y,x]A = [(y,x)]\<bullet>A" and "y \<sharp> As \<Longrightarrow> [y,x]As = [(y,x)]\<bullet>As"
proof (nominal_induct A and As avoiding: x y rule:form_form_list.inducts)
print_cases
case (At n xs s t)
   then have "t \<sharp> xs" using form.fresh by auto
   then show ?case using perm_nat_def[where pi="[(t,s)]" and i=n] and switchAux[where y=t and Xs=xs] by auto
next
case FNil
   then show ?case by auto
next
case (FCons B Bs s t)
   then show ?case by auto
next
case (Cpd0 Str Bs s t)
   then show ?case using prems(1)[where ba=t and b=s] and form.fresh 
                   and perm_string[where s="Str" and pi="[(t,s)]"] by auto
next
case (Cpd1 F a B s t)
   then have "t \<sharp> B" using form.fresh(3)[where ?x3.0=F and ?x1.0=a and ?x2.0=B and a=t] 
                      and fresh_atm[where a=a and b=t] and fresh_string[where a=t and s=F] 
                      and fresh_abs_funE[OF pt_var_inst, OF at_var_inst,where x=B and b=t and a=a]
                      and finSupp(1)[where A=B] by auto
   then show ?case using prems(4)[where ba=t and b=s] and form.fresh and prems(1,2)
                   and perm_string[where pi="[(t,s)]" and s=F] and fresh_atm by (perm_simp)
qed
    
lemma formSubst:
shows "y \<sharp> x \<and> y \<sharp> A \<Longrightarrow> F \<nabla> [x].A = F \<nabla> [y].([y,x]A)"
proof-
assume "y \<sharp> x \<and> y \<sharp> A" then have "[x].A = [y].([y,x]A)" 
  using abs_fun_eq3[OF pt_var_inst, OF at_var_inst,where x="[y,x]A" and y=A and a=y and b=x]
  and switch(1)[where y=y and A=A and x=x] and fresh_atm[where a=y and b=x] by (perm_simp)
then show ?thesis using form.inject(3) by auto
qed

lemma extend_for_any_seq:
fixes S :: "sequent"
assumes rules: "R1 \<subseteq> propRules \<and> R2 \<subseteq> nprovRules \<and> R3 \<subseteq> provRules"
    and rules2: "R = idRules \<union> R1 \<union> R2 \<union> R3"
    and rin: "r \<in> R"
shows "extendRule S r \<in> R*"
proof-
from rin and rules2 have "r \<in> idRules \<or> r \<in> R1 \<or> r \<in> R2 \<or> r \<in> R3" by auto
moreover
    {assume "r \<in> idRules"
     then have "extendRule S r \<in> R*" using extRules.id[where r=r and R=R and S=S] and rin by auto
    }
moreover
    {assume "r \<in> R1"
     then have "r \<in> propRules" using rules by auto
     then have "extendRule S r \<in> R*" using extRules.sc[where r=r and R=R and S=S] and rin by auto
    }
moreover
    {assume "r \<in> R2"
     then have "r \<in> nprovRules" using rules by auto
     then have "extendRule S r \<in> R*" using extRules.np[where r=r and R=R and S=S] and rin by auto
    }
moreover
    {assume "r \<in> R3"
     then have "r \<in> provRules" using rules by auto
     obtain ps c where "r = (ps,c)" by (cases r) auto
     then have r1:"(ps,c) \<in> R" and r2:"(ps,c) \<in> provRules" using `r \<in> provRules` and rin by auto
     with `r = (ps,c)` obtain F x A 
          where "(c = ( {#} \<Rightarrow>* {#F \<nabla> [x].A#}) \<or> c = ( {#F \<nabla> [x].A#} \<Rightarrow>* {#})) \<and> x \<sharp> set_of_prem ( ps - A )"
          using provRuleCharacterise[where Ps=ps and C=c] and `r \<in> provRules` by auto
     then have "mset c = {# F \<nabla> [x].A #} \<and> x \<sharp> set_of_prem (ps - A)" using mset_def by auto
     moreover obtain y where fr:"y \<sharp> x \<and> y \<sharp> A \<and> y \<sharp> set_of_seq S \<and> (y :: var) \<sharp> set_of_prem (ps-A)"
          using getFresh[where x=x and A=A and S=S and Ps="ps-A"] by auto
     then have fr2: "y \<sharp> set_of_seq S" by auto 
     ultimately have "mset c = {# F \<nabla> [y].([y,x]A) #} \<and> y \<sharp> set_of_prem (ps - A)" using formSubst and fr by auto
     then have "mset c = {# F \<nabla> [y].([y,x]A) #}" by auto
     then have "extendRule S (ps,c) \<in> R*" using r1 and r2 and fr2
          and extRules.p[where ps=ps and c=c and R=R and F=F and x=y and A="[y,x]A" and S=S] by auto
     then have "extendRule S r \<in> R*" using `r = (ps,c)` by simp
    }
ultimately show ?thesis by blast
qed

end