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