20 proof (intro rel_funI) |
20 proof (intro rel_funI) |
21 fix p p' z z' X X' and s s'::"'c \<Rightarrow> _" |
21 fix p p' z z' X X' and s s'::"'c \<Rightarrow> _" |
22 assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'" |
22 assume transfer_rules[transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'" |
23 have "Domainp A z" using \<open>A z z'\<close> by force |
23 have "Domainp A z" using \<open>A z z'\<close> by force |
24 have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t |
24 have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t |
25 by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp) |
25 by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD) |
26 note swt=sum_with_transfer[OF assms(1,2,2), THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD, OF transfer_rules(1,2)] |
26 note swt=sum_with_transfer[OF assms(1,2,2), THEN rel_funD, THEN rel_funD, THEN rel_funD, THEN rel_funD, OF transfer_rules(1,2)] |
27 have DsI: "Domainp A (sum_with p z r t)" if "\<And>x. x \<in> t \<Longrightarrow> Domainp A (r x)" "t \<subseteq> Collect (Domainp A)" for r t |
27 have DsI: "Domainp A (sum_with p z r t)" if "\<And>x. x \<in> t \<Longrightarrow> Domainp A (r x)" "t \<subseteq> Collect (Domainp A)" for r t |
28 proof cases |
28 proof cases |
29 assume ex: "\<exists>C. r ` t \<subseteq> C \<and> comm_monoid_add_on_with C p z" |
29 assume ex: "\<exists>C. r ` t \<subseteq> C \<and> comm_monoid_add_on_with C p z" |
30 have "Domainp (rel_set A) t" using that by (auto simp: Domainp_set) |
30 have "Domainp (rel_set A) t" using that by (auto simp: Domainp_set) |
57 unfolding dependent_with_def dependent_with_def |
57 unfolding dependent_with_def dependent_with_def |
58 proof (intro rel_funI) |
58 proof (intro rel_funI) |
59 fix p p' z z' X X' and s s'::"'c \<Rightarrow> _" |
59 fix p p' z z' X X' and s s'::"'c \<Rightarrow> _" |
60 assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'" |
60 assume [transfer_rule]: "(A ===> A ===> A) p p'" "A z z'" "((=) ===> A ===> A) s s'" "rel_set A X X'" |
61 have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t |
61 have *: "t \<subseteq> X \<Longrightarrow> (\<forall>x\<in>t. Domainp A x)" for t |
62 by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 set_mp) |
62 by (meson Domainp.DomainI \<open>rel_set A X X'\<close> rel_setD1 subsetD) |
63 show "(\<exists>t u. finite t \<and> t \<subseteq> X \<and> sum_with p z (\<lambda>v. s (u v) v) t = z \<and> (\<exists>v\<in>t. u v \<noteq> 0)) = |
63 show "(\<exists>t u. finite t \<and> t \<subseteq> X \<and> sum_with p z (\<lambda>v. s (u v) v) t = z \<and> (\<exists>v\<in>t. u v \<noteq> 0)) = |
64 (\<exists>t u. finite t \<and> t \<subseteq> X' \<and> sum_with p' z' (\<lambda>v. s' (u v) v) t = z' \<and> (\<exists>v\<in>t. u v \<noteq> 0))" |
64 (\<exists>t u. finite t \<and> t \<subseteq> X' \<and> sum_with p' z' (\<lambda>v. s' (u v) v) t = z' \<and> (\<exists>v\<in>t. u v \<noteq> 0))" |
65 apply (transfer_prover_start, transfer_step+) |
65 apply (transfer_prover_start, transfer_step+) |
66 using * |
66 using * |
67 by (auto simp: intro!: comm_monoid_add_on_with.sum_with_mem) |
67 by (auto simp: intro!: comm_monoid_add_on_with.sum_with_mem) |