Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@jvanbruegge
jvanbruegge committed Nov 1, 2024
1 parent a2910b8 commit 334c5e4
Show file tree
Hide file tree
Showing 2 changed files with 157 additions and 40 deletions.
163 changes: 144 additions & 19 deletions Tools/mrbnf_fp.ML
View file
Original file line number Diff line number Diff line change
Expand Up @@ -558,12 +558,12 @@ fun construct_binder_fp fp_kind mrbnf_ks binding_relation lthy =

fun nonempty f xs = case xs of [] => I | _ => f xs

val FVars_raw_introsss = @{map 7} (fn rec_sets => fn raw => fn x =>
fun mk_FVars_introsss rec_setss ctors xs fsetss bound_setsss bfree_setsss FVarsss tac = @{map 7} (fn rec_sets => fn ctor => fn x =>
@{map 8} (fn a => fn bfree_boundss => fn rec_boundss => fn FVarss => fn fset => fn bsets => fn bfsets => fn FVars =>
let
val mem = HOLogic.mk_Trueprop o HOLogic.mk_mem
val not_mem = HOLogic.mk_Trueprop o HOLogic.mk_not o HOLogic.mk_mem
val concl = mem (a, fst FVars $ (#ctor raw $ x));
val concl = mem (a, fst FVars $ (ctor $ x));
val goals = Logic.mk_implies (mem (a, fset $ x), concl)
:: map2 (fn bfset => fn bfree_bounds => fold_rev (curry Logic.mk_implies) [
mem (a, bfset $ x), not_mem (a, foldl1 mk_Un (map (fn i => nth bsets i $ x) bfree_bounds))
Expand All @@ -573,27 +573,35 @@ fun construct_binder_fp fp_kind mrbnf_ks binding_relation lthy =
nonempty (fn xs => cons (not_mem (a, foldl1 mk_Un (map (fn i => nth bsets i $ x) xs)))) rec_bounds []
) concl
) rec_sets (replicate_rec FVarss) rec_boundss (replicate_rec raw_zs);
in map (fn goal => Goal.prove_sorry lthy (names (a::x::zs)) [] goal (fn {context=ctxt, ...} => EVERY1 [
K (Local_Defs.unfold0_tac ctxt (@{thm mem_Collect_eq} :: maps (map snd) FVars_rawss)),
eresolve_tac ctxt (maps #intrs is_freess),
REPEAT_DETERM o assume_tac ctxt
])) goals end
) aa bfree_boundsss rec_boundsss (transpose FVars_rawss)
) raw_rec_setss raw_Ts raw_xs raw_fsetss raw_bound_setsss raw_bfree_setsss FVars_rawss;

val FVars_raw_ctorss = @{map 7} (fn rec_sets => fn raw => fn x =>
@{map 8} (fn bfree_boundss => fn rec_boundss => fn FVarss => fn is_frees => fn fset => fn bsets => fn bfsets => fn FVars =>
let
val goal = mk_Trueprop_eq (fst FVars $ (#ctor raw $ x), foldl1 mk_Un (fset $ x ::
in map (fn goal => Goal.prove_sorry lthy (names (a::x::zs)) [] goal (fn {context=ctxt, ...} => tac ctxt)) goals end
) aa bfree_boundsss rec_boundsss (transpose FVarsss)
) rec_setss ctors xs fsetss bound_setsss bfree_setsss FVarsss;

val FVars_raw_introsss = mk_FVars_introsss raw_rec_setss (map #ctor raw_Ts) raw_xs raw_fsetss raw_bound_setsss raw_bfree_setsss FVars_rawss
(fn ctxt => EVERY1 [
K (Local_Defs.unfold0_tac ctxt (@{thm mem_Collect_eq} :: maps (map snd) FVars_rawss)),
eresolve_tac ctxt (maps #intrs is_freess),
REPEAT_DETERM o assume_tac ctxt
]);

fun mk_FVars_ctor_goalss rec_setss ctors xs fsetss bound_setsss bfree_setsss FVarsss =
@{map 7} (fn rec_sets => fn ctor => fn x =>
@{map 7} (fn bfree_boundss => fn rec_boundss => fn FVarss => fn fset => fn bsets => fn bfsets => fn FVars =>
mk_Trueprop_eq (fst FVars $ (ctor $ x), foldl1 mk_Un (fset $ x ::
map2 (fn bfset => fn bfree_bounds =>
mk_minus (bfset $ x, foldl1 mk_Un (map (fn i => nth bsets i $ x) bfree_bounds))
) bfsets bfree_boundss
@ @{map 3} (fn rec_set => fn FVars => fn rec_bounds =>
nonempty (fn xs => fn t => mk_minus (t, foldl1 mk_Un (map (fn i => nth bsets i $ x) xs))) rec_bounds
(mk_UNION (rec_set $ x) (fst FVars))
) rec_sets (replicate_rec FVarss) rec_boundss
));
val m = 1 + nrecs + length bfsets;
))
) bfree_boundsss rec_boundsss (transpose FVarsss)
) rec_setss ctors xs fsetss bound_setsss bfree_setsss FVarsss;

val FVars_raw_ctorss = @{map 4} (fn raw => fn x =>
@{map 4} (fn FVarss => fn is_frees => fn bfsets => fn goal =>
let val m = 1 + nrecs + length bfsets;
in Goal.prove_sorry lthy (names [x]) [] goal (fn {context=ctxt, ...} => EVERY1 [
K (Local_Defs.unfold_tac ctxt (map snd FVarss)),
rtac ctxt @{thm subset_antisym},
Expand Down Expand Up @@ -625,8 +633,8 @@ fun construct_binder_fp fp_kind mrbnf_ks binding_relation lthy =
REPEAT_DETERM o assume_tac ctxt
]
]) end
) bfree_boundsss rec_boundsss (transpose FVars_rawss) is_freess
) raw_rec_setss raw_Ts raw_xs raw_fsetss raw_bound_setsss raw_bfree_setsss FVars_rawss;
) (transpose FVars_rawss) is_freess
) raw_Ts raw_xs raw_bfree_setsss (mk_FVars_ctor_goalss raw_rec_setss (map #ctor raw_Ts) raw_xs raw_fsetss raw_bound_setsss raw_bfree_setsss FVars_rawss);

val FVars_raw_permute_leqss = transpose (@{map 6} (fn FVarss => fn is_frees => fn a => fn f => fn bfsets => fn FVars_ctors =>
let
Expand Down Expand Up @@ -1745,7 +1753,124 @@ fun construct_binder_fp fp_kind mrbnf_ks binding_relation lthy =
]) end
) permutes ctors xs mrbnfs deadss TT_total_abs_eq_iffs alpha_bij_eq_invs;

val _ = @{print} permute_simps
val permute_id0s = map2 (fn permute => fn quot =>
Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (
Term.list_comb (fst permute, map (HOLogic.id_const o fst o Term.dest_funT o fastype_of) fs),
HOLogic.id_const (#abs_type (fst quot))
)) (fn {context=ctxt, ...} => EVERY [
Local_Defs.unfold_tac ctxt (snd permute :: raw_permute_ids @ TT_abs_reps),
Local_Defs.unfold_tac ctxt @{thms id_def[symmetric]},
HEADGOAL (rtac ctxt refl)
])
) permutes quots;

val permute_ids = map (fn thm => trans OF [fun_cong OF [thm], @{thm id_apply}]) permute_id0s;

val permute_comp0s = @{map 4} (fn permute => fn permute_raw_comp => fn TT_total_abs_eq_iff => fn alpha_bij_eq =>
Goal.prove_sorry lthy (names (fs @ gs)) (f_prems @ g_prems) (mk_Trueprop_eq (
HOLogic.mk_comp (Term.list_comb (fst permute, gs), Term.list_comb (fst permute, fs)),
Term.list_comb (fst permute, map2 (curry HOLogic.mk_comp) gs fs)
)) (fn {context=ctxt, prems} => EVERY1 [
rtac ctxt ext,
rtac ctxt @{thm trans[OF comp_apply]},
K (Local_Defs.unfold_tac ctxt [snd permute]),
EqSubst.eqsubst_tac ctxt [0] [permute_raw_comp RS sym],
REPEAT_DETERM o resolve_tac ctxt prems,
rtac ctxt (iffD2 OF [TT_total_abs_eq_iff]),
rtac ctxt (iffD2 OF [alpha_bij_eq]),
REPEAT_DETERM o resolve_tac ctxt prems,
resolve_tac ctxt TT_rep_abss
])
) permutes raw_permute_comps TT_total_abs_eq_iffs alpha_bij_eqs;

val permute_comps = map (fn thm => @{thm trans[OF comp_apply[symmetric]]} OF [fun_cong OF [thm]]) permute_comp0s;

val permute_bijs = map (fn permute => Goal.prove_sorry lthy (names fs) f_prems (HOLogic.mk_Trueprop (
mk_bij (Term.list_comb (fst permute, fs))
)) (fn {context=ctxt, prems} => EVERY1 [
rtac ctxt @{thm iffD2[OF bij_iff]},
rtac ctxt exI,
rtac ctxt conjI,
rtac ctxt trans,
resolve_tac ctxt permute_comp0s,
K (prefer_tac (4 * nvars + 1)),
REPEAT_DETERM o EVERY' [
EqSubst.eqsubst_tac ctxt [0] @{thms inv_o_simp1},
resolve_tac ctxt prems
],
resolve_tac ctxt permute_id0s,
REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems),
rtac ctxt trans,
resolve_tac ctxt permute_comp0s,
REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems),
REPEAT_DETERM o EVERY' [
EqSubst.eqsubst_tac ctxt [0] @{thms inv_o_simp2},
resolve_tac ctxt prems
],
resolve_tac ctxt permute_id0s
])) permutes;

val permute_inv_simps = map (fn permute => Goal.prove_sorry lthy (names fs) f_prems (mk_Trueprop_eq (
mk_inv (Term.list_comb (fst permute, fs)),
Term.list_comb (fst permute, map mk_inv fs)
)) (fn {context=ctxt, prems} => REPEAT_DETERM (EVERY1 [
TRY o rtac ctxt @{thm inv_unique_comp},
rtac ctxt trans,
resolve_tac ctxt permute_comp0s,
REPEAT_DETERM o resolve_tac ctxt (@{thms supp_inv_bound bij_imp_bij_inv} @ prems),
REPEAT_DETERM o EVERY' [
EqSubst.eqsubst_tac ctxt [0] @{thms inv_o_simp1 inv_o_simp2},
resolve_tac ctxt prems
],
resolve_tac ctxt permute_id0s
]))) permutes;

fun mk_bd_thms f_bd raw_thms = map2 (fn z => map_index (fn (i, FVars) => Goal.prove_sorry lthy (names [z]) [] (HOLogic.mk_Trueprop (
mk_ordLess (mk_card_of (fst FVars $ z)) (f_bd i)
)) (fn {context=ctxt, ...} =>
Local_Defs.unfold0_tac ctxt [snd FVars] THEN HEADGOAL (resolve_tac ctxt raw_thms)
))) zs FVarsss;

val FVars_bds = mk_bd_thms (K (MRBNF_Def.bd_of_mrbnf (hd mrbnfs))) (flat FVars_raw_bds);
val FVars_bd_UNIVs = mk_bd_thms (fn i =>
mk_card_of (HOLogic.mk_UNIV (fst (Term.dest_funT (fastype_of (nth fs i)))))
) (flat FVars_raw_bd_UNIVs);

val FVars_permutess = @{map 5} (fn z => fn permute => @{map 4} (fn f => fn FVars => fn alpha_FVars => fn FVars_raw_permute =>
Goal.prove_sorry lthy (names (fs @ [z])) f_prems (mk_Trueprop_eq (
fst FVars $ (Term.list_comb (fst permute, fs) $ z),
mk_image f $ (fst FVars $ z)
)) (fn {context=ctxt, prems} => EVERY1 [
K (Local_Defs.unfold_tac ctxt [snd permute, snd FVars]),
rtac ctxt trans,
rtac ctxt alpha_FVars,
resolve_tac ctxt TT_rep_abss,
rtac ctxt (FVars_raw_permute OF prems)
])
) fs) zs permutes FVarsss alpha_FVarss FVars_raw_permutes;

val setss = mk_setss (map (#abs_type o fst) quots);
val (fsetss, bound_setsss, bfree_setsss, rec_setss) = split_setss setss;

val FVars_ctorss = @{map 6} (fn x => fn ctor => fn mrbnf => @{map 3} (fn alpha_FVars => fn FVars_ctor => fn goal =>
Goal.prove_sorry lthy (names [x]) [] goal (fn {context=ctxt, ...} => EVERY1 [
K (Local_Defs.unfold_tac ctxt (snd ctor :: maps (map snd) FVarsss)),
rtac ctxt trans,
rtac ctxt alpha_FVars,
resolve_tac ctxt TT_rep_abss,
rtac ctxt trans,
rtac ctxt FVars_ctor,
REPEAT_DETERM o EVERY' [
EqSubst.eqsubst_tac ctxt [0] (MRBNF_Def.set_map_of_mrbnf mrbnf),
REPEAT_DETERM o resolve_tac ctxt @{thms supp_id_bound bij_id}
],
K (Local_Defs.unfold0_tac ctxt @{thms image_id image_comp[unfolded comp_def]}),
rtac ctxt refl
])
)) xs ctors mrbnfs alpha_FVarss FVars_raw_ctorss
(mk_FVars_ctor_goalss rec_setss (map fst ctors) xs fsetss bound_setsss bfree_setsss FVarsss)

val _ = @{print} FVars_ctorss
in error "foo" end

end
34 changes: 13 additions & 21 deletions operations/Least_Fixpoint.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4737,7 +4737,6 @@ lemma permute_simps:
(* END REPEAT_DETERM *)
done


lemma permute_id0s:
"permute_T1 id id = id"
"permute_T2 id id = id"
Expand All @@ -4748,14 +4747,16 @@ lemma permute_id0s:

lemmas permute_ids = trans[OF fun_cong[OF permute_id0s(1)] id_apply] trans[OF fun_cong[OF permute_id0s(2)] id_apply]

lemma permute_comps:
lemma permute_comp0s:
fixes f1::"'a::{var_T1_pre,var_T2_pre} \<Rightarrow> 'a" and f2::"'b::{var_T1_pre,var_T2_pre} \<Rightarrow> 'b"
and g1::"'a::{var_T1_pre,var_T2_pre} \<Rightarrow> 'a" and g2::"'b::{var_T1_pre,var_T2_pre} \<Rightarrow> 'b"
assumes "bij f1" "|supp f1| <o |UNIV::'a set|" "bij f2" "|supp f2| <o |UNIV::'b set|"
and "bij g1" "|supp g1| <o |UNIV::'a set|" "bij g2" "|supp g2| <o |UNIV::'b set|"
shows
"permute_T1 g1 g2 (permute_T1 f1 f2 x) = permute_T1 (g1 \<circ> f1) (g2 \<circ> f2) x"
"permute_T2 g1 g2 (permute_T2 f1 f2 x2) = permute_T2 (g1 \<circ> f1) (g2 \<circ> f2) x2"
"permute_T1 g1 g2 \<circ> permute_T1 f1 f2 = permute_T1 (g1 \<circ> f1) (g2 \<circ> f2)"
"permute_T2 g1 g2 \<circ> permute_T2 f1 f2 = permute_T2 (g1 \<circ> f1) (g2 \<circ> f2)"
apply (rule ext)
apply (rule trans[OF comp_apply])
apply (unfold permute_T1_def permute_T2_def)
apply (subst permute_raw_comps[symmetric])
apply (rule assms)+
Expand All @@ -4764,6 +4765,9 @@ lemma permute_comps:
apply (rule assms)+
apply (rule TT_rep_abs)
(* second goal, same tactic *)
apply (rule ext)
apply (rule trans[OF comp_apply])
apply (unfold permute_T1_def permute_T2_def)?
apply (subst permute_raw_comps[symmetric])
apply (rule assms)+
apply (rule TT_total_abs_eq_iffs[THEN iffD2])
Expand All @@ -4772,21 +4776,9 @@ lemma permute_comps:
apply (rule TT_rep_abs)
done

lemma permute_comp0s:
fixes f1::"'a::{var_T1_pre,var_T2_pre} \<Rightarrow> 'a" and f2::"'b::{var_T1_pre,var_T2_pre} \<Rightarrow> 'b"
and g1::"'a::{var_T1_pre,var_T2_pre} \<Rightarrow> 'a" and g2::"'b::{var_T1_pre,var_T2_pre} \<Rightarrow> 'b"
assumes "bij f1" "|supp f1| <o |UNIV::'a set|" "bij f2" "|supp f2| <o |UNIV::'b set|"
and "bij g1" "|supp g1| <o |UNIV::'a set|" "bij g2" "|supp g2| <o |UNIV::'b set|"
shows
"permute_T1 g1 g2 \<circ> permute_T1 f1 f2 = permute_T1 (g1 \<circ> f1) (g2 \<circ> f2)"
"permute_T2 g1 g2 \<circ> permute_T2 f1 f2 = permute_T2 (g1 \<circ> f1) (g2 \<circ> f2)"
apply (rule ext)
apply (rule trans[OF comp_apply])
apply (rule permute_comps[OF assms])
apply (rule ext)
apply (rule trans[OF comp_apply])
apply (rule permute_comps[OF assms])
done
lemmas permute_comps =
trans[OF comp_apply[symmetric] fun_cong[OF permute_comp0s(1)]]
trans[OF comp_apply[symmetric] fun_cong[OF permute_comp0s(2)]]

lemma permute_bijs:
fixes f1::"'a::{var_T1_pre,var_T2_pre} \<Rightarrow> 'a" and f2::"'b::{var_T1_pre,var_T2_pre} \<Rightarrow> 'b"
Expand Down Expand Up @@ -4879,8 +4871,8 @@ lemma FVars_bd_UNIVs:
"|FVars_T22 x2| <o |UNIV::'b set|"
apply (unfold FVars_defs)
apply (rule FVars_raw_bd_UNIVs)+
done

done
lemma FVars_permutes:
fixes f1::"'a::{var_T1_pre,var_T2_pre} \<Rightarrow> 'a" and f2::"'b::{var_T1_pre,var_T2_pre} \<Rightarrow> 'b"
and x::"('a::{var_T1_pre,var_T2_pre}, 'b::{var_T1_pre,var_T2_pre}, 'c::{var_T1_pre,var_T2_pre}, 'd) T1"
Expand Down

0 comments on commit 334c5e4

Please sign in to comment.