Theory Fixrec_HOLCF
chapter ‹The HOLCF Instance of ▩‹Fixrec››
theory Fixrec_HOLCF
imports "GenFixrec-HOLCF"
begin
section‹The Instance Setup›
text ‹The tests are organised by concept; currently, there are instances of the generic Fixrec
package for Scott-Spaces (formalised in the library session HOLCF) and Restriction Spaces (RS).
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 HOLCF_instance.holcf, dest_fix = #dest_fix HOLCF_instance.holcf, lambda' = #lambda' HOLCF_instance.holcf,
apply = #apply HOLCF_instance.holcf, shift_tac = #shift_tac HOLCF_instance.holcf, fix_tac = K no_tac,
proj_tac = #proj_tac HOLCF_instance.holcf, fixind_tac = #fixind_tac HOLCF_instance.holcf}
|> Context.the_theory›
text ‹Without brackets, ‹HOLCF› is the default:›
Fixrec l1 :: ‹int process› where l1_eq : ‹l1 = 1 → l1›
text ‹Explicit selection:›
Fixrec [HOLCF] 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, HOLCF] l3 :: ‹int process› where l3_eq : ‹l3 = 3 → l3›
ML ‹
val proc = "int process"
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 ["holcf"] [("e3", proc)] [("e3_eq", "e3 = 1 → e3")]
"Undefined Fixrec language: \"holcf\""
val _ = expect_failure [] [("e4", proc)] [("e4_eq", "e4 = 1 → e4")]
"no language given"
›
section ‹Unshifted Equations›
text ‹The classical form ‹c = E›, with explicit abstractions on the right-hand side:›
Fixrec u1 :: ‹int ⇒ int process› where u1_eq : ‹u1 = (λx. x → u1 (x+1))›
Fixrec u2 :: ‹int → int process› where u2_eq : ‹u2 = (Λ x. x → u2⋅(x+1))›
section ‹Generic Shift over HOL Application›
text ‹Arguments on the left-hand side are shifted to abstractions on the right-hand side by the
core, independently of the language: single and curried arguments, tuples, curried tuples.›
Fixrec s1 :: ‹int ⇒ int process› where s1_eq : ‹s1 x = x → s1 (x+1)›
Fixrec s2 :: ‹int ⇒ nat ⇒ int process› where s2_eq : ‹s2 x n = x → s2 (x+1) (Suc n)›
Fixrec s3 :: ‹int × nat ⇒ int process› where s3_eq : ‹s3 (x,n) = x → s3 (x+1,n)›
Fixrec s4 :: ‹int × int × int ⇒ int process› where s4_eq : ‹s4 (x,y,z) = x → s4 (y,z,x)›
Fixrec 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 ["HOLCF"] [("e5", "int ⇒ int process")] [("e5_eq", "e5 0 = 0 → e5 0")]
"args must be free variables or tuples of them"
val _ = expect_failure ["HOLCF"] [("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: HOLCF Application and Abstraction›
text ‹HOLCF comes with its own function space ‹→› and the pair ‹f⋅x› / ‹Λ x. E›.
Shifting over ‹⋅› produces ‹Λ›-abstractions (‹lambda'› of the language); it can be mixed
with the generic shift over HOL application.›
Fixrec c1 :: ‹int → int process› where c1_eq : ‹c1⋅x = x → c1⋅(x+1)›
Fixrec c2 :: ‹int → int → int process› where c2_eq : ‹c2⋅x⋅y = x → c2⋅y⋅x›
Fixrec c3 :: ‹int × int → int process› where c3_eq : ‹c3⋅(x,y) = x → c3⋅(y,x)›
Fixrec c4 :: ‹int × int × int → int process› where c4_eq : ‹c4⋅(x,y,z) = x → c4⋅(y,z,x)›
Fixrec c5 :: ‹nat ⇒ int → int process› where c5_eq : ‹c5 n⋅x = x → c5 (Suc n)⋅(x+1)›
Fixrec c6 :: ‹int ⇒ nat × bool ⇒ int × int → int process›
where c6_eq : ‹c6 k (n,b)⋅(x,y) = x → c6 k (n,b)⋅(y,x+k)›
text ‹The shift is equivalent to the unshifted form:›
lemma ‹c1 = (Λ x. x → c1⋅(x+1))› by (rule cfun_eqI, subst c1_eq, simp)
section ‹Mutual Recursion›
Fixrec 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)›
text ‹Mixing shifted and unshifted equations, functions and constants:›
Fixrec m3 :: ‹int ⇒ int process› and m4 :: ‹int process›
where m3_eq : ‹m3 x = x → m4›
| m4_eq : ‹m4 = 0 → m3 1›
text ‹Mixing both function spaces:›
Fixrec m5 :: ‹int → int process› and m6 :: ‹int ⇒ int process›
where m5_eq : ‹m5⋅x = 1 → m6 x›
| m6_eq : ‹m6 x = 2 → m5⋅(x+1)›
text ‹Equations that are not (self-)recursive, alone or within a system:›
Fixrec n1 :: ‹int ⇒ int process› where n1_eq : ‹n1 x = x → Skip›
Fixrec 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 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)›
section ‹Polymorphism›
Fixrec p1 :: ‹'a ⇒ 'a process› where p1_eq : ‹p1 x = x → p1 x›
text ‹Mutually recursive equations must share their type variables:›
Fixrec 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›
text ‹For an equation system ‹c⇩1 … c⇩n›, ▩‹Fixrec› generates the fixpoint definition
‹c⇩1_…_c⇩n_rec_def›, its unfolding ‹c⇩1_…_c⇩n_rec_unfold›, the projections ‹c⇩i_def›, the
equations under their given names (exactly in the stated form) and a fixpoint induction
rule ‹c⇩1_…_c⇩n_induct›.›
thm m1_m2_rec_def m1_m2_rec_unfold m1_def m2_def m1_eq m2_eq m1_m2_induct
lemma ‹c6 k (n,b)⋅(x,y) = x → c6 k (n,b)⋅(y,x+k)› by (fact c6_eq)
lemma ‹s5 (x,n) (b,y) = x → s5 (y,Suc n) (¬b,x)› by (fact s5_eq)
text ‹Fixpoint induction over the HOLCF fixpoint: admissibility, base case ‹⊥›, step.›
ML ‹
val _ = @{assert} (Thm.nprems_of @{thm c1_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 sa :: ‹int ⇒ int process› where sa_eq : ‹sa x = x → Skip›
Fixrec 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 HOLCF, every continuous equation has a (least) solution, even an unguarded one;
here it is ‹⊥›:›
Fixrec d1 :: ‹int ⇒ int process› where d1_eq : ‹d1 x = d1 (x+1)›
lemma ‹d1 = ⊥›
by (induct rule: d1_induct) simp_all
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 r1 :: ‹int ⇒ int process›
where r1_eq : ‹r1 x = x → r1 (x + k)›
Fixrec 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 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 r5 :: ‹'a process› where r5_eq : ‹r5 = e → r5›
end
text ‹Locale assumptions are available in the proofs of the construction: ‹⊓ a ∈ A. _›
is only continuous (in HOLCF) for finite ‹A›.›
locale L2 = fixes A :: ‹int set› assumes finite_A [simp] : ‹finite A›
begin
Fixrec r6 :: ‹int process› where r6_eq : ‹r6 = (⊓ a ∈ A. a → r6)›
end
text ‹Without the assumption, the construction fails:›
ML ‹
val _ = expect_failure ["HOLCF"] [("e8", "int set ⇒ int process")]
[("e8_eq", "e8 A = (⊓ a ∈ A. a → e8 A)")] "no language succeeded"
›
chapter ‹Tests Moved from the Instance Theory (verbatim)›
section‹Tests›
fixrec f⇩1 :: ‹'a :: pcpo → 'a›
and g⇩1 :: ‹'a :: pcpo → 'a›
where ‹f⇩1 ⋅ n = g⇩1 ⋅ n›
| ‹g⇩1 ⋅ n = f⇩1 ⋅ n›
Fixrec g :: ‹'a::cpo ⇒ int process›
and h :: ‹('a → int process)›
and j :: ‹('a → int process)›
where a : ‹g = (λ x. 3 → g x)›
| b : ‹h = (Λ x. 4 → j ⋅ x)›
| c : ‹j = (Λ x. 5 → h ⋅ x)›
thm g_h_j_rec_def g_h_j_rec_unfold g_def h_def j_def a b c
thm g_h_j_induct[simplified , simplified case_prod_beta,
simplified, folded g_def h_def j_def]
text‹ Making recursive equation unnecessarily interdependent in an ▩‹Fixrec› definition is never
a good idea: Induction schemes tend to complicate things up to a point where they become unusable.
Another problem comes with polymorphism: mutual recursive equations can be polymorphic, but
they ❙‹must› contain all the same polymorphic variables (otherwise, the proof of the projections
will fail necessarily; the error-message is in these cases rather spurious.).
Try to replace the \<^typ>‹int› in the equations ‹hh› and ‹jj› in the following equation system
in order to see the problem.›
term‹ (AA ⋅ x) ⋅ (y,z)›
Fixrec [HOLCF] gg :: ‹(int × int) ⇒ (int list × bool) ⇒ int process›
and hh :: ‹int → (int × int) → int process›
and jj :: ‹int → int process›
where aa : ‹gg (x,y)(L,z) = x → gg (x+1,y-1)(x#L, - z)›
| bb : ‹(hh⋅x)⋅(y,z) = (4 → jj ⋅ x)›
| cc : ‹jj⋅x = (5 → hh ⋅ x ⋅ (x*x,x))›
thm aa bb cc
text‹Mixing one-ary arguments and tuples.›
Fixrec [HOLCF] ggg :: ‹(int × int) ⇒ (int list × bool) ⇒ int process›
and hhh :: ‹int → (tr × int) → int process›
and jjj :: ‹int → tr → int process›
where aaa : ‹ggg (x,y)(L,z) = x → ggg (x+1,y-1)(x#L, ¬ z)›
| bbb : ‹hhh⋅x⋅(y,z) = (4 → jjj⋅x⋅y)›
| ccc : ‹jjj⋅x⋅y = (5 → hhh⋅x⋅(neg⋅y,x))›
text‹Mixing total and continuous function spaces requires care: a ‹Λ›-abstraction is only a
proper continuous function if its body is continuous in the bound variable. In the following
system, ‹hhhh x = Λ(y,z). 4 → (jjjj⋅x) y› with ‹y :: tr› requires the ∗‹total› function
‹jjjj⋅x :: tr ⇒ int process› to be continuous on the non-discrete type \<^typ>‹tr›, which does not
hold in general; the continuity proof of the fixpoint construction fails (as it would for
HOLCF's ▩‹fixrec›). Over discrete argument types (see below), such mixtures are unproblematic.›
ML ‹
val _ = expect_failure ["HOLCF"]
[("g5", "(int × int) ⇒ (int list × bool) ⇒ int process"),
("h5", "int ⇒ ((tr × int) → int process)"),
("j5", "int → (tr ⇒ int process)")]
[("a5", "g5 (x,y)(L,z) = x → g5 (x+1,y-1)(x#L, ¬ z)"),
("b5", "(h5 x)⋅(y,z) = (4 → (j5⋅x) y)"),
("c5", "(j5⋅x) y = (5 → (h5 x)⋅(neg⋅y,x))")]
"cont"
›
text‹The same mixture over a discrete argument type:›
Fixrec [HOLCF] g4 :: ‹(int × int) ⇒ (int list × bool) ⇒ int process›
and h4 :: ‹(int ⇒ ((int × int) → int process))›
and j4 :: ‹(int → (int ⇒ int process))›
where a4 : ‹g4 (x,y)(L,z) = x → g4 (x+1,y-1)(x#L, ¬ z)›
| b4 : ‹(h4 x)⋅(y,z) = (4 → (j4 ⋅ x) y)›
| c4 : ‹(j4⋅x) y = (5 → (h4 x) ⋅ (- y,x))›
ML‹
fun prove_projection' defs unfold ctxt def =
EVERY [resolve0_tac [def RS HOLCF_instance.aux2'] 1,
resolve0_tac [unfold RS HOLCF_instance.aux2] 1,
auto_tac (HOLCF_instance.add_prod_splits ctxt),
HOLCF_instance.metis_step ctxt defs 1]
›
ML‹val prove_projection = HOLCF_instance.prove_projection›
lemma "gg (x,y)(L,z) = ( x → gg (x+1,y-1)(x#L, - z))" by (fact aa)
text‹The projection proof as performed by the package (structural: pair rules and refolding):›
lemma "gg (x,y)(L,z) = ( x → gg (x+1,y-1)(x#L, - z))"
by(tactic ‹prove_projection [@{thm gg_def},@{thm hh_def},@{thm jj_def}] @{thm gg_hh_jj_rec_unfold} @{context} @{thm gg_def} ›)
section‹Simulations (for Comprehension and Debugging)›
ML‹
local open HOLogic in
fun substitute_curried_pred ctxt vartab thm =
let val frees = map (fn((s,t,_),_) => Free(Binding.name_of s,t)) vartab;
val Var ((P, idx), ty') $ S = dest_Trueprop(Thm.concl_of thm);
val prodT'= strip_tupleT (domain_type ty')
val frees'= map (fn (Free(s,_),t) => Free(s,t)) (frees ~~ prodT')
val P' = list_comb (Var((P^"'",idx),prodT' ---> boolT), frees')
val proJT' = tupled_lambda (mk_tuple frees') P'
val subst = Vars.make1(((P,idx),ty'), Thm.cterm_of ctxt proJT');
in thm |> Thm.instantiate(TVars.empty,subst) end
end›
thm def_cont_fix_ind[OF g_h_j_rec_def,
where P = ‹λ(x, y, z). P' x y z›,
simplified, simplified case_prod_beta, simplified]
definition g_h_j_rec'
where "g_h_j_rec' ≡ μ x. case x of (g', h', j') ⇒ (λx. 3 → g' x, Λ x. 4 → j'⋅x, Λ x. 5 → h'⋅x)"
definition g' where "g' ≡ fst g_h_j_rec'"
definition h' where "h' ≡ fst (snd g_h_j_rec')"
lemma a' : "g = (λ x. 3 → g x)"
by(tactic ‹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 → j ⋅ x)"
by(tactic ‹prove_projection [@{thm g_def},@{thm h_def},@{thm j_def}]
@{thm g_h_j_rec_unfold}
@{context}
@{thm h_def}›)
lemma g_h_j_induct' :
assumes ** : ‹adm ( λ(g, h, j). P' g h j)›
and ***: ‹P' (⊥::'a::cpo ⇒ int process) (⊥::'a → int process) (⊥::'a → int process)›
and ****: "(⋀g h j. P' g h j ⟹ P' (λxa. 3 → g xa) (Λ xa. 4 → j⋅xa) (Λ xa. 5 → h⋅xa))"
shows‹P' g h j›
proof (rule def_cont_fix_ind[OF g_h_j_rec_def,
where P = ‹λ(x, y, z). P' x y z›,
simplified, simplified case_prod_beta,
simplified, folded g_def h_def j_def])
show ‹cont (λx. (λxa. 3 → fst x xa, Λ xa. 4 → snd (snd x)⋅xa, Λ xa. 5 → fst (snd x)⋅xa))›
by (simp add: prod_cont_iff cont_fun)
next
show ‹adm ( λ(g, h, j). P' g h j)› by fact
next
show ‹P' ⊥ ⊥ ⊥› by fact
next
from ****
show ‹P' (fst x) (fst (snd x)) (snd (snd x)) ⟹
P' (λxa. 3 → fst x xa) (Λ xa. 4 → snd (snd x)⋅xa) (Λ xa. 5 → fst (snd x)⋅xa)› for x
by simp
qed
end