Skip to content

Commit

Permalink
Have one Vrs operator per injection and (optionally) var type
Browse files Browse the repository at this point in the history
  • Loading branch information
@jvanbruegge
jvanbruegge committed Dec 12, 2024
1 parent 40559d4 commit 637e16f
Show file tree
Hide file tree
Showing 3 changed files with 133 additions and 142 deletions.
82 changes: 48 additions & 34 deletions Tools/bmv_monad_def.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@ signature BMV_MONAD_DEF = sig
Sb_comp: 'a,
Sb_cong: 'a,
(* TODO: Add Vrs_bd axiom *)
Vrs_Injs: 'a list, (* TODO: One per Inj AND var kind *)
Vrs_Sbs: 'a list
Vrs_Injs: 'a option list list,
Vrs_Sbs: 'a option list list
(* Add optional Map_Sb axiom (dependent on iff Map exists) *)
};

Expand All @@ -24,7 +24,7 @@ signature BMV_MONAD_DEF = sig
Injs: term list list,
Sbs: term list,
Maps: term option list,
Vrs: term list list,
Vrs: term option list list list,
tacs: (Proof.context -> tactic) bmv_monad_axioms list
}

Expand All @@ -37,7 +37,7 @@ signature BMV_MONAD_DEF = sig
val Injs_of_bmv_monad: bmv_monad -> term list list;
val Sbs_of_bmv_monad: bmv_monad -> term list;
val Maps_of_bmv_monad: bmv_monad -> term option list;
val Vrs_of_bmv_monad: bmv_monad -> term list list;
val Vrs_of_bmv_monad: bmv_monad -> term option list list list;

val morph_bmv_monad: morphism -> bmv_monad -> bmv_monad;

Expand All @@ -56,8 +56,8 @@ type 'a bmv_monad_axioms = {
Sb_comp_Injs: 'a list,
Sb_comp: 'a,
Sb_cong: 'a,
Vrs_Injs: 'a list,
Vrs_Sbs: 'a list
Vrs_Injs: 'a option list list,
Vrs_Sbs: 'a option list list
};

fun morph_bmv_axioms phi {
Expand All @@ -67,8 +67,8 @@ fun morph_bmv_axioms phi {
Sb_comp_Injs = map (Morphism.thm phi) Sb_comp_Injs,
Sb_comp = Morphism.thm phi Sb_comp,
Sb_cong = Morphism.thm phi Sb_cong,
Vrs_Injs = map (Morphism.thm phi) Vrs_Injs,
Vrs_Sbs = map (Morphism.thm phi) Vrs_Sbs
Vrs_Injs = map (map (Option.map (Morphism.thm phi))) Vrs_Injs,
Vrs_Sbs = map (map (Option.map (Morphism.thm phi))) Vrs_Sbs
} : thm bmv_monad_axioms

datatype bmv_monad = BMV of {
Expand All @@ -81,7 +81,7 @@ datatype bmv_monad = BMV of {
Injs: term list list,
Sbs: term list,
Maps: term option list,
Vrs: term list list (*list*), (* TODO: Need Vr operator per Injection *)
Vrs: term option list list list,
axioms: thm bmv_monad_axioms list
}

Expand All @@ -97,7 +97,7 @@ fun morph_bmv_monad phi (BMV {
Injs = map (map (Morphism.term phi)) Injs,
Sbs = map (Morphism.term phi) Sbs,
Maps = map (Option.map (Morphism.term phi)) Maps,
Vrs = map (map (Morphism.term phi)) Vrs,
Vrs = map (map (map (Option.map (Morphism.term phi)))) Vrs,
axioms = map (morph_bmv_axioms phi) axioms
}

Expand Down Expand Up @@ -127,11 +127,11 @@ type bmv_monad_model = {
Injs: term list list,
Sbs: term list,
Maps: term option list,
Vrs: term list list,
Vrs: term option list list list,
tacs: (Proof.context -> tactic) bmv_monad_axioms list
}

fun morph_bmv_monad_model phi { ops, bd, var_class, frees, lives, bmv_ops, leader, Injs, Sbs, Maps, Vrs, tacs } = {
fun morph_bmv_monad_model phi ({ ops, bd, var_class, frees, lives, bmv_ops, leader, Injs, Sbs, Maps, Vrs, tacs }: bmv_monad_model) = {
ops = map (Morphism.typ phi) ops,
bd = Morphism.term phi bd,
var_class = var_class,
Expand All @@ -142,7 +142,7 @@ fun morph_bmv_monad_model phi { ops, bd, var_class, frees, lives, bmv_ops, leade
Injs = map (map (Morphism.term phi)) Injs,
Sbs = map (Morphism.term phi) Sbs,
Maps = map (Option.map (Morphism.term phi)) Maps,
Vrs = map (map (Morphism.term phi)) Vrs,
Vrs = map (map (map (Option.map (Morphism.term phi)))) Vrs,
tacs = tacs
} : bmv_monad_model;

Expand All @@ -155,7 +155,8 @@ fun prove_axioms (model: bmv_monad_model) lthy =

val axioms = @{map 5} (fn T => fn Injs => fn Sb => fn Vrs => fn tacs =>
let
val (own_Injs, other_Injs) = partition (fn Inj => body_type (fastype_of Inj) = T) Injs;
val (own_Injs, other_Injs) = partition (fn Inj => member (op=) (#ops model) (body_type (fastype_of Inj))) Injs;
val is_own_Inj = map (member (op=) (#ops model) o body_type o fastype_of) Injs;
val other_idxs = map (fn Inj => find_index (fn T => body_type (fastype_of Inj) = T) Ts) other_Injs;
val ((((rhos, rhos'), aa), x), _) = lthy
|> mk_Frees "\<rho>" (map fastype_of Injs)
Expand Down Expand Up @@ -199,30 +200,42 @@ fun prove_axioms (model: bmv_monad_model) lthy =
))
)) (fn {context=ctxt, ...} => #Sb_comp tacs ctxt);

val Vrs_Injs = @{map 4} (fn Vrs => fn Inj => fn a => fn tac => Goal.prove_sorry lthy [] [] (
Logic.all a (mk_Trueprop_eq (Vrs $ (Inj $ a), mk_singleton a))
) (fn {context=ctxt, ...} => tac ctxt)) (take nown Vrs) own_Injs (take nown aa) (#Vrs_Injs tacs);

val Vrs_Sbs = map2 (fn Vr => fn tac => Goal.prove_sorry lthy [] [] (fold_rev Logic.all (rhos @ [x]) (
fold_rev (curry Logic.mk_implies) small_prems (mk_Trueprop_eq (
Vr $ (Term.list_comb (Sb, rhos) $ x),
foldl1 mk_Un (@{map_filter 2} (fn rho => Option.map (fn Vrs' => mk_UNION (Vr $ x) (
Term.abs ("a", HOLogic.dest_setT (snd (dest_funT (fastype_of Vrs')))) (
Vrs' $ (rho $ Bound 0)
)
))) rhos (map SOME (take nown Vrs) @ map (fn idx =>
List.find (fn t => body_type (fastype_of t) = body_type (fastype_of Vr)) (nth Vrss idx)
) other_idxs))
))
)) (fn {context=ctxt, ...} => tac ctxt)) Vrs (#Vrs_Sbs tacs);
val Vrs_Injs = @{map 3} (fn Inj => map2 (@{map_option 2} (fn tac => fn Vrs =>
let
val a = the (List.find (fn a => fastype_of a = hd (binder_types (fastype_of Inj))) aa);
val T = HOLogic.dest_setT (body_type (fastype_of Vrs));
in Goal.prove_sorry lthy [] [] (
Logic.all a (mk_Trueprop_eq (
Vrs $ (Inj $ a),
if fastype_of a = T then mk_singleton a else mk_bot T))
) (fn {context=ctxt, ...} => tac ctxt) end))) own_Injs (#Vrs_Injs tacs) (cond_keep Vrs is_own_Inj);

val Vrs_Sbs = @{map 3} (fn rho => map2 (@{map_option 2} (fn Vrs => fn tac =>
let
val var = HOLogic.dest_setT (body_type (fastype_of Vrs));
val idx = find_index (fn T => body_type (fastype_of rho) = T) Ts;
val idx' = find_index (fn t => fastype_of t = fastype_of rho) (nth Injss idx);
val Vrs' = hd (map_filter (Option.mapPartial (fn t =>
if HOLogic.dest_setT (body_type (fastype_of t)) = var then SOME t else NONE
)) (nth (nth Vrss idx) idx'));

val goal = fold_rev Logic.all (rhos @ [x]) (
fold_rev (curry Logic.mk_implies) small_prems (mk_Trueprop_eq (
Vrs $ (Term.list_comb (Sb, rhos) $ x),
mk_UNION (Vrs $ x) (Term.abs ("a", var) (Vrs' $ (rho $ Bound 0)))
))
);
in Goal.prove_sorry lthy [] [] goal (fn {context=ctxt, ...} => tac ctxt) end
))) rhos Vrs (#Vrs_Sbs tacs);

val Sb_cong = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (rhos @ rhos' @ [x]) (
fold_rev (curry Logic.mk_implies) (small_prems @ small_prems' @ @{map 4} (fn rho => fn rho' => fn Vrs => fn a =>
Logic.all a (Logic.mk_implies (
fold_rev (curry Logic.mk_implies) (small_prems @ small_prems' @ flat (@{map 3} (fn rho => fn rho' => map_filter (Option.map (fn Vrs =>
let val a = the (List.find (fn t => fastype_of t = HOLogic.dest_setT (body_type (fastype_of Vrs))) aa)
in Logic.all a (Logic.mk_implies (
HOLogic.mk_Trueprop (HOLogic.mk_mem (a, Vrs $ x)),
mk_Trueprop_eq (rho $ a, rho' $ a)
))
) rhos rhos' Vrs aa) (mk_Trueprop_eq (
)) end
))) rhos rhos' Vrs)) (mk_Trueprop_eq (
Term.list_comb (Sb, rhos) $ x,
Term.list_comb (Sb, rhos') $ x
)
Expand All @@ -247,6 +260,7 @@ fun bmv_monad_def inline_policy fact_policy qualify (model: bmv_monad_model) lth
fst (dest_ordLeq (HOLogic.dest_Trueprop (Thm.prop_of var_large)))
)));
in if bd' <> #bd model then error "var_class does not match bound" else () end

val frees = map (fn T => TFree (apsnd (
Sign.minimize_sort (Proof_Context.theory_of lthy) o cons (#var_class model)
) (dest_TFree T))) (#frees model);
Expand Down
11 changes: 11 additions & 0 deletions Tools/mrbnf_util.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -360,6 +360,7 @@ val parameter = Parse.position Parse.nat >> (fn (n, pos) =>

fun indices n = map string_of_int (1 upto n);
fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n));
fun some n = implode (map (fn a => " (SOME x" ^ a ^ ")") (indices n));
fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n));

in
Expand All @@ -373,6 +374,16 @@ val _ = Theory.setup
\ | map_filter f" ^ cons n ^ " = let val ys = map_filter f" ^ vars "xs" n ^ " in the_default ys (Option.map (fn y => y::ys) (f" ^ vars "x" n ^ ")) end\n\
\ | map_filter _" ^ replicate_string n " _" ^ " = raise ListPair.UnequalLengths\n" ^
" in map_filter f end")))

val _ = Theory.setup
(ML_Antiquotation.value \<^binding>\<open>map_option\<close>
(Scan.lift parameter >> (fn n =>
"fn f =>\n\
\ let\n\
\ fun map_option _" ^ replicate_string n " NONE" ^ " = NONE\n\
\ | map_option f" ^ some n ^ " = SOME (f" ^ vars "x" n ^ ")\n\
\ | map_option _" ^ replicate_string n " _" ^ " = raise ListPair.UnequalLengths\n" ^
" in map_option f end")))
end;

end;
Loading

0 comments on commit 637e16f

Please sign in to comment.