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