deaa63707b60a8f026b208a37089d92e7ab1e9b9
[darcs-mirror-isa-launchbury.git] / Launchbury / Sestoft.thy
1 theory Sestoft 
2 imports SestoftConf
3 begin
4
5 inductive step :: "conf \<Rightarrow> conf \<Rightarrow> bool" (infix "\<Rightarrow>" 50) where
6   app\<^sub>1:  "(\<Gamma>, App e x, S) \<Rightarrow> (\<Gamma>, e , Arg x # S)"
7 | app\<^sub>2:  "(\<Gamma>, Lam [y]. e, Arg x # S) \<Rightarrow> (\<Gamma>, e[y ::= x] , S)"
8 | var\<^sub>1:  "map_of \<Gamma> x = Some e \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow> (delete x \<Gamma>, e , Upd x # S)"
9 | var\<^sub>2:  "x \<notin> domA \<Gamma> \<Longrightarrow> isVal e \<Longrightarrow> (\<Gamma>, e, Upd x # S) \<Rightarrow> ((x,e)# \<Gamma>, e , S)"
10 | let\<^sub>1:  "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> (\<Gamma>, Let \<Delta> e, S) \<Rightarrow> (\<Delta>@\<Gamma>, e , S)"
11 (* | if\<^sub>1:  "(\<Gamma>, scrut ? e1 : e2, S) \<Rightarrow> (\<Gamma>, scrut, Alts e1 e2 # S)" *)
12
13 abbreviation steps (infix "\<Rightarrow>\<^sup>*" 50) where "steps \<equiv> step\<^sup>*\<^sup>*"
14
15 lemma SmartLet_stepI:
16    "atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> (\<Gamma>, SmartLet \<Delta> e, S) \<Rightarrow>\<^sup>*  (\<Delta>@\<Gamma>, e , S)"
17 unfolding SmartLet_def by (auto intro: let\<^sub>1)
18
19 lemma lambda_var: "map_of \<Gamma> x = Some e \<Longrightarrow> isVal e  \<Longrightarrow> (\<Gamma>, Var x, S) \<Rightarrow>\<^sup>* ((x,e) # delete x \<Gamma>, e , S)"
20   by (rule rtranclp_trans[OF r_into_rtranclp r_into_rtranclp])
21      (auto intro: var\<^sub>1 var\<^sub>2)
22
23 text {* An induction rule that skips the annoying case of a lambda taken off the heap *}
24
25 lemma step_induction[consumes 2, case_names app\<^sub>1 app\<^sub>2 thunk lamvar var\<^sub>2 let\<^sub>1 refl trans]:
26   assumes "c \<Rightarrow>\<^sup>* c'"
27   assumes "\<not> boring_step c'"
28   assumes app\<^sub>1:  "\<And> \<Gamma> e x S . P (\<Gamma>, App e x, S)  (\<Gamma>, e , Arg x # S)"
29   assumes app\<^sub>2:  "\<And> \<Gamma> y e x S . P (\<Gamma>, Lam [y]. e, Arg x # S) (\<Gamma>, e[y ::= x] , S)"
30   assumes thunk:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> \<not> isVal e \<Longrightarrow> P (\<Gamma>, Var x, S) (delete x \<Gamma>, e , Upd x # S)"
31   assumes lamvar:  "\<And> \<Gamma> x e S . map_of \<Gamma> x = Some e \<Longrightarrow> isVal e \<Longrightarrow> P (\<Gamma>, Var x, S) ((x,e) # delete x \<Gamma>, e , S)"
32   assumes var\<^sub>2:  "\<And> \<Gamma> x e S . x \<notin> domA \<Gamma> \<Longrightarrow> isVal e \<Longrightarrow> P (\<Gamma>, e, Upd x # S) ((x,e)# \<Gamma>, e , S)"
33   assumes let\<^sub>1:  "\<And> \<Delta> \<Gamma> e S . atom ` domA \<Delta> \<sharp>* \<Gamma> \<Longrightarrow> atom ` domA \<Delta> \<sharp>* S \<Longrightarrow> P (\<Gamma>, Let \<Delta> e, S) (\<Delta>@\<Gamma>, e, S)"
34   assumes refl: "\<And> c. P c c"
35   assumes trans[trans]: "\<And> c c' c''. c \<Rightarrow>\<^sup>* c' \<Longrightarrow> c' \<Rightarrow>\<^sup>* c'' \<Longrightarrow> P c c' \<Longrightarrow> P c' c'' \<Longrightarrow> P c c''"
36   shows "P c c'"
37 proof-
38   from assms(1)
39   have "P c c' \<or> (boring_step c' \<and> (\<forall> c''. c' \<Rightarrow> c'' \<longrightarrow> P c c''))"
40   proof(induction)
41   case base
42     have "P c c" by (rule refl)
43     thus ?case..
44   next
45   case (step y z)
46     from step(3)
47     show ?case
48     proof
49       assume "P c y"
50
51       note t = trans[OF `c \<Rightarrow>\<^sup>* y` r_into_rtranclp[where r = step, OF `y \<Rightarrow> z`]]
52       
53       from `y \<Rightarrow> z`
54       show ?thesis
55       proof (cases)
56         case app\<^sub>1 hence "P y z" using assms(3) by metis
57         with `P c y` show ?thesis by (metis t)
58       next
59         case app\<^sub>2 hence "P y z" using assms(4) by metis
60         with `P c y` show ?thesis by (metis t)
61       next
62         case (var\<^sub>1 \<Gamma> x e S)
63         show ?thesis
64         proof (cases "isVal e")
65           case False with var\<^sub>1 have "P y z" using assms(5) by metis
66           with `P c y` show ?thesis by (metis t)
67         next
68           case True
69           have *: "y \<Rightarrow>\<^sup>* ((x,e) # delete x \<Gamma>, e , S)" using var\<^sub>1 True lambda_var by metis
70
71           have "boring_step (delete x \<Gamma>, e, Upd x # S)" using True ..
72           moreover
73           have "P y ((x,e) # delete x \<Gamma>, e , S)" using var\<^sub>1 True assms(6) by metis
74           with `P c y` have "P c ((x,e) # delete x \<Gamma>, e , S)" by (rule trans[OF `c \<Rightarrow>\<^sup>* y` *])
75           ultimately
76           show ?thesis using var\<^sub>1(2,3) True by (auto elim!: step.cases)
77         qed
78       next
79         case var\<^sub>2 hence "P y z" using assms(7) by metis
80         with `P c y` show ?thesis by (metis t)
81       next
82         case let\<^sub>1 hence "P y z" using assms(8) by metis
83         with `P c y` show ?thesis by (metis t)
84       qed
85     next
86       assume "boring_step y \<and> (\<forall>c''. y \<Rightarrow> c'' \<longrightarrow> P c c'')"
87       with `y \<Rightarrow> z`
88       have "P c z" by blast
89       thus ?thesis..
90     qed
91   qed
92   with assms(2)
93   show ?thesis by auto
94 qed
95
96
97
98 end