--- a/NEWS Thu Jul 18 15:57:07 2024 +0200
+++ b/NEWS Thu Jul 18 16:00:40 2024 +0200
@@ -32,6 +32,9 @@
wfP_trancl ~> wfp_tranclp
wfP_wf_eq ~> wfp_wf_eq
wf_acc_iff ~> wf_iff_acc
+ - Added lemmas.
+ wf_on_antimono_stronger
+ wfp_on_antimono_stronger
* Theory "HOL-Library.Multiset":
- Renamed lemmas. Minor INCOMPATIBILITY.
--- a/src/HOL/Nominal/Examples/Class1.thy Thu Jul 18 15:57:07 2024 +0200
+++ b/src/HOL/Nominal/Examples/Class1.thy Thu Jul 18 16:00:40 2024 +0200
@@ -50,17 +50,17 @@
nominal_datatype trm =
Ax "name" "coname"
- | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut <_>._ (_)._" [100,100,100,100] 100)
- | NotR "\<guillemotleft>name\<guillemotright>trm" "coname" ("NotR (_)._ _" [100,100,100] 100)
- | NotL "\<guillemotleft>coname\<guillemotright>trm" "name" ("NotL <_>._ _" [100,100,100] 100)
- | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
- | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL1 (_)._ _" [100,100,100] 100)
- | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL2 (_)._ _" [100,100,100] 100)
- | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR1 <_>._ _" [100,100,100] 100)
- | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR2 <_>._ _" [100,100,100] 100)
- | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("OrL (_)._ (_)._ _" [100,100,100,100,100] 100)
- | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR (_).<_>._ _" [100,100,100,100] 100)
- | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 100)
+ | Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut <_>._ (_)._" [0,100,1000,100] 101)
+ | NotR "\<guillemotleft>name\<guillemotright>trm" "coname" ("NotR (_)._ _" [100,100,100] 101)
+ | NotL "\<guillemotleft>coname\<guillemotright>trm" "name" ("NotL <_>._ _" [0,100,100] 101)
+ | AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [0,100,0,100,100] 101)
+ | AndL1 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL1 (_)._ _" [100,100,100] 101)
+ | AndL2 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL2 (_)._ _" [100,100,100] 101)
+ | OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR1 <_>._ _" [100,100,100] 101)
+ | OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR2 <_>._ _" [100,100,100] 101)
+ | OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("OrL (_)._ (_)._ _" [100,100,100,100,100] 101)
+ | ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR (_).<_>._ _" [100,100,100,100] 101)
+ | ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("ImpL <_>._ (_)._ _" [100,100,100,100,100] 101)
text \<open>named terms\<close>
@@ -1319,217 +1319,151 @@
lemma better_NotL_substn:
assumes a: "y\<sharp>M"
shows "(NotL <a>.M y){y:=<c>.P} = fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.M x')"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(subgoal_tac "NotL <a>.M y = NotL <ca>.([(ca,a)]\<bullet>M) y")
-apply(auto simp: fresh_left calc_atm forget)
-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(perm_simp add: trm.inject alpha fresh_prod fresh_atm fresh_left, auto)
-done
+proof (generate_fresh "coname")
+ fix ca :: coname
+ assume d: "ca \<sharp> (M, P, a, c, y)"
+ then have "NotL <a>.M y = NotL <ca>.([(ca,a)]\<bullet>M) y"
+ by (metis alpha(2) fresh_prod perm_fresh_fresh(2) trm.inject(4))
+ with a d show ?thesis
+ apply(simp add: fresh_left calc_atm forget)
+ apply (metis trm.inject(4))
+ done
+qed
lemma better_AndL1_substn:
assumes a: "y\<sharp>[x].M"
shows "(AndL1 (x).M y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).M z')"
-using a
-apply -
-apply(generate_fresh "name")
-apply(subgoal_tac "AndL1 (x).M y = AndL1 (ca).([(ca,x)]\<bullet>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 \<sharp> (M, P, c, x, y)"
+ then have \<section>: "AndL1 (x).M y = AndL1 (d).([(d,x)]\<bullet>M) y"
+ by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(6))
+ with d have "(\<lambda>z'. Cut <c>.P (z').AndL1 (d).([(d, x)] \<bullet> M){x:=<c>.P} (z'))
+ = (\<lambda>z'. Cut <c>.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 "(\<lambda>z'. Cut <c>.P (z').AndL1 d.([(d, x)] \<bullet> M){y:=<c>.P} z')
+ = (\<lambda>z'. Cut <c>.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 \<section> show ?thesis
+ by (simp add: fresh_left calc_atm)
+qed
lemma better_AndL2_substn:
assumes a: "y\<sharp>[x].M"
shows "(AndL2 (x).M y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).M z')"
-using a
-apply -
-apply(generate_fresh "name")
-apply(subgoal_tac "AndL2 (x).M y = AndL2 (ca).([(ca,x)]\<bullet>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 \<sharp> (M, P, c, x, y)"
+ then have \<section>: "AndL2 (x).M y = AndL2 (d).([(d,x)]\<bullet>M) y"
+ by (metis alpha(1) fresh_prodD(1) perm_fresh_fresh(1) trm.inject(7))
+ with d have "(\<lambda>z'. Cut <c>.P (z').AndL2 (d).([(d, x)] \<bullet> M){x:=<c>.P} (z'))
+ = (\<lambda>z'. Cut <c>.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 "(\<lambda>z'. Cut <c>.P (z').AndL2 d.([(d, x)] \<bullet> M){y:=<c>.P} z')
+ = (\<lambda>z'. Cut <c>.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 \<section> show ?thesis
+ by (simp add: fresh_left calc_atm)
+qed
lemma better_AndR_substc:
- assumes a: "c\<sharp>([a].M,[b].N)"
+ assumes "c\<sharp>([a].M,[b].N)"
shows "(AndR <a>.M <b>.N c){c:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.M <b>.N a') (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(generate_fresh "coname")
-apply(subgoal_tac "AndR <a>.M <b>.N c = AndR <ca>.([(ca,a)]\<bullet>M) <caa>.([(caa,b)]\<bullet>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 \<sharp> (M, N, P, a, b, c, z)"
+ and e: "e \<sharp> (M, N, P, a, b, c, z, d)"
+ then have "AndR <a>.M <b>.N c = AndR <d>.([(d,a)]\<bullet>M) <e>.([(e,b)]\<bullet>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\<sharp>([y].M,[z].N)"
+ assumes "x\<sharp>([y].M,[z].N)"
shows "(OrL (y).M (z).N x){x:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.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)]\<bullet>M) (caa).([(caa,z)]\<bullet>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 \<sharp> (M, N, P, c, x, y, z)"
+ and e: "e \<sharp> (M, N, P, c, x, y, z, d)"
+ with assms have "OrL (y).M (z).N x = OrL (d).([(d,y)]\<bullet>M) (e).([(e,z)]\<bullet>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\<sharp>[a].M"
shows "(OrR1 <a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.M a' (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(subgoal_tac "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>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 \<sharp> (M, P, a, d, z)"
+ then have "OrR1 <a>.M d = OrR1 <c>.([(c,a)]\<bullet>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\<sharp>[a].M"
shows "(OrR2 <a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.M a' (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(subgoal_tac "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>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 \<sharp> (M, P, a, d, z)"
+ then have "OrR2 <a>.M d = OrR2 <c>.([(c,a)]\<bullet>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\<sharp>[a].M"
+ assumes "d\<sharp>[a].M"
shows "(ImpR (x).<a>.M d){d:=(z).P} = fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.M a' (z).P)"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(generate_fresh "name")
-apply(subgoal_tac "ImpR (x).<a>.M d = ImpR (ca).<c>.([(c,a)]\<bullet>[(ca,x)]\<bullet>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 \<sharp> (M, P, a, d, x, z)"
+ and c': "c' \<sharp> (M, P, a, d, x, z, c)"
+ have \<dagger>: "ImpR (x).<a>.M d = ImpR (c').<c>.([(c,a)]\<bullet>[(c',x)]\<bullet>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
+ (\<lambda>a'. Cut <a'>.ImpR (c').<c>.(([(c, a)] \<bullet> [(c', x)] \<bullet> M)){d:=(z).P} a' (z).P)
+ = fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.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' \<dagger> show ?thesis
+ by (auto simp: fresh_left calc_atm forget abs_fresh)
+qed
lemma better_ImpL_substn:
- assumes a: "y\<sharp>(M,[x].N)"
+ assumes "y\<sharp>(M,[x].N)"
shows "(ImpL <a>.M (x).N y){y:=<c>.P} = fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.M (x).N z')"
-using a
-apply -
-apply(generate_fresh "coname")
-apply(generate_fresh "name")
-apply(subgoal_tac "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>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 \<sharp> (M, N, P, a, c, x, y)"
+ and e: "caa \<sharp> (M, N, P, a, c, x, y, ca)"
+ have "ImpL <a>.M (x).N y = ImpL <ca>.([(ca,a)]\<bullet>M) (caa).([(caa,x)]\<bullet>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\<noteq>a" "c\<noteq>b"
+ assumes "c\<noteq>a" "c\<noteq>b"
shows "M{x:=<c>.P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{x:=<c>.(P[a\<turnstile>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 "\<exists>x'::name. x'\<sharp>(P,x,c)")
-apply(erule exE)
-apply(subgoal_tac "Cut <c>.P (x).Ax x a = Cut <c>.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 "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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 "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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 "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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 "\<exists>x'::name. x'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a\<turnstile>c>b],name1,name2,
- trm1[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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 "\<exists>x'::name. x'\<sharp>(trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,P[a\<turnstile>c>b],name1,
- trm1[a\<turnstile>c>b]{name2:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{name2:=<c>.P[a\<turnstile>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'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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'\<sharp>(trm{x:=<c>.P},P,P[a\<turnstile>c>b],name1,trm[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a\<turnstile>c>b],name1,name2,
+ trm1[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[a\<turnstile>c>b],name1,name2,
+ trm1[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{x:=<c>.P[a\<turnstile>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\<noteq>a" "c\<noteq>b"
+ assumes "c\<noteq>a" "c\<noteq>b"
shows "M{c:=(x).P}[a\<turnstile>c>b] = M[a\<turnstile>c>b]{c:=(x).(P[a\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(a,b,trm{coname:=(x).P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{coname:=(x).P[a\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
- P,P[a\<turnstile>c>b],x,trm1[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b,
- trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b,
- trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b,
- trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>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'\<sharp>(a,b,trm{coname:=(x).P},P,P[a\<turnstile>c>b],x,trm[a\<turnstile>c>b]{coname:=(x).P[a\<turnstile>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'\<sharp>(coname1,coname2,a,b,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
+ P,P[a\<turnstile>c>b],x,trm1[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>c>b]},trm2[a\<turnstile>c>b]{coname3:=(x).P[a\<turnstile>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'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b, trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>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'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b, trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>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'\<sharp>(coname1,trm{coname2:=(x).P},P,P[a\<turnstile>c>b],a,b, trm[a\<turnstile>c>b]{coname2:=(x).P[a\<turnstile>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\<noteq>y" "x\<noteq>z"
+ assumes "x\<noteq>y" "x\<noteq>z"
shows "M{x:=<c>.P}[y\<turnstile>n>z] = M[y\<turnstile>n>z]{x:=<c>.(P[y\<turnstile>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 "\<exists>x'::name. x'\<sharp>(y,z,trm{x:=<c>.P},P,P[y\<turnstile>n>z],x,trm[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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 "\<exists>x'::name. x'\<sharp>(trm{x:=<c>.P},P,P[y\<turnstile>n>z],name1,trm[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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 "\<exists>x'::name. x'\<sharp>(y,z,trm{x:=<c>.P},P,P[y\<turnstile>n>z],name1,trm[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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 "\<exists>x'::name. x'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y\<turnstile>n>z],name1,name2,y,z,
- trm1[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>n>z]},trm2[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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 "\<exists>x'::name. x'\<sharp>(trm1{name2:=<c>.P},trm2{name2:=<c>.P},P,P[y\<turnstile>n>z],y,z,name1,
- trm1[y\<turnstile>n>z]{name2:=<c>.P[y\<turnstile>n>z]},trm2[y\<turnstile>n>z]{name2:=<c>.P[y\<turnstile>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'\<sharp>(y,z,trm{x:=<c>.P},P,P[y\<turnstile>n>z],x,trm[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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'\<sharp>(trm{x:=<c>.P},P,P[y\<turnstile>n>z],name1,trm[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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'\<sharp>(trm{x:=<c>.P},P,P[y\<turnstile>n>z],name1,trm[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y\<turnstile>n>z],name1,name2,y,z,
+ trm1[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>n>z]},trm2[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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'\<sharp>(trm1{x:=<c>.P},trm2{x:=<c>.P},P,P[y\<turnstile>n>z],name1,name2,y,z,
+ trm1[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>n>z]},trm2[y\<turnstile>n>z]{x:=<c>.P[y\<turnstile>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\<noteq>y" "x\<noteq>z"
+ assumes "x\<noteq>y" "x\<noteq>z"
shows "M{c:=(x).P}[y\<turnstile>n>z] = M[y\<turnstile>n>z]{c:=(x).(P[y\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(y,z,trm{coname:=(x).P},P,P[y\<turnstile>n>z],x,trm[y\<turnstile>n>z]{coname:=(x).P[y\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,coname2,y,z,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
- P,P[y\<turnstile>n>z],x,trm1[y\<turnstile>n>z]{coname3:=(x).P[y\<turnstile>n>z]},trm2[y\<turnstile>n>z]{coname3:=(x).P[y\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[y\<turnstile>n>z],y,z,
- trm[y\<turnstile>n>z]{coname2:=(x).P[y\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[y\<turnstile>n>z],y,z,
- trm[y\<turnstile>n>z]{coname2:=(x).P[y\<turnstile>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 "\<exists>c'::coname. c'\<sharp>(coname1,trm{coname2:=(x).P},P,P[y\<turnstile>n>z],y,z,
- trm[y\<turnstile>n>z]{coname2:=(x).P[y\<turnstile>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'\<sharp>(y,z,trm{coname:=(x).P},P,P[y\<turnstile>n>z],x,trm[y\<turnstile>n>z]{coname:=(x).P[y\<turnstile>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'\<sharp>(coname1,coname2,y,z,trm1{coname3:=(x).P},trm2{coname3:=(x).P},
+ P,P[y\<turnstile>n>z],x,trm1[y\<turnstile>n>z]{coname3:=(x).P[y\<turnstile>n>z]},trm2[y\<turnstile>n>z]{coname3:=(x).P[y\<turnstile>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'\<sharp>(coname1,trm{coname2:=(x).P},P,P[y\<turnstile>n>z],y,z,
+ trm[y\<turnstile>n>z]{coname2:=(x).P[y\<turnstile>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'\<sharp>(coname1,trm{coname2:=(x).P},P,P[y\<turnstile>n>z],y,z,
+ trm[y\<turnstile>n>z]{coname2:=(x).P[y\<turnstile>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'\<sharp>(coname1,trm{coname2:=(x).P},P,P[y\<turnstile>n>z],y,z,
+ trm[y\<turnstile>n>z]{coname2:=(x).P[y\<turnstile>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\<noteq>c" "a\<sharp>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 \<and> b\<sharp>M"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-apply(subgoal_tac "b\<sharp>[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 <a>.M b) c"
+ assumes "fic (OrR1 <a>.M b) c"
shows "b=c \<and> c\<sharp>[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 <a>.M b) c"
+ assumes "fic (OrR2 <a>.M b) c"
shows "b=c \<and> c\<sharp>[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 <a>.M <b>.N c) d"
+ assumes "fic (AndR <a>.M <b>.N c) d"
shows "c=d \<and> d\<sharp>[a].M \<and> d\<sharp>[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).<a>.M b) c"
shows "b=c \<and> b\<sharp>[a].M"
-using a
-apply(erule_tac fic.cases)
-apply(auto simp: trm.inject)
-apply(subgoal_tac "c\<sharp>[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 <a>.M (x).N) d \<Longrightarrow> False"
--- 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 \<open>Some fairly large proof:\<close>
ML_val \<open>
- 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);
\<close>
end
--- 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 \<open>Antimonotonicity\<close>
+
+lemma wfp_on_antimono_stronger:
+ fixes
+ A :: "'a set" and B :: "'b set" and
+ f :: "'a \<Rightarrow> 'b" and
+ R :: "'b \<Rightarrow> 'b \<Rightarrow> bool" and Q :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+ assumes
+ wf: "wfp_on B R" and
+ sub: "f ` A \<subseteq> B" and
+ mono: "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> 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' \<subseteq> A" and "A' \<noteq> {}"
+ have "f ` A' \<subseteq> B"
+ using \<open>A' \<subseteq> A\<close> sub by blast
+ moreover have "f ` A' \<noteq> {}"
+ using \<open>A' \<noteq> {}\<close> by blast
+ ultimately have "\<exists>z\<in>f ` A'. \<forall>y. R y z \<longrightarrow> y \<notin> f ` A'"
+ using wf wfp_on_iff_ex_minimal by blast
+ hence "\<exists>z\<in>A'. \<forall>y. R (f y) (f z) \<longrightarrow> y \<notin> A'"
+ by blast
+ thus "\<exists>z\<in>A'. \<forall>y. Q y z \<longrightarrow> y \<notin> A'"
+ using \<open>A' \<subseteq> A\<close> mono by blast
+qed
+
+lemma wf_on_antimono_stronger:
+ assumes
+ "wf_on B r" and
+ "f ` A \<subseteq> B" and
+ "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (f x, f y) \<in> 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 \<subseteq> B" and "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (x, y) \<in> r)"
shows "wf_on A q"
- unfolding wf_on_iff_ex_minimal
-proof (intro allI impI)
- fix AA assume "AA \<subseteq> A" and "AA \<noteq> {}"
- hence "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> AA"
- using \<open>wf_on B r\<close> \<open>A \<subseteq> B\<close>
- by (simp add: wf_on_iff_ex_minimal)
- then show "\<exists>z\<in>AA. \<forall>y. (y, z) \<in> q \<longrightarrow> y \<notin> AA"
- using \<open>AA \<subseteq> A\<close> assms(3) by blast
-qed
+ using assms wf_on_antimono_stronger[of B r "\<lambda>x. x" A q] by blast
lemma wfp_on_antimono_strong:
"wfp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R x y) \<Longrightarrow> wfp_on A Q"
--- 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 = {
--- 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)
})
--- 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
}
--- 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())
}
--- 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;
--- 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'
--- 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 {
--- 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]);
--- 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 = {
--- 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 *)
--- 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)))))
+ }
}
}
}
--- 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;
--- 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') =
--- 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)))
}
}
}
--- 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;
--- 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
}
--- 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));
--- 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
--- 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 }]
\<close>
generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
@@ -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)]
\<close>
generate_file "Isabelle/XML/Classes.hs" = \<open>
--- 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)
}
}
}
--- 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)
+ }
}
--- 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)