c41c46aecb4658060a9eb3147dc70b417fc3a45e
[darcs-mirror-isa-launchbury.git] / Launchbury / SestoftConf.thy
1 theory SestoftConf
2 imports Terms Substitution
3 begin
4
5 datatype stack_elem = Alts exp exp | Arg var | Upd var | Dummy var
6
7 instantiation stack_elem :: pt
8 begin
9 definition  "\<pi> \<bullet> x = (case x of (Alts e1 e2) \<Rightarrow> Alts (\<pi> \<bullet> e1) (\<pi> \<bullet> e2) | (Arg v) \<Rightarrow> Arg (\<pi> \<bullet> v) | (Upd v) \<Rightarrow> Upd (\<pi> \<bullet> v) | (Dummy v) \<Rightarrow> Dummy (\<pi> \<bullet> v))"
10 instance
11   by default (auto simp add: permute_stack_elem_def split:stack_elem.split)
12 end
13
14 lemma Alts_eqvt[eqvt]: "\<pi> \<bullet> (Alts e1 e2) = Alts (\<pi> \<bullet> e1) (\<pi> \<bullet> e2)"
15   and Arg_eqvt[eqvt]: "\<pi> \<bullet> (Arg v) = Arg (\<pi> \<bullet> v)"
16   and Upd_eqvt[eqvt]: "\<pi> \<bullet> (Upd v) = Upd (\<pi> \<bullet> v)"
17   and Dummy_eqvt[eqvt]: "\<pi> \<bullet> (Dummy v) = Dummy (\<pi> \<bullet> v)"
18   by (auto simp add: permute_stack_elem_def split:stack_elem.split)
19
20 find_theorems supp name:Pair
21 lemma supp_Alts[simp]: "supp (Alts e1 e2) = supp e1 \<union> supp e2" unfolding supp_def by (auto simp add: Collect_imp_eq Collect_neg_eq)
22 lemma supp_Arg[simp]: "supp (Arg v) = supp v"  unfolding supp_def by auto
23 lemma supp_Upd[simp]: "supp (Upd v) = supp v"  unfolding supp_def by auto
24 lemma supp_Dummy[simp]: "supp (Dummy v) = supp v"  unfolding supp_def by auto
25 lemma fresh_Alts[simp]: "a \<sharp> Alts e1 e2 = (a \<sharp> e1 \<and> a \<sharp> e2)" unfolding fresh_def by auto
26 lemma fresh_star_Alts[simp]: "a \<sharp>* Alts e1 e2 = (a \<sharp>* e1 \<and> a \<sharp>* e2)" unfolding fresh_star_def by auto
27 lemma fresh_Arg[simp]: "a \<sharp> Arg v = a \<sharp> v" unfolding fresh_def by auto
28 lemma fresh_Upd[simp]: "a \<sharp> Upd v = a \<sharp> v" unfolding fresh_def by auto
29 lemma fresh_Dummy[simp]: "a \<sharp> Dummy v = a \<sharp> v" unfolding fresh_def by auto
30 lemma fv_Alts[simp]: "fv (Alts e1 e2) = fv e1 \<union> fv e2"  unfolding fv_def by auto
31 lemma fv_Arg[simp]: "fv (Arg v) = fv v"  unfolding fv_def by auto
32 lemma fv_Upd[simp]: "fv (Upd v) = fv v"  unfolding fv_def by auto
33
34 instance stack_elem :: fs  by (default, case_tac x) (auto simp add: finite_supp)
35
36 type_synonym stack = "stack_elem list"
37
38 fun ap :: "stack \<Rightarrow> var set" where
39   "ap [] = {}"
40 | "ap (Alts e1 e2 # S) = ap S"
41 | "ap (Arg x # S) = insert x (ap S)"
42 | "ap (Upd x # S) = ap S"
43 | "ap (Dummy x # S) = ap S"
44 fun upds :: "stack \<Rightarrow> var set" where
45   "upds [] = {}"
46 | "upds (Alts e1 e2 # S) = upds S"
47 | "upds (Upd x # S) = insert x (upds S)"
48 | "upds (Arg x # S) = upds S"
49 | "upds (Dummy x # S) = upds S"
50 fun flattn :: "stack \<Rightarrow> var list" where
51   "flattn [] = []"
52 | "flattn (Alts e1 e2 # S) = fv_list e1 @ fv_list e2 @ flattn S"
53 | "flattn (Upd x # S) = x # flattn S"
54 | "flattn (Arg x # S) = x # flattn S"
55 | "flattn (Dummy x # S) = x # flattn S"
56 fun upds_list :: "stack \<Rightarrow> var list" where
57   "upds_list [] = []"
58 | "upds_list (Alts e1 e2 # S) = upds_list S"
59 | "upds_list (Upd x # S) = x # upds_list S"
60 | "upds_list (Arg x # S) = upds_list S"
61 | "upds_list (Dummy x # S) = upds_list S"
62
63 lemma set_upds_list[simp]:
64   "set (upds_list S) = upds S"
65   by (induction S rule: upds_list.induct) auto
66
67 lemma ups_fv_subset: "upds S \<subseteq> fv S"
68   by (induction S rule: upds.induct) auto
69 lemma ap_fv_subset: "ap S \<subseteq> fv S"
70   by (induction S rule: upds.induct) auto
71
72 lemma fresh_flattn[simp]: "atom (a::var) \<sharp> flattn S \<longleftrightarrow> atom a \<sharp> S"
73   by (induction S rule:flattn.induct) (auto simp add: fresh_Nil fresh_Cons fresh_append fresh_fv[OF finite_fv])
74 lemma fresh_star_flattn[simp]: "atom ` (as:: var set) \<sharp>* flattn S \<longleftrightarrow> atom ` as \<sharp>* S"
75   by (auto simp add: fresh_star_def)
76
77 type_synonym conf = "(heap \<times> exp \<times> stack)"
78
79 inductive boring_step where
80   "isVal e \<Longrightarrow> boring_step (\<Gamma>, e, Upd x # S)"
81
82
83 fun heap_upds_ok where "heap_upds_ok (\<Gamma>,S) \<longleftrightarrow> domA \<Gamma> \<inter> upds S = {} \<and> distinct (upds_list S)"
84
85 lemma heap_upds_okE: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> x \<in> domA \<Gamma> \<Longrightarrow> x \<notin> upds S"
86   by auto
87
88 lemma heap_upds_ok_Nil[simp]: "heap_upds_ok (\<Gamma>, [])" by auto
89 lemma heap_upds_ok_app1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Arg x # S)" by auto
90 lemma heap_upds_ok_app2: "heap_upds_ok (\<Gamma>, Arg x # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
91 lemma heap_upds_ok_alts1: "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (\<Gamma>,Alts e1 e2 # S)" by auto
92 lemma heap_upds_ok_alts2: "heap_upds_ok (\<Gamma>, Alts e1 e2 # S) \<Longrightarrow> heap_upds_ok (\<Gamma>, S)" by auto
93
94 lemma heap_upds_ok_append:
95   assumes "domA \<Delta> \<inter> domA \<Gamma> = {}"
96   assumes "domA \<Delta> \<inter> upds S = {}"
97   assumes "heap_upds_ok (\<Gamma>,S)"
98   shows "heap_upds_ok (\<Delta>@\<Gamma>, S)"
99   using assms
100   unfolding heap_upds_ok.simps
101   by auto
102
103 lemma heap_upds_ok_to_stack:
104   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, Upd x #S)"
105   by (auto)
106
107 lemma heap_upds_ok_delete:
108   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (delete x \<Gamma>, S)"
109   by auto
110
111 lemma heap_upds_ok_restrictA:
112   "heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok (restrictA V \<Gamma>, S)"
113   by auto
114
115 lemma heap_upds_ok_to_heap:
116   "heap_upds_ok (\<Gamma>, Upd x # S) \<Longrightarrow> heap_upds_ok ((x,e) # \<Gamma>, S)"
117   by auto
118
119 lemma heap_upds_ok_reorder:
120   "x \<in> domA \<Gamma> \<Longrightarrow> heap_upds_ok (\<Gamma>, S) \<Longrightarrow> heap_upds_ok ((x,e) # delete x \<Gamma>, S)"
121   by (intro heap_upds_ok_to_heap heap_upds_ok_to_stack)
122
123 lemmas heap_upds_ok_intros[intro] = heap_upds_ok_to_heap heap_upds_ok_to_stack heap_upds_ok_reorder heap_upds_ok_app1 heap_upds_ok_app2 heap_upds_ok_alts1 heap_upds_ok_alts2 heap_upds_ok_delete heap_upds_ok_restrictA
124 lemmas heap_upds_ok.simps[simp del]
125
126 fun restr_stack :: "var set \<Rightarrow> stack \<Rightarrow> stack"
127   where "restr_stack V [] = []"
128       | "restr_stack V (Alts e1 e2 # S) = Alts e1 e2 # restr_stack V S"
129       | "restr_stack V (Arg x # S) = Arg x # restr_stack V S"
130       | "restr_stack V (Upd x # S) = (if x \<in> V then Upd x # restr_stack V S else restr_stack V S)"
131       | "restr_stack V (Dummy x # S) = Dummy x # restr_stack V S"
132
133 lemma restr_stack_cong:
134   "(\<And> x. x \<in> upds S \<Longrightarrow> x \<in> V \<longleftrightarrow> x \<in> V') \<Longrightarrow> restr_stack V S = restr_stack V' S"
135   by (induction V S rule: restr_stack.induct) auto
136
137 lemma upds_restr_stack[simp]: "upds (restr_stack V S) = upds S \<inter> V"
138   by (induction V S rule: restr_stack.induct) auto
139
140 lemma fresh_star_restict_stack[intro]:
141   "a \<sharp>* S \<Longrightarrow> a \<sharp>* restr_stack V S"
142   by (induction V S rule: restr_stack.induct) (auto simp add: fresh_star_Cons)
143
144
145 end