| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Wed, 24 Mar 2010 12:36:58 +0100 | |
| changeset 1631 | e94bfef17bb8 |
| parent 1630 | b295a928c56b |
| child 1632 | 68c8666453f7 |
| permissions | -rw-r--r-- |
| 1601 | 1 |
theory ExCoreHaskell |
2 |
imports "Parser" |
|
3 |
begin |
|
4 |
||
5 |
(* core haskell *) |
|
6 |
||
|
1624
91ab98dd9999
Experiments with Core Haskell support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1621
diff
changeset
|
7 |
ML {* val _ = recursive := false *}
|
|
91ab98dd9999
Experiments with Core Haskell support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1621
diff
changeset
|
8 |
ML {* val _ = cheat_bn_eqvt := true *}
|
|
91ab98dd9999
Experiments with Core Haskell support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1621
diff
changeset
|
9 |
ML {* val _ = cheat_bn_rsp := true *}
|
|
91ab98dd9999
Experiments with Core Haskell support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1621
diff
changeset
|
10 |
ML {* val _ = cheat_const_rsp := true *}
|
|
91ab98dd9999
Experiments with Core Haskell support.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1621
diff
changeset
|
11 |
ML {* val _ = cheat_alpha_bn_rsp := true *}
|
| 1601 | 12 |
atom_decl var |
13 |
atom_decl tvar |
|
14 |
||
|
1606
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
15 |
(* there are types, coercion types and regular types list-data-structure *) |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
16 |
|
| 1601 | 17 |
nominal_datatype tkind = |
18 |
KStar |
|
19 |
| KFun "tkind" "tkind" |
|
20 |
and ckind = |
|
21 |
CKEq "ty" "ty" |
|
22 |
and ty = |
|
23 |
TVar "tvar" |
|
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
24 |
| TC "char" |
| 1601 | 25 |
| TApp "ty" "ty" |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
26 |
| TFun "char" "ty_lst" |
| 1601 | 27 |
| TAll tv::"tvar" "tkind" T::"ty" bind tv in T |
28 |
| TEq "ty" "ty" "ty" |
|
|
1606
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
29 |
and ty_lst = |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
30 |
TsNil |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
31 |
| TsCons "ty" "ty_lst" |
| 1601 | 32 |
and co = |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
33 |
CC "char" |
| 1601 | 34 |
| CApp "co" "co" |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
35 |
| CFun "char" "co_lst" |
| 1601 | 36 |
| CAll tv::"tvar" "ckind" C::"co" bind tv in C |
37 |
| CEq "co" "co" "co" |
|
38 |
| CSym "co" |
|
39 |
| CCir "co" "co" |
|
40 |
| CLeft "co" |
|
41 |
| CRight "co" |
|
42 |
| CSim "co" |
|
43 |
| CRightc "co" |
|
44 |
| CLeftc "co" |
|
45 |
| CCoe "co" "co" |
|
|
1606
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
46 |
and co_lst = |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
47 |
CsNil |
|
75403378068b
Initial list unfoldings in Core Haskell.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1601
diff
changeset
|
48 |
| CsCons "co" "co_lst" |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
49 |
and trm = |
| 1601 | 50 |
Var "var" |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
51 |
| C "char" |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
52 |
| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
53 |
| LAMC tv::"tvar" "ckind" t::"trm" bind tv in t |
| 1601 | 54 |
| APP "trm" "ty" |
55 |
| Lam v::"var" "ty" t::"trm" bind v in t |
|
56 |
| App "trm" "trm" |
|
57 |
| Let x::"var" "ty" "trm" t::"trm" bind x in t |
|
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
58 |
| Case "trm" "assoc_lst" |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
59 |
| Cast "trm" "ty" --"ty is supposed to be a coercion type only" |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
60 |
and assoc_lst = |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
61 |
ANil |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
62 |
| ACons p::"pat" t::"trm" "assoc_lst" bind "bv p" in t |
| 1601 | 63 |
and pat = |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
64 |
K "char" "tvtk_lst" "tvck_lst" "vt_lst" |
|
1621
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
65 |
and vt_lst = |
|
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
66 |
VTNil |
|
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
67 |
| VTCons "var" "ty" "vt_lst" |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
68 |
and tvtk_lst = |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
69 |
TVTKNil |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
70 |
| TVTKCons "tvar" "tkind" "tvtk_lst" |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
71 |
and tvck_lst = |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
72 |
TVCKNil |
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
73 |
| TVCKCons "tvar" "ckind" "tvck_lst" |
| 1601 | 74 |
binder |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
75 |
bv :: "pat \<Rightarrow> atom set" |
|
1621
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
76 |
and bv_vt :: "vt_lst \<Rightarrow> atom set" |
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
77 |
and bv_tvtk :: "tvtk_lst \<Rightarrow> atom set" |
|
1621
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
78 |
and bv_tvck :: "tvck_lst \<Rightarrow> atom set" |
| 1601 | 79 |
where |
|
1621
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
80 |
"bv (K s tvts tvcs vs) = (bv_tvtk tvts) \<union> (bv_tvck tvcs) \<union> (bv_vt vs)" |
|
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
81 |
| "bv_vt VTNil = {}"
|
|
1609
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
82 |
| "bv_vt (VTCons v k t) = {atom v} \<union> bv_vt t"
|
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
83 |
| "bv_tvtk TVTKNil = {}"
|
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
84 |
| "bv_tvtk (TVTKCons v k t) = {atom v} \<union> bv_tvtk t"
|
|
c9bc3b61046c
Modification to Core Haskell to make it accepted with an empty binding function.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1606
diff
changeset
|
85 |
| "bv_tvck TVCKNil = {}"
|
|
1621
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
86 |
| "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t"
|
|
a40dbea68d0b
Core Haskell experiments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1615
diff
changeset
|
87 |
|
|
1626
0d7d0b8adca5
Showed support of Core Haskell
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1624
diff
changeset
|
88 |
lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15) |
|
0d7d0b8adca5
Showed support of Core Haskell
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1624
diff
changeset
|
89 |
lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
|
1615
0ea578c6dae3
Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1609
diff
changeset
|
90 |
|
|
1630
b295a928c56b
Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1626
diff
changeset
|
91 |
lemma |
|
1631
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
92 |
assumes a01: "\<And>b. P1 b KStar" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
93 |
and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
94 |
and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
95 |
and a04: "\<And>tvar b. P3 b (TVar tvar)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
96 |
and a05: "\<And>char b. P3 b (TC char)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
97 |
and a06: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P3 b (TApp ty1 ty2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
98 |
and a07: "\<And>char ty_lst b. \<lbrakk>\<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P3 b (TFun char ty_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
99 |
and a08: "\<And>tvar tkind ty b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P3 b (TAll tvar tkind ty)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
100 |
and a09: "\<And>ty1 ty2 ty3 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2; \<And>c. P3 c ty3\<rbrakk> \<Longrightarrow> P3 b (TEq ty1 ty2 ty3)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
101 |
and a10: "\<And>b. P4 b TsNil" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
102 |
and a11: "\<And>ty ty_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P4 c ty_lst\<rbrakk> \<Longrightarrow> P4 b (TsCons ty ty_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
103 |
and a12: "\<And>char b. P5 b (CC char)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
104 |
and a13: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CApp co1 co2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
105 |
and a14: "\<And>char co_lst b. \<lbrakk>\<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P5 b (CFun char co_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
106 |
and a15: "\<And>tvar ckind co b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CAll tvar ckind co)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
107 |
and a16: "\<And>co1 co2 co3 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2; \<And>c. P5 c co3\<rbrakk> \<Longrightarrow> P5 b (CEq co1 co2 co3)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
108 |
and a17: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSym co)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
109 |
and a18: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCir co1 co2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
110 |
and a19: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeft co)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
111 |
and a20: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRight co)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
112 |
and a21: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CSim co)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
113 |
and a22: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CRightc co)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
114 |
and a23: "\<And>co b. \<lbrakk>\<And>c. P5 c co\<rbrakk> \<Longrightarrow> P5 b (CLeftc co)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
115 |
and a24: "\<And>co1 co2 b. \<lbrakk>\<And>c. P5 c co1; \<And>c. P5 c co2\<rbrakk> \<Longrightarrow> P5 b (CCoe co1 co2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
116 |
and a25: "\<And>b. P6 b CsNil" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
117 |
and a26: "\<And>co co_lst b. \<lbrakk>\<And>c. P5 c co; \<And>c. P6 c co_lst\<rbrakk> \<Longrightarrow> P6 b (CsCons co co_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
118 |
and a27: "\<And>var b. P7 b (Var var)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
119 |
and a28: "\<And>char b. P7 b (C char)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
120 |
and a29: "\<And>tvar tkind trm b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P7 c trm\<rbrakk> \<Longrightarrow> P7 b (LAMT tvar tkind trm)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
121 |
and a30: "\<And>tvar ckind trm b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P7 c trm\<rbrakk> \<Longrightarrow> P7 b (LAMC tvar ckind trm)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
122 |
and a31: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (APP trm ty)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
123 |
and a32: "\<And>var ty trm b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm\<rbrakk> \<Longrightarrow> P7 b (Lam var ty trm)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
124 |
and a33: "\<And>trm1 trm2 b. \<lbrakk>\<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> \<Longrightarrow> P7 b (App trm1 trm2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
125 |
and a34: "\<And>var ty trm1 trm2 b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P7 c trm1; \<And>c. P7 c trm2\<rbrakk> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
126 |
\<Longrightarrow> P7 b (Let var ty trm1 trm2)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
127 |
and a35: "\<And>trm assoc_lst b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> \<Longrightarrow> P7 b (Case trm assoc_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
128 |
and a36: "\<And>trm ty b. \<lbrakk>\<And>c. P7 c trm; \<And>c. P3 c ty\<rbrakk> \<Longrightarrow> P7 b (Cast trm ty)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
129 |
and a37: "\<And>b. P8 b ANil" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
130 |
and a38: "\<And>pat trm assoc_lst b. \<lbrakk>\<And>c. P9 c pat; \<And>c. P7 c trm; \<And>c. P8 c assoc_lst\<rbrakk> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
131 |
\<Longrightarrow> P8 b (ACons pat trm assoc_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
132 |
and a39: "\<And>char tvtk_lst tvck_lst vt_lst b. \<lbrakk>\<And>c. P11 c tvtk_lst; \<And>c. P12 c tvck_lst; \<And>c. P10 c vt_lst\<rbrakk> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
133 |
\<Longrightarrow> P9 b (K char tvtk_lst tvck_lst vt_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
134 |
and a40: "\<And>b. P10 b VTNil" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
135 |
and a41: "\<And>var ty vt_lst b. \<lbrakk>\<And>c. P3 c ty; \<And>c. P10 c vt_lst\<rbrakk> \<Longrightarrow> P10 b (VTCons var ty vt_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
136 |
and a42: "\<And>b. P11 b TVTKNil" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
137 |
and a43: "\<And>tvar tkind tvtk_lst b. \<lbrakk>\<And>c. P1 c tkind; \<And>c. P11 c tvtk_lst\<rbrakk> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
138 |
\<Longrightarrow> P11 b (TVTKCons tvar tkind tvtk_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
139 |
and a44: "\<And>b. P12 b TVCKNil" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
140 |
and a45: "\<And>tvar ckind tvck_lst b. \<lbrakk>\<And>c. P2 c ckind; \<And>c. P12 c tvck_lst\<rbrakk> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
141 |
\<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
142 |
shows "P1 (a :: 'a :: pt) tkind \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
143 |
P2 (b :: 'b :: pt) ckind \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
144 |
P3 (c :: 'c :: pt) ty \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
145 |
P4 (d :: 'd :: pt) ty_lst \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
146 |
P5 (e :: 'e :: pt) co \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
147 |
P6 (f :: 'f :: pt) co_lst \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
148 |
P7 (g :: 'g :: pt) trm \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
149 |
P8 (h :: 'h :: pt) assoc_lst \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
150 |
P9 (i :: 'i :: pt) pat \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
151 |
P10 (j :: 'j :: pt) vt_lst \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
152 |
P11 (k :: 'k :: pt) tvtk_lst \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
153 |
P12 (l :: 'l :: pt) tvck_lst" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
154 |
proof - |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
155 |
have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))" |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
156 |
apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
157 |
apply (simp add: a01) |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
158 |
sorry |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
159 |
have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
160 |
have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
161 |
have g3: "P3 c (0 \<bullet> ty) \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
162 |
P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
163 |
P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and> |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
164 |
P10 j (0 \<bullet> vt_lst) \<and> P11 k (0 \<bullet> tvtk_lst) \<and> P12 l (0 \<bullet> tvck_lst)" using a by blast |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
165 |
show ?thesis using g1 g2 g3 by simp |
|
e94bfef17bb8
stating the strong induction; further.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1630
diff
changeset
|
166 |
qed |
|
1615
0ea578c6dae3
Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1609
diff
changeset
|
167 |
|
| 1601 | 168 |
end |
169 |