-
Notifications
You must be signed in to change notification settings - Fork 1
/
Fun_Algebra.thy
90 lines (57 loc) · 3.52 KB
/
Fun_Algebra.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
theory Fun_Algebra imports
"jormungand/sep_algebra/Sep_Tactics"
"jormungand/Hoare_Sep_Tactics/Extended_Separation_Algebra"
Lens
begin
instantiation unit :: stronger_sep_algebra begin
fun sep_disj_unit :: "unit \<Rightarrow> unit \<Rightarrow> bool" where
"sep_disj_unit x y \<longleftrightarrow> True"
fun plus_unit :: "unit \<Rightarrow> unit \<Rightarrow> unit" where
"plus_unit x y = ()"
definition "zero_unit = ()"
instance
by (standard, case_tac x; (clarsimp simp: zero_unit_def)?)
end
lemma [simp]: "None ## x" by (clarsimp simp: sep_disj_option_def)
definition "add_lens l l' = Lens (\<lambda>s. (get l s, get l' s)) (\<lambda>s (a, b). set l' (set l s a) b) (\<lambda>(a, b). valid l a \<and> valid l' b)"
definition "disj_lens l l' \<equiv> (\<forall>s v. get l s = get l (set l' s v)) \<and> (\<forall>s v. get l' s = get l' (set l s v)) "
definition "ptr_lens p = Lens (\<lambda>s. s p) (\<lambda>s v. s(p := v)) (\<lambda>s. True)"
lemma "p \<noteq> p' \<Longrightarrow> disj_lens (ptr_lens p) (ptr_lens p')"
apply (clarsimp simp: disj_lens_def, safe; clarsimp simp: ptr_lens_def)
done
definition "disj_cylindric_set S S' \<equiv> \<forall>f\<in>S. \<forall>f'\<in>S'. f o f' = f' o f"
datatype 'a domain_pair = Pair (dom_funs : "('a \<Rightarrow> 'a) set") (state_of: "'a \<Rightarrow> 'a")
abbreviation "pointed_set \<equiv> {d. state_of d \<in> dom_funs d \<and> id \<in> dom_funs d}"
typedef ('a) p_set = "pointed_set :: 'a domain_pair set"
by (rule_tac x="Pair {id} id" in exI, clarsimp)
definition "point_of p = state_of (Rep_p_set p)"
definition "set_of p = dom_funs (Rep_p_set p)"
definition "id_p \<equiv> Abs_p_set (Pair {id} id)"
lemma set_of_id [simp]: "set_of (id_p) = {id}"
apply (clarsimp simp: set_of_def id_p_def)
by (subst Abs_p_set_inverse; clarsimp)
lemma point_of_id [simp]: "point_of (id_p) = id"
apply (clarsimp simp: point_of_def id_p_def)
by (subst Abs_p_set_inverse; clarsimp)
lemma p_set_eqI: "set_of A = set_of B \<Longrightarrow> point_of A = point_of B \<Longrightarrow> A = B"
by (metis Rep_p_set_inject domain_pair.expand point_of_def set_of_def)
lemma point_in_set[simp]: "point_of S \<in> set_of S"
by (metis (mono_tags, lifting) Rep_p_set mem_Collect_eq point_of_def set_of_def)
lemma id_in_set[simp]: "id \<in> set_of S"
by (metis (mono_tags, lifting) Rep_p_set mem_Collect_eq point_of_def set_of_def)
definition "valid_dp S \<equiv> \<forall>f\<in>S. \<forall>g\<in>S. f o g = f"
lemma commutative_lens_get_set: "valid_lens b \<Longrightarrow> valid_lens c \<Longrightarrow>
(\<lambda>s. set b s v) o (\<lambda>s. set c s v') = (\<lambda>s. set c s v') o (\<lambda>s. set b s v) \<Longrightarrow>
v = get b (set c (set b s v) v')"
by (metis comp_apply get_set_def valid_lens_def)
lemma surj_setter: "valid_lens l \<Longrightarrow> surj (\<lambda>(s, v). set l s v)"
apply (clarsimp simp: surj_def)
by (metis set_get_def valid_lens_def)
lemma lens_commuteI: "valid_lens b \<Longrightarrow> valid_lens c \<Longrightarrow>
((\<lambda>s. set b s v) o (\<lambda>s. set c s v') = (\<lambda>s. set b s v) \<and> (\<lambda>s. set b s v) o (\<lambda>s. set c s v') = (\<lambda>s. set c s v')) \<or>
(\<forall>v v'. (\<lambda>s. set b s v) o (\<lambda>s. set c s v') = (\<lambda>s. set c s v') o (\<lambda>s. set b s v)) \<Longrightarrow> (\<lambda>s. set b s v) o (\<lambda>s. set c s v') = (\<lambda>s. set c s v') o (\<lambda>s. set b s v)"
apply (intro ext; clarsimp)
apply (elim disjE; clarsimp?)
apply metis
by (metis comp_apply)
end