Theory Higher_Order_Constructs

section‹Fully relational versions of higher order constructs›
theory Higher_Order_Constructs
  imports
    Recursion_Thms
    Least
begin

syntax
  "_sats"  :: "[i, i, i] ⇒ o"  ("(_, _ ⊨ _)" [36,36,36] 25)
translations
  "(M,env ⊨ φ)" ⇌ "CONST sats(M,φ,env)"

definition
  is_If :: "[i⇒o,o,i,i,i] ⇒ o" where
  "is_If(M,b,t,f,r) ≡ (b ⟶ r=t) ∧ (¬b ⟶ r=f)"

lemma (in M_trans) If_abs:
  "is_If(M,b,t,f,r) ⟷ r = If(b,t,f)"
  by (simp add: is_If_def)


definition
  is_If_fm :: "[i,i,i,i] ⇒ i" where
  "is_If_fm(φ,t,f,r) ≡ Or(And(φ,Equal(t,r)),And(Neg(φ),Equal(f,r)))"

lemma is_If_fm_type [TC]: "φ ∈ formula ⟹ t ∈ nat ⟹ f ∈ nat ⟹ r ∈ nat ⟹
  is_If_fm(φ,t,f,r) ∈ formula"
  unfolding is_If_fm_def by auto

lemma sats_is_If_fm:
  assumes Qsats: "Q ⟷ A, env ⊨ φ" "env ∈ list(A)"
  shows "is_If(##A, Q, nth(t, env), nth(f, env), nth(r, env)) ⟷ A, env ⊨ is_If_fm(φ,t,f,r)"
  using assms unfolding is_If_def is_If_fm_def by auto

lemma is_If_fm_iff_sats [iff_sats]:
  assumes Qsats: "Q ⟷ A, env ⊨ φ" and
    "nth(t, env) = ta" "nth(f, env) = fa" "nth(r, env) = ra"
    "t ∈ nat" "f ∈ nat" "r ∈ nat" "env ∈ list(A)"
  shows "is_If(##A,Q,ta,fa,ra) ⟷ A, env ⊨ is_If_fm(φ,t,f,r)"
  using assms sats_is_If_fm[of Q A φ env t f r] by simp

lemma arity_is_If_fm [arity]:
  "φ ∈ formula ⟹ t ∈ nat ⟹ f ∈ nat ⟹ r ∈ nat ⟹
    arity(is_If_fm(φ, t, f, r)) = arity(φ) ∪ succ(t) ∪ succ(r) ∪ succ(f)"
  unfolding is_If_fm_def
  by auto

definition
  is_The :: "[i⇒o,i⇒o,i] ⇒ o" where
  "is_The(M,Q,i) ≡ (Q(i) ∧ (∃x[M]. Q(x) ∧ (∀y[M]. Q(y) ⟶ y = x))) ∨
                   (¬(∃x[M]. Q(x) ∧ (∀y[M]. Q(y) ⟶ y = x))) ∧ empty(M,i) "

(*
definition
  is_The_fm :: "[i,i] ⇒ i" where
  "is_The_fm(q,i) ≡ Or(And(Exists(And(Equal(succ(i),0),q)),
                  Exists(And(q,Forall(Implies(q,Equal(1,0)))))),
                          And(Neg(Exists(And(q,Forall(Implies(q,Equal(1,0)))))),empty_fm(i)))"

(* this doesn't work yet *)
lemma sats_The_fm :
  assumes p_iff_sats:
    "⋀a. a ∈ A ⟹ P(a) ⟷ sats(A, p, Cons(a, env))"
  shows
    "⟦y ∈ nat; env ∈ list(A) ; 0∈A⟧
    ⟹ sats(A, is_The_fm(p,y), env) ⟷
        is_The(##A, P, nth(y,env))"
  using nth_closed p_iff_sats
  unfolding is_The_def is_The_fm_def
  oops

lemma The_iff_sats [iff_sats]:
  assumes is_Q_iff_sats:
      "⋀a. a ∈ A ⟹ is_Q(a) ⟷ sats(A, q, Cons(a,env))"
  shows
  "⟦nth(j,env) = y; j ∈ nat; env ∈ list(A); 0∈A⟧
   ⟹ is_The(##A, is_Q, y) ⟷ sats(A, is_The_fm(q,j), env)"
  using sats_The_fm [OF is_Q_iff_sats, of j , symmetric]
  by simp
*)

lemma (in M_trans) The_abs:
  assumes "⋀x. Q(x) ⟹ M(x)" "M(a)"
  shows "is_The(M,Q,a) ⟷ a = (THE x. Q(x))"
proof (cases "∃x[M]. Q(x) ∧ (∀y[M]. Q(y) ⟶ y = x)")
  case True
  with assms
  show ?thesis
    unfolding is_The_def
    by (intro iffI the_equality[symmetric])
      (auto, blast intro:theI)
next
  case False
  with ‹⋀x. Q(x) ⟹ M(x)›
  have " ¬ (∃x. Q(x) ∧ (∀y. Q(y) ⟶ y = x))"
    by auto
  then
  have "The(Q) = 0"
    by (intro the_0) auto
  with assms and False
  show ?thesis
    unfolding is_The_def
    by auto
qed

(*
definition
  recursor  :: "[i, [i,i]=>i, i]=>i"  where
    "recursor(a,b,k) ≡  transrec(k, λn f. nat_case(a, λm. b(m, f`m), n))"
*)

definition
  is_recursor :: "[i⇒o,i,[i,i,i]⇒o,i,i] ⇒o" where
  "is_recursor(M,a,is_b,k,r) ≡ is_transrec(M, λn f ntc. is_nat_case(M,a,
      λm bmfm.
      ∃fm[M]. fun_apply(M,f,m,fm) ∧ is_b(m,fm,bmfm),n,ntc),k,r)"

lemma (in M_eclose) recursor_abs:
  assumes "Ord(k)" and
    types: "M(a)" "M(k)" "M(r)" and
    b_iff: "⋀m f bmf. M(m) ⟹ M(f) ⟹ M(bmf) ⟹ is_b(m,f,bmf)  ⟷ bmf = b(m,f)" and
    b_closed: "⋀m f bmf. M(m) ⟹ M(f) ⟹ M(b(m,f))" and
    repl: "transrec_replacement(M, λn f ntc. is_nat_case(M, a,
        λm bmfm. ∃fm[M]. fun_apply(M, f, m, fm) ∧ is_b( m, fm, bmfm), n, ntc), k)"
  shows
    "is_recursor(M,a,is_b,k,r) ⟷ r = recursor(a,b,k)"
  unfolding is_recursor_def recursor_def
  using assms
  apply (rule_tac transrec_abs)
       apply (auto simp:relation2_def)
   apply (rule nat_case_abs[THEN iffD1, where is_b1="λm bmfm.
      ∃fm[M]. fun_apply(M,_,m,fm) ∧ is_b(m,fm,bmfm)"])
      apply (auto simp:relation1_def)
  apply (rule nat_case_abs[THEN iffD2, where is_b1="λm bmfm.
      ∃fm[M]. fun_apply(M,_,m,fm) ∧ is_b(m,fm,bmfm)"])
     apply (auto simp:relation1_def)
  done

definition
  is_wfrec_on :: "[i=>o,[i,i,i]=>o,i,i,i, i] => o" where
  "is_wfrec_on(M,MH,A,r,a,z) == is_wfrec(M,MH,r,a,z)"

lemma (in M_trancl) trans_wfrec_on_abs:
  "[|wf(r);  trans(r);  relation(r);  M(r);  M(a);  M(z);
     wfrec_replacement(M,MH,r);  relation2(M,MH,H);
     ∀x[M]. ∀g[M]. function(g) ⟶ M(H(x,g));
     r-``{a}⊆A; a ∈ A|]
   ==> is_wfrec_on(M,MH,A,r,a,z) ⟷ z=wfrec[A](r,a,H)"
  using trans_wfrec_abs wfrec_trans_restr
  unfolding is_wfrec_on_def by simp

end