1 include "basics/types.ma".
2 include "arithmetics/nat.ma".
4 (********************************** pairing ***********************************)
5 axiom pair: nat → nat → nat.
9 interpretation "abstract pair" 'pair f g = (pair f g).
11 axiom fst_pair: ∀a,b. fst 〈a,b〉 = a.
12 axiom snd_pair: ∀a,b. snd 〈a,b〉 = b.
13 axiom surj_pair: ∀x. ∃a,b. x = 〈a,b〉.
15 axiom le_fst : ∀p. fst p ≤ p.
16 axiom le_snd : ∀p. snd p ≤ p.
17 axiom le_pair: ∀a,a1,b,b1. a ≤ a1 → b ≤ b1 → 〈a,b〉 ≤ 〈a1,b1〉.
19 lemma expand_pair: ∀x. x = 〈fst x, snd x〉.
20 #x lapply (surj_pair x) * #a * #b #Hx >Hx >fst_pair >snd_pair //
23 (************************************* U **************************************)
24 axiom U: nat → nat →nat → option nat.
26 axiom monotonic_U: ∀i,x,n,m,y.n ≤m →
27 U i x n = Some ? y → U i x m = Some ? y.
29 lemma unique_U: ∀i,x,n,m,yn,ym.
30 U i x n = Some ? yn → U i x m = Some ? ym → yn = ym.
31 #i #x #n #m #yn #ym #Hn #Hm cases (decidable_le n m)
32 [#lenm lapply (monotonic_U … lenm Hn) >Hm #HS destruct (HS) //
33 |#ltmn lapply (monotonic_U … n … Hm) [@lt_to_le @not_le_to_lt //]
34 >Hn #HS destruct (HS) //
38 definition code_for ≝ λf,i.∀x.
39 ∃n.∀m. n ≤ m → U i x m = f x.
41 definition terminate ≝ λi,x,r. ∃y. U i x r = Some ? y.
43 notation "{i ⊙ x} ↓ r" with precedence 60 for @{terminate $i $x $r}.
45 lemma terminate_dec: ∀i,x,n. {i ⊙ x} ↓ n ∨ ¬ {i ⊙ x} ↓ n.
46 #i #x #n normalize cases (U i x n)
47 [%2 % * #y #H destruct|#y %1 %{y} //]
50 lemma monotonic_terminate: ∀i,x,n,m.
51 n ≤ m → {i ⊙ x} ↓ n → {i ⊙ x} ↓ m.
52 #i #x #n #m #lenm * #z #H %{z} @(monotonic_U … H) //
55 definition termb ≝ λi,x,t.
56 match U i x t with [None ⇒ false |Some y ⇒ true].
58 lemma termb_true_to_term: ∀i,x,t. termb i x t = true → {i ⊙ x} ↓ t.
59 #i #x #t normalize cases (U i x t) normalize [#H destruct | #y #_ %{y} //]
62 lemma term_to_termb_true: ∀i,x,t. {i ⊙ x} ↓ t → termb i x t = true.
63 #i #x #t * #y #H normalize >H //
66 definition out ≝ λi,x,r.
67 match U i x r with [ None ⇒ 0 | Some z ⇒ z].
69 definition bool_to_nat: bool → nat ≝
70 λb. match b with [true ⇒ 1 | false ⇒ 0].
74 definition pU : nat → nat → nat → nat ≝ λi,x,r.〈termb i x r,out i x r〉.
76 lemma pU_vs_U_Some : ∀i,x,r,y. pU i x r = 〈1,y〉 ↔ U i x r = Some ? y.
77 #i #x #r #y % normalize
78 [cases (U i x r) normalize
79 [#H cut (0=1) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H @H]
81 |#a #H cut (a=y) [lapply (eq_f … snd … H) >snd_pair >snd_pair #H1 @H1]
87 lemma pU_vs_U_None : ∀i,x,r. pU i x r = 〈0,0〉 ↔ U i x r = None ?.
89 [cases (U i x r) normalize //
90 #a #H cut (1=0) [lapply (eq_f … fst … H) >fst_pair >fst_pair #H1 @H1]
95 lemma fst_pU: ∀i,x,r. fst (pU i x r) = termb i x r.
96 #i #x #r normalize cases (U i x r) normalize >fst_pair //
99 lemma snd_pU: ∀i,x,r. snd (pU i x r) = out i x r.
100 #i #x #r normalize cases (U i x r) normalize >snd_pair //
104 definition total ≝ λf.λx:nat. Some nat (f x).