# 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)"

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```