6 lemmas app = Ltgt1_app |
6 lemmas app = Ltgt1_app |
7 |
7 |
8 lemma Num: |
8 lemma Num: |
9 shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" |
9 shows "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" |
10 proof (induct M rule: lam.induct) |
10 proof (induct M rule: lam.induct) |
11 case (V n) |
11 case (Var n) |
12 have "Num \<cdot> \<lbrace>V n\<rbrace> = Num \<cdot> (Var \<cdot> V n)" by simp |
12 have "Num \<cdot> \<lbrace>Var n\<rbrace> = Num \<cdot> (VAR \<cdot> Var n)" by simp |
13 also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Var \<cdot> V n)" by simp |
13 also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (VAR \<cdot> Var n)" by simp |
14 also have "... \<approx> Var \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app . |
14 also have "... \<approx> VAR \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app . |
15 also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 2 \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Var_app . |
15 also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 2 \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using VAR_app . |
16 also have "... \<approx> A1 \<cdot> V n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp |
16 also have "... \<approx> A1 \<cdot> Var n \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp |
17 also have "... \<approx> F1 \<cdot> V n" using A_app(1) . |
17 also have "... \<approx> F1 \<cdot> Var n" using A_app(1) . |
18 also have "... \<approx> App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V n)" using F_app(1) . |
18 also have "... \<approx> APP \<cdot> \<lbrace>VAR\<rbrace> \<cdot> (VAR \<cdot> Var n)" using F_app(1) . |
19 also have "... = \<lbrace>\<lbrace>V n\<rbrace>\<rbrace>" by simp |
19 also have "... = \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>" by simp |
20 finally show "Num \<cdot> \<lbrace>V n\<rbrace> \<approx> \<lbrace>\<lbrace>V n\<rbrace>\<rbrace>". |
20 finally show "Num \<cdot> \<lbrace>Var n\<rbrace> \<approx> \<lbrace>\<lbrace>Var n\<rbrace>\<rbrace>". |
21 next |
21 next |
22 case (Ap M N) |
22 case (App M N) |
23 assume IH: "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" "Num \<cdot> \<lbrace>N\<rbrace> \<approx> \<lbrace>\<lbrace>N\<rbrace>\<rbrace>" |
23 assume IH: "Num \<cdot> \<lbrace>M\<rbrace> \<approx> \<lbrace>\<lbrace>M\<rbrace>\<rbrace>" "Num \<cdot> \<lbrace>N\<rbrace> \<approx> \<lbrace>\<lbrace>N\<rbrace>\<rbrace>" |
24 have "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> = Num \<cdot> (App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp |
24 have "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> = Num \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp |
25 also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp |
25 also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>)" by simp |
26 also have "... \<approx> App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app . |
26 also have "... \<approx> APP \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app . |
27 also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 1 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using App_app . |
27 also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 1 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using APP_app . |
28 also have "... \<approx> A2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp |
28 also have "... \<approx> A2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp |
29 also have "... \<approx> F2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> Num" using A_app(2) by simp |
29 also have "... \<approx> F2 \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace> \<cdot> Num" using A_app(2) by simp |
30 also have "... \<approx> App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (Num \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) . |
30 also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (Num \<cdot> \<lbrace>M\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using F_app(2) . |
31 also have "... \<approx> App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using IH by simp |
31 also have "... \<approx> APP \<cdot> (APP \<cdot> \<lbrace>APP\<rbrace> \<cdot> (\<lbrace>\<lbrace>M\<rbrace>\<rbrace>)) \<cdot> (Num \<cdot> \<lbrace>N\<rbrace>)" using IH by simp |
32 also have "... \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>" using IH by simp |
32 also have "... \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>" using IH by simp |
33 finally show "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>". |
33 finally show "Num \<cdot> \<lbrace>M \<cdot> N\<rbrace> \<approx> \<lbrace>\<lbrace>M \<cdot> N\<rbrace>\<rbrace>". |
34 next |
34 next |
35 case (Lm x P) |
35 case (Lam x P) |
36 assume IH: "Num \<cdot> \<lbrace>P\<rbrace> \<approx> \<lbrace>\<lbrace>P\<rbrace>\<rbrace>" |
36 assume IH: "Num \<cdot> \<lbrace>P\<rbrace> \<approx> \<lbrace>\<lbrace>P\<rbrace>\<rbrace>" |
37 have "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> = Num \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp |
37 have "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> = Num \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp |
38 also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp |
38 also have "... = \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>P\<rbrace>)" by simp |
39 also have "... \<approx> Abs \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app . |
39 also have "... \<approx> Abs \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using app . |
40 also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 0 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Abs_app . |
40 also have "... \<approx> \<guillemotleft>[A1,A2,A3]\<guillemotright> \<cdot> Umn 2 0 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using Abs_app . |
41 also have "... \<approx> A3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp |
41 also have "... \<approx> A3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[A1,A2,A3]\<guillemotright>" using U_app by simp |
42 also have "... \<approx> F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" using A_app(3) . |
42 also have "... \<approx> F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>" using A_app(3) . |
43 also have "... = F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Num" by simp |
43 also have "... = F3 \<cdot> (\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Num" by simp |
44 also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> V x)))" by (rule F3_app) simp_all |
44 also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> ((\<integral> x. \<lbrace>P\<rbrace>) \<cdot> Var x)))" by (rule F3_app) simp_all |
45 also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp |
45 also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. (Num \<cdot> \<lbrace>P\<rbrace>))" using beta_app by simp |
46 also have "... \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>\<lbrace>P\<rbrace>\<rbrace>)" using IH by simp |
46 also have "... \<approx> APP \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> \<integral> x. \<lbrace>\<lbrace>P\<rbrace>\<rbrace>)" using IH by simp |
47 also have "... = \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" by simp |
47 also have "... = \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" by simp |
48 finally show "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> \<approx> \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" . |
48 finally show "Num \<cdot> \<lbrace>\<integral> x. P\<rbrace> \<approx> \<lbrace>\<lbrace>\<integral> x. P\<rbrace>\<rbrace>" . |
49 qed |
49 qed |
50 |
50 |
51 lemmas [simp] = Ap Num |
51 lemmas [simp] = Ap Num |
54 theorem SFP: |
54 theorem SFP: |
55 fixes F :: lam |
55 fixes F :: lam |
56 shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>" |
56 shows "\<exists>X. X \<approx> F \<cdot> \<lbrace>X\<rbrace>" |
57 proof - |
57 proof - |
58 obtain x :: var where [simp]:"atom x \<sharp> F" using obtain_fresh by blast |
58 obtain x :: var where [simp]:"atom x \<sharp> F" using obtain_fresh by blast |
59 def W \<equiv> "\<integral>x. (F \<cdot> (App \<cdot> V x \<cdot> (Num \<cdot> V x)))" |
59 def W \<equiv> "\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))" |
60 def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>" |
60 def X \<equiv> "W \<cdot> \<lbrace>W\<rbrace>" |
61 have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def .. |
61 have a: "X = W \<cdot> \<lbrace>W\<rbrace>" unfolding X_def .. |
62 also have "... = (\<integral>x. (F \<cdot> (App \<cdot> V x \<cdot> (Num \<cdot> V x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def .. |
62 also have "... = (\<integral>x. (F \<cdot> (APP \<cdot> Var x \<cdot> (Num \<cdot> Var x)))) \<cdot> \<lbrace>W\<rbrace>" unfolding W_def .. |
63 also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp |
63 also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> (Num \<cdot> \<lbrace>W\<rbrace>))" by simp |
64 also have "... \<approx> F \<cdot> (App \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp |
64 also have "... \<approx> F \<cdot> (APP \<cdot> \<lbrace>W\<rbrace> \<cdot> \<lbrace>\<lbrace>W\<rbrace>\<rbrace>)" by simp |
65 also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp |
65 also have "... \<approx> F \<cdot> \<lbrace>W \<cdot> \<lbrace>W\<rbrace>\<rbrace>" by simp |
66 also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def .. |
66 also have "... = F \<cdot> \<lbrace>X\<rbrace>" unfolding X_def .. |
67 finally show ?thesis by blast |
67 finally show ?thesis by blast |
68 qed |
68 qed |
69 |
69 |