Theory Example_Hybrid_Logic

(*
  Title:  Example Completeness Proof for a Natural Deduction Calculus for Basic Hybrid Logic
  Author: Asta Halkjær From
*)

chapter ‹Example: Hybrid Logic›

theory Example_Hybrid_Logic imports Derivations begin

section ‹Syntax›

datatype (nominals_fm: 'i, 'p) fm
  = Fls ()
  | Pro 'p ()
  | Nom 'i ()
  | Imp ('i, 'p) fm ('i, 'p) fm (infixr  55)
  | Dia ('i, 'p) fm ()
  | Sat 'i ('i, 'p) fm (@)

abbreviation Neg (¬ _› [70] 70) where ¬ p  p  

type_synonym ('i, 'p) lbd = 'i × ('i, 'p) fm

primrec nominals_lbd :: ('i, 'p) lbd  'i set where
  nominals_lbd (i, p) = {i}  nominals_fm p

abbreviation nominals :: ('i, 'p) lbd set  'i set where
  nominals S  ip  S. nominals_lbd ip

lemma finite_nominals_fm: finite (nominals_fm p)
  by (induct p) simp_all

lemma finite_nominals_lbd: finite (nominals_lbd p)
  by (cases p) (simp add: finite_nominals_fm)

section ‹Semantics›

datatype ('w, 'p) model =
  Model (R: 'w  'w set) (V: 'w  'p  bool)

type_synonym ('i, 'p, 'w) ctx = ('w, 'p) model × ('i  'w) × 'w

fun semantics :: ('i, 'p, 'w) ctx  ('i, 'p) fm  bool (‹_  _› [50, 50] 50) where
  (M, g, w)    False
| (M, _, w)  P  V M w P
| (_, g, w)  i  w = g i
| (M, g, w)  (p  q)  (M, g, w)  p  (M, g, w)  q
| (M, g, w)   p  (v  R M w. (M, g, v)  p)
| (M, g, _)  @i p  (M, g, g i)  p

lemma semantics_fresh: i  nominals_fm p  ((M, g, w)  p) = ((M, g(i := v), w)  p)
  by (induct p arbitrary: w) auto

lemma semantics_fresh_lbd:
  k  nominals_lbd (i, p)  ((M, g, w)  p) = ((M, g(k := v), w)  p)
  by (induct p arbitrary: w) auto

section ‹Calculus›

inductive Calculus :: ('i, 'p) lbd list  ('i, 'p) lbd  bool (‹_ @ _› [50, 50] 50) where
  Assm [intro]: (i, p)  set A  A @ (i, p)
| Ref [intro]: A @ (i, i)
| Nom [intro]: A @ (i, k)  A @ (i, p)  A @ (k, p)
| FlsE [elim]: A @ (i, )  A @ (k, p)
| ImpI [intro]: (i, p) # A @ (i, q)  A @ (i, p  q)
| ImpE [elim]: A @ (i, p  q)  A @ (i, p)  A @ (i, q)
| SatI [intro]: A @ (i, p)  A @ (k, @i p)
| SatE [elim]: A @ (i, @k p)  A @ (k, p)
| DiaI [intro]: A @ (i,  (k))  A @ (k, p)  A @ (i,  p)
| DiaE [elim]: A @ (i,  p)  k  nominals ({(i, p), (j, q)}  set A) 
    (k, p) # (i,  (k)) # A @ (j, q)  A @ (j, q)
| Clas: (i, p  q) # A @ (i, p)  A @ (i, p)
| Weak: A @ (i, p)  (k, q) # A @ (i, p)

section ‹Soundness›

theorem soundness: A @ (i, p)  list_all (λ(i, p). (M, g, g i)  p) A  (M, g, g i)  p
proof (induct (i, p) arbitrary: i p g rule: Calculus.induct)
  case (Nom A i k p)
  then show ?case
    by fastforce
next
  case (DiaE A i p k j q)
  then have (M, g, g i)   p
    by blast
  then obtain v where v: v  R M (g i) (M, g, v)  p
    by auto
  let ?g = g(k := v)
  have (M, ?g, ?g k)  p (M, ?g, ?g i)   (k)
    using v fun_upd_same DiaE(3) semantics_fresh_lbd by fastforce+
  moreover have list_all (λ(i, p). (M, ?g, ?g i)  p) A
    using DiaE.prems DiaE.hyps(3) semantics_fresh_lbd by (induct A) fastforce+
  ultimately have list_all (λ(i, p). (M, ?g, ?g i)  p) ((k, p) # (i,  (k)) # A)
    by simp
  then have (M, ?g, ?g j)  q
    using DiaE.hyps by fast
  then show ?case
    using DiaE.hyps(3) semantics_fresh_lbd by fastforce
qed (auto simp: list_all_iff)

corollary soundness': [] @ (i, p)  i  nominals_fm p  (M, g, w)  p
  using soundness semantics_fresh by (metis fun_upd_same list.pred_inject(1))

corollary ¬ ([] @ (i, ))
  using soundness' by fastforce

section ‹Admissible Rules›

lemma Assm_head: (p, i) # A @ (p, i)
  by auto

lemma deduct1: A @ (i, p  q)  (i, p) # A @ (i, q)
  by (meson ImpE Weak Assm_head)

lemma Boole: (i, ¬ p) # A @ (i, )  A @ (i, p)
  using Clas FlsE by meson

lemma Weak': A @ (i, p)  B @ A @ (i, p)
proof (induct B)
  case (Cons b B)
  then show ?case
    by (cases b) (metis Cons Weak append_Cons)
qed simp

lemma ImpI':
  assumes (k, q) # A @ (i, p)
  shows A @ (i, (@k q)  p)
  using assms
proof -
  have (k, q) # A @ (k, @i p)
    using assms by fast
  then show ?thesis
    by (meson Assm_head ImpE ImpI SatE Weak)
qed

lemma Weaken: A @ (i, p)  set A  set B  B @ (i, p)
proof (induct A arbitrary: i p)
  case Nil
  then show ?case
    using Weak' by fastforce
next
  case (Cons kq A)
  then show ?case
  proof (cases kq)
    case (Pair k q)
    then show ?thesis
      using Cons by (meson Assm ImpI' ImpE SatI list.set_intros(1) set_subset_Cons subset_eq)
  qed
qed

interpretation Derivations Calculus
proof
  fix A B and p :: ('i, 'p) lbd
  assume A @ p set A  set B
  then show B @ p
    by (cases p) (metis Weaken)
qed

section ‹Maximal Consistent Sets›

definition consistent :: ('i, 'p) lbd set  bool where
  consistent S  S' a. set S'  S  S' @ (a, )

lemma consistent_add_witness:
  assumes consistent S (i,  p)  S k  nominals S
  shows consistent ({(k, p), (i,  (k))}  S)
  unfolding consistent_def
proof
  assume S' a. set S'  {(k, p), (i,  (k))}  S  S' @ (a, )
  then obtain S' a where set S'  S (k, p) # (i,  (k)) # S' @ (a, )
    using assms derive_split[where X=S and B=[(k, p), (i,  (k))]]
    by (metis append_Cons append_Nil list.simps(15) set_empty)
  then have (k, p) # (i,  (k)) # S' @ (i, )
    by fast
  then have (k, p) # (i,  (k)) # (i,  p) # S' @ (i, )
    by (fastforce intro: Weaken)
  moreover have k  nominals ({(i, p), (i, )}  set ((i,  p) # S'))
    using set S'  S assms(2-3) by auto
  moreover have (i,  p) # S' @ (i,  p)
    by auto
  ultimately have (i,  p) # S' @ (i, )
    by fastforce
  moreover have set ((i,  p) # S')  S
    using set S'  S assms(2) by simp
  ultimately show False
    using assms(1) unfolding consistent_def by blast
qed

fun witness :: ('i, 'p) lbd  ('i, 'p) lbd set  ('i, 'p) lbd set where
  witness (i,  p) S = (let k = (SOME k. k  nominals ({(i, p)}  S)) in {(k, p), (i,  (k))})
| witness (_, _) _ = {}

lemma consistent_witness':
  assumes consistent ({(i, p)}  S) infinite (UNIV - nominals S)
  shows consistent (witness (i, p) S  {(i, p)}  S)
  using assms
proof (induct (i, p) S arbitrary: i p rule: witness.induct)
  case (1 i p S)
  have infinite (UNIV - nominals ({(i, p)}  S))
    using 1(2) finite_nominals_lbd
    by (metis UN_Un finite.emptyI finite.insertI finite_UN_I infinite_Diff_fin_Un)
  then have k. k  nominals ({(i, p)}  S)
    by (simp add: not_finite_existsD set_diff_eq)
  then have (SOME k. k  nominals ({(i, p)}  S))  nominals ({(i, p)}  S)
    by (rule someI_ex)
  then obtain k where witness (i,  p) S = {(k, p), (i,  (k))}
    k  nominals ({(i,  p)}  S)
    by (simp add: Let_def)
  then show ?case
    using 1(1-2) consistent_add_witness[where S={(i,  p)}  S] by simp
qed (auto simp: assms)

interpretation MCS_Saturation consistent nominals_lbd witness
proof
  fix S S' :: ('i, 'p) lbd set
  assume consistent S S'  S
  then show consistent S'
    unfolding consistent_def by fast
next
  fix S :: ('i, 'p) lbd set
  assume ¬ consistent S
  then show S'S. finite S'  ¬ consistent S'
    unfolding consistent_def by blast
next
  fix ip :: ('i, 'p) lbd
  show finite (nominals_lbd ip)
    using finite_nominals_fm by (cases ip) simp
next
  fix ip :: ('i, 'p) lbd and S :: ('i, 'p) lbd set
  show finite (nominals (witness ip S))
    by (induct ip S rule: witness.induct) (auto simp: finite_nominals_fm Let_def)
next
  fix ip and S :: ('i, 'p) lbd set
  assume consistent ({ip}  S) infinite (UNIV - nominals S)
  then show consistent (witness ip S  {ip}  S)
    using consistent_witness' by (cases ip) simp
next
  have infinite (UNIV :: ('i, 'p) fm set)
    using infinite_UNIV_size[of ] by simp
  then show infinite (UNIV :: ('i, 'p) lbd set)
    using finite_prod by blast
qed

interpretation Derivations_MCS_Cut Calculus consistent (undefined, )
proof
  fix S :: ('i, 'p) lbd set
  show consistent S = (S'. set S'  S  S' @ (undefined, ))
    unfolding consistent_def by fast
next
  fix A and p :: ('i, 'p) lbd
  assume p  set A
  then show A @ p
    by (metis Assm surj_pair)
next
  fix A B and p q :: ('i, 'p) lbd
  assume A @ p p # B @ q
  then have A @ B @ p p # A @ B @ q
    by (simp_all add: derive_struct subsetI)
  then show A @ B @ q
    by (cases p, cases q) (meson ImpE ImpI' SatI)
qed

lemma saturated: saturated H  (i, p)  H  k. (i,  (k))  H  (k, p)  H
  unfolding saturated_def by (metis insert_subset witness.simps(1))

section ‹Nominals›

lemma MCS_Nom_refl:
  assumes consistent S maximal S
  shows (i, i)  S
  using assms Ref by (metis MCS_derive MCS_derive_fls)

lemma MCS_Nom_sym:
  assumes consistent S maximal S (i, k)  S
  shows (k, i)  S
  using assms Nom Ref by (metis MCS_derive)

lemma MCS_Nom_trans:
  assumes consistent S maximal S (i, j)  S (j, k)  S
  shows (i, k)  S
proof -
  have S'. set S'  S  S' @ (i, j)
    using assms MCS_derive by blast
  then have S'. set S'  S  S' @ (i, j)  S' @ (j, k)
    by (metis Assm_head Calculus.intros(12) assms(4) insert_subset list.set(2))
  then have S'. set S'  S  S' @ (i, k)
    using Nom Ref by metis
  then show ?thesis
    using assms MCS_derive by blast
qed

section ‹Truth Lemma›

fun semics :: ('i, 'p, 'w) ctx  (('i, 'p, 'w) ctx  ('i, 'p) fm  bool)  ('i, 'p) fm  bool
  where
    semics _ _   False
  | semics (M, _, w) _ (P)  V M w P
  | semics (_, g, w) _ (i)  w = g i
  | semics (M, g, w) rel (p  q)  rel (M, g, w) p  rel (M, g, w) q
  | semics (M, g, w) rel ( p)  (v  R M w. rel (M, g, v) p)
  | semics (M, g, _) rel (@ i p)  rel (M, g, g i) p

fun rel :: ('i, 'p) lbd set  ('i, 'p, 'i) ctx  ('i, 'p) fm  bool where
  rel H (_, _, i) p = ((i, p)  H)

definition val :: ('i, 'p) lbd set  'i  'p  bool where
  val H i P  (i, P)  H

definition hequiv :: ('i, 'p) lbd set  'i  'i  bool where
  hequiv H i k  (i, k)  H

lemma hequiv_reflp:
  assumes consistent H maximal H
  shows reflp (hequiv H)
  unfolding hequiv_def reflp_def using assms MCS_Nom_refl by fast

lemma hequiv_symp:
  assumes consistent H maximal H
  shows symp (hequiv H)
  unfolding hequiv_def symp_def using assms MCS_Nom_sym by fast

lemma hequiv_transp:
  assumes consistent H maximal H
  shows transp (hequiv H)
  unfolding hequiv_def transp_def using assms MCS_Nom_trans by fast

lemma hequiv_equivp:
  assumes consistent H maximal H
  shows equivp (hequiv H)
  using assms by (simp add: equivpI hequiv_reflp hequiv_symp hequiv_transp)

definition assign :: ('i, 'p) lbd set  'i  'i where
  assign H i  minim ( |UNIV| ) {k. hequiv H i k}

lemma hequiv_ne:
  assumes consistent H maximal H
  shows {k. hequiv H i k}  {}
  unfolding hequiv_def using assms MCS_Nom_refl by fast

lemma hequiv_assign:
  assumes consistent H maximal H
  shows hequiv H i (assign H i)
  unfolding assign_def using assms hequiv_ne wo_rel.minim_in
  by (metis Field_card_of card_of_well_order_on mem_Collect_eq top.extremum wo_rel_def)

lemma hequiv_Nom:
  assumes consistent H maximal H hequiv H i k (i, p)  H
  shows (k, p)  H
proof -
  have A. set A  H  A @ (i, p)
    using assms MCS_derive by fast
  then have A. set A  H  A @ (i, p)  A @ (i, k)
    using assms(3) unfolding hequiv_def by (metis Assm_head Weak insert_subset list.simps(15))
  then have A. set A  H  A @ (k, p)
    using Nom by fast
  then show ?thesis
    using assms MCS_derive by fast
qed

definition reach :: ('i, 'p) lbd set  'i  'i set where
  reach H i  {assign H k |k. (i,  (k))  H}

abbreviation canonical :: ('i × ('i, 'p) fm) set  'i  ('i, 'p, 'i) ctx where
  canonical H i  (Model (reach H) (val H), assign H, assign H i)

lemma Hintikka_model':
  assumes i p. semics (canonical H i) (rel H) p  rel H (canonical H i) p
  shows (canonical H i  p)  rel H (canonical H i) p
proof (induct p arbitrary: i rule: wf_induct[where r=measure size])
  case 1
  then show ?case ..
next
  case (2 x)
  then show ?case
    using assms[of i x] by (cases x) (auto simp: reach_def)
qed

lemma Hintikka_Extend':
  assumes consistent H maximal H saturated H
  shows semics (canonical H i) (rel H) p  rel H (canonical H i) p
proof (cases p)
  case Fls
  have (assign H i, )  H
    using assms(1-2) MCS_derive unfolding consistent_def by fast
  then show ?thesis
    using Fls by simp
next
  case (Pro P)
  have val H (assign H i) P  (assign H i, P)  H
    unfolding val_def ..
  then show ?thesis
    using Pro by simp
next
  case (Nom k)
  have assign H i = assign H k  (assign H i, k)  H
    using assms(1-2) hequiv_equivp hequiv_assign by (metis assign_def equivp_def hequiv_def)
  then show ?thesis
    using Nom by simp
next
  case (Imp p q)
  have (i, p) # A @ (a, )  A @ (i, p  q) A @ (i, q)  A @ (i, p  q) for A a i
    by (auto simp: Weak)
  moreover have A @ (i, p  q)  (i, p) # A @ (i, q) for A i
    using deduct1 .
  ultimately have ((assign H i, p)  H  (assign H i, q)  H)  (assign H i, p  q)  H
    using assms(1-2) MCS_derive MCS_derive_fls by (metis insert_subset list.simps(15))
  then show ?thesis
    using Imp by simp
next
  case (Dia p)
  have (k  reach H (assign H i). (k, p)  H)  (assign H i,  p)  H
  proof
    assume k  reach H (assign H i). (k, p)  H
    then have k. (assign H i,  (k))  H  (assign H k, p)  H
      unfolding reach_def by fast
    then have k. (assign H i,  (k))  H  (k, p)  H
      by (metis assms(1-2) hequiv_Nom hequiv_assign hequiv_symp sympD)
    then have k. A. set A  H  A @ (assign H i,  (k))  A @ (k, p)
      by (metis Assm_head Weak assms(1-2) MCS_derive insert_subset list.simps(15))
    then have A. set A  H  A @ (assign H i,  p)
      by fast
    then show (assign H i,  p)  H
      by (simp add: assms(1-2) MCS_derive)
  next
    assume (assign H i,  p)  H
    then have k. (assign H i,  (k))  H  (k, p)  H
      using assms(3) saturated by fast
    then have k. (assign H i,  (k))  H  (assign H k, p)  H
      by (meson assms(1-2) hequiv_Nom hequiv_assign)
    then show k  reach H (assign H i). (k, p)  H
      unfolding reach_def by fast
  qed
  then show ?thesis
    using Dia by simp
next
  case (Sat k p)
  have (assign H k, p)  H  (assign H i, @k p)  H
    by (metis SatE SatI assms(1-2) MCS_derive hequiv_Nom hequiv_assign hequiv_symp sympD)
  then show ?thesis
    using Sat by simp
qed

interpretation Truth_Saturation
  consistent nominals_lbd witness semics semantics λH. {canonical H i |i. True} rel
proof unfold_locales
  fix p and M :: ('i, 'p, 'w) ctx
  show (M  p) = semics M semantics p
    by (cases M, induct p) auto
next
  fix p H and M :: ('i, 'p, 'i) ctx
  assume M  {canonical H i |i. True}. p. semics M (rel H) p = rel H M p
    M  {canonical H i |i. True}
  then show (M  p) = rel H M p
    using Hintikka_model' by fast
next
  fix H :: ('i, 'p) lbd set
  assume consistent H maximal H saturated H
  then show M{canonical H i |i. True}. p. semics M (rel H) p = rel H M p
    using Hintikka_Extend' by fast
qed

lemma Truth_lemma:
  assumes consistent H maximal H saturated H
  shows (canonical H i  p)  (i, p)  H
proof -
  have (canonical H i  p)  (assign H i, p)  H
    using truth_lemma_saturation assms by fastforce
  then show ?thesis
    using assms by (meson MCS_Nom_sym hequiv_Nom hequiv_assign hequiv_def)
qed

section ‹Cardinalities›

datatype marker = FlsM | ImpM | DiaM | SatM

type_synonym ('i, 'p) enc = ('i + 'p) + marker × nat

abbreviation NOM i  Inl (Inl i)
abbreviation PRO x  Inl (Inr x)
abbreviation FLS  Inr (FlsM, 0)
abbreviation IMP n  Inr (FlsM, n)
abbreviation DIA  Inr (DiaM, 0)
abbreviation SAT  Inr (SatM, 0)

primrec encode :: ('i, 'p) fm  ('i, 'p) enc list where
  encode  = [FLS]
| encode (P) = [PRO P]
| encode (i) = [NOM i]
| encode (p  q) = IMP (length (encode p)) # encode p @ encode q
| encode ( p) = DIA # encode p
| encode (@ i p) = SAT # NOM i # encode p

lemma encode_ne [simp]: encode p  []
  by (induct p) auto

lemma inj_encode': encode p = encode q  p = q
proof (induct p arbitrary: q)
  case Fls
  then show ?case 
    by (cases q) auto
next
  case (Pro P)
  then show ?case 
    by (cases q) auto
next
  case (Nom i)
  then show ?case 
    by (cases q) auto
next
  case (Imp p1 p2)
  then show ?case 
    by (cases q) auto
next
  case (Dia p)
  then show ?case 
    by (cases q) auto
next
  case (Sat x1a p)
  then show ?case 
    by (cases q) auto
qed

lemma inj_encode: inj encode
  unfolding inj_def using inj_encode' by blast

primrec encode_lbd :: ('i, 'p) lbd  ('i, 'p) enc list where
  encode_lbd (i, p) = NOM i # encode p

lemma inj_encode_lbd': encode_lbd (i, p) = encode_lbd (k, q)  i = k  p = q
  using inj_encode' by auto

lemma inj_encode_lbd: inj encode_lbd
  unfolding inj_def using inj_encode_lbd' by auto

lemma finite_marker: finite (UNIV :: marker set)
proof -
  have p  {FlsM, ImpM, DiaM, SatM} for p
    by (cases p) auto
  then show ?thesis
    by (meson ex_new_if_finite finite.emptyI finite_insert)
qed

lemma card_of_lbd:
  assumes infinite (UNIV :: 'i set)
  shows |UNIV :: ('i, 'p) lbd set| ≤o |UNIV :: 'i set| +c |UNIV :: 'p set|
proof -
  have |UNIV :: marker set| ≤o |UNIV :: nat set|
    using finite_marker by (simp add: ordLess_imp_ordLeq)
  moreover have infinite (UNIV :: ('i + 'p) set)
    using assms by simp
  ultimately have |UNIV :: ('i, 'p) enc list set| ≤o |UNIV :: ('i + 'p) set|
    using card_of_params_marker_lists by blast
  moreover have |UNIV :: ('i, 'p) lbd set| ≤o |UNIV :: ('i, 'p) enc list set|
    using card_of_ordLeq inj_encode_lbd by blast
  ultimately have |UNIV :: ('i, 'p) lbd set| ≤o |UNIV :: ('i + 'p) set|
    using ordLeq_transitive by blast
  then show ?thesis
    unfolding csum_def by simp
qed

section ‹Completeness›

theorem strong_completeness:
  fixes p :: ('i, 'p) fm
  assumes M :: ('i, 'p) model. g w.
      ((k, q)  X. (M, g, g k)  q)  (M, g, w)  p
    infinite (UNIV :: 'i set)
    |UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - nominals X|
  shows A. set A  X  A @ (i, p)
proof (rule ccontr)
  assume A. set A  X  A @ (i, p)
  then have *: A. a. set A  X  ((i, ¬ p) # A @ (a, ))
    using Boole FlsE by metis

  let ?S = {(i, ¬ p)}  X
  let ?H = Extend ?S

  have consistent ?S
    unfolding consistent_def using * derive_split1 by metis
  moreover have infinite (UNIV - nominals X)
    using assms(2-3)
    by (metis Cinfinite_csum Cnotzero_UNIV Field_card_of cinfinite_def cinfinite_mono)
  then have |UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - nominals X - nominals_lbd (i, ¬ p)|
    using assms(3) finite_nominals_lbd card_of_infinite_diff_finite
    by (metis ordIso_iff_ordLeq ordLeq_transitive)
  then have |UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - (nominals X  nominals_lbd (i, ¬ p))|
    by (metis Set_Diff_Un)
  then have |UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV - nominals ?S|
    by (metis UN_insert insert_is_Un sup_commute)
  then have |UNIV :: ('i, 'p) lbd set| ≤o |UNIV - nominals ?S|
    using assms card_of_lbd ordLeq_transitive by blast
  ultimately have consistent ?H maximal ?H saturated ?H
    using MCS_Extend by fast+
  then have canonical ?H i  p  (i, p)  ?H for i p
    using Truth_lemma by fast
  then have (i, p)  ?S  canonical ?H i  p for i p
    using Extend_subset by blast
  then have canonical ?H i  ¬ p (k, q)  X. canonical ?H k  q
    by blast+
  moreover from this have canonical ?H i  p
    using assms(1) by blast
  ultimately show False
    by simp
qed

abbreviation valid :: ('i, 'p) fm  bool where
  valid p  (M :: ('i, 'p) model) g w. (M, g, w)  p

theorem completeness:
  fixes p :: ('i, 'p) fm
  assumes valid p infinite (UNIV :: 'i set) |UNIV :: 'p set| ≤o |UNIV :: 'i set|
  shows [] @ (i, p)
proof -
  have |UNIV :: 'i set| +c |UNIV :: 'p set| ≤o |UNIV :: 'i set|
    using assms(2-3) by (simp add: cinfinite_def csum_absorb1 ordIso_imp_ordLeq)
  then show ?thesis
    using assms strong_completeness[where X={} and p=p] infinite_UNIV_listI by auto
qed

corollary completeness':
  fixes p :: ('i, 'i) fm
  assumes valid p infinite (UNIV :: 'i set)
  shows [] @ (i, p)
  using assms completeness[of p] by simp

theorem main:
  fixes p :: ('i, 'p) fm
  assumes i  nominals_fm p infinite (UNIV :: 'i set) |UNIV :: 'p set| ≤o |UNIV :: 'i set|
  shows valid p  [] @ (i, p)
  using assms completeness soundness' by metis

corollary main':
  fixes p :: ('i, 'i) fm
  assumes i  nominals_fm p infinite (UNIV :: 'i set)
  shows valid p  [] @ (i, p)
  using assms completeness' soundness' by metis

end