: "AndL1 (x).M y = AndL1 (d).([(d,x)]\M) y" + by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(6)) + with d have "(\z'. Cut .P (z').AndL1 (d).([(d, x)] \ M){x:=.P} (z')) + = (\z'. Cut .P (z').AndL1 (x).M (z'))" + by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(6)) + with d have "(\z'. Cut .P (z').AndL1 d.([(d, x)] \ M){y:=.P} z') + = (\z'. Cut .P (z').AndL1 (x).M (z'))" + apply(simp add: trm.inject alpha fresh_prod fresh_atm) + by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap) + with d \

show ?thesis + by (simp add: fresh_left calc_atm) +qed lemma better_AndL2_substn: assumes a: "y\[x].M" shows "(AndL2 (x).M y){y:=.P} = fresh_fun (\z'. Cut .P (z').AndL2 (x).M z')" -using a -apply - -apply(generate_fresh "name") -apply(subgoal_tac "AndL2 (x).M y = AndL2 (ca).([(ca,x)]\M) y") -apply(auto simp: fresh_left calc_atm forget abs_fresh)[1] -apply(generate_fresh "name") -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) -apply(auto) -done +proof (generate_fresh "name") + fix d:: name + assume d: "d \ (M, P, c, x, y)" + then have \

: "AndL2 (x).M y = AndL2 (d).([(d,x)]\M) y" + by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(7)) + with d have "(\z'. Cut .P (z').AndL2 (d).([(d, x)] \ M){x:=.P} (z')) + = (\z'. Cut .P (z').AndL2 (x).M (z'))" + by (metis forget(1) fresh_bij(1) fresh_prodD(1) swap_simps(1) trm.inject(7)) + with d have "(\z'. Cut .P (z').AndL2 d.([(d, x)] \ M){y:=.P} z') + = (\z'. Cut .P (z').AndL2 (x).M (z'))" + apply(simp add: trm.inject alpha fresh_prod fresh_atm) + by (metis abs_fresh(1) assms forget(1) fresh_atm(1) fresh_aux(1) nrename_nfresh nrename_swap) + with d \

show ?thesis + by (simp add: fresh_left calc_atm) +qed lemma better_AndR_substc: - assumes a: "c\([a].M,[b].N)" + assumes "c\([a].M,[b].N)" shows "(AndR .M .N c){c:=(z).P} = fresh_fun (\a'. Cut .(AndR .M .N a') (z).P)" -using a -apply - -apply(generate_fresh "coname") -apply(generate_fresh "coname") -apply(subgoal_tac "AndR .M .N c = AndR .([(ca,a)]\M) .([(caa,b)]\N) c") -apply(auto simp: fresh_left calc_atm forget abs_fresh)[1] -apply(rule trans) -apply(rule substc.simps) -apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1] -apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1] -apply(auto simp: fresh_prod fresh_atm)[1] -apply(simp) -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule conjI) -apply(rule forget) -apply(auto simp: fresh_left calc_atm abs_fresh)[1] -apply(rule forget) -apply(auto simp: fresh_left calc_atm abs_fresh)[1] -apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) -apply(auto) -done +proof (generate_fresh "coname" , generate_fresh "coname") + fix d :: coname + and e :: coname + assume d: "d \ (M, N, P, a, b, c, z)" + and e: "e \ (M, N, P, a, b, c, z, d)" + then have "AndR .M .N c = AndR .([(d,a)]\M) .([(e,b)]\N) c" + by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto + with assms d e show ?thesis + apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) + by (metis (no_types, opaque_lifting) abs_fresh(2) forget(2) trm.inject(5)) +qed lemma better_OrL_substn: - assumes a: "x\([y].M,[z].N)" + assumes "x\([y].M,[z].N)" shows "(OrL (y).M (z).N x){x:=.P} = fresh_fun (\z'. Cut .P (z').OrL (y).M (z).N z')" -using a -apply - -apply(generate_fresh "name") -apply(generate_fresh "name") -apply(subgoal_tac "OrL (y).M (z).N x = OrL (ca).([(ca,y)]\M) (caa).([(caa,z)]\N) x") -apply(auto simp: fresh_left calc_atm forget abs_fresh)[1] -apply(rule trans) -apply(rule substn.simps) -apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1] -apply(auto simp: fresh_left calc_atm fresh_prod fresh_atm)[1] -apply(auto simp: fresh_prod fresh_atm)[1] -apply(simp) -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule conjI) -apply(rule forget) -apply(auto simp: fresh_left calc_atm abs_fresh)[1] -apply(rule forget) -apply(auto simp: fresh_left calc_atm abs_fresh)[1] -apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) -apply(auto) -done +proof (generate_fresh "name" , generate_fresh "name") + fix d :: name + and e :: name + assume d: "d \ (M, N, P, c, x, y, z)" + and e: "e \ (M, N, P, c, x, y, z, d)" + with assms have "OrL (y).M (z).N x = OrL (d).([(d,y)]\M) (e).([(e,z)]\N) x" + by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto + with assms d e show ?thesis + apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) + by (metis (no_types, lifting) abs_fresh(1) forget(1) trm.inject(10)) +qed lemma better_OrR1_substc: assumes a: "d\[a].M" shows "(OrR1 .M d){d:=(z).P} = fresh_fun (\a'. Cut .OrR1 .M a' (z).P)" -using a -apply - -apply(generate_fresh "coname") -apply(subgoal_tac "OrR1 .M d = OrR1 .([(c,a)]\M) d") -apply(auto simp: fresh_left calc_atm forget abs_fresh)[1] -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) -apply(auto) -done +proof (generate_fresh "coname") + fix c :: coname + assume c: "c \ (M, P, a, d, z)" + then have "OrR1 .M d = OrR1 .([(c,a)]\M) d" + by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto + with assms c show ?thesis + apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) + by (metis abs_fresh(2) forget(2) trm.inject(8)) +qed lemma better_OrR2_substc: assumes a: "d\[a].M" shows "(OrR2 .M d){d:=(z).P} = fresh_fun (\a'. Cut .OrR2 .M a' (z).P)" -using a -apply - -apply(generate_fresh "coname") -apply(subgoal_tac "OrR2 .M d = OrR2 .([(c,a)]\M) d") -apply(auto simp: fresh_left calc_atm forget abs_fresh)[1] -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) -apply(auto) -done +proof (generate_fresh "coname") + fix c :: coname + assume c: "c \ (M, P, a, d, z)" + then have "OrR2 .M d = OrR2 .([(c,a)]\M) d" + by (perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm) auto + with assms c show ?thesis + apply (auto simp: fresh_left calc_atm fresh_prod fresh_atm) + by (metis abs_fresh(2) forget(2) trm.inject(9)) +qed lemma better_ImpR_substc: - assumes a: "d\[a].M" + assumes "d\[a].M" shows "(ImpR (x)..M d){d:=(z).P} = fresh_fun (\a'. Cut .ImpR (x)..M a' (z).P)" -using a -apply - -apply(generate_fresh "coname") -apply(generate_fresh "name") -apply(subgoal_tac "ImpR (x)..M d = ImpR (ca)..([(c,a)]\[(ca,x)]\M) d") -apply(auto simp: fresh_left calc_atm forget abs_fresh)[1] -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(rule sym) -apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm) -done +proof (generate_fresh "coname" , generate_fresh "name") + fix c :: coname + and c' :: name + assume c: "c \ (M, P, a, d, x, z)" + and c': "c' \ (M, P, a, d, x, z, c)" + have \: "ImpR (x)..M d = ImpR (c')..([(c,a)]\[(c',x)]\M) d" + apply (rule sym) + using c c' + apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm) + done + with assms c c' have "fresh_fun + (\a'. Cut .ImpR (c')..(([(c, a)] \ [(c', x)] \ M)){d:=(z).P} a' (z).P) + = fresh_fun (\a'. Cut .ImpR (x)..M a' (z).P)" + apply(intro arg_cong [where f="fresh_fun"]) + by(fastforce simp add: trm.inject alpha fresh_prod fresh_atm abs_perm fresh_left calc_atm abs_fresh forget) + with assms c c' \ show ?thesis + by (auto simp: fresh_left calc_atm forget abs_fresh) +qed lemma better_ImpL_substn: - assumes a: "y\(M,[x].N)" + assumes "y\(M,[x].N)" shows "(ImpL .M (x).N y){y:=.P} = fresh_fun (\z'. Cut .P (z').ImpL .M (x).N z')" -using a -apply - -apply(generate_fresh "coname") -apply(generate_fresh "name") -apply(subgoal_tac "ImpL .M (x).N y = ImpL .([(ca,a)]\M) (caa).([(caa,x)]\N) y") -apply(auto simp: fresh_left calc_atm forget abs_fresh)[1] -apply(rule_tac f="fresh_fun" in arg_cong) -apply(simp add: fun_eq_iff) -apply(rule allI) -apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) -apply(rule forget) -apply(simp add: fresh_left calc_atm) -apply(auto)[1] -apply(rule sym) -apply(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm) -done +proof (generate_fresh "coname" , generate_fresh "name") + fix ca :: coname + and caa :: name + assume d: "ca \ (M, N, P, a, c, x, y)" + and e: "caa \ (M, N, P, a, c, x, y, ca)" + have "ImpL .M (x).N y = ImpL .([(ca,a)]\M) (caa).([(caa,x)]\N) y" + apply(rule sym) + using d e + by(perm_simp add: trm.inject alpha fresh_left calc_atm fresh_prod fresh_atm abs_fresh abs_perm) + with d e assms show ?thesis + apply(simp add: fresh_left calc_atm forget abs_fresh) + apply(intro arg_cong [where f="fresh_fun"] ext) + apply(simp add: trm.inject alpha fresh_prod fresh_atm abs_perm abs_fresh fresh_left calc_atm) + by (metis forget(1) fresh_aux(1) fresh_bij(1) swap_simps(1)) +qed lemma freshn_after_substc: fixes x::"name" @@ -1556,332 +1490,222 @@ by (meson assms fresh_def subset_iff supp_subst6) lemma substn_crename_comm: - assumes a: "c\a" "c\b" + assumes "c\a" "c\b" shows "M{x:=.P}[a\c>b] = M[a\c>b]{x:=.(P[a\c>b])}" -using a -apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct) -apply(auto simp: subst_fresh rename_fresh trm.inject) -apply(subgoal_tac "\x'::name. x'\(P,x,c)") -apply(erule exE) -apply(subgoal_tac "Cut .P (x).Ax x a = Cut .P (x').Ax x' a") -apply(simp) -apply(rule trans) -apply(rule crename.simps) -apply(simp add: fresh_prod fresh_atm) -apply(simp) -apply(simp add: trm.inject) -apply(simp add: alpha trm.inject calc_atm fresh_atm) -apply(simp add: trm.inject) -apply(simp add: alpha trm.inject calc_atm fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm) -apply(simp) -apply(simp add: crename_id) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(auto simp: fresh_atm)[1] -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm) -apply(auto simp: fresh_atm)[1] -apply(drule crename_ax) -apply(simp add: fresh_atm) -apply(simp add: fresh_atm) -apply(simp) -apply(subgoal_tac "\x'::name. x'\(trm{x:=.P},P,P[a\c>b],x,trm[a\c>b]{x:=.P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_NotL) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(trm{x:=.P},P,P[a\c>b],name1,trm[a\c>b]{x:=.P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL1) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(trm{x:=.P},P,P[a\c>b],name1,trm[a\c>b]{x:=.P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL2) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(trm1{x:=.P},trm2{x:=.P},P,P[a\c>b],name1,name2, - trm1[a\c>b]{x:=.P[a\c>b]},trm2[a\c>b]{x:=.P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrL) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh subst_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},trm2{name2:=.P},P,P[a\c>b],name1, - trm1[a\c>b]{name2:=.P[a\c>b]},trm2[a\c>b]{name2:=.P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_ImpL) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh subst_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -done +using assms +proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct) + case (Ax name coname) + then show ?case + by(auto simp: better_crename_Cut fresh_atm) +next + case (Cut coname trm1 name trm2) + then show ?case + apply(simp add: rename_fresh better_crename_Cut fresh_atm) + by (meson crename_ax) +next + case (NotL coname trm name) + obtain x'::name where "x'\(trm{x:=.P},P,P[a\c>b],x,trm[a\c>b]{x:=.P[a\c>b]})" + by (meson exists_fresh(1) fs_name1) + with NotL show ?case + apply (simp add: subst_fresh rename_fresh trm.inject) + by (force simp: fresh_prod fresh_fun_simp_NotL better_crename_Cut fresh_atm) +next + case (AndL1 name1 trm name2) + obtain x'::name where "x'\(trm{x:=.P},P,P[a\c>b],name1,trm[a\c>b]{x:=.P[a\c>b]})" + by (meson exists_fresh(1) fs_name1) + with AndL1 show ?case + apply (simp add: subst_fresh rename_fresh trm.inject) + apply (force simp: fresh_prod fresh_fun_simp_AndL1 better_crename_Cut fresh_atm) + done +next + case (AndL2 name1 trm name2) + obtain x'::name where x': "x'\(trm{x:=.P},P,P[a\c>b],name1,trm[a\c>b]{x:=.P[a\c>b]})" + by (meson exists_fresh(1) fs_name1) + with AndL2 show ?case + apply (simp add: subst_fresh rename_fresh trm.inject) + apply (auto simp: fresh_prod fresh_fun_simp_AndL2 better_crename_Cut fresh_atm) + done +next + case (OrL name1 trm1 name2 trm2 name3) + obtain x'::name where x': "x'\(trm1{x:=.P},trm2{x:=.P},P,P[a\c>b],name1,name2, + trm1[a\c>b]{x:=.P[a\c>b]},trm2[a\c>b]{x:=.P[a\c>b]})" + by (meson exists_fresh(1) fs_name1) + with OrL show ?case + apply (simp add: subst_fresh rename_fresh trm.inject) + apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_OrL better_crename_Cut) + done + next + case (ImpL coname trm1 name1 trm2 name2) + obtain x'::name where x': "x'\(trm1{x:=.P},trm2{x:=.P},P,P[a\c>b],name1,name2, + trm1[a\c>b]{x:=.P[a\c>b]},trm2[a\c>b]{x:=.P[a\c>b]})" + by (meson exists_fresh(1) fs_name1) + with ImpL show ?case + apply (simp add: subst_fresh rename_fresh trm.inject) + apply (auto simp: fresh_atm subst_fresh fresh_prod fresh_fun_simp_ImpL better_crename_Cut) + done +qed (auto simp: subst_fresh rename_fresh) + lemma substc_crename_comm: - assumes a: "c\a" "c\b" + assumes "c\a" "c\b" shows "M{c:=(x).P}[a\c>b] = M[a\c>b]{c:=(x).(P[a\c>b])}" -using a -apply(nominal_induct M avoiding: x c P a b rule: trm.strong_induct) -apply(auto simp: subst_fresh rename_fresh trm.inject) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(drule crename_ax) -apply(simp add: fresh_atm) -apply(simp add: fresh_atm) -apply(simp) -apply(subgoal_tac "\c'::coname. c'\(a,b,trm{coname:=(x).P},P,P[a\c>b],x,trm[a\c>b]{coname:=(x).P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_NotR) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P}, - P,P[a\c>b],x,trm1[a\c>b]{coname3:=(x).P[a\c>b]},trm2[a\c>b]{coname3:=(x).P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndR) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh subst_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,trm{coname2:=(x).P},P,P[a\c>b],a,b, - trm[a\c>b]{coname2:=(x).P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrR1) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,trm{coname2:=(x).P},P,P[a\c>b],a,b, - trm[a\c>b]{coname2:=(x).P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrR2) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,trm{coname2:=(x).P},P,P[a\c>b],a,b, - trm[a\c>b]{coname2:=(x).P[a\c>b]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_ImpR) -apply(rule trans) -apply(rule better_crename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -done +using assms +proof (nominal_induct M avoiding: x c P a b rule: trm.strong_induct) + case (Ax name coname) + then show ?case + by(auto simp: better_crename_Cut fresh_atm) +next + case (Cut coname trm1 name trm2) + then show ?case + apply(simp add: rename_fresh better_crename_Cut) + by (meson crename_ax) +next + case (NotR name trm coname) + obtain c'::coname where "c'\(a,b,trm{coname:=(x).P},P,P[a\c>b],x,trm[a\c>b]{coname:=(x).P[a\c>b]})" + by (meson exists_fresh' fs_coname1) + with NotR show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by(auto simp: fresh_prod fresh_fun_simp_NotR better_crename_Cut fresh_atm) +next + case (AndR coname1 trm1 coname2 trm2 coname3) + obtain c'::coname where "c'\(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P}, + P,P[a\c>b],x,trm1[a\c>b]{coname3:=(x).P[a\c>b]},trm2[a\c>b]{coname3:=(x).P[a\c>b]})" + by (meson exists_fresh' fs_coname1) + with AndR show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by (auto simp: fresh_prod fresh_fun_simp_AndR better_crename_Cut subst_fresh fresh_atm) +next + case (OrR1 coname1 trm coname2) + obtain c'::coname where "c'\(coname1,trm{coname2:=(x).P},P,P[a\c>b],a,b, trm[a\c>b]{coname2:=(x).P[a\c>b]})" + by (meson exists_fresh' fs_coname1) + with OrR1 show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by(auto simp: fresh_prod fresh_fun_simp_OrR1 better_crename_Cut fresh_atm) +next + case (OrR2 coname1 trm coname2) + obtain c'::coname where "c'\(coname1,trm{coname2:=(x).P},P,P[a\c>b],a,b, trm[a\c>b]{coname2:=(x).P[a\c>b]})" + by (meson exists_fresh' fs_coname1) + with OrR2 show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by(auto simp: fresh_prod fresh_fun_simp_OrR2 better_crename_Cut fresh_atm) +next + case (ImpR name coname1 trm coname2) + obtain c'::coname where "c'\(coname1,trm{coname2:=(x).P},P,P[a\c>b],a,b, trm[a\c>b]{coname2:=(x).P[a\c>b]})" + by (meson exists_fresh' fs_coname1) + with ImpR show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by(auto simp: fresh_prod fresh_fun_simp_ImpR better_crename_Cut fresh_atm) +qed (auto simp: subst_fresh rename_fresh trm.inject) + lemma substn_nrename_comm: - assumes a: "x\y" "x\z" + assumes "x\y" "x\z" shows "M{x:=.P}[y\n>z] = M[y\n>z]{x:=.(P[y\n>z])}" -using a -apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct) -apply(auto simp: subst_fresh rename_fresh trm.inject) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_prod fresh_atm) -apply(simp add: trm.inject) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm) -apply(simp) -apply(drule nrename_ax) -apply(simp add: fresh_atm) -apply(simp add: fresh_atm) -apply(simp) -apply(subgoal_tac "\x'::name. x'\(y,z,trm{x:=.P},P,P[y\n>z],x,trm[y\n>z]{x:=.P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_NotL) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(trm{x:=.P},P,P[y\n>z],name1,trm[y\n>z]{x:=.P[y\n>z]},y,z)") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL1) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(y,z,trm{x:=.P},P,P[y\n>z],name1,trm[y\n>z]{x:=.P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndL2) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(trm1{x:=.P},trm2{x:=.P},P,P[y\n>z],name1,name2,y,z, - trm1[y\n>z]{x:=.P[y\n>z]},trm2[y\n>z]{x:=.P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrL) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh subst_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\x'::name. x'\(trm1{name2:=.P},trm2{name2:=.P},P,P[y\n>z],y,z,name1, - trm1[y\n>z]{name2:=.P[y\n>z]},trm2[y\n>z]{name2:=.P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_ImpL) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh subst_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -done +using assms +proof (nominal_induct M avoiding: x c P y z rule: trm.strong_induct) + case (Ax name coname) + then show ?case + by (auto simp: better_nrename_Cut fresh_atm) +next + case (Cut coname trm1 name trm2) + then show ?case + apply(clarsimp simp: subst_fresh rename_fresh trm.inject better_nrename_Cut) + by (meson nrename_ax) +next + case (NotL coname trm name) + obtain x'::name where "x'\(y,z,trm{x:=.P},P,P[y\n>z],x,trm[y\n>z]{x:=.P[y\n>z]})" + by (meson exists_fresh' fs_name1) + with NotL show ?case + apply(clarsimp simp: rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_NotL better_nrename_Cut fresh_atm) +next + case (AndL1 name1 trm name2) + obtain x'::name where "x'\(trm{x:=.P},P,P[y\n>z],name1,trm[y\n>z]{x:=.P[y\n>z]},y,z)" + by (meson exists_fresh' fs_name1) + with AndL1 show ?case + apply(clarsimp simp: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_AndL1 better_nrename_Cut fresh_atm) +next + case (AndL2 name1 trm name2) + obtain x'::name where "x'\(trm{x:=.P},P,P[y\n>z],name1,trm[y\n>z]{x:=.P[y\n>z]},y,z)" + by (meson exists_fresh' fs_name1) + with AndL2 show ?case + apply(clarsimp simp: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_AndL2 better_nrename_Cut fresh_atm) +next + case (OrL name1 trm1 name2 trm2 name3) + obtain x'::name where "x'\(trm1{x:=.P},trm2{x:=.P},P,P[y\n>z],name1,name2,y,z, + trm1[y\n>z]{x:=.P[y\n>z]},trm2[y\n>z]{x:=.P[y\n>z]})" + by (meson exists_fresh' fs_name1) + with OrL show ?case + apply (clarsimp simp: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_OrL better_nrename_Cut subst_fresh fresh_atm) +next + case (ImpL coname trm1 name1 trm2 name2) + obtain x'::name where "x'\(trm1{x:=.P},trm2{x:=.P},P,P[y\n>z],name1,name2,y,z, + trm1[y\n>z]{x:=.P[y\n>z]},trm2[y\n>z]{x:=.P[y\n>z]})" + by (meson exists_fresh' fs_name1) + with ImpL show ?case + apply (clarsimp simp: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_ImpL better_nrename_Cut subst_fresh fresh_atm) +qed (auto simp: subst_fresh rename_fresh trm.inject) + + lemma substc_nrename_comm: - assumes a: "x\y" "x\z" + assumes "x\y" "x\z" shows "M{c:=(x).P}[y\n>z] = M[y\n>z]{c:=(x).(P[y\n>z])}" -using a -apply(nominal_induct M avoiding: x c P y z rule: trm.strong_induct) -apply(auto simp: subst_fresh rename_fresh trm.inject) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(drule nrename_ax) -apply(simp add: fresh_atm) -apply(simp add: fresh_atm) -apply(simp) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(drule nrename_ax) -apply(simp add: fresh_atm) -apply(simp add: fresh_atm) -apply(simp) -apply(subgoal_tac "\c'::coname. c'\(y,z,trm{coname:=(x).P},P,P[y\n>z],x,trm[y\n>z]{coname:=(x).P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_NotR) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,coname2,y,z,trm1{coname3:=(x).P},trm2{coname3:=(x).P}, - P,P[y\n>z],x,trm1[y\n>z]{coname3:=(x).P[y\n>z]},trm2[y\n>z]{coname3:=(x).P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_AndR) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh subst_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,trm{coname2:=(x).P},P,P[y\n>z],y,z, - trm[y\n>z]{coname2:=(x).P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrR1) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,trm{coname2:=(x).P},P,P[y\n>z],y,z, - trm[y\n>z]{coname2:=(x).P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_OrR2) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -apply(subgoal_tac "\c'::coname. c'\(coname1,trm{coname2:=(x).P},P,P[y\n>z],y,z, - trm[y\n>z]{coname2:=(x).P[y\n>z]})") -apply(erule exE, simp add: fresh_prod) -apply(erule conjE)+ -apply(simp add: fresh_fun_simp_ImpR) -apply(rule trans) -apply(rule better_nrename_Cut) -apply(simp add: fresh_atm fresh_prod) -apply(simp add: rename_fresh fresh_atm) -apply(rule exists_fresh') -apply(rule fin_supp) -done +using assms +proof (nominal_induct M avoiding: x c P y z rule: trm.strong_induct) + case (Ax name coname) + then show ?case + by (auto simp: subst_fresh rename_fresh trm.inject better_nrename_Cut fresh_atm) +next + case (Cut coname trm1 name trm2) + then show ?case + apply (clarsimp simp: subst_fresh rename_fresh trm.inject better_nrename_Cut fresh_atm) + by (metis nrename_ax) +next + case (NotR name trm coname) + obtain c'::coname where "c'\(y,z,trm{coname:=(x).P},P,P[y\n>z],x,trm[y\n>z]{coname:=(x).P[y\n>z]})" + by (meson exists_fresh' fs_coname1) + with NotR show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_NotR better_nrename_Cut fresh_atm) +next + case (AndR coname1 trm1 coname2 trm2 coname3) + obtain c'::coname where "c'\(coname1,coname2,y,z,trm1{coname3:=(x).P},trm2{coname3:=(x).P}, + P,P[y\n>z],x,trm1[y\n>z]{coname3:=(x).P[y\n>z]},trm2[y\n>z]{coname3:=(x).P[y\n>z]})" + by (meson exists_fresh' fs_coname1) + with AndR show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_AndR better_nrename_Cut fresh_atm subst_fresh) +next + case (OrR1 coname1 trm coname2) + obtain c'::coname where "c'\(coname1,trm{coname2:=(x).P},P,P[y\n>z],y,z, + trm[y\n>z]{coname2:=(x).P[y\n>z]})" + by (meson exists_fresh' fs_coname1) + with OrR1 show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_OrR1 better_nrename_Cut fresh_atm subst_fresh) +next + case (OrR2 coname1 trm coname2) + obtain c'::coname where "c'\(coname1,trm{coname2:=(x).P},P,P[y\n>z],y,z, + trm[y\n>z]{coname2:=(x).P[y\n>z]})" + by (meson exists_fresh' fs_coname1) + with OrR2 show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_OrR2 better_nrename_Cut fresh_atm subst_fresh) +next + case (ImpR name coname1 trm coname2) + obtain c'::coname where "c'\(coname1,trm{coname2:=(x).P},P,P[y\n>z],y,z, + trm[y\n>z]{coname2:=(x).P[y\n>z]})" + by (meson exists_fresh' fs_coname1) + with ImpR show ?case + apply(simp add: subst_fresh rename_fresh trm.inject) + by (auto simp add: fresh_prod fresh_fun_simp_ImpR better_nrename_Cut fresh_atm subst_fresh) +qed (auto simp: subst_fresh rename_fresh trm.inject) + lemma substn_crename_comm': assumes "a\c" "a\P" @@ -2421,58 +2245,35 @@ equivariance fic lemma fic_Ax_elim: - assumes a: "fic (Ax x a) b" + assumes "fic (Ax x a) b" shows "a=b" -using a -apply(erule_tac fic.cases) -apply(auto simp: trm.inject) -done + using assms by (auto simp: trm.inject elim!: fic.cases) lemma fic_NotR_elim: - assumes a: "fic (NotR (x).M a) b" + assumes "fic (NotR (x).M a) b" shows "a=b \ b\M" -using a -apply(erule_tac fic.cases) -apply(auto simp: trm.inject) -apply(subgoal_tac "b\[xa].Ma") -apply(drule sym) -apply(simp_all add: abs_fresh) -done + using assms + by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6)) lemma fic_OrR1_elim: - assumes a: "fic (OrR1 .M b) c" + assumes "fic (OrR1 .M b) c" shows "b=c \ c\[a].M" -using a -apply(erule_tac fic.cases) -apply(auto simp: trm.inject) -done + using assms by (auto simp: trm.inject elim!: fic.cases) lemma fic_OrR2_elim: - assumes a: "fic (OrR2 .M b) c" + assumes "fic (OrR2 .M b) c" shows "b=c \ c\[a].M" -using a -apply(erule_tac fic.cases) -apply(auto simp: trm.inject) -done + using assms by (auto simp: trm.inject elim!: fic.cases) lemma fic_AndR_elim: - assumes a: "fic (AndR .M .N c) d" + assumes "fic (AndR .M .N c) d" shows "c=d \ d\[a].M \ d\[b].N" -using a -apply(erule_tac fic.cases) -apply(auto simp: trm.inject) -done + using assms by (auto simp: trm.inject elim!: fic.cases) lemma fic_ImpR_elim: assumes a: "fic (ImpR (x)..M b) c" shows "b=c \ b\[a].M" -using a -apply(erule_tac fic.cases) -apply(auto simp: trm.inject) -apply(subgoal_tac "c\[xa].[aa].Ma") -apply(drule sym) -apply(simp_all add: abs_fresh) -done + using assms by (auto simp: trm.inject elim!: fic.cases) (metis abs_fresh(6)) lemma fic_rest_elims: shows "fic (Cut .M (x).N) d \ False" diff -r 97dab09aa727 -r 27e66a8323b2 src/HOL/Proofs/ex/XML_Data.thy --- a/src/HOL/Proofs/ex/XML_Data.thy Thu Jul 18 15:57:07 2024 +0200 +++ b/src/HOL/Proofs/ex/XML_Data.thy Thu Jul 18 16:00:40 2024 +0200 @@ -48,11 +48,11 @@ text \Some fairly large proof:\ ML_val \ - val xml = export_proof thy1 @{thm abs_less_iff}; + val xml = export_proof thy1 @{thm Int.times_int.abs_eq}; val thm = import_proof thy1 xml; - val xml_size = size (YXML.string_of_body xml); - \<^assert> (xml_size > 100000); + val xml_size = Bytes.size (YXML.bytes_of_body xml); + \<^assert> (xml_size > 10000000); \ end diff -r 97dab09aa727 -r 27e66a8323b2 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Thu Jul 18 15:57:07 2024 +0200 +++ b/src/HOL/Wellfounded.thy Thu Jul 18 16:00:40 2024 +0200 @@ -309,18 +309,45 @@ subsubsection \Antimonotonicity\ + +lemma wfp_on_antimono_stronger: + fixes + A :: "'a set" and B :: "'b set" and + f :: "'a \ 'b" and + R :: "'b \ 'b \ bool" and Q :: "'a \ 'a \ bool" + assumes + wf: "wfp_on B R" and + sub: "f ` A \ B" and + mono: "\x y. x \ A \ y \ A \ Q x y \ R (f x) (f y)" + shows "wfp_on A Q" + unfolding wfp_on_iff_ex_minimal +proof (intro allI impI) + fix A' :: "'a set" + assume "A' \ A" and "A' \ {}" + have "f ` A' \ B" + using \A' \ A\ sub by blast + moreover have "f ` A' \ {}" + using \A' \ {}\ by blast + ultimately have "\z\f ` A'. \y. R y z \ y \ f ` A'" + using wf wfp_on_iff_ex_minimal by blast + hence "\z\A'. \y. R (f y) (f z) \ y \ A'" + by blast + thus "\z\A'. \y. Q y z \ y \ A'" + using \A' \ A\ mono by blast +qed + +lemma wf_on_antimono_stronger: + assumes + "wf_on B r" and + "f ` A \ B" and + "(\x y. x \ A \ y \ A \ (x, y) \ q \ (f x, f y) \ r)" + shows "wf_on A q" + using assms wfp_on_antimono_stronger[to_set, of B r f A q] by blast + lemma wf_on_antimono_strong: assumes "wf_on B r" and "A \ B" and "(\x y. x \ A \ y \ A \ (x, y) \ q \ (x, y) \ r)" shows "wf_on A q" - unfolding wf_on_iff_ex_minimal -proof (intro allI impI) - fix AA assume "AA \ A" and "AA \ {}" - hence "\z\AA. \y. (y, z) \ r \ y \ AA" - using \wf_on B r\ \A \ B\ - by (simp add: wf_on_iff_ex_minimal) - then show "\z\AA. \y. (y, z) \ q \ y \ AA" - using \AA \ A\ assms(3) by blast -qed + using assms wf_on_antimono_stronger[of B r "\x. x" A q] by blast lemma wfp_on_antimono_strong: "wfp_on B R \ A \ B \ (\x y. x \ A \ y \ A \ Q x y \ R x y) \ wfp_on A Q" diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/Admin/build_log.scala Thu Jul 18 16:00:40 2024 +0200 @@ -349,8 +349,8 @@ val engine = "build_manager" val Start = new Regex("""^Starting job \S+ at ([^,]+), on (\S+)$""") val End = new Regex("""^Job ended at ([^,]+), with status \w+$""") - val Isabelle_Version = List(new Regex("""^Using Isabelle/(\w+)$""")) - val AFP_Version = List(new Regex("""^Using AFP/(\w+)$""")) + val Isabelle_Version = List(new Regex("""^Using Isabelle/?(\w*)$""")) + val AFP_Version = List(new Regex("""^Using AFP/?(\w*)$""")) } private def parse_meta_info(log_file: Log_File): Meta_Info = { diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Thu Jul 18 16:00:40 2024 +0200 @@ -17,18 +17,20 @@ object Component { def parse(s: String): Component = space_explode('/', s) match { + case name :: Nil => Component(name) case name :: rev :: Nil => Component(name, rev) case _ => error("Malformed component: " + quote(s)) } + val Isabelle = "Isabelle" val AFP = "AFP" - def isabelle(rev: String = "") = Component("Isabelle", rev) + def isabelle(rev: String = "") = Component(Isabelle, rev) def afp(rev: String = "") = Component(AFP, rev) } case class Component(name: String, rev: String = "") { - override def toString: String = name + "/" + rev + override def toString: String = name + if_proper(rev, "/" + rev) def is_local: Boolean = rev.isEmpty } @@ -635,11 +637,32 @@ Report.Data(build_log, component_logs, component_diffs) } - def write_component_diff(name: String, diff: String): Unit = - if (diff.nonEmpty) File.write_gzip(dir + Path.basic(name).ext(diff_ext).gz, diff) + def write_log( + component: String, + repository: Mercurial.Repository, + rev0: String, + rev: String + ): Unit = + if (rev0.nonEmpty && rev.nonEmpty && rev0 != rev) { + val log_opts = "--graph --color always" + val rev1 = "children(" + rev0 + ")" + val cmd = repository.command_line("log", Mercurial.opt_rev(rev1 + ":" + rev), log_opts) + val log = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out + if (log.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(log_ext).gz, log) + } - def write_component_log(name: String, log: String): Unit = - if (log.nonEmpty) File.write_gzip(dir + Path.basic(name).ext(log_ext).gz, log) + def write_diff( + component: String, + repository: Mercurial.Repository, + rev0: String, + rev: String + ): Unit = + if (rev0.nonEmpty && rev.nonEmpty) { + val diff_opts = "--noprefix --nodates --ignore-all-space --color always" + val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts) + val diff = Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out + if (diff.nonEmpty) File.write_gzip(dir + Path.basic(component).ext(diff_ext).gz, diff) + } def result(uuid: Option[UUID.T]): Result = { val End = """^Job ended at [^,]+, with status (\w+)$""".r @@ -801,22 +824,6 @@ } } - private def diff(repository: Mercurial.Repository, rev0: String, rev: String): String = - if (rev0.isEmpty || rev.isEmpty) "" - else { - val diff_opts = "--noprefix --nodates --ignore-all-space --color always" - val cmd = repository.command_line("diff", Mercurial.opt_rev(rev0 + ":" + rev), diff_opts) - Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out - } - - private def log(repository: Mercurial.Repository, rev0: String, rev: String): String = - if (rev0.isEmpty || rev.isEmpty) "" - else { - val log_opts = "--graph --color always" - val cmd = repository.command_line("log", Mercurial.opt_rev(rev0 + ":" + rev), log_opts) - Isabelle_System.bash("export HGPLAINEXCEPT=color\n" + cmd).check.out - } - private def start_next(): Option[Context] = synchronized_database("start_next") { for ((name, task) <- _state.pending if Exn.is_exn(Exn.capture(task.build_hosts))) { @@ -872,10 +879,10 @@ val previous = _state.get_finished(task.kind).maxBy(_.id) for (isabelle_rev0 <- previous.isabelle_version) { - context.report.write_component_log("Isabelle", - log(isabelle_repository, isabelle_rev0, isabelle_rev)) - context.report.write_component_diff("Isabelle", - diff(isabelle_repository, isabelle_rev0, isabelle_rev)) + context.report.write_log(Component.Isabelle, + isabelle_repository, isabelle_rev0, isabelle_rev) + context.report.write_diff(Component.Isabelle, + isabelle_repository, isabelle_rev0, isabelle_rev) } for { @@ -883,8 +890,8 @@ afp <- extra_components.find(_.name == Component.AFP) sync_dir <- sync_dirs.find(_.name == afp.name) } { - context.report.write_component_log(afp.name, log(sync_dir.hg, afp_rev0, afp.rev)) - context.report.write_component_diff(afp.name, diff(sync_dir.hg, afp_rev0, afp.rev)) + context.report.write_log(afp.name, sync_dir.hg, afp_rev0, afp.rev) + context.report.write_diff(afp.name, sync_dir.hg, afp_rev0, afp.rev) } } @@ -894,7 +901,7 @@ case Exn.Res(job) => _state = _state.add_running(job) - for (component <- job.components if !component.is_local) + for (component <- job.components) context.report.progress.echo("Using " + component.toString) Some(context) @@ -973,8 +980,7 @@ /* repository poller */ object Poller { - case class Versions(isabelle: String, components: List[Component]) - case class State(current: Versions, next: Future[Versions]) + case class State(current: List[Component], next: Future[List[Component]]) } class Poller( @@ -987,11 +993,11 @@ override def delay = options.seconds("build_manager_poll_delay") - private def current: Poller.Versions = - Poller.Versions(isabelle_repository.id("default"), sync_dirs.map(dir => - Component(dir.name, dir.hg.id("default")))) + private def current: List[Component] = + Component.isabelle(isabelle_repository.id("default")) :: + sync_dirs.map(dir => Component(dir.name, dir.hg.id("default"))) - private def poll: Future[Poller.Versions] = Future.fork { + private def poll: Future[List[Component]] = Future.fork { Par_List.map((repo: Mercurial.Repository) => repo.pull(), isabelle_repository :: sync_dirs.map(_.hg)) @@ -1000,17 +1006,24 @@ val init: Poller.State = Poller.State(current, poll) - private def add_tasks(current: Poller.Versions, next: Poller.Versions): Unit = { - val isabelle_updated = current.isabelle != next.isabelle - val updated_components = - next.components.zip(current.components).filter(_ != _).map(_._1.name).toSet + private def add_tasks(current: List[Component], next: List[Component]): Unit = { + val next_rev = next.map(component => component.name -> component.rev).toMap + + def is_unchanged(components: List[Component]): Boolean = + components.forall(component => next_rev.get(component.name).contains(component.rev)) + + def is_changed(component_names: List[String]): Boolean = + !is_unchanged(current.filter(component => component_names.contains(component.name))) + + def is_current(job: Job): Boolean = is_unchanged(job.components) synchronized_database("add_tasks") { for { ci_job <- ci_jobs if ci_job.trigger == Build_CI.On_Commit - if isabelle_updated || ci_job.components.exists(updated_components.contains) + if is_changed(Component.Isabelle :: ci_job.components) if !_state.pending.values.exists(_.kind == ci_job.name) + if !_state.running.values.filter(_.kind == ci_job.name).exists(is_current) } _state = _state.add_pending(CI_Build.task(ci_job)) } } @@ -1218,22 +1231,18 @@ submit_form("", List(hidden(ID, uuid.toString), api_button(paths.api_route(API.BUILD_CANCEL), "cancel build"))))) - def non_local(components: List[Component]): List[Component] = - for (component <- components if !component.is_local) yield component + def render_rev(components: List[Component], data: Report.Data): XML.Body = { + val hg_info = data.component_logs.map(_._1) ++ data.component_diffs.map(_._1) + val s = components.mkString(", ") - def render_rev(components: List[Component], data: Report.Data): XML.Body = { - val relevant = non_local(components) - val hg_info = data.component_logs.map(_._1) ++ data.component_diffs.map(_._1) - val s = relevant.mkString(", ") - - if (!relevant.map(_.name).exists(hg_info.toSet)) text(s) - else List(page_link(Page.DIFF, s, Markup.Name(build.name))) + if (!components.map(_.name).exists(hg_info.toSet)) text("Components: " + s) + else text("Components: ") :+ page_link(Page.DIFF, s, Markup.Name(build.name)) } build match { case task: Task => par(text("Task from " + Build_Log.print_date(task.submit_date) + ". ")) :: - par(text(non_local(task.components).mkString(", "))) :: + par(text(task.components.mkString(", "))) :: render_cancel(task.uuid) case job: Job => @@ -1284,7 +1293,8 @@ data.component_logs.toMap.get(component.name).toList.flatMap(colored) ::: data.component_diffs.toMap.get(component.name).toList.flatMap(colored) - par(if (infos.isEmpty) text(component.toString) else text(component.name) ::: infos) + val header = if (infos.isEmpty) component.toString else component.name + ":" + par(subsubsection(header) :: infos) }) build match { @@ -1620,7 +1630,12 @@ /** restore build manager database **/ - def build_manager_database(options: Options, progress: Progress = new Progress): Unit = { + def build_manager_database( + options: Options, + sync_dirs: List[Sync.Dir] = Sync.afp_dirs(), + update_reports: Boolean = false, + progress: Progress = new Progress + ): Unit = { val store = Store(options) using(store.open_database()) { db => db.transaction { @@ -1632,16 +1647,44 @@ } } - val results = + val reports = for { kind <- File.read_dir(store.finished) entry <- File.read_dir(store.finished + Path.basic(kind)) id <- Value.Long.unapply(entry) report = store.report(kind, id) if report.ok - } yield report.result(None) + } yield report + + val results = reports.map(report => report -> report.result(None)) + + if (update_reports) { + val isabelle_repository = Mercurial.self_repository() + val afp_repository = + sync_dirs.find(_.name == Component.AFP).getOrElse(error("Missing AFP for udpate")).hg + + isabelle_repository.pull() + afp_repository.pull() - val state = State(finished = results.map(result => result.name -> result).toMap) + for ((kind, results0) <- results.groupBy(_._1.kind) if kind != User_Build.name) { + val results1 = results0.sortBy(_._1.id) + results1.foldLeft(("", "")) { + case ((isabelle_rev0, afp_rev0), (report, result)) => + val isabelle_rev = result.isabelle_version.getOrElse("") + val afp_rev = result.afp_version.getOrElse("") + + report.write_log(Component.Isabelle, isabelle_repository, isabelle_rev0, isabelle_rev) + report.write_log(Component.AFP, afp_repository, afp_rev0, afp_rev) + report.write_diff( + Component.Isabelle, isabelle_repository, isabelle_rev0, isabelle_rev) + report.write_diff(Component.AFP, afp_repository, afp_rev0, afp_rev) + + (isabelle_rev, afp_rev) + } + } + } + + val state = State(finished = results.map((_, result) => result.name -> result).toMap) Build_Manager.private_data.transaction_lock(db, create = true, label = "Build_Manager.build_manager_database") { @@ -1659,24 +1702,31 @@ "restore build_manager database from log files", Scala_Project.here, { args => + var afp_root: Option[Path] = None var options = Options.init() + var update_reports = false val getopts = Getopts(""" Usage: isabelle build_manager_database [OPTIONS] Options are: + -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """) -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -u update reports Restore build_manager database from log files. """, - "o:" -> (arg => options = options + arg)) + "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))), + "o:" -> (arg => options = options + arg), + "u" -> (_ => update_reports = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() - build_manager_database(options, progress = progress) + build_manager_database(options, sync_dirs = Sync.afp_dirs(afp_root), + update_reports = update_reports, progress = progress) }) diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/GUI/gui.scala Thu Jul 18 16:00:40 2024 +0200 @@ -13,7 +13,7 @@ import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute} import java.awt.geom.AffineTransform import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, - JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities} + RootPaneContainer, JTextField, JWindow, JComboBox, LookAndFeel, UIManager, SwingUtilities} import scala.swing.{CheckBox, ComboBox, ScrollPane, TextArea, ListView, Label, Separator, Orientation} @@ -365,13 +365,11 @@ } def parent_window(component: Component): Option[Window] = - ancestors(component).collectFirst({ case x: Window => x }) + ancestors(component).collectFirst({ case c: Window => c }) def layered_pane(component: Component): Option[JLayeredPane] = parent_window(component) match { - case Some(w: JWindow) => Some(w.getLayeredPane) - case Some(w: JFrame) => Some(w.getLayeredPane) - case Some(w: JDialog) => Some(w.getLayeredPane) + case Some(c: RootPaneContainer) => Some(c.getLayeredPane) case _ => None } diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/GUI/popup.scala --- a/src/Pure/GUI/popup.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/GUI/popup.scala Thu Jul 18 16:00:40 2024 +0200 @@ -22,7 +22,7 @@ component.setSize(size) component.setPreferredSize(size) component.setOpaque(true) - layered.add(component, JLayeredPane.DEFAULT_LAYER) + layered.add(component, JLayeredPane.POPUP_LAYER) layered.moveToFront(component) layered.repaint(component.getBounds()) } diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/General/bytes.ML --- a/src/Pure/General/bytes.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/General/bytes.ML Thu Jul 18 16:00:40 2024 +0200 @@ -13,7 +13,7 @@ val chunk_size: int type T val eq: T * T -> bool - val length: T -> int + val size: T -> int val contents: T -> string list val contents_blob: T -> XML.body val content: T -> string @@ -54,7 +54,7 @@ {buffer: string list, chunks: string list, m: int (*buffer size*), n: int (*chunks size*)} with -fun length (Bytes {m, n, ...}) = m + n; +fun size (Bytes {m, n, ...}) = m + n; val compact = implode o rev; @@ -69,7 +69,7 @@ val content = implode o contents; -fun is_empty bytes = length bytes = 0; +fun is_empty bytes = size bytes = 0; val empty = Bytes {buffer = [], chunks = [], m = 0, n = 0}; @@ -132,10 +132,10 @@ fun beginning n bytes = let val dots = " ..."; - val m = (String.maxSize - size dots) div chunk_size; + val m = (String.maxSize - String.size dots) div chunk_size; val a = implode (take m (contents bytes)); - val b = String.substring (a, 0, Int.min (n, size a)); - in if size b < length bytes then b ^ dots else b end; + val b = String.substring (a, 0, Int.min (n, String.size a)); + in if String.size b < size bytes then b ^ dots else b end; fun append bytes1 bytes2 = (*left-associative*) if is_empty bytes1 then bytes2 @@ -155,7 +155,7 @@ fun space_explode sep bytes = if is_empty bytes then [] - else if size sep <> 1 then [content bytes] + else if String.size sep <> 1 then [content bytes] else let val sep_char = String.nth sep 0; @@ -199,7 +199,7 @@ fun read_stream limit stream = let fun read bytes = - (case read_block (limit - length bytes) stream of + (case read_block (limit - size bytes) stream of "" => bytes | s => read (add s bytes)) in read empty end; @@ -216,6 +216,8 @@ val _ = ML_system_pp (fn _ => fn _ => fn bytes => - PolyML.PrettyString ("Bytes {length = " ^ string_of_int (length bytes) ^ "}")) + PolyML.PrettyString + (if is_empty bytes then "Bytes.empty" + else "Bytes {size = " ^ string_of_int (size bytes) ^ "}")) end; diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/General/symbol.scala Thu Jul 18 16:00:40 2024 +0200 @@ -51,6 +51,7 @@ def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9' + def is_ascii_digit(b: Byte): Boolean = is_ascii_digit(b.toChar) def is_ascii_hex(c: Char): Boolean = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f' diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/General/value.scala --- a/src/Pure/General/value.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/General/value.scala Thu Jul 18 16:00:40 2024 +0200 @@ -22,7 +22,7 @@ object Nat { def unapply(bs: Bytes): Option[scala.Int] = - if (bs.byte_iterator.forall(b => '0' <= b && b <= '9')) unapply(bs.text) + if (bs.byte_iterator.forall(Symbol.is_ascii_digit)) unapply(bs.text) else None def unapply(s: java.lang.String): Option[scala.Int] = s match { diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/PIDE/byte_message.ML --- a/src/Pure/PIDE/byte_message.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/PIDE/byte_message.ML Thu Jul 18 16:00:40 2024 +0200 @@ -44,7 +44,7 @@ fun read_block stream n = let val msg = read stream n; - val len = Bytes.length msg; + val len = Bytes.size msg; in (if len = n then SOME msg else NONE, len) end; fun read_line stream = @@ -66,7 +66,7 @@ [Bytes.string (space_implode "," (map Value.print_int ns)), Bytes.newline]; fun write_message stream chunks = - (write stream (make_header (map Bytes.length chunks) @ chunks); flush stream); + (write stream (make_header (map Bytes.size chunks) @ chunks); flush stream); fun write_message_string stream = write_message stream o map Bytes.string; @@ -110,7 +110,7 @@ if is_length msg orelse is_terminated msg then error ("Bad content for line message:\n" ^ Bytes.beginning 100 msg) else - let val n = Bytes.length msg in + let val n = Bytes.size msg in write stream ((if n > 100 orelse Bytes.exists_string (fn s => s = "\n") msg then make_header [n + 1] else []) @ [msg, Bytes.newline]); diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/PIDE/byte_message.scala --- a/src/Pure/PIDE/byte_message.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/PIDE/byte_message.scala Thu Jul 18 16:00:40 2024 +0200 @@ -44,7 +44,7 @@ builder += c.toByte } } - if (c == -1 && line.size == 0) None else Some(line.trim_line) + if (c == -1 && line.is_empty) None else Some(line.trim_line) } @@ -82,7 +82,7 @@ Value.Long.unapply(str).isDefined private def is_length(msg: Bytes): Boolean = - !msg.is_empty && msg.byte_iterator.forall(b => Symbol.is_ascii_digit(b.toChar)) && + !msg.is_empty && msg.byte_iterator.forall(Symbol.is_ascii_digit) && Value.Long.unapply(msg.text).isDefined def write_line_message(stream: OutputStream, msg: Bytes): Unit = { diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/PIDE/yxml.ML --- a/src/Pure/PIDE/yxml.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/PIDE/yxml.ML Thu Jul 18 16:00:40 2024 +0200 @@ -24,6 +24,8 @@ val body_size: XML.body -> int val string_of_body: XML.body -> string val string_of: XML.tree -> string + val bytes_of_body: XML.body -> Bytes.T + val bytes_of: XML.tree -> Bytes.T val write_body: Path.T -> XML.body -> unit val output_markup: Markup.T -> string * string val output_markup_elem: Markup.T -> (string * string) * string @@ -76,6 +78,9 @@ val string_of_body = Buffer.build_content o fold (traverse Buffer.add); val string_of = string_of_body o single; +val bytes_of_body = Bytes.build o fold (traverse Bytes.add); +val bytes_of = bytes_of_body o single; + fun write_body path body = path |> File_Stream.open_output (fn file => fold (traverse (fn s => fn () => File_Stream.output file s)) body ()); @@ -109,8 +114,7 @@ val split_bytes = Bytes.space_explode X - #> filter (fn "" => false | _ => true) - #> map (space_explode Y); + #> map_filter (fn "" => NONE | s => SOME (space_explode Y s)); (* structural errors *) diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/PIDE/yxml.scala --- a/src/Pure/PIDE/yxml.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/PIDE/yxml.scala Thu Jul 18 16:00:40 2024 +0200 @@ -148,14 +148,16 @@ /* parse chunks */ - for (chunk <- source.iterator_X if !chunk.is_empty) { - if (chunk.is_Y) pop() - else { - chunk.iterator_Y.toList match { - case ch :: name :: atts if ch.is_empty => - push(parse_string(name), atts.map(parse_attrib)) - case txts => - for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt))))) + for (chunk <- source.iterator_X) { + if (!chunk.is_empty) { + if (chunk.is_Y) pop() + else { + chunk.iterator_Y.toList match { + case ch :: name :: atts if ch.is_empty => + push(parse_string(name), atts.map(parse_attrib)) + case txts => + for (txt <- txts) add(cache.tree0(XML.Text(cache.string(parse_string(txt))))) + } } } } diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Jul 18 16:00:40 2024 +0200 @@ -188,7 +188,7 @@ {oracles = Ord_List.make Proofterm.oracle_ord oracles, thms = Ord_List.make Proofterm.thm_ord thms, zboxes = [], - zproof = ZDummy, + zproof = ZNop, proof = prf}; in Proofterm.thm_body body end; diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/proofterm.ML Thu Jul 18 16:00:40 2024 +0200 @@ -336,7 +336,7 @@ fun no_proof_body zproof proof = PBody {oracles = [], thms = [], zboxes = [], zproof = zproof, proof = proof}; -val no_thm_body = thm_body (no_proof_body ZDummy MinProof); +val no_thm_body = thm_body (no_proof_body ZNop MinProof); fun no_thm_names (Abst (x, T, prf)) = Abst (x, T, no_thm_names prf) | no_thm_names (AbsP (x, t, prf)) = AbsP (x, t, no_thm_names prf) @@ -405,7 +405,12 @@ fn Var (a, _) => (indexname a, []), fn Bound a => ([], int a), fn Abs (a, b, c) => ([a], pair typ (standard_term consts) (b, c)), - fn op $ a => ([], pair (standard_term consts) (standard_term consts) a)]; + fn t as op $ a => + if can Logic.match_of_class t then raise Match + else ([], pair (standard_term consts) (standard_term consts) a), + fn t => + let val (T, c) = Logic.match_of_class t + in ([c], typ T) end]; fun standard_proof consts prf = prf |> variant [fn MinProof => ([], []), @@ -459,7 +464,7 @@ val (a, b, c) = triple (list (pair (pair string (Position.of_properties o properties)) (option (term consts)))) (list (thm consts)) (proof consts) x; - in PBody {oracles = a, thms = b, zboxes = [], zproof = ZDummy, proof = c} end + in PBody {oracles = a, thms = b, zboxes = [], zproof = ZNop, proof = c} end and thm consts x = let val (a, (b, (c, (d, e)))) = @@ -2187,7 +2192,7 @@ val (zproof1, zboxes1) = if zproof_enabled proofs then ZTerm.add_box_proof {unconstrain = unconstrain} thy hyps concl zproof0 zboxes0 - else (ZDummy, []); + else (ZNop, []); val proof1 = if proof_enabled proofs then fold_rev implies_intr_proof hyps proof0 else MinProof; @@ -2198,7 +2203,7 @@ val unconstrainT = unconstrainT_proof (Sign.classes_of thy) sorts_proof ucontext; val postproc = map_proof_of (unconstrainT #> named ? rew_proof thy); val body1 = - {oracles = oracles0, thms = thms0, zboxes = [], zproof = ZDummy, proof = proof1}; + {oracles = oracles0, thms = thms0, zboxes = [], zproof = ZNop, proof = proof1}; in (i, fulfill_proof_future thy promises postproc (Future.value (PBody body1))) end; val (i, body') = diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/term.scala --- a/src/Pure/term.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/term.scala Thu Jul 18 16:00:40 2024 +0200 @@ -96,17 +96,17 @@ case class App(fun: Term, arg: Term) extends Term { private lazy val hash: Int = ("App", fun, arg).hashCode() override def hashCode(): Int = hash - - override def toString: String = - this match { - case OFCLASS(ty, c) => "OFCLASS(" + ty + "," + c + ")" - case _ => "App(" + fun + "," + arg + ")" - } + } + case class OFCLASS(typ: Typ, name: String) extends Term { + private lazy val hash: Int = ("OFCLASS", typ, name).hashCode() + override def hashCode(): Int = hash } def dummy_pattern(ty: Typ): Term = Const("Pure.dummy_pattern", List(ty)) val dummy: Term = dummy_pattern(dummyT) + def mk_of_sort(typ: Typ, s: Sort): List[Term] = s.map(c => OFCLASS(typ, c)) + sealed abstract class Proof case object MinProof extends Proof case class PBound(index: Int) extends Proof @@ -148,30 +148,6 @@ } - /* type classes within the logic */ - - object Class_Const { - val suffix = "_class" - def apply(c: Class): String = c + suffix - def unapply(s: String): Option[Class] = - if (s.endsWith(suffix)) Some(s.substring(0, s.length - suffix.length)) else None - } - - object OFCLASS { - def apply(ty: Typ, s: Sort): List[Term] = s.map(c => apply(ty, c)) - - def apply(ty: Typ, c: Class): Term = - App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty))) - - def unapply(t: Term): Option[(Typ, String)] = - t match { - case App(Const(Class_Const(c), List(ty)), Const(Pure_Thy.TYPE, List(ty1))) - if ty == ty1 => Some((ty, c)) - case _ => None - } - } - - /** cache **/ @@ -230,6 +206,7 @@ case Abs(name, typ, body) => store(Abs(cache_string(name), cache_typ(typ), cache_term(body))) case App(fun, arg) => store(App(cache_term(fun), cache_term(arg))) + case OFCLASS(typ, name) => store(OFCLASS(cache_typ(typ), cache_string(name))) } } } diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/term_xml.ML --- a/src/Pure/term_xml.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/term_xml.ML Thu Jul 18 16:00:40 2024 +0200 @@ -55,7 +55,12 @@ fn Var (a, b) => (indexname a, typ_body b), fn Bound a => ([], int a), fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)), - fn op $ a => ([], pair (term consts) (term consts) a)]; + fn t as op $ a => + if can Logic.match_of_class t then raise Match + else ([], pair (term consts) (term consts) a), + fn t => + let val (T, c) = Logic.match_of_class t + in ([c], typ T) end]; end; @@ -91,7 +96,8 @@ fn (a, b) => Var (indexname a, typ_body b), fn ([], a) => Bound (int a), fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end, - fn ([], a) => op $ (pair (term consts) (term consts) a)]; + fn ([], a) => op $ (pair (term consts) (term consts) a), + fn ([a], b) => Logic.mk_of_class (typ b, a)]; end; diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/term_xml.scala --- a/src/Pure/term_xml.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/term_xml.scala Thu Jul 18 16:00:40 2024 +0200 @@ -34,7 +34,8 @@ { case Var(a, b) => (indexname(a), typ_body(b)) }, { case Bound(a) => (Nil, int(a)) }, { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) }, - { case App(a, b) => (Nil, pair(term, term)(a, b)) })) + { case App(a, b) => (Nil, pair(term, term)(a, b)) }, + { case OFCLASS(a, b) => (List(b), typ(a)) })) } object Decode { @@ -61,7 +62,8 @@ { case (a, b) => Var(indexname(a), typ_body(b)) }, { case (Nil, a) => Bound(int(a)) }, { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }, + { case (List(a), b) => OFCLASS(typ(b), a) })) def term_env(env: Map[String, Typ]): T[Term] = { def env_type(x: String, t: Typ): Typ = @@ -74,7 +76,8 @@ { case (a, b) => Var(indexname(a), typ_body(b)) }, { case (Nil, a) => Bound(int(a)) }, { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }, + { case (List(a), b) => OFCLASS(typ(b), a) })) term } diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/thm.ML Thu Jul 18 16:00:40 2024 +0200 @@ -757,7 +757,7 @@ make_deriv0 promises (PBody {oracles = oracles, thms = thms, zboxes = zboxes, zproof = zproof, proof = proof}); -val empty_deriv = make_deriv [] [] [] [] ZDummy MinProof; +val empty_deriv = make_deriv [] [] [] [] ZNop MinProof; (* inference rules *) @@ -778,7 +778,7 @@ val zboxes' = ZTerm.union_zboxes zboxes1 zboxes2; val proofs = Proofterm.get_proofs_level (); - val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZDummy; + val zproof' = if Proofterm.zproof_enabled proofs then zproof zprf1 zprf2 else ZNop; val proof' = if Proofterm.proof_enabled proofs then proof prf1 prf2 else MinProof; in make_deriv ps' oracles' thms' zboxes' zproof' proof' end; @@ -788,7 +788,7 @@ let val proofs = Proofterm.get_proofs_level () in if Proofterm.proof_enabled proofs orelse Proofterm.zproof_enabled proofs then deriv_rule1 I I (make_deriv [] [] [] [] - (if Proofterm.zproof_enabled proofs then zproof () else ZDummy) + (if Proofterm.zproof_enabled proofs then zproof () else ZNop) (if Proofterm.proof_enabled proofs then proof () else MinProof)) else empty_deriv end; @@ -853,7 +853,7 @@ val i = serial (); val future = future_thm |> Future.map (future_result i cert sorts prop); in - Thm (make_deriv [(i, future)] [] [] [] ZDummy MinProof, + Thm (make_deriv [(i, future)] [] [] [] ZNop MinProof, {cert = cert, tags = [], maxidx = maxidx, @@ -1203,7 +1203,7 @@ val thy = Context.certificate_theory cert handle ERROR msg => raise CONTEXT (msg, [], [ct], [], NONE); in ZTerm.oracle_proof thy name prop end - else ZDummy; + else ZNop; in Thm (make_deriv [] [oracle] [] [] zproof proof, {cert = cert, @@ -2115,7 +2115,7 @@ raise THM ("store_zproof: theorem may not use promises", 0, [thm]); val ((i, (_, zproof1)), zproof2) = ZTerm.thm_proof thy name hyps prop zproof; - val der1 = if Options.default_bool "prune_proofs" then deriv [] ZDummy else deriv zboxes zproof1; + val der1 = if Options.default_bool "prune_proofs" then deriv [] ZNop else deriv zboxes zproof1; val der2 = deriv [] zproof2; val thm' = trim_context (Thm (der1, args)); diff -r 97dab09aa727 -r 27e66a8323b2 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Pure/zterm.ML Thu Jul 18 16:00:40 2024 +0200 @@ -200,7 +200,7 @@ type zproof_const = (zproof_name * zterm) * (ztyp ZTVars.table * zterm ZVars.table); datatype zproof = - ZDummy (*dummy proof*) + ZNop | ZConstp of zproof_const | ZBoundp of int | ZAbst of string * ztyp * zproof @@ -480,7 +480,7 @@ fun fold_proof {hyps} typ term = let - fun proof ZDummy = I + fun proof ZNop = I | proof (ZConstp (_, (instT, inst))) = ZTVars.fold (typ o #2) instT #> ZVars.fold (term o #2) inst | proof (ZBoundp _) = I @@ -538,7 +538,7 @@ fun map_proof_same {hyps} typ term = let - fun proof ZDummy = raise Same.SAME + fun proof ZNop = raise Same.SAME | proof (ZConstp (a, (instT, inst))) = ZConstp (a, map_insts_same typ term (instT, inst)) | proof (ZBoundp _) = raise Same.SAME diff -r 97dab09aa727 -r 27e66a8323b2 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Tools/Haskell/Haskell.thy Thu Jul 18 16:00:40 2024 +0200 @@ -2347,6 +2347,7 @@ | Bound Int | Abs (Name, Typ, Term) | App (Term, Term) + | OFCLASS (Typ, Name) deriving (Show, Eq, Ord) @@ -2681,7 +2682,8 @@ \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing }, \case { Bound a -> Just ([], int a); _ -> Nothing }, \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing }, - \case { App a -> Just ([], pair term term a); _ -> Nothing }] + \case { App a -> Just ([], pair term term a); _ -> Nothing }, + \case { OFCLASS (a, b) -> Just ([b], typ a); _ -> Nothing }] \ generate_file "Isabelle/Term_XML/Decode.hs" = \ @@ -2730,7 +2732,8 @@ \(a, b) -> Var (indexname a, typ_body b), \([], a) -> Bound (int a), \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d), - \([], a) -> App (pair term term a)] + \([], a) -> App (pair term term a), + \([a], b) -> OFCLASS (typ b, a)] \ generate_file "Isabelle/XML/Classes.hs" = \ diff -r 97dab09aa727 -r 27e66a8323b2 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Thu Jul 18 16:00:40 2024 +0200 @@ -196,7 +196,7 @@ private val delay_caret_update = Delay.last(PIDE.session.input_delay, gui = true) { session.caret_focus.post(Session.Caret_Focus) - JEdit_Lib.invalidate(text_area) + JEdit_Lib.invalidate_screen(text_area) } private val caret_listener = new CaretListener { @@ -229,7 +229,7 @@ changed.commands.exists(snapshot.node.commands.contains))) text_overview.foreach(_.invoke()) - JEdit_Lib.invalidate(text_area) + JEdit_Lib.invalidate_screen(text_area) } } } diff -r 97dab09aa727 -r 27e66a8323b2 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Jul 18 16:00:40 2024 +0200 @@ -205,9 +205,13 @@ } } - def invalidate(text_area: TextArea): Unit = { + def invalidate_screen(text_area: TextArea, start: Int = -1, end: Int = -1): Unit = { val visible_lines = text_area.getVisibleLines - if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) + if (visible_lines > 0) { + val start_line = if (start >= 0) start else 0 + val end_line = if (end >= 0) end else visible_lines + text_area.invalidateScreenLineRange(start_line, end_line) + } } diff -r 97dab09aa727 -r 27e66a8323b2 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Thu Jul 18 15:57:07 2024 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Jul 18 16:00:40 2024 +0200 @@ -18,10 +18,11 @@ import java.text.AttributedString import scala.util.matching.Regex +import scala.collection.mutable import org.gjt.sp.util.Log import org.gjt.sp.jedit.View -import org.gjt.sp.jedit.syntax.Chunk +import org.gjt.sp.jedit.syntax.{Chunk => JEditChunk, SyntaxStyle} import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea} @@ -145,8 +146,9 @@ /* active areas within the text */ private class Active_Area[A]( - rendering: JEdit_Rendering => Text.Range => Option[Text.Info[A]], - cursor: Option[Int] + render: JEdit_Rendering => Text.Range => Option[Text.Info[A]], + val require_control: Boolean = false, + cursor: Int = -1 ) { private var the_text_info: Option[(String, Text.Info[A])] = None @@ -161,11 +163,11 @@ if (new_text_info != old_text_info) { caret_update() - if (cursor.isDefined) { - if (new_text_info.isDefined) - text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) - else - text_area.getPainter.resetCursor() + if (cursor >= 0) { + if (new_text_info.isDefined) { + text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor)) + } + else text_area.getPainter.resetCursor() } for { r0 <- JEdit_Lib.visible_range(text_area) @@ -177,8 +179,8 @@ } } - def update_rendering(r: JEdit_Rendering, range: Text.Range): Unit = - update(rendering(r)(range)) + def update_rendering(rendering: JEdit_Rendering, range: Text.Range): Unit = + update(render(rendering)(range)) def reset(): Unit = update(None) } @@ -186,23 +188,18 @@ // owned by GUI thread private val highlight_area = - new Active_Area[Color]( - (rendering: JEdit_Rendering) => rendering.highlight, None) + new Active_Area[Color](_.highlight, require_control = true) private val hyperlink_area = new Active_Area[PIDE.editor.Hyperlink]( - (rendering: JEdit_Rendering) => rendering.hyperlink, Some(Cursor.HAND_CURSOR)) + _.hyperlink, require_control = true, cursor = Cursor.HAND_CURSOR) private val active_area = - new Active_Area[XML.Elem]( - (rendering: JEdit_Rendering) => rendering.active, Some(Cursor.DEFAULT_CURSOR)) + new Active_Area[XML.Elem](_.active, cursor = Cursor.DEFAULT_CURSOR) - private val active_areas = - List((highlight_area, true), (hyperlink_area, true), (active_area, false)) - def active_reset(): Unit = active_areas.foreach(_._1.reset()) - - private def area_active(): Boolean = - active_areas.exists({ case (area, _) => area.is_active }) + private val active_areas = List(highlight_area, hyperlink_area, active_area) + private def active_exists(): Boolean = active_areas.exists(_.is_active) + def active_reset(): Unit = active_areas.foreach(_.reset()) private val focus_listener = new FocusAdapter { override def focusLost(e: FocusEvent): Unit = { robust_body(()) { active_reset() } } @@ -270,9 +267,10 @@ case None => active_reset() case Some(range) => val rendering = get_rendering() - for ((area, require_control) <- active_areas) { - if (control == require_control && !rendering.snapshot.is_outdated) + for (area <- active_areas) { + if (control == area.require_control && !rendering.snapshot.is_outdated) { area.update_rendering(rendering, range) + } else area.reset() } } @@ -413,47 +411,64 @@ def get(codepoint: Int): Option[Font] = cache.getOrElse(codepoint, { - val field = classOf[Chunk].getDeclaredField("lastSubstFont") + val field = classOf[JEditChunk].getDeclaredField("lastSubstFont") field.setAccessible(true) field.set(null, null) - val res = Option(Chunk.getSubstFont(codepoint)) + val res = Option(JEditChunk.getSubstFont(codepoint)) cache += (codepoint -> res) res }) } + sealed case class Chunk( + id: Byte, + style: SyntaxStyle, + offset: Int, + length: Int, + width: Float, + font_subst: Boolean, + str: String + ) + + private def make_chunk_list(chunk_head: JEditChunk): List[Chunk] = { + val buf = new mutable.ListBuffer[Chunk] + var chunk = chunk_head + while (chunk != null) { + val str = + if (chunk.chars == null) Symbol.spaces(chunk.length) + else { + if (chunk.str == null) { chunk.str = new String(chunk.chars) } + chunk.str + } + buf += Chunk(chunk.id, chunk.style, chunk.offset, chunk.length, chunk.width, + chunk.usedFontSubstitution, str) + chunk = chunk.next.asInstanceOf[JEditChunk] + } + buf.toList + } + private def paint_chunk_list( rendering: JEdit_Rendering, font_subst: Font_Subst, gfx: Graphics2D, line_start: Text.Offset, - head: Chunk, - x: Float, - y: Float + caret_range: Text.Range, + chunk_list: List[Chunk], + x0: Int, + y0: Int ): Float = { val clip_rect = gfx.getClipBounds - val caret_range = - if (caret_enabled) JEdit_Lib.caret_range(text_area) - else Text.Range.offside - - var w = 0.0f - var chunk = head - while (chunk != null) { + val x = x0.toFloat + val y = y0.toFloat + chunk_list.foldLeft(0.0f) { case (w, chunk) => val chunk_offset = line_start + chunk.offset if (x + w + chunk.width > clip_rect.x && x + w < clip_rect.x + clip_rect.width && chunk.length > 0) { val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length) - val chunk_str = - if (chunk.chars == null) Symbol.spaces(chunk.length) - else { - if (chunk.str == null) { chunk.str = new String(chunk.chars) } - chunk.str - } val chunk_font = chunk.style.getFont val chunk_color = chunk.style.getForegroundColor - - val chunk_text = new AttributedString(chunk_str) + val chunk_text = new AttributedString(chunk.str) def chunk_attrib(attrib: TextAttribute, value: AnyRef, r: Text.Range): Unit = chunk_text.addAttribute(attrib, value, r.start - chunk_offset, r.stop - chunk_offset) @@ -461,13 +476,13 @@ // font chunk_text.addAttribute(TextAttribute.RUN_DIRECTION, TextAttribute.RUN_DIRECTION_LTR) chunk_text.addAttribute(TextAttribute.FONT, chunk_font) - if (chunk.usedFontSubstitution) { + if (chunk.font_subst) { for { - (c, i) <- Codepoint.iterator_offset(chunk_str) if !chunk_font.canDisplay(c) + (c, i) <- Codepoint.iterator_offset(chunk.str) if !chunk_font.canDisplay(c) subst_font <- font_subst.get(c) } { val r = Text.Range(i, i + Character.charCount(c)) + chunk_offset - val font = Chunk.deriveSubstFont(chunk_font, subst_font) + val font = JEditChunk.deriveSubstFont(chunk_font, subst_font) chunk_attrib(TextAttribute.FONT, font, r) } } @@ -487,10 +502,8 @@ gfx.drawString(chunk_text.getIterator, x + w, y) } - w += chunk.width - chunk = chunk.next.asInstanceOf[Chunk] + w + chunk.width } - w } private val text_painter = new TextAreaExtension { @@ -529,14 +542,17 @@ // text chunks val screen_line = first_line + i - val chunks = text_area.getChunksOfScreenLine(screen_line) - if (chunks != null) { + val chunk_list = make_chunk_list(text_area.getChunksOfScreenLine(screen_line)) + if (chunk_list.nonEmpty) { try { val line_start = buffer.getLineStartOffset(line) + val caret_range = + if (caret_enabled) JEdit_Lib.caret_range(text_area) + else Text.Range.offside gfx.clipRect(x0, y + line_height * i, Int.MaxValue, line_height) val w = paint_chunk_list(rendering, font_subst, gfx, - line_start, chunks, x0.toFloat, y0.toFloat) + line_start, caret_range, chunk_list, x0, y0) gfx.clipRect(x0 + w.toInt, 0, Int.MaxValue, Int.MaxValue) orig_text_painter.paintValidLine(gfx, screen_line, line, start(i), end(i), y + line_height * i) @@ -621,7 +637,7 @@ } // entity def range - if (!area_active() && caret_visible) { + if (!active_exists() && caret_visible) { for { Text.Info(range, color) <- rendering.entity_ref(line_range, caret_focus) r <- JEdit_Lib.gfx_range(text_area, range) @@ -632,7 +648,7 @@ } // completion range - if (!area_active() && caret_visible) { + if (!active_exists() && caret_visible) { for { completion <- Completion_Popup.Text_Area(text_area) Text.Info(range, color) <- completion.rendering(rendering, line_range)