Skip to content

Commit 6894628

Browse files
jvanbrueggejvanbruegge
committed
Revive old refreshability proofs
1 parent d2e05f9 commit 6894628

File tree

7 files changed

+106
-53
lines changed

7 files changed

+106
-53
lines changed

‎thys/POPLmark/SystemFSub.thy‎

Lines changed: 28 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -285,14 +285,34 @@ binder_inductive_split ty
285285
| ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
286286
| ((rule exI[of _ "rrename_typ \<sigma> _"])+, (rule conjI)?, rule in_context_eqvt))+
287287
subgoal premises prems for R B \<Gamma> T1 T2
288-
by (tactic \<open>refreshability_tac false
289-
[@{term "\<lambda>\<Gamma>. dom \<Gamma> \<union> FFVars_ctxt \<Gamma>"}, @{term "FFVars_typ :: type \<Rightarrow> var set"}, @{term "FFVars_typ :: type \<Rightarrow> var set"}]
290-
[@{term "rrename_typ :: (var \<Rightarrow> var) \<Rightarrow> type \<Rightarrow> type"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
291-
[NONE, NONE, NONE, NONE, SOME [NONE, NONE, NONE, SOME 1, SOME 0, SOME 0]]
292-
@{thm prems(3)} @{thm prems(2)} @{thms prems(1)[THEN ty_fresh_extend] id_onD}
293-
@{thms emp_bound insert_bound ID.set_bd Un_bound UN_bound typ.card_of_FFVars_bounds infinite_UNIV}
294-
@{thms typ_inject image_iff} @{thms typ.rrename_cong_ids context_map_cong_id map_idI}
295-
@{thms cong[OF cong[OF cong[OF refl[of R]] refl] refl, THEN iffD1, rotated -1] id_onD} @{context}\<close>)
288+
using prems
289+
unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
290+
apply (elim disj_forward exE; clarsimp)
291+
apply (((rule exI, rule conjI[rotated], assumption) |
292+
(((rule exI conjI)+)?, rule Forall_rrename) |
293+
(auto))+) []
294+
subgoal premises prems for T\<^sub>1 S\<^sub>1 x S\<^sub>2 T\<^sub>2
295+
using prems(3-)
296+
using exists_fresh[of "[x]" \<Gamma> T1 T2] apply(elim exE conjE)
297+
subgoal for z
298+
apply (rule exI)
299+
apply (rule exI[of _ "{z}"])
300+
apply (intro exI conjI)
301+
apply (rule refl)+
302+
apply (rule Forall_swap)
303+
apply simp
304+
apply (rule Forall_swap)
305+
apply simp
306+
apply assumption+
307+
apply (frule prems(1)[rule_format, of "(\<Gamma>, x <: T\<^sub>1)" "S\<^sub>2" "T\<^sub>2"])
308+
apply (drule prems(2)[rule_format, of "id(x := z, z := x)" "\<Gamma>, x <: T\<^sub>1" "S\<^sub>2" "T\<^sub>2", rotated 2])
309+
apply (auto simp: extend_eqvt)
310+
apply (erule cong[OF cong[OF cong], THEN iffD1, of R, OF refl, rotated -1]) back
311+
apply (drule ty_fresh_extend)
312+
apply (simp_all add: supp_swap_bound)
313+
by (metis (no_types, opaque_lifting) image_iff map_context_def map_context_swap_FFVars)
314+
done
315+
done
296316
done
297317

298318
end

‎thys/Pi_Calculus/Pi_Transition_Early.thy‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ binder_inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
3131
| (rule exI[of _ "rrename \<sigma> _"])
3232
| ((rule exI[of _ "\<sigma> _"])+; auto))+
3333
subgoal premises prems for R B P Q
34+
(* This is a prototype implemetation of the refreshability heuristic mentioned in sections 5 and 6. *)
3435
by (tactic \<open>refreshability_tac false
3536
[@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars_commit :: cmt \<Rightarrow> var set"}]
3637
[@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"},

‎thys/Pi_Calculus/Pi_Transition_Late.thy‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@ binder_inductive trans :: "trm \<Rightarrow> cmt \<Rightarrow> bool" where
1919
| (rule exI[of _ "map_action \<sigma> _"] exI[of _ "rrename \<sigma> _"])
2020
| ((rule exI[of _ "\<sigma> _"])+; auto))+
2121
subgoal premises prems for R B P Q
22+
(* This is a prototype implemetation of the refreshability heuristic mentioned in sections 5 and 6. *)
2223
by (tactic \<open>refreshability_tac false
2324
[@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars_commit :: cmt \<Rightarrow> var set"}]
2425
[@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"},

‎thys/Pi_Calculus/Pi_cong.thy‎

Lines changed: 30 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -24,15 +24,16 @@ binder_inductive cong :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<e
2424
(auto simp: isPerm_def term.rrename_comps
2525
| ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
2626
| ((rule exI[of _ "\<sigma> _"])+; auto))+
27-
subgoal premises prems for R B P Q
28-
by (tactic \<open>refreshability_tac false
29-
[@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
30-
[@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
31-
[NONE, NONE, NONE, NONE, SOME [SOME 1, SOME 1, SOME 0], SOME [SOME 1], NONE, SOME [SOME 1, SOME 0, SOME 0]]
32-
@{thm prems(3)} @{thm prems(2)} @{thms }
33-
@{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite_UNIV}
34-
@{thms Res_inject term.FFVars_rrenames} @{thms term.rrename_cong_ids[symmetric]}
35-
@{thms id_onD} @{context}\<close>)
27+
subgoal premises prems for R B x1 x2
28+
apply simp
29+
using fresh[of x1 x2] prems(2-) unfolding
30+
(**)isPerm_def conj_assoc[symmetric] split_beta
31+
unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
32+
apply (elim disj_forward exE; simp)
33+
apply ((rule exI, rule conjI[rotated], assumption) |
34+
(((rule exI conjI)+)?, rule Res_refresh) |
35+
(auto))+
36+
done
3637
done
3738

3839
thm cong.strong_induct
@@ -65,15 +66,26 @@ binder_inductive trans :: "trm \<Rightarrow> trm \<Rightarrow> bool" (infix "(\<
6566
| ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
6667
| ((rule exI[of _ "\<sigma> _"])+; auto))+
6768
by (metis cong.equiv bij_imp_inv' term.rrename_bijs term.rrename_inv_simps)
68-
subgoal premises prems for R B P Q
69-
by (tactic \<open>refreshability_tac false
70-
[@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
71-
[@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
72-
[SOME [NONE, NONE, NONE, SOME 1, SOME 0], NONE, SOME [SOME 0, SOME 0, SOME 1], NONE]
73-
@{thm prems(3)} @{thm prems(2)} @{thms }
74-
@{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite_UNIV}
75-
@{thms Res_inject Inp_inject term.FFVars_rrenames} @{thms Inp_eq_usub term.rrename_cong_ids[symmetric]}
76-
@{thms } @{context}\<close>)
69+
subgoal for R B x1 x2
70+
unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib ex_simps(1,2)[symmetric]
71+
ex_comm[where P = P for P :: "_ set \<Rightarrow> _ \<Rightarrow> _"]
72+
apply (elim disj_forward exE; simp; clarsimp)
73+
apply (auto simp only: fst_conv snd_conv term.set)
74+
subgoal for x z P y Q
75+
apply (rule exE[OF exists_fresh[of "[x, y, z]" P Q]])
76+
subgoal for w
77+
apply (rule exI[of _ w])
78+
apply simp
79+
by (meson Inp_refresh usub_refresh)
80+
done
81+
subgoal for x z P y Q
82+
apply (rule exE[OF exists_fresh[of "[x, y, z]" P Q]])
83+
subgoal for w
84+
apply (rule exI[of _ w])
85+
apply simp
86+
by (meson Inp_refresh usub_refresh)
87+
done
88+
done
7789
done
7890

7991
thm trans.strong_induct

‎thys/Untyped_Lambda_Calculus/LC_Beta.thy‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -23,15 +23,12 @@ binder_inductive step :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
2323
(auto simp: isPerm_def term.rrename_comps rrename_tvsubst_comp
2424
| ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
2525
| ((rule exI[of _ "\<sigma> _"])+; auto))+
26-
subgoal premises prems for R B t1 t2 \<comment> \<open>refreshability\<close>
27-
by (tactic \<open>refreshability_tac false
28-
[@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
29-
[@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
30-
[SOME [SOME 1, SOME 0, NONE], NONE, NONE, SOME [SOME 0, SOME 0, SOME 1]]
31-
@{thm prems(3)} @{thm prems(2)} @{thms }
32-
@{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite}
33-
@{thms Lam_inject} @{thms Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
34-
@{thms } @{context}\<close>)
26+
subgoal premises prems for R B x1 x2 \<comment> \<open>refreshability\<close>
27+
using fresh[of x1 x2] prems(2-) unfolding isPerm_def conj_assoc[symmetric] split_beta
28+
unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
29+
apply (elim disj_forward exE; simp)
30+
apply (metis Lam_eq_tvsubst Lam_inject_swap singletonD)
31+
by blast
3532
done
3633

3734
thm step.strong_induct step.equiv

‎thys/Untyped_Lambda_Calculus/LC_Beta_depth.thy‎

Lines changed: 6 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -23,15 +23,12 @@ binder_inductive stepD :: "nat \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow>
2323
(auto simp: isPerm_def term.rrename_comps rrename_tvsubst_comp
2424
| ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
2525
| ((rule exI[of _ "\<sigma> _"])+; auto))+
26-
subgoal premises prems for R B d t1 t2
27-
by (tactic \<open>refreshability_tac false
28-
[@{term "(\<lambda>_. {}) :: nat \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
29-
[@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
30-
[SOME [SOME 1, SOME 0, NONE], NONE, NONE, SOME [NONE, SOME 0, SOME 0, SOME 1]]
31-
@{thm prems(3)} @{thm prems(2)} @{thms }
32-
@{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite}
33-
@{thms Lam_inject} @{thms Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
34-
@{thms } @{context}\<close>)
26+
subgoal premises prems for R B x1 x2 x3
27+
using fresh[of x2 x3] prems(2-)
28+
unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
29+
apply (elim disj_forward exE; simp)
30+
apply (metis Lam_eq_tvsubst Lam_refresh singletonD)
31+
by blast
3532
done
3633

3734
thm stepD.strong_induct

‎thys/Untyped_Lambda_Calculus/LC_Parallel_Beta.thy‎

Lines changed: 34 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -20,15 +20,40 @@ binder_inductive pstep :: "trm \<Rightarrow> trm \<Rightarrow> bool" where
2020
term.rrename_comps rrename_tvsubst_comp
2121
| ((rule exI[of _ "\<sigma> _"] exI)+, (rule conjI)?, rule refl)
2222
| ((rule exI[of _ "\<sigma> _"])+; auto))+
23-
subgoal premises prems for R B t1 t2
24-
by (tactic \<open>refreshability_tac false
25-
[@{term "FFVars :: trm \<Rightarrow> var set"}, @{term "FFVars :: trm \<Rightarrow> var set"}]
26-
[@{term "rrename :: (var \<Rightarrow> var) \<Rightarrow> trm \<Rightarrow> trm"}, @{term "(\<lambda>f x. f x) :: (var \<Rightarrow> var) \<Rightarrow> var \<Rightarrow> var"}]
27-
[NONE, NONE, SOME [SOME 0, SOME 0, SOME 1], SOME [SOME 0, SOME 0, NONE, NONE, SOME 1]]
28-
@{thm prems(3)} @{thm prems(2)} @{thms }
29-
@{thms emp_bound singl_bound term.Un_bound term.card_of_FFVars_bounds infinite}
30-
@{thms Lam_inject} @{thms Lam_eq_tvsubst term.rrename_cong_ids[symmetric]}
31-
@{thms id_on_antimono} @{context}\<close>)
23+
subgoal premises prems for R B x1 x2
24+
using fresh[of x1 x2] prems(2-)
25+
unfolding ex_push_inwards conj_disj_distribL ex_disj_distrib
26+
apply (elim disj_forward exE)
27+
apply (((rule exI, rule conjI[rotated], assumption) |
28+
(((rule exI conjI)+)?, rule Lam_refresh tvsubst_refresh) |
29+
(auto split: if_splits))+) [3]
30+
subgoal for xx e1 e1' e2 e2' x
31+
apply (erule conjE)+
32+
apply hypsubst_thin
33+
apply (subst (asm) FFVars_tvsubst)
34+
apply simp
35+
apply (unfold term.set)
36+
apply (unfold Un_iff de_Morgan_disj)
37+
apply (erule conjE)+
38+
apply (subst (2 3) ex_comm)
39+
apply (rule exI)
40+
apply (rule exI[of _ "{xx}"])
41+
apply (rule conjI)
42+
apply (rule exI)+
43+
apply (rule conjI[OF refl])
44+
apply (rule conjI)
45+
apply simp
46+
apply (rule conjI)
47+
apply (rule Lam_refresh)
48+
apply simp
49+
apply (rule refl)
50+
apply (rule conjI[rotated])+
51+
apply assumption
52+
apply auto[1]
53+
apply (fastforce intro!: tvsubst_refresh)
54+
apply simp
55+
done
56+
done
3257
done
3358

3459
thm pstep.strong_induct

0 commit comments

Comments
 (0)