Theory GenFixrec-RS
chapter ‹Instantiation of the Generic Fixrec Package for Restriction-Spaces›
theory "GenFixrec-RS"
imports "HOL-CSP.GenFixrec"
"HOL-CSP_RS"
begin
default_sort type
subsection‹Example setup›
lemma def_constructive_fix_eq :
‹f ≡ (υ x. F x) ⟹ constructive F ⟹ f = F f›
by(simp, rule restriction_fix_eq,simp)
text ‹Case distinctions on conditions not depending on the recursion variable (the rules of
\<^session>‹Restriction_Spaces› state the condition as ‹P x›, which the simplifier cannot match):›
lemma non_destructive_if [simp] :
‹(b ⟹ non_destructive f)
⟹ (¬ b ⟹ non_destructive g)
⟹ non_destructive (λx. if b then f x else g x)›
by (cases b) simp_all
lemma constructive_if [simp] :
‹(b ⟹ constructive f)
⟹ (¬ b ⟹ constructive g)
⟹ constructive (λx. if b then f x else g x)›
by (cases b) simp_all
text ‹The rules on the constructiveness of \<^const>‹Throw›, in particular in its continuation
(@{thm [source] ThrowR_constructive}, @{thm [source] Throw_constructive_continuation}), are in
@{theory "HOL-CSP_RS.Throw_Non_Destructive"}; the constructiveness proofs of the RS instance use:›
declare Throw_constructive_continuation [simp]
lemma def_restriction_fix_ind :
"⟦f ≡ υ x. F x; constructive F; adm⇩↓ P; P x; ⋀x. P x ⟹ P (F x)⟧ ⟹ P f"
by (simp add: restriction_fix_ind)
ML‹
structure RS_instance =
struct
local open GenFixrec in
val E = @{term "restriction_fix"};
val a_ty = (snd o dest_funT o fastype_of) E;
fun mk_rs_fix [] E = let val a_ty = (fst o dest_funT o fastype_of) E
in Const (\<^const_name>‹complete_restriction_space_class.restriction_fix›,
(a_ty --> a_ty) --> a_ty)
$ E
end
fun dest_rs_fix (Const (\<^const_name>‹complete_restriction_space_class.restriction_fix›, t) $ E) = E
fun set_context_fix ctxt = ctxt |> fold Splitter.add_split @{thms prod.split}
|> fold Simplifier.add_simp [@{thm case_prod_beta}]
val def_rs_fix_eq = @{thm "def_constructive_fix_eq"}
val aux = (Goal.prove_global @{theory} [] []
(@{prop ‹s ≡ s' ⟹ s' = t ⟹ s = t›})
(fn {context,...} =>auto_tac context))
val aux2 = (Goal.prove_global @{theory} [] []
(@{prop ‹s = s' ⟹ P s' = t ⟹ P s = t›})
(fn {context,...} =>auto_tac context))
val fst_conv = @{thm "fst_conv"}
val snd_conv = @{thm "snd_conv"}
val add_prod_splits = fold Splitter.add_split @{thms prod.split};
fun metis_step ctxt defs = Metis_Tactic.metis_tac [] "combs"
ctxt (fst_conv :: snd_conv :: defs)
val aux2' = meta_eq_to_obj_eq RS aux2
fun prove_projection defs unfold ctxt def =
structural_projection_tac defs unfold ctxt def
ORELSE
EVERY [resolve0_tac [def RS aux2'] 1,
resolve0_tac [unfold RS aux2] 1,
auto_tac (add_prod_splits ctxt),
TRY (metis_step ctxt defs 1)]
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 vars_proj = map (fn((s,t,_),_) => Var((Binding.name_of s,0),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 frees'' = map (fn (Free(s,_),t) => Var((s^"0",0),t)) (frees ~~ prodT')
val tuple_witness = HOLogic.mk_tuple frees''
val P' = list_comb (Var((P^"'",idx),prodT' ---> boolT), frees')
val proJT' = tupled_lambda (mk_tuple frees') P'
val subst = Vars.make2(((P,idx),ty'), Thm.cterm_of ctxt proJT')
((("x",0),domain_type ty'), Thm.cterm_of ctxt tuple_witness);
in thm |> Thm.instantiate(TVars.empty,subst) end
end
val def_restriction_fix_ind = @{thm def_restriction_fix_ind}
fun add_case_prod_beta ctxt = Simplifier.add_simp @{thm case_prod_beta} ctxt
val rs = {mk_fix = mk_rs_fix,
dest_fix = dest_rs_fix,
lambda' = HOLogic.tupled_lambda,
apply = Bound 0,
shift_tac = (fn {context,...} => all_tac),
fix_tac = (fn {context,prems} =>
resolve0_tac [hd prems RS def_rs_fix_eq] 1
THEN (SOLVED' (asm_full_simp_tac (set_context_fix context)) 1
ORELSE auto_tac (set_context_fix context))),
proj_tac = (fn {proj_def, projs, unfold} =>
fn {context,prems} => prove_projection projs unfold context proj_def),
fixind_tac = (fn {eqns, varstab, projs, rec_def, unfold} =>
fn {context,prems} => ((rec_def RS def_restriction_fix_ind)
|> substitute_curried_pred context varstab
|> Simplifier.asm_full_simplify
(add_case_prod_beta context)
|> Local_Defs.fold context projs
|> Simplifier.asm_full_simplify context
))
} : language;
fun define_rs_space thy = Context.Theory thy
|> update_language (Binding.make("RS",@{here})) rs
|> Context.the_theory;
end
end
›
setup ‹RS_instance.define_rs_space›
end