src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
author blanchet
Mon, 24 Nov 2014 12:35:13 +0100
changeset 59044 c04eccae1de8
parent 59043 a00110bdb4a3
child 59058 a78612c67ec0
permissions -rw-r--r--
tuned whitespace
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55061
a0adf838e2d1 adjusted comments
blanchet
parents: 55060
diff changeset
     1
(*  Title:      HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     2
    Author:     Lorenz Panny, TU Muenchen
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     4
    Copyright   2013
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     5
55538
blanchet
parents: 55529
diff changeset
     6
Corecursor sugar ("primcorec" and "primcorecursive").
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     7
*)
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
     8
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
     9
signature BNF_GFP_REC_SUGAR =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    10
sig
54899
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54883
diff changeset
    11
  datatype primcorec_option = Sequential_Option | Exhaustive_Option
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54883
diff changeset
    12
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    13
  datatype corec_call =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    14
    Dummy_No_Corec of int |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    15
    No_Corec of int |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    16
    Mutual_Corec of int * int * int |
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    17
    Nested_Corec of int
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    18
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    19
  type corec_ctr_spec =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    20
    {ctr: term,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    21
     disc: term,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    22
     sels: term list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    23
     pred: int option,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    24
     calls: corec_call list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    25
     discI: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    26
     sel_thms: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    27
     distinct_discss: thm list list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    28
     collapse: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    29
     corec_thm: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    30
     corec_disc: thm,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    31
     corec_sels: thm list}
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    32
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    33
  type corec_spec =
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    34
    {corec: term,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    35
     exhaust_discs: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    36
     sel_defs: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    37
     fp_nesting_maps: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    38
     fp_nesting_map_ident0s: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    39
     fp_nesting_map_comps: thm list,
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    40
     ctr_specs: corec_ctr_spec list}
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    41
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    42
  val corec_specs_of: binding list -> typ list -> typ list -> term list ->
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
    43
    (term * term list list) list list -> local_theory ->
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
    44
    corec_spec list * typ list * thm * thm * thm list * thm list * (Token.src list * Token.src list)
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
    45
    * bool * local_theory
54591
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
    46
  val add_primcorecursive_cmd: primcorec_option list ->
53831
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    47
    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    48
    Proof.context -> Proof.state
54591
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
    49
  val add_primcorec_cmd: primcorec_option list ->
53831
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    50
    (binding * string option * mixfix) list * ((Attrib.binding * string) * string option) list ->
80423b9080cf support "of" syntax to disambiguate selector equations
panny
parents: 53830
diff changeset
    51
    local_theory -> local_theory
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    52
end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    53
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    54
structure BNF_GFP_Rec_Sugar : BNF_GFP_REC_SUGAR =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    55
struct
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    56
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
    57
open Ctr_Sugar_General_Tactics
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    58
open Ctr_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    59
open BNF_Util
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    60
open BNF_Def
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    61
open BNF_FP_Util
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    62
open BNF_FP_Def_Sugar
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54239
diff changeset
    63
open BNF_FP_N2M_Sugar
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    64
open BNF_FP_Rec_Sugar_Util
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    65
open BNF_GFP_Rec_Sugar_Tactics
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
    66
58387
blanchet
parents: 58335
diff changeset
    67
val codeN = "code";
blanchet
parents: 58335
diff changeset
    68
val ctrN = "ctr";
blanchet
parents: 58335
diff changeset
    69
val discN = "disc";
blanchet
parents: 58335
diff changeset
    70
val disc_iffN = "disc_iff";
blanchet
parents: 58335
diff changeset
    71
val excludeN = "exclude";
blanchet
parents: 58335
diff changeset
    72
val selN = "sel";
53791
0ddf045113c9 tuned code
blanchet
parents: 53753
diff changeset
    73
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54133
diff changeset
    74
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
53794
af7d1533a25b undid copy-paste
blanchet
parents: 53793
diff changeset
    75
val simp_attrs = @{attributes [simp]};
54145
297d1c603999 make sure that registered code equations are actually equations
blanchet
parents: 54133
diff changeset
    76
val code_nitpicksimp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    77
55527
blanchet
parents: 55480
diff changeset
    78
exception PRIMCOREC of string * term list;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    79
55527
blanchet
parents: 55480
diff changeset
    80
fun primcorec_error str = raise PRIMCOREC (str, []);
blanchet
parents: 55480
diff changeset
    81
fun primcorec_error_eqn str eqn = raise PRIMCOREC (str, [eqn]);
blanchet
parents: 55480
diff changeset
    82
fun primcorec_error_eqns str eqns = raise PRIMCOREC (str, eqns);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    83
54899
7a01387c47d5 added tactic to prove 'disc_iff' properties in 'primcorec'
blanchet
parents: 54883
diff changeset
    84
datatype primcorec_option = Sequential_Option | Exhaustive_Option;
54591
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
    85
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    86
datatype corec_call =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    87
  Dummy_No_Corec of int |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    88
  No_Corec of int |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    89
  Mutual_Corec of int * int * int |
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    90
  Nested_Corec of int;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    91
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    92
type basic_corec_ctr_spec =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    93
  {ctr: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    94
   disc: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    95
   sels: term list};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    96
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    97
type corec_ctr_spec =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    98
  {ctr: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    99
   disc: term,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   100
   sels: term list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   101
   pred: int option,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   102
   calls: corec_call list,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   103
   discI: thm,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   104
   sel_thms: thm list,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   105
   distinct_discss: thm list list,
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   106
   collapse: thm,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   107
   corec_thm: thm,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   108
   corec_disc: thm,
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   109
   corec_sels: thm list};
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   110
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   111
type corec_spec =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   112
  {corec: term,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   113
   exhaust_discs: thm list,
56858
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   114
   sel_defs: thm list,
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   115
   fp_nesting_maps: thm list,
57399
cfc19f0a6261 compile
blanchet
parents: 57397
diff changeset
   116
   fp_nesting_map_ident0s: thm list,
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   117
   fp_nesting_map_comps: thm list,
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   118
   ctr_specs: corec_ctr_spec list};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   119
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   120
exception NO_MAP of term;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   121
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   122
fun not_codatatype ctxt T =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   123
  error ("Not a codatatype: " ^ Syntax.string_of_typ ctxt T);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   124
fun ill_formed_corec_call ctxt t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   125
  error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   126
fun invalid_map ctxt t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   127
  error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   128
fun unexpected_corec_call ctxt t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   129
  error ("Unexpected corecursive call: " ^ quote (Syntax.string_of_term ctxt t));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   130
55870
2f90476e3e61 avoid duplicate 'disc_iff' theorems
blanchet
parents: 55869
diff changeset
   131
fun sort_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs);
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   132
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   133
val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   134
val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   135
val mk_dnf = mk_disjs o map mk_conjs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   136
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
   137
val conjuncts_s = filter_out (curry (op aconv) @{const True}) o HOLogic.conjuncts;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   138
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   139
fun s_not @{const True} = @{const False}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   140
  | s_not @{const False} = @{const True}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   141
  | s_not (@{const Not} $ t) = t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   142
  | s_not (@{const conj} $ t $ u) = @{const disj} $ s_not t $ s_not u
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   143
  | s_not (@{const disj} $ t $ u) = @{const conj} $ s_not t $ s_not u
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   144
  | s_not t = @{const Not} $ t;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   145
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   146
val s_not_conj = conjuncts_s o s_not o mk_conjs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   147
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   148
fun propagate_unit_pos u cs = if member (op aconv) cs u then [@{const False}] else cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   149
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   150
fun propagate_unit_neg not_u cs = remove (op aconv) not_u cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   151
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   152
fun propagate_units css =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   153
  (case List.partition (can the_single) css of
58393
blanchet
parents: 58387
diff changeset
   154
    ([], _) => css
blanchet
parents: 58387
diff changeset
   155
  | ([u] :: uss, css') =>
blanchet
parents: 58387
diff changeset
   156
    [u] :: propagate_units (map (propagate_unit_neg (s_not u))
blanchet
parents: 58387
diff changeset
   157
      (map (propagate_unit_pos u) (uss @ css'))));
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   158
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   159
fun s_conjs cs =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   160
  if member (op aconv) cs @{const False} then @{const False}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   161
  else mk_conjs (remove (op aconv) @{const True} cs);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   162
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   163
fun s_disjs ds =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   164
  if member (op aconv) ds @{const True} then @{const True}
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   165
  else mk_disjs (remove (op aconv) @{const False} ds);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   166
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   167
fun s_dnf css0 =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   168
  let val css = propagate_units css0 in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   169
    if null css then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   170
      [@{const False}]
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   171
    else if exists null css then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   172
      []
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   173
    else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   174
      map (fn c :: cs => (c, cs)) css
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   175
      |> AList.coalesce (op =)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   176
      |> map (fn (c, css) => c :: s_dnf css)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   177
      |> (fn [cs] => cs | css => [s_disjs (map s_conjs css)])
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   178
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   179
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   180
fun fold_rev_let_if_case ctxt f bound_Ts =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   181
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   182
    val thy = Proof_Context.theory_of ctxt;
53794
af7d1533a25b undid copy-paste
blanchet
parents: 53793
diff changeset
   183
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   184
    fun fld conds t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   185
      (case Term.strip_comb t of
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   186
        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   187
      | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   188
        fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   189
      | (Const (c, _), args as _ :: _ :: _) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   190
        let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   191
          if n >= 0 andalso n < length args then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   192
            (case fastype_of1 (bound_Ts, nth args n) of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   193
              Type (s, Ts) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   194
              (case dest_case ctxt s Ts t of
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   195
                SOME ({split_sels = _ :: _, ...}, conds', branches) =>
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   196
                fold_rev (uncurry fld) (map (append conds o conjuncts_s) conds' ~~ branches)
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   197
              | _ => f conds t)
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   198
            | _ => f conds t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   199
          else
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   200
            f conds t
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   201
        end
55342
blanchet
parents: 55341
diff changeset
   202
      | _ => f conds t);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   203
  in
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   204
    fld []
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   205
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   206
54970
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   207
fun case_of ctxt s =
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   208
  (case ctr_sugar_of ctxt s of
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   209
    SOME {casex = Const (s', _), split_sels = _ :: _, ...} => SOME s'
54970
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   210
  | _ => NONE);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   211
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   212
fun massage_let_if_case ctxt has_call massage_leaf =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   213
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   214
    val thy = Proof_Context.theory_of ctxt;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   215
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   216
    fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   217
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   218
    fun massage_abs bound_Ts 0 t = massage_rec bound_Ts t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   219
      | massage_abs bound_Ts m (Abs (s, T, t)) = Abs (s, T, massage_abs (T :: bound_Ts) (m - 1) t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   220
      | massage_abs bound_Ts m t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   221
        let val T = domain_type (fastype_of1 (bound_Ts, t)) in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   222
          Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m - 1) (incr_boundvars 1 t $ Bound 0))
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   223
        end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   224
    and massage_rec bound_Ts t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   225
      let val typof = curry fastype_of1 bound_Ts in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   226
        (case Term.strip_comb t of
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   227
          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   228
        | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   229
          let val branches' = map (massage_rec bound_Ts) branches in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   230
            Term.list_comb (If_const (typof (hd branches')) $ tap check_no_call obj, branches')
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   231
          end
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55400
diff changeset
   232
        | (c as Const (@{const_name case_prod}, _), arg :: args) =>
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   233
          massage_rec bound_Ts
57895
a85e0ab840c1 less aggressive unfolding; removed debugging;
blanchet
parents: 57551
diff changeset
   234
            (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   235
        | (Const (c, _), args as _ :: _ :: _) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   236
          (case try strip_fun_type (Sign.the_const_type thy c) of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   237
            SOME (gen_branch_Ts, gen_body_fun_T) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   238
            let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   239
              val gen_branch_ms = map num_binder_types gen_branch_Ts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   240
              val n = length gen_branch_ms;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   241
            in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   242
              if n < length args then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   243
                (case gen_body_fun_T of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   244
                  Type (_, [Type (T_name, _), _]) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   245
                  if case_of ctxt T_name = SOME c then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   246
                    let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   247
                      val (branches, obj_leftovers) = chop n args;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   248
                      val branches' = map2 (massage_abs bound_Ts) gen_branch_ms branches;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   249
                      val branch_Ts' = map typof branches';
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   250
                      val body_T' = snd (strip_typeN (hd gen_branch_ms) (hd branch_Ts'));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   251
                      val casex' = Const (c, branch_Ts' ---> map typof obj_leftovers ---> body_T');
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   252
                    in
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   253
                      Term.list_comb (casex',
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   254
                        branches' @ tap (List.app check_no_call) obj_leftovers)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   255
                    end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   256
                  else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   257
                    massage_leaf bound_Ts t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   258
                | _ => massage_leaf bound_Ts t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   259
              else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   260
                massage_leaf bound_Ts t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   261
            end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   262
          | NONE => massage_leaf bound_Ts t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   263
        | _ => massage_leaf bound_Ts t)
55342
blanchet
parents: 55341
diff changeset
   264
      end;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   265
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   266
    massage_rec
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   267
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   268
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   269
fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   270
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   271
fun massage_nested_corec_call ctxt has_call raw_massage_call bound_Ts U t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   272
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   273
    fun check_no_call t = if has_call t then unexpected_corec_call ctxt t else ();
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   274
57303
498a62e65f5f tune the implementation of 'rel_coinduct'
desharna
parents: 56945
diff changeset
   275
    val build_map_Inl = build_map ctxt [] (uncurry Inl_const o dest_sumT o snd);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   276
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   277
    fun massage_mutual_call bound_Ts U T t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   278
      if has_call t then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   279
        (case try dest_sumT U of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   280
          SOME (U1, U2) => if U1 = T then raw_massage_call bound_Ts T U2 t else invalid_map ctxt t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   281
        | NONE => invalid_map ctxt t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   282
      else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   283
        build_map_Inl (T, U) $ t;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   284
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   285
    fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   286
        (case try (dest_map ctxt s) t of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   287
          SOME (map0, fs) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   288
          let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   289
            val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t));
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   290
            val map' = mk_map (length fs) dom_Ts Us map0;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   291
            val fs' =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   292
              map_flattened_map_args ctxt s (@{map 3} (massage_map_or_map_arg bound_Ts) Us Ts) fs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   293
          in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   294
            Term.list_comb (map', fs')
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   295
          end
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   296
        | NONE => raise NO_MAP t)
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   297
      | massage_map _ _ _ t = raise NO_MAP t
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   298
    and massage_map_or_map_arg bound_Ts U T t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   299
      if T = U then
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   300
        tap check_no_call t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   301
      else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   302
        massage_map bound_Ts U T t
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   303
        handle NO_MAP _ => massage_mutual_fun bound_Ts U T t
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   304
    and massage_mutual_fun bound_Ts U T t =
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   305
      (case t of
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   306
        Const (@{const_name comp}, _) $ t1 $ t2 =>
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   307
        mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   308
      | _ =>
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   309
        let
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   310
          val var = Var ((Name.uu, Term.maxidx_of_term t + 1),
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   311
            domain_type (fastype_of1 (bound_Ts, t)));
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   312
        in
59041
2a23235632b2 careful with de Bruijn indices
blanchet
parents: 58634
diff changeset
   313
          Term.lambda var (Term.incr_boundvars 1 (massage_call bound_Ts U T (betapply (t, var))))
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   314
        end)
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   315
    and massage_call bound_Ts U T =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   316
      massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   317
        if has_call t then
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   318
          (case U of
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   319
            Type (s, Us) =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   320
            (case try (dest_ctr ctxt s) t of
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   321
              SOME (f, args) =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   322
              let
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   323
                val typof = curry fastype_of1 bound_Ts;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   324
                val f' = mk_ctr Us f
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   325
                val f'_T = typof f';
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   326
                val arg_Ts = map typof args;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   327
              in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   328
                Term.list_comb (f', @{map 3} (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   329
              end
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   330
            | NONE =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   331
              (case t of
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55400
diff changeset
   332
                Const (@{const_name case_prod}, _) $ t' =>
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   333
                let
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   334
                  val U' = curried_type U;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   335
                  val T' = curried_type T;
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   336
                in
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55400
diff changeset
   337
                  Const (@{const_name case_prod}, U' --> U) $ massage_call bound_Ts U' T' t'
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   338
                end
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   339
              | t1 $ t2 =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   340
                (if has_call t2 then
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   341
                  massage_mutual_call bound_Ts U T t
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   342
                else
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   343
                  massage_map bound_Ts U T t1 $ t2
58223
ba7a2d19880c export useful functions for users of (co)recursors
blanchet
parents: 58211
diff changeset
   344
                  handle NO_MAP _ => massage_mutual_call bound_Ts U T t)
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   345
              | Abs (s, T', t') =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   346
                Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   347
              | _ => massage_mutual_call bound_Ts U T t))
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   348
          | _ => ill_formed_corec_call ctxt t)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   349
        else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   350
          build_map_Inl (T, U) $ t) bound_Ts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   351
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   352
    val T = fastype_of1 (bound_Ts, t);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   353
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   354
    if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   355
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   356
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   357
fun expand_to_ctr_term ctxt s Ts t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   358
  (case ctr_sugar_of ctxt s of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   359
    SOME {ctrs, casex, ...} =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   360
    Term.list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   361
  | NONE => raise Fail "expand_to_ctr_term");
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   362
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   363
fun expand_corec_code_rhs ctxt has_call bound_Ts t =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   364
  (case fastype_of1 (bound_Ts, t) of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   365
    Type (s, Ts) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   366
    massage_let_if_case ctxt has_call (fn _ => fn t =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   367
      if can (dest_ctr ctxt s) t then t else expand_to_ctr_term ctxt s Ts t) bound_Ts t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   368
  | _ => raise Fail "expand_corec_code_rhs");
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   369
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   370
fun massage_corec_code_rhs ctxt massage_ctr =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   371
  massage_let_if_case ctxt (K false)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   372
    (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   373
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   374
fun fold_rev_corec_code_rhs ctxt f =
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   375
  fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   376
55400
blanchet
parents: 55344
diff changeset
   377
fun case_thms_of_term ctxt t =
blanchet
parents: 55344
diff changeset
   378
  let val ctr_sugars = map_filter (Ctr_Sugar.ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   379
    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #exhaust_discs ctr_sugars,
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   380
     maps #split_sels ctr_sugars, maps #split_sel_asms ctr_sugars)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   381
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   382
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   383
fun basic_corec_specs_of ctxt res_T =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   384
  (case res_T of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   385
    Type (T_name, _) =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   386
    (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   387
      NONE => not_codatatype ctxt res_T
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   388
    | SOME {T = fpT, ctrs, discs, selss, ...} =>
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   389
      let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   390
        val thy = Proof_Context.theory_of ctxt;
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   391
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   392
        val As_rho = tvar_subst thy [fpT] [res_T];
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   393
        val substA = Term.subst_TVars As_rho;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   394
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   395
        fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   396
      in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   397
        @{map 3} mk_spec ctrs discs selss
54911
6a6980245ce0 robustness
blanchet
parents: 54910
diff changeset
   398
        handle ListPair.UnequalLengths => not_codatatype ctxt res_T
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   399
      end)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   400
  | _ => not_codatatype ctxt res_T);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   401
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   402
fun map_thms_of_typ ctxt (Type (s, _)) =
58462
b46874f2090f refactor fp_sugar move theorems
desharna
parents: 58461
diff changeset
   403
    (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => [])
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   404
  | map_thms_of_typ _ _ = [];
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   405
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   406
fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   407
  let
55005
38ea5ee18a06 use the right context in 'unfold_thms id_def'
blanchet
parents: 54979
diff changeset
   408
    val thy = Proof_Context.theory_of lthy0;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   409
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   410
    val ((missing_res_Ts, perm0_kks, fp_sugars as {fp_nesting_bnfs,
58461
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   411
          fp_co_induct_sugar = {common_co_inducts = common_coinduct_thms, ...}, ...} :: _,
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   412
          (_, gfp_sugar_thms)), lthy) =
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58286
diff changeset
   413
      nested_to_mutual_fps (K true) Greatest_FP bs res_Ts callers callssss0 lthy0;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   414
58286
a15731cf1835 compile
blanchet
parents: 58283
diff changeset
   415
    val coinduct_attrs_pair =
a15731cf1835 compile
blanchet
parents: 58283
diff changeset
   416
      (case gfp_sugar_thms of SOME ((_, attrs_pair), _, _, _, _) => attrs_pair | NONE => ([], []));
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   417
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   418
    val perm_fp_sugars = sort (int_ord o pairself #fp_res_index) fp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   419
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   420
    val indices = map #fp_res_index fp_sugars;
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   421
    val perm_indices = map #fp_res_index perm_fp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   422
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   423
    val perm_fpTs = map #T perm_fp_sugars;
58460
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   424
    val perm_ctrXs_Tsss' =
a88eb33058f7 refactor fp_sugar move theorems
desharna
parents: 58459
diff changeset
   425
      map (repair_nullary_single_ctr o #ctrXs_Tss o #fp_ctr_sugar) perm_fp_sugars;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   426
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   427
    val nn0 = length res_Ts;
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   428
    val nn = length perm_fpTs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   429
    val kks = 0 upto nn - 1;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   430
    val perm_ns' = map length perm_ctrXs_Tsss';
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   431
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   432
    val perm_Ts = map #T perm_fp_sugars;
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   433
    val perm_Xs = map #X perm_fp_sugars;
58461
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   434
    val perm_Cs =
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   435
      map (domain_type o body_fun_type o fastype_of o #co_rec o #fp_co_induct_sugar) perm_fp_sugars;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   436
    val Xs_TCs = perm_Xs ~~ (perm_Ts ~~ perm_Cs);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   437
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   438
    fun zip_corecT (Type (s, Us)) = [Type (s, map (mk_sumTN o zip_corecT) Us)]
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   439
      | zip_corecT U =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   440
        (case AList.lookup (op =) Xs_TCs U of
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   441
          SOME (T, C) => [T, C]
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   442
        | NONE => [U]);
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   443
55869
54ddb003e128 rationalized internals
blanchet
parents: 55863
diff changeset
   444
    val perm_p_Tss = mk_corec_p_pred_types perm_Cs perm_ns';
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   445
    val perm_f_Tssss =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   446
      map2 (fn C => map (map (map (curry (op -->) C) o zip_corecT))) perm_Cs perm_ctrXs_Tsss';
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   447
    val perm_q_Tssss =
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   448
      map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) perm_f_Tssss;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   449
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   450
    val (perm_p_hss, h) = indexedd perm_p_Tss 0;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   451
    val (perm_q_hssss, h') = indexedddd perm_q_Tssss h;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   452
    val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   453
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   454
    val fun_arg_hs =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   455
      flat (@{map 3} flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   456
55480
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55462
diff changeset
   457
    fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
59cc4a8bc28a allow different functions to recurse on the same type, like in the old package
blanchet
parents: 55462
diff changeset
   458
    fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   459
55539
0819931d652d simplified data structure by reducing the incidence of clumsy indices
blanchet
parents: 55538
diff changeset
   460
    val coinduct_thmss = map (unpermute0 o conj_dests nn) common_coinduct_thms;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   461
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   462
    val p_iss = map (map (find_index_eq fun_arg_hs)) (unpermute perm_p_hss);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   463
    val q_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_q_hssss);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   464
    val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
53358
b46e6cd75dc6 improved interfaces
panny
parents: 53357
diff changeset
   465
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   466
    val f_Tssss = unpermute perm_f_Tssss;
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   467
    val fpTs = unpermute perm_fpTs;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   468
    val Cs = unpermute perm_Cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   469
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58131
diff changeset
   470
    val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   471
    val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   472
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   473
    val substA = Term.subst_TVars As_rho;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   474
    val substAT = Term.typ_subst_TVars As_rho;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   475
    val substCT = Term.typ_subst_TVars Cs_rho;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   476
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   477
    val perm_Cs' = map substCT perm_Cs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   478
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   479
    fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   480
        (if exists_subtype_in Cs T then Nested_Corec
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   481
         else if nullary then Dummy_No_Corec
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   482
         else No_Corec) g_i
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   483
      | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   484
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   485
    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms distinct_discss collapse
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   486
        corec_thm corec_disc corec_sels =
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   487
      let val nullary = not (can dest_funT (fastype_of ctr)) in
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   488
        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   489
         calls = @{map 3} (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   490
         distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm,
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   491
         corec_disc = corec_disc, corec_sels = corec_sels}
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   492
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   493
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   494
    fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...}
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   495
        : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss =
55863
fa3a1ec69a1b rationalize internals
blanchet
parents: 55860
diff changeset
   496
      let val p_ios = map SOME p_is @ [NONE] in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   497
        @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   498
          distinct_discsss collapses corec_thms corec_discs corec_selss
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   499
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   500
58461
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   501
    fun mk_spec ({T, fp_ctr_sugar = {ctr_sugar as {exhaust_discs, sel_defs, ...}, ...},
75ee8d49c724 refactor fp_sugar move theorems
desharna
parents: 58460
diff changeset
   502
        fp_co_induct_sugar = {co_rec = corec, co_rec_thms = corec_thms, co_rec_discs = corec_discs,
58459
f70bffabd7cf refactor fp_sugar move theorems
desharna
parents: 58394
diff changeset
   503
        co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss =
58211
c1f3fa32d322 extended 'datatype_compat' to generate the expected, old-style recursor in the presence of recursion through functions
blanchet
parents: 58187
diff changeset
   504
      {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs,
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   505
       sel_defs = sel_defs,
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   506
       fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs,
57399
cfc19f0a6261 compile
blanchet
parents: 57397
diff changeset
   507
       fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs,
57397
5004aca20821 tuned variable names
blanchet
parents: 57303
diff changeset
   508
       fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs,
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   509
       ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
   510
         corec_selss};
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   511
  in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   512
    (@{map 5} mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   513
     co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   514
     co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair,
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
   515
     is_some gfp_sugar_thms, lthy)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   516
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   517
53358
b46e6cd75dc6 improved interfaces
panny
parents: 53357
diff changeset
   518
val undef_const = Const (@{const_name undefined}, dummyT);
53357
46b0c7a08af7 simplified rewriting of map arguments
panny
parents: 53354
diff changeset
   519
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   520
val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
55005
38ea5ee18a06 use the right context in 'unfold_thms id_def'
blanchet
parents: 54979
diff changeset
   521
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   522
fun abstract vs =
55342
blanchet
parents: 55341
diff changeset
   523
  let
blanchet
parents: 55341
diff changeset
   524
    fun abs n (t $ u) = abs n t $ abs n u
blanchet
parents: 55341
diff changeset
   525
      | abs n (Abs (v, T, b)) = Abs (v, T, abs (n + 1) b)
blanchet
parents: 55341
diff changeset
   526
      | abs n t =
blanchet
parents: 55341
diff changeset
   527
        let val j = find_index (curry (op =) t) vs in
blanchet
parents: 55341
diff changeset
   528
          if j < 0 then t else Bound (n + j)
blanchet
parents: 55341
diff changeset
   529
        end;
blanchet
parents: 55341
diff changeset
   530
  in abs 0 end;
54271
blanchet
parents: 54246
diff changeset
   531
58393
blanchet
parents: 58387
diff changeset
   532
type coeqn_data_disc =
blanchet
parents: 58387
diff changeset
   533
  {fun_name: string,
blanchet
parents: 58387
diff changeset
   534
   fun_T: typ,
blanchet
parents: 58387
diff changeset
   535
   fun_args: term list,
blanchet
parents: 58387
diff changeset
   536
   ctr: term,
blanchet
parents: 58387
diff changeset
   537
   ctr_no: int,
blanchet
parents: 58387
diff changeset
   538
   disc: term,
blanchet
parents: 58387
diff changeset
   539
   prems: term list,
blanchet
parents: 58387
diff changeset
   540
   auto_gen: bool,
blanchet
parents: 58387
diff changeset
   541
   ctr_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   542
   code_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   543
   eqn_pos: int,
blanchet
parents: 58387
diff changeset
   544
   user_eqn: term};
54001
65fc58793ed5 made SML/NJ happier
blanchet
parents: 53925
diff changeset
   545
58393
blanchet
parents: 58387
diff changeset
   546
type coeqn_data_sel =
blanchet
parents: 58387
diff changeset
   547
  {fun_name: string,
blanchet
parents: 58387
diff changeset
   548
   fun_T: typ,
blanchet
parents: 58387
diff changeset
   549
   fun_args: term list,
blanchet
parents: 58387
diff changeset
   550
   ctr: term,
blanchet
parents: 58387
diff changeset
   551
   sel: term,
blanchet
parents: 58387
diff changeset
   552
   rhs_term: term,
blanchet
parents: 58387
diff changeset
   553
   ctr_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   554
   code_rhs_opt: term option,
blanchet
parents: 58387
diff changeset
   555
   eqn_pos: int,
blanchet
parents: 58387
diff changeset
   556
   user_eqn: term};
54001
65fc58793ed5 made SML/NJ happier
blanchet
parents: 53925
diff changeset
   557
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   558
datatype coeqn_data =
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   559
  Disc of coeqn_data_disc |
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   560
  Sel of coeqn_data_sel;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   561
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   562
fun check_extra_variables lthy vars names eqn =
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   563
  let val b = fold_aterms (fn x as Free (v, _) =>
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   564
    if (not (member (op =) vars x) andalso
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   565
      not (member (op =) names v) andalso
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   566
      v <> Name.uu_ andalso
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   567
      not (Variable.is_fixed lthy v)) then cons x else I | _ => I) eqn []
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   568
  in
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   569
    null b orelse
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   570
    primcorec_error_eqn ("extra variable(s) in equation: " ^
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   571
      commas (map (Syntax.string_of_term lthy) b)) eqn
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   572
  end;
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   573
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   574
fun dissect_coeqn_disc lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   575
    eqn_pos ctr_rhs_opt code_rhs_opt prems' concl matchedsss =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   576
  let
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   577
    fun find_subterm p =
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   578
      let (* FIXME \<exists>? *)
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   579
        fun find (t as u $ v) = if p t then SOME t else merge_options (find u, find v)
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   580
          | find t = if p t then SOME t else NONE;
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   581
      in find end;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   582
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   583
    val applied_fun = concl
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
   584
      |> find_subterm (member (op = o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   585
      |> the
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   586
      handle Option.Option => primcorec_error_eqn "malformed discriminator formula" concl;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   587
    val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   588
58393
blanchet
parents: 58387
diff changeset
   589
    val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args;
blanchet
parents: 58387
diff changeset
   590
    val _ = null fixeds orelse
blanchet
parents: 58387
diff changeset
   591
      primcorec_error_eqns "function argument(s) are fixed in context" fixeds;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   592
58393
blanchet
parents: 58387
diff changeset
   593
    val bad =
blanchet
parents: 58387
diff changeset
   594
      filter (exists_subterm (fn Free (v, _) => member (op =) fun_names v | _ => false)) prems';
blanchet
parents: 58387
diff changeset
   595
    val _ = null bad orelse primcorec_error_eqns "corecursive call(s) in condition(s)" bad;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   596
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   597
    val _ = forall is_Free fun_args orelse
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   598
      primcorec_error_eqn ("non-variable function argument \"" ^
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   599
        Syntax.string_of_term lthy (find_first (not o is_Free) fun_args |> the) ^
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   600
          "\" (pattern matching is not supported by primcorec(ursive))") applied_fun
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   601
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   602
    val _ = let val d = duplicates (op =) fun_args in null d orelse
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   603
      primcorec_error_eqn ("duplicate variable \"" ^ Syntax.string_of_term lthy (hd d) ^ "\"")
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   604
        applied_fun end;
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   605
58393
blanchet
parents: 58387
diff changeset
   606
    val (sequential, basic_ctr_specs) =
blanchet
parents: 58387
diff changeset
   607
      the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   608
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   609
    val discs = map #disc basic_ctr_specs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   610
    val ctrs = map #ctr basic_ctr_specs;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   611
    val not_disc = head_of concl = @{term Not};
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   612
    val _ = not_disc andalso length ctrs <> 2 andalso
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   613
      primcorec_error_eqn "negated discriminator for a type with \<noteq> 2 constructors" concl;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   614
    val disc' = find_subterm (member (op =) discs o head_of) concl;
54209
blanchet
parents: 54208
diff changeset
   615
    val eq_ctr0 = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd)
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   616
        |> (fn SOME t => let val n = find_index (curry (op =) t) ctrs in
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   617
          if n >= 0 then SOME n else NONE end | _ => NONE);
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   618
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   619
    val _ = if is_some disc' andalso perhaps (try HOLogic.dest_not) concl <> the disc'
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   620
      then primcorec_error_eqn "malformed discriminator formula" concl else ();
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   621
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   622
    val _ = is_some disc' orelse is_some eq_ctr0 orelse
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   623
      primcorec_error_eqn "no discriminator in equation" concl;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   624
    val ctr_no' =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   625
      if is_none disc' then the eq_ctr0 else find_index (curry (op =) (head_of (the disc'))) discs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   626
    val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   627
    val {ctr, disc, ...} = nth basic_ctr_specs ctr_no;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   628
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   629
    val catch_all = try (fst o dest_Free o the_single) prems' = SOME Name.uu_;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   630
    val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   631
    val prems = map (abstract (List.rev fun_args)) prems';
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   632
    val actual_prems =
54901
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
   633
      (if catch_all orelse sequential then maps s_not_conj matchedss else []) @
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   634
      (if catch_all then [] else prems);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   635
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   636
    val matchedsss' = AList.delete (op =) fun_name matchedsss
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   637
      |> cons (fun_name, if sequential then matchedss @ [prems] else matchedss @ [actual_prems]);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   638
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   639
    val user_eqn =
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   640
      (actual_prems, concl)
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   641
      |>> map HOLogic.mk_Trueprop ||> HOLogic.mk_Trueprop o abstract (List.rev fun_args)
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   642
      |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   643
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   644
    val _ = check_extra_variables lthy fun_args fun_names user_eqn;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   645
  in
58393
blanchet
parents: 58387
diff changeset
   646
    (Disc {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = ctr_no,
blanchet
parents: 58387
diff changeset
   647
       disc = disc, prems = actual_prems, auto_gen = catch_all, ctr_rhs_opt = ctr_rhs_opt,
blanchet
parents: 58387
diff changeset
   648
       code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = user_eqn},
blanchet
parents: 58387
diff changeset
   649
     matchedsss')
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   650
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   651
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   652
fun dissect_coeqn_sel lthy fun_names (basic_ctr_specss : basic_corec_ctr_spec list list) eqn_pos
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   653
    ctr_rhs_opt code_rhs_opt eqn0 of_spec_opt eqn =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   654
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   655
    val (lhs, rhs) = HOLogic.dest_eq eqn
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   656
      handle TERM _ =>
55527
blanchet
parents: 55480
diff changeset
   657
             primcorec_error_eqn "malformed function equation (expected \"lhs = rhs\")" eqn;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   658
    val sel = head_of lhs;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   659
    val ((fun_name, fun_T), fun_args) = dest_comb lhs |> snd |> strip_comb |> apfst dest_Free
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   660
      handle TERM _ =>
55527
blanchet
parents: 55480
diff changeset
   661
             primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   662
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   663
    val _ = let val fixeds = filter (Variable.is_fixed lthy o fst o dest_Free) fun_args in
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   664
        null fixeds orelse primcorec_error_eqns "function argument(s) are fixed in context" fixeds
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   665
      end;
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   666
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   667
    val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name)
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   668
      handle Option.Option =>
55527
blanchet
parents: 55480
diff changeset
   669
             primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   670
    val {ctr, ...} =
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   671
      (case of_spec_opt of
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   672
        SOME of_spec => the (find_first (curry (op =) of_spec o #ctr) basic_ctr_specs)
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   673
      | NONE => filter (exists (curry (op =) sel) o #sels) basic_ctr_specs |> the_single
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   674
          handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn);
54979
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   675
    val user_eqn = drop_all eqn0;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   676
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   677
    val _ = check_extra_variables lthy fun_args fun_names user_eqn;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   678
  in
58393
blanchet
parents: 58387
diff changeset
   679
    Sel {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, sel = sel,
blanchet
parents: 58387
diff changeset
   680
      rhs_term = rhs, ctr_rhs_opt = ctr_rhs_opt, code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos,
blanchet
parents: 58387
diff changeset
   681
      user_eqn = user_eqn}
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   682
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   683
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   684
fun dissect_coeqn_ctr lthy fun_names sequentials (basic_ctr_specss : basic_corec_ctr_spec list list)
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   685
    eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
53910
2c5055a3583d strengthen tactic
blanchet
parents: 53909
diff changeset
   686
  let
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   687
    val (lhs, rhs) = HOLogic.dest_eq concl;
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   688
    val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   689
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   690
    val _ = check_extra_variables lthy fun_args fun_names (drop_all eqn0);
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   691
58393
blanchet
parents: 58387
diff changeset
   692
    val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   693
    val (ctr, ctr_args) = strip_comb (unfold_lets_splits rhs);
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   694
    val {disc, sels, ...} = the (find_first (curry (op =) ctr o #ctr) basic_ctr_specs)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   695
      handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   696
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   697
    val disc_concl = betapply (disc, lhs);
54976
b502f04c0442 repair 'exhaustive' feature for one-constructor types
blanchet
parents: 54975
diff changeset
   698
    val (eqn_data_disc_opt, matchedsss') =
59042
ef0074e812cd smoothly handle unit codatatypes in 'primcorec'
blanchet
parents: 59041
diff changeset
   699
      if null (tl basic_ctr_specs) andalso not (null sels) then
54976
b502f04c0442 repair 'exhaustive' feature for one-constructor types
blanchet
parents: 54975
diff changeset
   700
        (NONE, matchedsss)
b502f04c0442 repair 'exhaustive' feature for one-constructor types
blanchet
parents: 54975
diff changeset
   701
      else
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   702
        apfst SOME (dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   703
          (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt prems disc_concl matchedsss);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   704
54159
eb5d58c99049 set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents: 54157
diff changeset
   705
    val sel_concls = sels ~~ ctr_args
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   706
      |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg))
56806
f7d0520e7be2 use qualified name (was interpreted as a catch-all variable name)
panny
parents: 56805
diff changeset
   707
        handle ListPair.UnequalLengths =>
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   708
          primcorec_error_eqn "partially applied constructor in right-hand side" rhs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   709
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   710
    val eqns_data_sel =
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   711
      map (dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   712
        (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   713
  in
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   714
    (the_list eqn_data_disc_opt @ eqns_data_sel, matchedsss')
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   715
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   716
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   717
fun dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss =
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   718
  let
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   719
    val (lhs, (rhs', rhs)) = HOLogic.dest_eq concl ||> `(expand_corec_code_rhs lthy has_call []);
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   720
    val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   721
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   722
    val _ = check_extra_variables lthy fun_args fun_names concl;
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   723
58393
blanchet
parents: 58387
diff changeset
   724
    val basic_ctr_specs = the (AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name);
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   725
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   726
    val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ =>
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
   727
        if member (op = o apsnd #ctr) basic_ctr_specs ctr then cons (ctr, cs)
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   728
        else primcorec_error_eqn "not a constructor" ctr) [] rhs' []
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   729
      |> AList.group (op =);
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   730
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   731
    val ctr_premss = (case cond_ctrs of [_] => [[]] | _ => map (s_dnf o snd) cond_ctrs);
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   732
    val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
58393
blanchet
parents: 58387
diff changeset
   733
      binder_types (fastype_of ctr)
blanchet
parents: 58387
diff changeset
   734
      |> map_index (fn (n, T) => massage_corec_code_rhs lthy (fn _ => fn ctr' => fn args =>
blanchet
parents: 58387
diff changeset
   735
        if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
blanchet
parents: 58387
diff changeset
   736
      |> curry Term.list_comb ctr
blanchet
parents: 58387
diff changeset
   737
      |> curry HOLogic.mk_eq lhs);
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   738
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   739
    val sequentials = replicate (length fun_names) false;
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   740
  in
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   741
    @{fold_map 2} (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   742
        (SOME (abstract (List.rev fun_args) rhs)))
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   743
      ctr_premss ctr_concls matchedsss
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   744
  end;
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   745
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   746
fun dissect_coeqn lthy has_call fun_names sequentials
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   747
    (basic_ctr_specss : basic_corec_ctr_spec list list) (eqn_pos, eqn0) of_spec_opt matchedsss =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   748
  let
54979
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   749
    val eqn = drop_all eqn0
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   750
      handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   751
    val (prems, concl) = Logic.strip_horn eqn
57527
1b07ca054327 add helper function map_prod
desharna
parents: 57399
diff changeset
   752
      |> map_prod (map HOLogic.dest_Trueprop) HOLogic.dest_Trueprop
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   753
        handle TERM _ => primcorec_error_eqn "malformed function equation" eqn;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   754
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   755
    val head = concl
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   756
      |> perhaps (try HOLogic.dest_not) |> perhaps (try (fst o HOLogic.dest_eq))
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   757
      |> head_of;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   758
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   759
    val rhs_opt = concl |> perhaps (try HOLogic.dest_not) |> try (snd o HOLogic.dest_eq);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   760
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   761
    val discs = maps (map #disc) basic_ctr_specss;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   762
    val sels = maps (maps #sels) basic_ctr_specss;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   763
    val ctrs = maps (map #ctr) basic_ctr_specss;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   764
  in
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   765
    if member (op =) discs head orelse
58393
blanchet
parents: 58387
diff changeset
   766
       (is_some rhs_opt andalso
blanchet
parents: 58387
diff changeset
   767
        member (op =) (map SOME fun_names) (try (fst o dest_Free) head) andalso
blanchet
parents: 58387
diff changeset
   768
        member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt)) then
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   769
      dissect_coeqn_disc lthy fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   770
        matchedsss
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   771
      |>> single
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   772
    else if member (op =) sels head then
58393
blanchet
parents: 58387
diff changeset
   773
      (null prems orelse primcorec_error_eqn "premise(s) in selector formula" eqn;
57550
934a54d04a9a throw error for bad input
panny
parents: 57527
diff changeset
   774
       ([dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos NONE NONE eqn0 of_spec_opt
934a54d04a9a throw error for bad input
panny
parents: 57527
diff changeset
   775
           concl], matchedsss))
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   776
    else if is_some rhs_opt andalso
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   777
        is_Free head andalso member (op =) fun_names (fst (dest_Free head)) then
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   778
      if member (op =) ctrs (head_of (unfold_lets_splits (the rhs_opt))) then
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   779
        dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
54979
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   780
          (if null prems then
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   781
             SOME (snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_assums_concl eqn0))))
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   782
           else
d7593bfccf25 correctly extract code RHS, with loose bound variables
blanchet
parents: 54978
diff changeset
   783
             NONE)
54975
451786451d04 pass right rhs as code rhs
blanchet
parents: 54974
diff changeset
   784
          prems concl matchedsss
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   785
      else if null prems then
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   786
        dissect_coeqn_code lthy has_call fun_names basic_ctr_specss eqn_pos eqn0 concl matchedsss
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   787
        |>> flat
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   788
      else
54956
80a1931267ce tuned error message
blanchet
parents: 54955
diff changeset
   789
        primcorec_error_eqn "cannot mix constructor and code views (see manual for details)" eqn
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   790
    else
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   791
      primcorec_error_eqn "malformed function equation" eqn
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   792
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   793
54002
01c8f9d3b084 made SML/NJ happy
blanchet
parents: 54001
diff changeset
   794
fun build_corec_arg_disc (ctr_specs : corec_ctr_spec list)
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   795
    ({fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
56858
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   796
  if is_none (#pred (nth ctr_specs ctr_no)) then
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   797
    I
0c3d0bc98abe simplify selectors in code views
blanchet
parents: 56806
diff changeset
   798
  else
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   799
    s_conjs prems
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   800
    |> curry subst_bounds (List.rev fun_args)
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   801
    |> abs_tuple_balanced fun_args
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   802
    |> K |> nth_map (the (#pred (nth ctr_specs ctr_no)));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   803
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   804
fun build_corec_arg_no_call (sel_eqns : coeqn_data_sel list) sel =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   805
  find_first (curry (op =) sel o #sel) sel_eqns
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   806
  |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple_balanced fun_args rhs_term)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   807
  |> the_default undef_const
53411
ab4edf89992f support indirect corecursion
panny
parents: 53401
diff changeset
   808
  |> K;
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   809
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   810
fun build_corec_args_mutual_call lthy has_call (sel_eqns : coeqn_data_sel list) sel =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   811
  (case find_first (curry (op =) sel o #sel) sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   812
    NONE => (I, I, I)
blanchet
parents: 54207
diff changeset
   813
  | SOME {fun_args, rhs_term, ... } =>
53876
fabf04d43a75 simplified code
panny
parents: 53875
diff changeset
   814
    let
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   815
      val bound_Ts = List.rev (map fastype_of fun_args);
54207
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   816
      fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   817
      fun rewrite_end _ t = if has_call t then undef_const else t;
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   818
      fun rewrite_cont bound_Ts t =
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   819
        if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   820
      fun massage f _ = massage_let_if_case lthy has_call f bound_Ts rhs_term
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   821
        |> abs_tuple_balanced fun_args;
53876
fabf04d43a75 simplified code
panny
parents: 53875
diff changeset
   822
    in
54207
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   823
      (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
54208
blanchet
parents: 54207
diff changeset
   824
    end);
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   825
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   826
fun build_corec_arg_nested_call lthy has_call (sel_eqns : coeqn_data_sel list) sel =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   827
  (case find_first (curry (op =) sel o #sel) sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   828
    NONE => I
blanchet
parents: 54207
diff changeset
   829
  | SOME {fun_args, rhs_term, ...} =>
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   830
    let
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   831
      fun massage bound_Ts U T =
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   832
        let
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   833
          fun rewrite bound_Ts (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) b)
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   834
            | rewrite bound_Ts (t as _ $ _) =
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   835
              let val (u, vs) = strip_comb t in
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   836
                if is_Free u andalso has_call u then
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   837
                  Inr_const U T $ mk_tuple1_balanced bound_Ts vs
55414
eab03e9cee8a renamed '{prod,sum,bool,unit}_case' to 'case_...'
blanchet
parents: 55400
diff changeset
   838
                else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   839
                  map (rewrite bound_Ts) vs |> chop 1
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   840
                  |>> HOLogic.mk_split o the_single
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   841
                  |> Term.list_comb
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   842
                else
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   843
                  Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   844
              end
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   845
            | rewrite _ t =
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   846
              if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   847
          in
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   848
            rewrite bound_Ts
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   849
          end;
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   850
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   851
      val bound_Ts = List.rev (map fastype_of fun_args);
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   852
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   853
      fun build t =
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   854
        rhs_term
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   855
        |> massage_nested_corec_call lthy has_call massage bound_Ts (range_type (fastype_of t))
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   856
        |> abs_tuple_balanced fun_args;
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   857
    in
55339
f09037306f25 properly massage 'if's / 'case's etc. under lambdas
blanchet
parents: 55100
diff changeset
   858
      build
54208
blanchet
parents: 54207
diff changeset
   859
    end);
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   860
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   861
fun build_corec_args_sel lthy has_call (all_sel_eqns : coeqn_data_sel list)
54002
01c8f9d3b084 made SML/NJ happy
blanchet
parents: 54001
diff changeset
   862
    (ctr_spec : corec_ctr_spec) =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   863
  (case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   864
    [] => I
blanchet
parents: 54207
diff changeset
   865
  | sel_eqns =>
blanchet
parents: 54207
diff changeset
   866
    let
blanchet
parents: 54207
diff changeset
   867
      val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
blanchet
parents: 54207
diff changeset
   868
      val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   869
      val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   870
      val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   871
    in
blanchet
parents: 54207
diff changeset
   872
      I
blanchet
parents: 54207
diff changeset
   873
      #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
blanchet
parents: 54207
diff changeset
   874
      #> fold (fn (sel, (q, g, h)) =>
blanchet
parents: 54207
diff changeset
   875
        let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in
blanchet
parents: 54207
diff changeset
   876
          nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
blanchet
parents: 54207
diff changeset
   877
      #> fold (fn (sel, n) => nth_map n
blanchet
parents: 54207
diff changeset
   878
        (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls'
blanchet
parents: 54207
diff changeset
   879
    end);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   880
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   881
fun build_codefs lthy bs mxs has_call arg_Tss (corec_specs : corec_spec list)
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   882
    (disc_eqnss : coeqn_data_disc list list) (sel_eqnss : coeqn_data_sel list list) =
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   883
  let
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   884
    val corecs = map #corec corec_specs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   885
    val ctr_specss = map #ctr_specs corec_specs;
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   886
    val corec_args = hd corecs
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   887
      |> fst o split_last o binder_types o fastype_of
59044
c04eccae1de8 tuned whitespace
blanchet
parents: 59043
diff changeset
   888
      |> map (fn T =>
c04eccae1de8 tuned whitespace
blanchet
parents: 59043
diff changeset
   889
          if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False})
54806
a0f024caa04c pass auto-proved exhaustiveness properties to tactic;
panny
parents: 54628
diff changeset
   890
          else Const (@{const_name undefined}, T))
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   891
      |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   892
      |> fold2 (fold o build_corec_args_sel lthy has_call) sel_eqnss ctr_specss;
59041
2a23235632b2 careful with de Bruijn indices
blanchet
parents: 58634
diff changeset
   893
53735
99331dac1e1c simplified code; eliminated some dummyTs
panny
parents: 53734
diff changeset
   894
    fun currys [] t = t
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   895
      | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
53735
99331dac1e1c simplified code; eliminated some dummyTs
panny
parents: 53734
diff changeset
   896
          |> fold_rev (Term.abs o pair Name.uu) Ts;
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   897
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   898
    val excludess' =
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   899
      disc_eqnss
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   900
      |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   901
        #> fst o (fn xs => fold_map (fn x => fn ys => ((x, ys), ys @ [x])) xs [])
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   902
        #> maps (uncurry (map o pair)
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   903
          #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   904
              ((c, c', a orelse a'), (x, s_not (s_conjs y)))
57527
1b07ca054327 add helper function map_prod
desharna
parents: 57399
diff changeset
   905
            ||> map_prod (map HOLogic.mk_Trueprop) HOLogic.mk_Trueprop
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   906
            ||> Logic.list_implies
55342
blanchet
parents: 55341
diff changeset
   907
            ||> curry Logic.list_all (map dest_Free fun_args))));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   908
  in
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   909
    map (Term.list_comb o rpair corec_args) corecs
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   910
    |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   911
    |> map2 currys arg_Tss
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   912
    |> Syntax.check_terms lthy
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   913
    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
54155
b964fad0cbbd conceal more ugly constructions
blanchet
parents: 54154
diff changeset
   914
      bs mxs
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   915
    |> rpair excludess'
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   916
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   917
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   918
fun mk_actual_disc_eqns fun_binding arg_Ts exhaustive ({ctr_specs, ...} : corec_spec)
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   919
    (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) =
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   920
  let val num_disc_eqns = length disc_eqns in
54912
4ecdea61181e proper handling of corner case, take 2
blanchet
parents: 54911
diff changeset
   921
    if (exhaustive andalso num_disc_eqns <> 0) orelse num_disc_eqns <> length ctr_specs - 1 then
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   922
      disc_eqns
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   923
    else
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   924
      let
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   925
        val n = 0 upto length ctr_specs
55342
blanchet
parents: 55341
diff changeset
   926
          |> the o find_first (fn j => not (exists (curry (op =) j o #ctr_no) disc_eqns));
54958
4933165fd112 do not use wrong constructor in auto-generated proof goal
panny
parents: 54956
diff changeset
   927
        val {ctr, disc, ...} = nth ctr_specs n;
58393
blanchet
parents: 58387
diff changeset
   928
        val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns;
blanchet
parents: 58387
diff changeset
   929
blanchet
parents: 58387
diff changeset
   930
        val fun_name = Binding.name_of fun_binding;
blanchet
parents: 58387
diff changeset
   931
        val fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs)));
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   932
        val fun_args = (try (#fun_args o hd) disc_eqns, try (#fun_args o hd) sel_eqns)
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   933
          |> the_default (map (curry Free Name.uu) arg_Ts) o merge_options;
58393
blanchet
parents: 58387
diff changeset
   934
        val prems = maps (s_not_conj o #prems) disc_eqns;
blanchet
parents: 58387
diff changeset
   935
        val ctr_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE;
blanchet
parents: 58387
diff changeset
   936
        val code_rhs_opt = Option.map #code_rhs_opt sel_eqn_opt |> the_default NONE;
blanchet
parents: 58387
diff changeset
   937
        val eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (* FIXME *);
blanchet
parents: 58387
diff changeset
   938
blanchet
parents: 58387
diff changeset
   939
        val extra_disc_eqn =
blanchet
parents: 58387
diff changeset
   940
          {fun_name = fun_name, fun_T = fun_T, fun_args = fun_args, ctr = ctr, ctr_no = n,
blanchet
parents: 58387
diff changeset
   941
           disc = disc, prems = prems, auto_gen = true, ctr_rhs_opt = ctr_rhs_opt,
blanchet
parents: 58387
diff changeset
   942
           code_rhs_opt = code_rhs_opt, eqn_pos = eqn_pos, user_eqn = undef_const};
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   943
      in
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   944
        chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   945
      end
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   946
  end;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   947
55100
697b41533e1a made SML/NJ happier
blanchet
parents: 55061
diff changeset
   948
fun find_corec_calls ctxt has_call (basic_ctr_specs : basic_corec_ctr_spec list)
697b41533e1a made SML/NJ happier
blanchet
parents: 55061
diff changeset
   949
    ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   950
  let
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   951
    val sel_no = find_first (curry (op =) ctr o #ctr) basic_ctr_specs
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   952
      |> find_index (curry (op =) sel) o #sels o the;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   953
  in
55341
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   954
    K (if has_call rhs_term then fold_rev_let_if_case ctxt (K cons) [] rhs_term [] else [])
3d2c97392e25 adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
blanchet
parents: 55339
diff changeset
   955
    |> nth_map sel_no |> AList.map_entry (op =) ctr
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   956
  end;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   957
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   958
fun applied_fun_of fun_name fun_T fun_args =
55343
5ebf832b58a1 expand 'split' in direct corecursion as well
blanchet
parents: 55342
diff changeset
   959
  Term.list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   960
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
   961
fun is_trivial_implies thm =
54967
78de75e3e52a exhaustive rules like '(False ==> P) ==> P ==> P' are now filtered out as trivial
blanchet
parents: 54959
diff changeset
   962
  uncurry (member (op aconv)) (Logic.strip_horn (Thm.prop_of thm));
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
   963
55009
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
   964
fun add_primcorec_ursive auto opts fixes specs of_specs_opt lthy =
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   965
  let
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   966
    val thy = Proof_Context.theory_of lthy;
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   967
53352
43a1cc050943 honor mixfix specifications
traytel
parents: 53341
diff changeset
   968
    val (bs, mxs) = map_split (apfst fst) fixes;
55969
8820ddb8f9f4 use balanced tuples in 'primcorec'
blanchet
parents: 55966
diff changeset
   969
    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   970
56254
a2dd9200854d more antiquotations;
wenzelm
parents: 56152
diff changeset
   971
    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   972
        [] => ()
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   973
      | (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   974
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   975
    val actual_nn = length bs;
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   976
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   977
    val sequentials = replicate actual_nn (member (op =) opts Sequential_Option);
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   978
    val exhaustives = replicate actual_nn (member (op =) opts Exhaustive_Option);
54591
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
   979
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   980
    val fun_names = map Binding.name_of bs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   981
    val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   982
    val frees = map (fst #>> Binding.name_of #> Free) fixes;
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
   983
    val has_call = exists_subterm (member (op =) frees);
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   984
    val eqns_data =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
   985
      @{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
55871
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55870
diff changeset
   986
        (tag_list 0 (map snd specs)) of_specs_opt []
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   987
      |> flat o fst;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   988
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   989
    val _ =
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   990
      let
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   991
        val missing = fun_names
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   992
          |> filter (map (fn Disc x => #fun_name x | Sel x => #fun_name x) eqns_data
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   993
            |> not oo member (op =))
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   994
      in
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   995
        null missing
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   996
          orelse primcorec_error_eqns ("missing equations for function(s): " ^ commas missing) []
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   997
      end;
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
   998
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   999
    val callssss =
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1000
      map_filter (try (fn Sel x => x)) eqns_data
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1001
      |> partition_eq (op = o pairself #fun_name)
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1002
      |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
54161
panny
parents: 54160 54159
diff changeset
  1003
      |> map (flat o snd)
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54239
diff changeset
  1004
      |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1005
      |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1006
        (ctr, map (K []) sels))) basic_ctr_specss);
a179353111db generate callssss
panny
parents: 54157
diff changeset
  1007
58283
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
  1008
    val (corec_specs', _, coinduct_thm, coinduct_strong_thm, coinduct_thms, coinduct_strong_thms,
71d74e641538 preserve case names in '(co)induct' theorems generated by prim(co)rec'
blanchet
parents: 58223
diff changeset
  1009
         (coinduct_attrs, common_coinduct_attrs), n2m, lthy') =
55772
367ec44763fd correct most general type for mutual recursion when several identical types are involved
blanchet
parents: 55571
diff changeset
  1010
      corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1011
    val corec_specs = take actual_nn corec_specs';
54178
d6dc359426b7 more informative abort
blanchet
parents: 54177
diff changeset
  1012
    val ctr_specss = map #ctr_specs corec_specs;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
  1013
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1014
    val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1015
      |> partition_eq (op = o pairself #fun_name)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1016
      |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1017
      |> map (sort (op < o pairself #ctr_no |> make_ord) o flat o snd);
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1018
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1019
    val _ = disc_eqnss' |> map (fn x =>
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1020
      let val d = duplicates (op = o pairself #ctr_no) x in null d orelse
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1021
        (if forall (is_some o #ctr_rhs_opt) x then
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1022
          primcorec_error_eqns "multiple equations for constructor(s)"
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1023
            (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1024
              |> map (the o #ctr_rhs_opt)) else
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1025
          primcorec_error_eqns "excess discriminator formula in definition"
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1026
            (maps (fn t => filter (curry (op =) (#ctr_no t) o #ctr_no) x) d |> map #user_eqn)) end);
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1027
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1028
    val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1029
      |> partition_eq (op = o pairself #fun_name)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1030
      |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1031
      |> map (flat o snd);
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1032
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
  1033
    val arg_Tss = map (binder_types o snd o fst) fixes;
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
  1034
    val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1035
      disc_eqnss';
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1036
    val (defs, excludess') =
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
  1037
      build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1038
55009
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1039
    val tac_opts =
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1040
      map (fn {code_rhs_opt, ...} :: _ =>
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1041
        if auto orelse is_some code_rhs_opt then SOME (auto_tac o #context) else NONE) disc_eqnss;
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1042
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1043
    fun exclude_tac tac_opt sequential (c, c', a) =
54901
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
  1044
      if a orelse c = c' orelse sequential then
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
  1045
        SOME (K (HEADGOAL (mk_primcorec_assumption_tac lthy [])))
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
  1046
      else
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1047
        tac_opt;
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
  1048
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
  1049
    val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) =>
55342
blanchet
parents: 55341
diff changeset
  1050
        (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
blanchet
parents: 55341
diff changeset
  1051
           (exclude_tac tac_opt sequential j), goal))))
55009
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1052
      tac_opts sequentials excludess';
56152
2a31945b9a58 add error messages for invalid inputs
panny
parents: 55969
diff changeset
  1053
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1054
    val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
55009
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1055
    val (goal_idxss, exclude_goalss) = excludess''
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1056
      |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1057
      |> split_list o map split_list;
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1058
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1059
    fun list_all_fun_args extras =
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
  1060
      map2 (fn [] => I
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1061
          | {fun_args, ...} :: _ => map (curry Logic.list_all (extras @ map dest_Free fun_args)))
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1062
        disc_eqnss;
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54842
diff changeset
  1063
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1064
    val syntactic_exhaustives =
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1065
      map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns
54913
7b18c41df27a consider code as exhaustive
blanchet
parents: 54912
diff changeset
  1066
          orelse exists #auto_gen disc_eqns)
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1067
        disc_eqnss;
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1068
    val de_facto_exhaustives =
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1069
      map2 (fn b => fn b' => b orelse b') exhaustives syntactic_exhaustives;
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1070
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1071
    val nchotomy_goalss =
54904
5d965f17b0e4 detect syntactic exhaustiveness
blanchet
parents: 54903
diff changeset
  1072
      map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems)
5d965f17b0e4 detect syntactic exhaustiveness
blanchet
parents: 54903
diff changeset
  1073
        de_facto_exhaustives disc_eqnss
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1074
      |> list_all_fun_args []
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1075
    val nchotomy_taut_thmss =
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
  1076
      @{map 5} (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1077
          fn {code_rhs_opt, ...} :: _ => fn [] => K []
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1078
            | [goal] => fn true =>
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1079
              let
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
  1080
                val (_, _, arg_exhaust_discs, _, _) =
55400
blanchet
parents: 55344
diff changeset
  1081
                  case_thms_of_term lthy (the_default Term.dummy code_rhs_opt);
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1082
              in
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1083
                [Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
  1084
                   mk_primcorec_nchotomy_tac ctxt (res_exhaust_discs @ arg_exhaust_discs))
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1085
                 |> Thm.close_derivation]
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1086
              end
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1087
            | false =>
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1088
              (case tac_opt of
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1089
                SOME tac => [Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation]
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1090
              | NONE => []))
55400
blanchet
parents: 55344
diff changeset
  1091
        tac_opts corec_specs disc_eqnss nchotomy_goalss syntactic_exhaustives;
55008
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1092
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1093
    val syntactic_exhaustives =
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1094
      map (fn disc_eqns => forall (null o #prems orf is_some o #code_rhs_opt) disc_eqns
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1095
          orelse exists #auto_gen disc_eqns)
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1096
        disc_eqnss;
b5b2e193ca33 use 'disc_exhausts' property both from types on which 'case's take place and on return type
blanchet
parents: 55005
diff changeset
  1097
55009
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1098
    val nchotomy_goalss =
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1099
      map2 (fn (NONE, false) => map (rpair []) | _ => K []) (tac_opts ~~ syntactic_exhaustives)
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1100
        nchotomy_goalss;
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1101
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1102
    val goalss = nchotomy_goalss @ exclude_goalss;
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54842
diff changeset
  1103
55462
78a06c7b5b87 added 'Spec_Rules' for 'primcorec'
blanchet
parents: 55414
diff changeset
  1104
    fun prove thmss'' def_infos lthy =
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1105
      let
55462
78a06c7b5b87 added 'Spec_Rules' for 'primcorec'
blanchet
parents: 55414
diff changeset
  1106
        val def_thms = map (snd o snd) def_infos;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1107
54972
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
  1108
        val (nchotomy_thmss, exclude_thmss) =
55009
d4b69107a86a automatically solve proof obligations produced for code equations
blanchet
parents: 55008
diff changeset
  1109
          (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'');
54613
985f8b49c050 more work towards "exhaustive"
panny
parents: 54591
diff changeset
  1110
54927
a5a2598f0651 proper name generation to avoid clash with 'P' in user specification
blanchet
parents: 54926
diff changeset
  1111
        val ps =
a5a2598f0651 proper name generation to avoid clash with 'P' in user specification
blanchet
parents: 54926
diff changeset
  1112
          Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
a5a2598f0651 proper name generation to avoid clash with 'P' in user specification
blanchet
parents: 54926
diff changeset
  1113
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1114
        val exhaust_thmss =
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1115
          map2 (fn false => K []
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1116
              | true => fn disc_eqns as {fun_args, ...} :: _ =>
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1117
                let
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1118
                  val p = Bound (length fun_args);
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1119
                  fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1120
                in
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1121
                  [mk_imp_p (map (mk_imp_p o map HOLogic.mk_Trueprop o #prems) disc_eqns)]
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1122
                end)
54904
5d965f17b0e4 detect syntactic exhaustiveness
blanchet
parents: 54903
diff changeset
  1123
            de_facto_exhaustives disc_eqnss
54927
a5a2598f0651 proper name generation to avoid clash with 'P' in user specification
blanchet
parents: 54926
diff changeset
  1124
          |> list_all_fun_args ps
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 58462
diff changeset
  1125
          |> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1126
              | [nchotomy_thm] => fn [goal] =>
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1127
                [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1128
                   (length disc_eqns) nchotomy_thm
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
  1129
                 |> K |> Goal.prove_sorry lthy [] [] goal
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1130
                 |> Thm.close_derivation])
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1131
            disc_eqnss nchotomy_thmss;
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1132
        val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54842
diff changeset
  1133
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1134
        val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1135
        fun mk_excludesss excludes n =
54973
b35859240103 tuning (no need for |-> here)
blanchet
parents: 54972
diff changeset
  1136
          fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])))
54974
d1c76303244e use correct default for exclude rules to avoid weird tactic failures
blanchet
parents: 54973
diff changeset
  1137
            excludes (map (fn k => replicate k [asm_rl] @ replicate (n - k) []) (0 upto n - 1));
54973
b35859240103 tuning (no need for |-> here)
blanchet
parents: 54972
diff changeset
  1138
        val excludessss =
b35859240103 tuning (no need for |-> here)
blanchet
parents: 54972
diff changeset
  1139
          map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs)
b35859240103 tuning (no need for |-> here)
blanchet
parents: 54972
diff changeset
  1140
            (map2 append excludess' taut_thmss) corec_specs;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1141
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1142
        fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1143
            ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1144
          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1145
            []
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1146
          else
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1147
            let
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
  1148
              val {disc, corec_disc, ...} = nth ctr_specs ctr_no;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1149
              val k = 1 + ctr_no;
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1150
              val m = length prems;
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1151
              val goal =
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1152
                applied_fun_of fun_name fun_T fun_args
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1153
                |> curry betapply disc
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1154
                |> HOLogic.mk_Trueprop
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1155
                |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1156
                |> curry Logic.list_all (map dest_Free fun_args);
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1157
            in
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1158
              if prems = [@{term False}] then
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1159
                []
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1160
              else
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57895
diff changeset
  1161
                mk_primcorec_disc_tac lthy def_thms corec_disc k m excludesss
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
  1162
                |> K |> Goal.prove_sorry lthy [] [] goal
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1163
                |> Thm.close_derivation