Nominal/ExCoreHaskell.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Wed, 24 Mar 2010 12:05:38 +0100
changeset 1630 b295a928c56b
parent 1626 0d7d0b8adca5
child 1631 e94bfef17bb8
permissions -rw-r--r--
Working on stating induct.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1601
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
theory ExCoreHaskell
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
imports "Parser"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
(* core haskell *)
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
atom_decl var
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
atom_decl tvar
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
nominal_datatype tkind =
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
  KStar
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
| KFun "tkind" "tkind"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
and ckind =
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
  CKEq "ty" "ty"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
and ty =
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
| CAll tv::"tvar" "ckind" C::"co"  bind tv in C
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
| CEq "co" "co" "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
| CSym "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
| CCir "co" "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
| CLeft "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
| CRight "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
| CSim "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
| CRightc "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
| CLeftc "co"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
| APP "trm" "ty"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
| Lam v::"var" "ty" t::"trm"       bind v in t
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
| App "trm" "trm"
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    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 
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    92
  assumes a01: "P1 KStar"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    93
  and a02: "\<And>tkind1 tkind2. \<lbrakk>P1 tkind1; P1 tkind2\<rbrakk> \<Longrightarrow> P1 (KFun tkind1 tkind2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    94
  and a03: "\<And>ty1 ty2. \<lbrakk>P3 ty1; P3 ty2\<rbrakk> \<Longrightarrow> P2 (CKEq ty1 ty2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    95
  and a04: "\<And>tvar. P3 (TVar tvar)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    96
  and a05: "\<And>char. P3 (TC char)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    97
  and a06: "\<And>ty1 ty2. \<lbrakk>P3 ty1; P3 ty2\<rbrakk> \<Longrightarrow> P3 (TApp ty1 ty2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    98
  and a07: "\<And>char ty_lst. P4 ty_lst \<Longrightarrow> P3 (TFun char ty_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
    99
  and a08: "\<And>tvar tkind ty. \<lbrakk>P1 tkind; P3 ty\<rbrakk> \<Longrightarrow> P3 (TAll tvar tkind ty)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   100
  and a09: "\<And>ty1 ty2 ty3. \<lbrakk>P3 ty1; P3 ty2; P3 ty3\<rbrakk> \<Longrightarrow> P3 (TEq ty1 ty2 ty3)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   101
  and a10: "P4 TsNil"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   102
  and a11: "\<And>ty ty_lst. \<lbrakk>P3 ty; P4 ty_lst\<rbrakk> \<Longrightarrow> P4 (TsCons ty ty_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   103
  and a12: "\<And>char. P5 (CC char)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   104
  and a13: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CApp co1 co2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   105
  and a14: "\<And>char co_lst. P6 co_lst \<Longrightarrow> P5 (CFun char co_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   106
  and a15: "\<And>tvar ckind co. \<lbrakk>P2 ckind; P5 co\<rbrakk> \<Longrightarrow> P5 (CAll tvar ckind co)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   107
  and a16: "\<And>co1 co2 co3. \<lbrakk>P5 co1; P5 co2; P5 co3\<rbrakk> \<Longrightarrow> P5 (CEq co1 co2 co3)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   108
  and a17: "\<And>co. P5 co \<Longrightarrow> P5 (CSym co)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   109
  and a18: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CCir co1 co2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   110
  and a19: "\<And>co. P5 co \<Longrightarrow> P5 (CLeft co)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   111
  and a20: "\<And>co. P5 co \<Longrightarrow> P5 (CRight co)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   112
  and a21: "\<And>co. P5 co \<Longrightarrow> P5 (CSim co)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   113
  and a22: "\<And>co. P5 co \<Longrightarrow> P5 (CRightc co)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   114
  and a23: "\<And>co. P5 co \<Longrightarrow> P5 (CLeftc co)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   115
  and a24: "\<And>co1 co2. \<lbrakk>P5 co1; P5 co2\<rbrakk> \<Longrightarrow> P5 (CCoe co1 co2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   116
  and a25: "P6 CsNil"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   117
  and a26: "\<And>co co_lst. \<lbrakk>P5 co; P6 co_lst\<rbrakk> \<Longrightarrow> P6 (CsCons co co_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   118
  and a27: "\<And>var. P7 (Var var)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   119
  and a28: "\<And>char. P7 (C char)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   120
  and a29: "\<And>tvar tkind trm. \<lbrakk>P1 tkind; P7 trm\<rbrakk> \<Longrightarrow> P7 (LAMT tvar tkind trm)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   121
  and a30: "\<And>tvar ckind trm. \<lbrakk>P2 ckind; P7 trm\<rbrakk> \<Longrightarrow> P7 (LAMC tvar ckind trm)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   122
  and a31: "\<And>trm ty. \<lbrakk>P7 trm; P3 ty\<rbrakk> \<Longrightarrow> P7 (APP trm ty)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   123
  and a32: "\<And>var ty trm. \<lbrakk>P3 ty; P7 trm\<rbrakk> \<Longrightarrow> P7 (Lam var ty trm)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   124
  and a33: "\<And>trm1 trm2. \<lbrakk>P7 trm1; P7 trm2\<rbrakk> \<Longrightarrow> P7 (App trm1 trm2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   125
  and a34: "\<And>var ty trm1 trm2. \<lbrakk>P3 ty; P7 trm1; P7 trm2\<rbrakk> \<Longrightarrow> P7 (ExCoreHaskell.Let var ty trm1 trm2)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   126
  and a35: "\<And>trm assoc_lst. \<lbrakk>P7 trm; P8 assoc_lst\<rbrakk> \<Longrightarrow> P7 (Case trm assoc_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   127
  and a36: "\<And>trm ty. \<lbrakk>P7 trm; P3 ty\<rbrakk> \<Longrightarrow> P7 (Cast trm ty)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   128
  and a37: "P8 ANil"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   129
  and a38: "\<And>pat trm assoc_lst. \<lbrakk>P9 pat; P7 trm; P8 assoc_lst\<rbrakk> \<Longrightarrow> P8 (ACons pat trm assoc_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   130
  and a39: "\<And>char tvtk_lst tvck_lst vt_lst. \<lbrakk>P11 tvtk_lst; P12 tvck_lst; P10 vt_lst\<rbrakk>
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   131
    \<Longrightarrow> P9 (K char tvtk_lst tvck_lst vt_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   132
  and a40: "P10 VTNil"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   133
  and a41: "\<And>var ty vt_lst. \<lbrakk>P3 ty; P10 vt_lst\<rbrakk> \<Longrightarrow> P10 (VTCons var ty vt_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   134
  and a42: "P11 TVTKNil"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   135
  and a43: "\<And>tvar tkind tvtk_lst. \<lbrakk>P1 tkind; P11 tvtk_lst\<rbrakk> \<Longrightarrow> P11 (TVTKCons tvar tkind tvtk_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   136
  and a44: "P12 TVCKNil"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   137
  and a45: "\<And>tvar ckind tvck_lst. \<lbrakk>P2 ckind; P12 tvck_lst\<rbrakk> \<Longrightarrow> P12 (TVCKCons tvar ckind tvck_lst)"
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   138
  shows "P1 tkind \<and> P2 ckind \<and> P3 ty \<and> P4 ty_lst \<and> P5 co \<and> P6 co_lst \<and>
b295a928c56b Working on stating induct.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1626
diff changeset
   139
         P7 trm \<and> P8 assoc_lst \<and> P9 pat \<and> P10 vt_lst \<and> P11 tvtk_lst \<and> P12 tvck_lst"
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
   140
1601
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   141
end
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   142
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   143
5f0bb35114c3 Added missing file
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   144