Theory Fixrec_RS
chapter ‹Conceptual Tests: the Restriction-Space Instance of ▩‹Fixrec››
theory Fixrec_RS
imports "GenFixrec-RS"
begin
text ‹The tests are organised by concept and mirror the theory ▩‹Fixrec_HOLCF›. Expected
failures are checked by ‹expect_failure›, which runs the command semantics on the current
theory and asserts that it fails with a message containing a given fragment.›
ML ‹
fun expect_failure langs vars eqns fragment =
let val spec = (map (fn (n, T) => (Binding.name n, SOME T, NoSyn)) vars,
map (fn (n, e) => (false, ((Binding.name n, []), e))) eqns)
val msg_of = Protocol_Message.clean_output o Runtime.exn_message
in case Exn.result (GenFixrec.add_fixrec_langs_global (map (rpair Position.none) langs) spec)
(Context.the_global_context ()) of
Exn.Res _ => error ("expected failure, but Fixrec succeeded: " ^ commas langs)
| Exn.Exn exn => if String.isSubstring fragment (msg_of exn) then ()
else error ("unexpected failure message:\n" ^ msg_of exn)
end
›
section ‹Language Selection›
text ‹A language that always fails to prove the fixpoint unfolding; used to test fallback.›
setup ‹fn thy => Context.Theory thy
|> GenFixrec.update_language (Binding.make ("BROKEN", ⌂))
{mk_fix = #mk_fix RS_instance.rs, dest_fix = #dest_fix RS_instance.rs, lambda' = #lambda' RS_instance.rs,
apply = #apply RS_instance.rs, shift_tac = #shift_tac RS_instance.rs, fix_tac = K no_tac,
proj_tac = #proj_tac RS_instance.rs, fixind_tac = #fixind_tac RS_instance.rs}
|> Context.the_theory›
text ‹Explicit selection:›
Fixrec [RS] l2 :: ‹int process› where l2_eq : ‹l2 = 2 → l2›
text ‹Languages are tried from left to right; the first one that succeeds is taken:›
Fixrec [BROKEN, RS] l3 :: ‹int process› where l3_eq : ‹l3 = 3 → l3›
ML ‹
val proc = "int process"
val _ = expect_failure ["HOLCF"] [("e0", proc)] [("e0_eq", "e0 = 1 → e0")]
"Undefined Fixrec language: \"HOLCF\""
val _ = expect_failure ["BROKEN"] [("e1", proc)] [("e1_eq", "e1 = 1 → e1")]
"no language succeeded"
val _ = expect_failure ["FOO"] [("e2", proc)] [("e2_eq", "e2 = 1 → e2")]
"Undefined Fixrec language: \"FOO\""
val _ = expect_failure ["rs"] [("e3", proc)] [("e3_eq", "e3 = 1 → e3")]
"Undefined Fixrec language: \"rs\""
val _ = expect_failure [] [("e4", proc)] [("e4_eq", "e4 = 1 → e4")]
"no language given"
›
section ‹Unshifted Equations›
Fixrec [RS] u1 :: ‹int ⇒ int process› where u1_eq : ‹u1 = (λx. x → u1 (x+1))›
section ‹Generic Shift over HOL Application›
text ‹The shift over HOL application is provided by the core, independently of the language;
no continuous function space is required.›
Fixrec [RS] s1 :: ‹int ⇒ int process› where s1_eq : ‹s1 x = x → s1 (x+1)›
Fixrec [RS] s2 :: ‹int ⇒ nat ⇒ int process› where s2_eq : ‹s2 x n = x → s2 (x+1) (Suc n)›
Fixrec [RS] s3 :: ‹int × nat ⇒ int process› where s3_eq : ‹s3 (x,n) = x → s3 (x+1,n)›
Fixrec [RS] s4 :: ‹int × int × int ⇒ int process› where s4_eq : ‹s4 (x,y,z) = x → s4 (y,z,x)›
Fixrec [RS] s5 :: ‹int × nat ⇒ bool × int ⇒ int process›
where s5_eq : ‹s5 (x,n) (b,y) = x → s5 (y,Suc n) (¬b,x)›
text ‹The shift is equivalent to the unshifted form:›
lemma ‹s1 = (λx. x → s1 (x+1))› using s1_eq by blast
ML ‹
val _ = expect_failure ["RS"] [("e5", "int ⇒ int process")] [("e5_eq", "e5 0 = 0 → e5 0")]
"args must be free variables or tuples of them"
val _ = expect_failure ["RS"] [("e6", "int ⇒ int process")]
[("e6_eq", "(if True then e6 else e6) x = x → e6 x")]
"lhs head must be one of the declared constants"
›
section ‹Domain-Specific Shift›
text ‹The restriction-space instance has no application/abstraction pair of its own; a lhs
using the HOLCF application ‹⋅› is not recognised:›
ML ‹
val _ = expect_failure ["RS"] [("e7", "int process → int process")] [("e7_eq", "e7⋅P = 1 → e7⋅P")]
"lhs head must be one of the declared constants"
›
section ‹Mutual Recursion›
Fixrec [RS] m1 :: ‹int ⇒ int process› and m2 :: ‹int ⇒ int process›
where m1_eq : ‹m1 x = 1 → m2 x›
| m2_eq : ‹m2 x = 2 → m1 (x+1)›
Fixrec [RS] m3 :: ‹int ⇒ int process› and m4 :: ‹int process›
where m3_eq : ‹m3 x = x → m4›
| m4_eq : ‹m4 = 0 → m3 1›
text ‹Equations that are not (self-)recursive, alone or within a system:›
Fixrec [RS] n1 :: ‹int ⇒ int process› where n1_eq : ‹n1 x = x → Skip›
Fixrec [RS] n2 :: ‹int ⇒ int process› and n3 :: ‹int ⇒ int process›
where n2_eq : ‹n2 x = x → n3 x›
| n3_eq : ‹n3 x = x → n3 (x+1)›
text ‹A larger mutual system (guarded equations, choices, finite non-determinism, a member
that is not self-recursive):›
Fixrec [RS] t1 :: ‹int ⇒ int process› and t2 :: ‹int ⇒ int process›
and t3 :: ‹int ⇒ int process› and t4 :: ‹int process› and t5 :: ‹int ⇒ int process›
where t1_eq : ‹t1 x = 1 → t2 x›
| t2_eq : ‹t2 x = (2 → t3 x) □ (3 → t1 (x+1))›
| t3_eq : ‹t3 x = (⊓ a ∈ {0..x}. a → t4)›
| t4_eq : ‹t4 = 0 → t5 1›
| t5_eq : ‹t5 x = (x → t1 x) ⊓ (x → t4)›
text ‹Recursion through the continuation of the exception operator ‹Θ› (FDR's ‹[| A |>›),
also when the exception event is initial (as in the crash handling of Dali):›
Fixrec [RS] cr :: ‹int process› and cr' :: ‹int process›
where cr_eq : ‹cr = ((1 → Skip) ||| (0 → Skip)) Θ a ∈ {0}. cr'›
| cr'_eq : ‹cr' = ((2 → Skip) ||| (0 → Skip)) Θ a ∈ {0}. cr'›
text ‹Recursion in both operands of ‹Θ› (guarded in the left one), with a parametrised
continuation:›
Fixrec [RS] tb :: ‹int ⇒ int process›
where tb_eq : ‹tb x = (x → tb (x+1) ||| (0 → Skip)) Θ a ∈ {0}. tb (x-1)›
section ‹Polymorphism›
Fixrec [RS] p1 :: ‹'a ⇒ 'a process› where p1_eq : ‹p1 x = x → p1 x›
Fixrec [RS] p2 :: ‹'a ⇒ 'a process› and p3 :: ‹'a ⇒ 'a process›
where p2_eq : ‹p2 x = x → p3 x›
| p3_eq : ‹p3 x = x → p2 x›
lemma ‹p1 x = x → p1 x› by (fact p1_eq)
text ‹Type variables are of sort ‹type›, not ‹cpo›/‹domain›:›
lemma ‹p1 (n::nat) = n → p1 n› by (fact p1_eq)
section ‹Generated Theorems›
thm m1_m2_rec_def m1_m2_rec_unfold m1_def m2_def m1_eq m2_eq m1_m2_induct
lemma ‹s5 (x,n) (b,y) = x → s5 (y,Suc n) (¬b,x)› by (fact s5_eq)
text ‹Fixpoint induction over the restriction fixpoint: admissibility, an arbitrary start
value, step.›
ML ‹
val _ = @{assert} (Thm.nprems_of @{thm s1_induct} = 3)
val _ = @{assert} (Thm.nprems_of @{thm m1_m2_induct} = 3)
›
text ‹Unlike HOLCF's ▩‹fixrec›, the equations are ∗‹not› simp rules by default (unguarded use
of recursive equations by the simplifier loops); ‹[simp]› declares them explicitly:›
Fixrec [RS] sa :: ‹int ⇒ int process› where sa_eq : ‹sa x = x → Skip›
Fixrec [RS] sb :: ‹int ⇒ int process› where sb_eq [simp] : ‹sb x = x → Skip›
lemma ‹sb 1 = 1 → Skip› by simp
ML ‹
val _ = @{assert} (is_none (try (Goal.prove \<^context> [] [] @{prop ‹sa 1 = 1 → Skip›})
(fn {context, ...} => asm_full_simp_tac context 1)))
›
section ‹Semantic Properties of the Instance›
text ‹In restriction spaces, the fixpoint exists only for constructive (guarded) equations;
an unguarded equation is rejected:›
ML ‹
val _ = expect_failure ["RS"] [("d1", "int ⇒ int process")] [("d1_eq", "d1 x = d1 (x+1)")]
"constructive"
›
section ‹Local Contexts: Locales, Contexts, Interpretation›
text ‹▩‹Fixrec› is a local-theory command: it can be used inside locales and other local
contexts. Locale parameters may occur in the equations; the generated constants are
abstracted over the parameters they depend on, and all theorems are available under
interpretation.›
locale L1 = fixes k :: int assumes k_pos : ‹0 < k›
begin
Fixrec [RS] r1 :: ‹int ⇒ int process› where r1_eq : ‹r1 x = x → r1 (x + k)›
Fixrec [RS] r2 :: ‹int ⇒ int process› and r3 :: ‹int process›
where r2_eq : ‹r2 x = x → r3›
| r3_eq : ‹r3 = k → r2 k›
lemma ‹r1 x = x → r1 (x + k)› by (fact r1_eq)
thm r1_rec_def r1_rec_unfold r1_def r1_induct r2_r3_induct
end
text ‹The global constants take the parameter as argument:›
term ‹L1.r1 :: int ⇒ int ⇒ int process›
text ‹Re-entering the locale:›
context L1 begin
lemma ‹r3 = k → r2 k› by (fact r3_eq)
end
text ‹Interpretation:›
interpretation L1_5 : L1 5 by standard simp
lemma ‹L1_5.r1 x = x → L1_5.r1 (x + 5)› by (fact L1_5.r1_eq)
text ‹Unnamed local contexts:›
context fixes m :: int begin
Fixrec [RS] r4 :: ‹int process› where r4_eq : ‹r4 = m → r4›
end
term ‹r4 :: int ⇒ int process›
text ‹Polymorphic locales:›
locale L3 = fixes e :: ‹'a›
begin
Fixrec [RS] r5 :: ‹'a process› where r5_eq : ‹r5 = e → r5›
end
text ‹In restriction spaces, ‹⊓ a ∈ A. _› preserves constructiveness for arbitrary ‹A›:
no finiteness assumption is needed (in contrast to the HOLCF instance).›
locale L2 = fixes A :: ‹int set›
begin
Fixrec [RS] r6 :: ‹int process› where r6_eq : ‹r6 = (⊓ a ∈ A. a → r6)›
end
chapter ‹Tests Moved from the Instance Theory (verbatim)›
section‹Test›
Fixrec [RS] g :: ‹'a ⇒ int process›
and h :: ‹'a ⇒ int process›
and j :: ‹'a ⇒ int process›
where a : ‹g = (λ x. □ a ∈ UNIV → g x)›
| b : ‹h = (λ x. 4 → j x)›
| c : ‹j = (λ x. 5 → h x)›
term g term h term j
thm g_h_j_rec_def g_h_j_rec_unfold g_def h_def j_def a b c g_h_j_induct
lemma g_h_j_induct' :
assumes * : ‹adm⇩↓ ( λ(g::'a ⇒ int process, h::'a ⇒ int process, j::'a ⇒ int process). P' g h j)›
and **: ‹P' g⇩0 h⇩0 j⇩0›
and ***: "(⋀g⇩0 h⇩0 j⇩0. P' g⇩0 h⇩0 j⇩0 ⟹ P' (λx. □ a ∈ UNIV → g⇩0 x)
(λ x. 4 → j⇩0 x)( λ x. 5 → h⇩0 x))"
shows‹P' g h j›
proof (rule def_restriction_fix_ind[OF g_h_j_rec_def,
where P = ‹λ(g, h, j). P' g h j›
and x = ‹(g⇩0,h⇩0,j⇩0)›,simplified, simplified case_prod_beta,
folded g_def h_def j_def, simplified] )
show ‹adm⇩↓ (λ(x, xa, y). P' x xa y)› by fact
next
show ‹P' g⇩0 h⇩0 j⇩0› by fact
next
from *** show ‹P' (fst x) (fst (snd x)) (snd (snd x)) ⟹
P' (λxa. □a∈UNIV → fst x xa)
(λxa. 4 → snd (snd x) xa)
(λxa. 5 → fst (snd x) xa)› for x by simp
qed
section‹Simulation and Tests›
ML‹
val t = @{term ‹g⇩0›}
val s = "g"^"⇩0"
›
lemma aux : "s ≡ s' ⟹ s' = t ⟹ s = t" by auto
lemma aux2: "s = s' ⟹ P s' = t ⟹ P s = t" by auto
lemma a' : ‹g = (λx. □ a ∈ UNIV → g x)›
thm g_def[THEN aux]
apply (rule g_def[THEN aux])
thm g_h_j_rec_unfold[THEN aux2]
apply (rule g_h_j_rec_unfold[THEN aux2])
apply (auto split: prod.split)
by (metis g_def fst_conv snd_conv)
lemma a'' : ‹g = (λx. □ a ∈ UNIV → g x)›
by(tactic ‹RS_instance.prove_projection [@{thm g_def},@{thm h_def},@{thm j_def}]
@{thm g_h_j_rec_unfold}
@{context}
@{thm g_def}›)
lemma b'' : ‹h = (λx. (4 :: int) → j x)›
by(tactic ‹RS_instance.prove_projection [@{thm g_def},@{thm h_def},@{thm j_def}]
@{thm g_h_j_rec_unfold}
@{context}
@{thm h_def}›)
lemma c'' : ‹j = (λ x. 5 → h x)›
by(tactic ‹RS_instance.prove_projection [@{thm g_def},@{thm h_def},@{thm j_def}]
@{thm g_h_j_rec_unfold}
@{context}
@{thm j_def}›)
lemma restriction_fix_eq_defined : ‹P = (υ X. f X) ⟹ constructive f ⟹ P = f P›
using restriction_fix_eq by blast
definition g_h_j' :: ‹('b ⇒ nat process) × ('b ⇒ nat process) × ('b ⇒ nat process)›
where ‹g_h_j' ≡ υ x. case x of
(g', h', j') ⇒ (λx. (3 :: nat) → g' x,
λ x. (4 :: nat) → j' x, λ x. 5 → h' x)›
definition g_h_j where ‹g_h_j ≡ υ (g, h, j). (λ x. □ a ∈ UNIV → g x,
λ x. 4 → j x,
λ x. 5 → h x)›
lemma g_h_j'_unfold : ‹g_h_j' = (case g_h_j' of
(g', h', j') ⇒ (λ x. 3 → g' x,
λ x. 4 → j' x,
λ x. 5 → h' x))›
apply (rule restriction_fix_eq_defined)
apply (fact g_h_j'_def[THEN meta_eq_to_obj_eq])
by auto
lemma [simp] : ‹constructive f ⟹ non_destructive (λx. f (x, y))›
by (simp add: constructive_prod_domain_iff)
end