src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
author blanchet
Fri, 10 Jan 2014 14:39:37 +0100
changeset 54972 5747fdd4ad3b
parent 54970 891141de5672
child 54973 b35859240103
permissions -rw-r--r--
fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
     1
(*  Title:      HOL/BNF/Tools/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
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
     6
Corecursor sugar.
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
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    45
exception Primcorec_Error of string * 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
    46
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    47
fun primcorec_error str = raise Primcorec_Error (str, []);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    48
fun primcorec_error_eqn str eqn = raise Primcorec_Error (str, [eqn]);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    49
fun primcorec_error_eqns str eqns = raise Primcorec_Error (str, eqns);
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,
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
    81
   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
    82
   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
    83
   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
    84
   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
    85
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    86
exception AINT_NO_MAP of term;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    87
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    88
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
    89
  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
    90
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
    91
  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
    92
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
    93
  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
    94
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
    95
  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
    96
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
    97
fun order_list_duplicates xs = map snd (sort (int_ord o pairself fst) xs)
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
    98
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
    99
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
   100
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
   101
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
   102
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   103
val conjuncts_s = filter_out (curry (op =) @{const True}) o HOLogic.conjuncts;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   104
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   105
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
   106
  | 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
   107
  | 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
   108
  | 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
   109
  | 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
   110
  | 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
   111
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   112
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
   113
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   114
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
   115
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   116
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
   117
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   118
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
   119
  (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
   120
     ([], _) => css
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   121
   | ([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
   122
     [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
   123
       (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
   124
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   125
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
   126
  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
   127
  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
   128
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   129
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
   130
  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
   131
  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
   132
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   133
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
   134
  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
   135
    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
   136
      [@{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
   137
    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
   138
      []
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   139
    else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   140
      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
   141
      |> 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
   142
      |> 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
   143
      |> (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
   144
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   145
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   146
fun fold_rev_let_if_case ctxt f 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
   147
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   148
    val thy = Proof_Context.theory_of ctxt;
53794
af7d1533a25b undid copy-paste
blanchet
parents: 53793
diff changeset
   149
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   150
    fun 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
   151
      (case Term.strip_comb 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
   152
        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_let t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   153
      | (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
   154
        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
   155
      | (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
   156
        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
   157
          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
   158
            (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
   159
              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
   160
              (case dest_case ctxt s Ts t of
54970
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   161
                SOME (ctr_sugar as {sel_splits = _ :: _, ...}, conds', branches) =>
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   162
                apfst (cons ctr_sugar) o fold_rev (uncurry fld)
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   163
                  (map (append conds o conjuncts_s) conds' ~~ branches)
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   164
              | _ => apsnd (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
   165
            | _ => apsnd (f 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
   166
          else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   167
            apsnd (f 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
   168
        end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   169
      | _ => apsnd (f 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
   170
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   171
    fld [] t o pair []
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
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   194
          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_let t)
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
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   199
        | (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
   200
          (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
   201
            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
   202
            let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   203
              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
   204
              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
   205
            in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   206
              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
   207
                (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
   208
                  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
   209
                  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
   210
                    let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   211
                      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
   212
                      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
   213
                      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
   214
                      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
   215
                      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
   216
                    in
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   217
                      Term.list_comb (casex',
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   218
                        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
   219
                    end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   220
                  else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   221
                    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
   222
                | _ => 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
   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
            end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   226
          | 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
   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
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   230
    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
   231
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   232
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   233
val massage_mutual_corec_call = massage_let_if_case;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   234
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   235
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
   236
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   237
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
   238
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   239
    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
   240
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   241
    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
   242
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   243
    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
   244
      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
   245
        (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
   246
          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
   247
        | 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
   248
      else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   249
        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
   250
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   251
    fun massage_mutual_fun 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
   252
      (case 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
   253
        Const (@{const_name comp}, _) $ t1 $ t2 =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   254
        mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, tap check_no_call t2)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   255
      | _ =>
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   256
        let
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 var = Var ((Name.uu, Term.maxidx_of_term t + 1),
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   258
            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
   259
        in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   260
          Term.lambda var (massage_mutual_call bound_Ts U T (t $ var))
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   261
        end);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   262
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   263
    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
   264
        (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
   265
          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
   266
          let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   267
            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
   268
            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
   269
            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
   270
              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
   271
          in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   272
            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
   273
          end
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   274
        | NONE => raise AINT_NO_MAP t)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   275
      | massage_map _ _ _ t = raise AINT_NO_MAP t
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   276
    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
   277
      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
   278
        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
   279
      else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   280
        massage_map 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
   281
        handle AINT_NO_MAP _ => massage_mutual_fun 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
   282
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   283
    fun 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
   284
      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
   285
        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
   286
          (case U of
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   287
            Type (s, Us) =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   288
            (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
   289
              SOME (f, args) =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   290
              let
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   291
                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
   292
                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
   293
                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
   294
                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
   295
              in
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   296
                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
   297
              end
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   298
            | NONE =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   299
              (case t of
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   300
                Const (@{const_name prod_case}, _) $ t' =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   301
                let
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   302
                  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
   303
                  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
   304
                in
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   305
                  Const (@{const_name prod_case}, U' --> U) $ massage_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
   306
                end
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   307
              | t1 $ t2 =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   308
                (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
   309
                  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
   310
                else
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   311
                  massage_map bound_Ts U T t1 $ t2
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   312
                  handle AINT_NO_MAP _ => 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
   313
              | Abs (s, T', t') =>
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   314
                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
   315
              | _ => 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
   316
          | _ => 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
   317
        else
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   318
          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
   319
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   320
    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
   321
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   322
    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
   323
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   324
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   325
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
   326
  (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
   327
    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
   328
    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
   329
  | 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
   330
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   331
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
   332
  (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
   333
    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
   334
    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
   335
      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
   336
  | _ => 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
   337
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   338
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
   339
  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
   340
    (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
   341
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   342
fun fold_rev_corec_code_rhs ctxt f =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   343
  snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) 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
   344
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   345
fun case_thms_of_term ctxt bound_Ts t =
54970
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   346
  let val (ctr_sugars, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t () in
54246
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   347
    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #sel_splits ctr_sugars,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   348
     maps #sel_split_asms ctr_sugars)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   349
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   350
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   351
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
   352
  (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
   353
    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
   354
    (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
   355
      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
   356
    | 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
   357
      let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   358
        val thy = Proof_Context.theory_of ctxt;
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   359
54246
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 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
   361
        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
   362
        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
   363
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   364
        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
   365
      in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   366
        map3 mk_spec ctrs discs selss
54911
6a6980245ce0 robustness
blanchet
parents: 54910
diff changeset
   367
        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
   368
      end)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   369
  | _ => 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
   370
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   371
fun map_thms_of_typ ctxt (Type (s, _)) =
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   372
    (case fp_sugar_of ctxt s of
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   373
      SOME {index, mapss, ...} => nth mapss index
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   374
    | NONE => [])
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   375
  | map_thms_of_typ _ _ = [];
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   376
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
fun corec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   378
  let
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   379
    val thy = Proof_Context.theory_of lthy;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   380
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   381
    val ((missing_res_Ts, perm0_kks,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   382
          fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   383
            co_inducts = coinduct_thms, ...} :: _, (_, gfp_sugar_thms)), lthy') =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   384
      nested_to_mutual_fps Greatest_FP bs res_Ts get_indices callssss0 lthy;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   385
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   386
    val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   387
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   388
    val indices = map #index fp_sugars;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   389
    val perm_indices = map #index perm_fp_sugars;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   390
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 perm_ctrss = map (#ctrs o of_fp_sugar #ctr_sugars) perm_fp_sugars;
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 perm_ctr_Tsss = map (map (binder_types o fastype_of)) perm_ctrss;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   393
    val perm_gfpTs = map (body_type o fastype_of o hd) perm_ctrss;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   394
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   395
    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
   396
    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
   397
    val kks = 0 upto nn - 1;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   398
    val perm_ns = map length perm_ctr_Tsss;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   399
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   400
    val perm_Cs = map (domain_type o body_fun_type o fastype_of o co_rec_of o
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   401
      of_fp_sugar (#xtor_co_iterss o #fp_res)) perm_fp_sugars;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   402
    val (perm_p_Tss, (perm_q_Tssss, _, 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
   403
      mk_coiter_fun_arg_types perm_ctr_Tsss perm_Cs perm_ns (co_rec_of dtor_coiters1);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   404
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   405
    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
   406
    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
   407
    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
   408
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   409
    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
   410
      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
   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
    fun unpermute0 perm0_xs = permute_like (op =) perm0_kks kks perm0_xs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   413
    fun unpermute perm_xs = permute_like (op =) perm_indices indices perm_xs;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   414
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   415
    val coinduct_thmss = map (unpermute0 o conj_dests nn) coinduct_thms;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   416
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   417
    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
   418
    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
   419
    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
   420
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
    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
   422
    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
   423
    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
   424
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 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
   426
    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
   427
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 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
   429
    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
   430
    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
   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 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
   433
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   434
    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
   435
        (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
   436
         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
   437
         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
   438
      | 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
   439
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   440
    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
   441
        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
   442
      let val nullary = not (can dest_funT (fastype_of ctr)) in
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   443
        {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
   444
         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
   445
         disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm,
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   446
         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
   447
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   448
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   449
    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   450
        sel_coiterssss =
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
      let
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   452
        val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar =
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   453
          nth ctr_sugars index;
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
        val p_ios = map SOME p_is @ [NONE];
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   455
        val discIs = #discIs (nth ctr_sugars index);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   456
        val corec_thms = co_rec_of (nth coiter_thmsss index);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   457
        val disc_corecs = co_rec_of (nth disc_coitersss index);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   458
        val sel_corecss = co_rec_of (nth sel_coiterssss index);
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   459
      in
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   460
        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
   461
          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
   462
      end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   463
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   464
    fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   465
          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} : fp_sugar)
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   466
        p_is q_isss f_isss f_Tsss =
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   467
      {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
54924
44373f3560c7 refactoring
blanchet
parents: 54923
diff changeset
   468
       disc_exhausts = #disc_exhausts (nth ctr_sugars index),
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
   469
       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
   470
       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
   471
       nested_map_comps = map map_comp_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
   472
       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   473
         disc_coitersss sel_coiterssss};
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   474
  in
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   475
    ((is_some gfp_sugar_thms, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_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
   476
      co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   477
      strong_co_induct_of coinduct_thmss), lthy')
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   478
  end;
8fdb4dc08ed1 split 'primrec_new' and 'primcorec' code (to ease bootstrapping, e.g. dependency on datatype 'String' in 'primcorec')
blanchet
parents: 54243
diff changeset
   479
53358
b46e6cd75dc6 improved interfaces
panny
parents: 53357
diff changeset
   480
val undef_const = Const (@{const_name undefined}, dummyT);
53357
46b0c7a08af7 simplified rewriting of map arguments
panny
parents: 53354
diff changeset
   481
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   482
val abs_tuple = HOLogic.tupled_lambda o HOLogic.mk_tuple;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   483
fun abstract vs =
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   484
  let fun a n (t $ u) = a n t $ a n u
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   485
        | a n (Abs (v, T, b)) = Abs (v, T, a (n + 1) b)
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   486
        | a n t = let val idx = find_index (curry (op =) t) vs in
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   487
            if idx < 0 then t else Bound (n + idx) end
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   488
  in a 0 end;
54271
blanchet
parents: 54246
diff changeset
   489
blanchet
parents: 54246
diff changeset
   490
fun mk_prod1 bound_Ts (t, u) =
blanchet
parents: 54246
diff changeset
   491
  HOLogic.pair_const (fastype_of1 (bound_Ts, t)) (fastype_of1 (bound_Ts, u)) $ t $ u;
blanchet
parents: 54246
diff changeset
   492
fun mk_tuple1 bound_Ts = the_default HOLogic.unit o try (foldr1 (mk_prod1 bound_Ts));
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   493
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   494
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
   495
  fun_name: string,
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   496
  fun_T: typ,
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   497
  fun_args: term list,
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   498
  ctr: term,
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   499
  ctr_no: int,
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   500
  disc: term,
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   501
  prems: term list,
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   502
  auto_gen: bool,
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   503
  ctr_rhs_opt: term option,
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   504
  code_rhs_opt: term option,
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   505
  eqn_pos: int,
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   506
  user_eqn: term
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   507
};
54001
65fc58793ed5 made SML/NJ happier
blanchet
parents: 53925
diff changeset
   508
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   509
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
   510
  fun_name: string,
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   511
  fun_T: typ,
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   512
  fun_args: term list,
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   513
  ctr: term,
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   514
  sel: term,
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   515
  rhs_term: term,
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   516
  ctr_rhs_opt: term option,
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   517
  code_rhs_opt: term option,
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   518
  eqn_pos: int,
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   519
  user_eqn: term
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   520
};
54001
65fc58793ed5 made SML/NJ happier
blanchet
parents: 53925
diff changeset
   521
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   522
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
   523
  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
   524
  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
   525
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   526
fun dissect_coeqn_disc 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
   527
    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
   528
  let
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   529
    fun find_subterm p =
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   530
      let (* FIXME \<exists>? *)
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   531
        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
   532
          | 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
   533
      in find end;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   534
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   535
    val applied_fun = concl
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   536
      |> find_subterm (member ((op =) o apsnd SOME) fun_names o try (fst o dest_Free o head_of))
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   537
      |> 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
   538
      handle Option.Option => primcorec_error_eqn "malformed discriminator formula" concl;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   539
    val ((fun_name, fun_T), fun_args) = strip_comb applied_fun |>> dest_Free;
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   540
    val SOME (sequential, basic_ctr_specs) =
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   541
      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
   542
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   543
    val discs = map #disc basic_ctr_specs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   544
    val ctrs = map #ctr basic_ctr_specs;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   545
    val not_disc = head_of concl = @{term Not};
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   546
    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
   547
      primcorec_error_eqn "negated discriminator for a type with \<noteq> 2 constructors" concl;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   548
    val disc' = find_subterm (member (op =) discs o head_of) concl;
54209
blanchet
parents: 54208
diff changeset
   549
    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
   550
        |> (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
   551
          if n >= 0 then SOME n else NONE end | _ => NONE);
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   552
    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
   553
      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
   554
    val ctr_no' =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   555
      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
   556
    val ctr_no = if not_disc then 1 - ctr_no' else ctr_no';
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   557
    val {ctr, disc, ...} = nth basic_ctr_specs ctr_no;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   558
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   559
    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
   560
    val matchedss = AList.lookup (op =) matchedsss fun_name |> the_default [];
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   561
    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
   562
    val actual_prems =
54901
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
   563
      (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
   564
      (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
   565
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   566
    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
   567
      |> 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
   568
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   569
    val user_eqn =
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   570
      (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
   571
      |>> 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
   572
      |> curry Logic.list_all (map dest_Free fun_args) o Logic.list_implies;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   573
  in
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   574
    (Disc {
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   575
      fun_name = fun_name,
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   576
      fun_T = fun_T,
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   577
      fun_args = fun_args,
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   578
      ctr = ctr,
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   579
      ctr_no = ctr_no,
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   580
      disc = disc,
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   581
      prems = actual_prems,
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   582
      auto_gen = catch_all,
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   583
      ctr_rhs_opt = ctr_rhs_opt,
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   584
      code_rhs_opt = code_rhs_opt,
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   585
      eqn_pos = eqn_pos,
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   586
      user_eqn = user_eqn
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   587
    }, matchedsss')
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   588
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   589
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   590
fun dissect_coeqn_sel 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
   591
    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
   592
  let
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   593
    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
   594
      handle 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
   595
        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
   596
    val sel = head_of lhs;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   597
    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
   598
      handle 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
   599
        primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   600
    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
   601
      handle Option.Option =>
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   602
        primcorec_error_eqn "malformed selector argument in left-hand side" eqn;
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   603
    val {ctr, ...} =
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   604
      (case of_spec_opt of
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   605
        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
   606
      | 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
   607
          handle List.Empty => primcorec_error_eqn "ambiguous selector - use \"of\"" eqn);
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
   608
    val user_eqn = drop_All eqn0;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   609
  in
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   610
    Sel {
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   611
      fun_name = fun_name,
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   612
      fun_T = fun_T,
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   613
      fun_args = fun_args,
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   614
      ctr = ctr,
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   615
      sel = sel,
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   616
      rhs_term = rhs,
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   617
      ctr_rhs_opt = ctr_rhs_opt,
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   618
      code_rhs_opt = code_rhs_opt,
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   619
      eqn_pos = eqn_pos,
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   620
      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
   621
    }
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   622
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   623
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   624
fun dissect_coeqn_ctr 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
   625
    eqn_pos eqn0 code_rhs_opt prems concl matchedsss =
53910
2c5055a3583d strengthen tactic
blanchet
parents: 53909
diff changeset
   626
  let
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   627
    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
   628
    val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
54209
blanchet
parents: 54208
diff changeset
   629
    val SOME basic_ctr_specs = AList.lookup (op =) (fun_names ~~ basic_ctr_specss) fun_name;
54074
43cdae9524bf allow 'let's around constructors in constructor view
blanchet
parents: 54068
diff changeset
   630
    val (ctr, ctr_args) = strip_comb (unfold_let rhs);
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   631
    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
   632
      handle Option.Option => primcorec_error_eqn "not a constructor" ctr;
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   633
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   634
    val disc_concl = betapply (disc, lhs);
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   635
    val (eqn_data_disc_opt, matchedsss') = if length basic_ctr_specs = 1
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   636
      then (NONE, matchedsss)
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   637
      else apfst SOME (dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   638
          (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
   639
54159
eb5d58c99049 set stage for more flexible 'primrec' syntax for recursion through functions
blanchet
parents: 54157
diff changeset
   640
    val sel_concls = sels ~~ ctr_args
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   641
      |> map (fn (sel, ctr_arg) => HOLogic.mk_eq (betapply (sel, lhs), ctr_arg));
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   642
53856
54c8dee1295a commented out debugging output in "primcorec"
blanchet
parents: 53835
diff changeset
   643
(*
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   644
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
   645
 (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
   646
 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
   647
 "\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
   648
 space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) prems));
53856
54c8dee1295a commented out debugging output in "primcorec"
blanchet
parents: 53835
diff changeset
   649
*)
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   650
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   651
    val eqns_data_sel =
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   652
      map (dissect_coeqn_sel 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
   653
        (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
   654
  in
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   655
    (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
   656
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   657
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
   658
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
   659
  let
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   660
    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
   661
    val (fun_name, fun_args) = strip_comb lhs |>> fst o dest_Free;
54209
blanchet
parents: 54208
diff changeset
   662
    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
   663
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   664
    val cond_ctrs = fold_rev_corec_code_rhs lthy (fn cs => fn ctr => fn _ =>
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   665
        if member ((op =) o apsnd #ctr) basic_ctr_specs ctr
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   666
        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
   667
        else primcorec_error_eqn "not a constructor" ctr) [] rhs' []
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   668
      |> AList.group (op =);
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   669
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   670
    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
   671
    val ctr_concls = cond_ctrs |> map (fn (ctr, _) =>
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   672
        binder_types (fastype_of ctr)
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   673
        |> 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
   674
          if ctr' = ctr then nth args n else Const (@{const_name undefined}, T)) [] rhs')
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   675
        |> curry list_comb ctr
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   676
        |> curry HOLogic.mk_eq lhs);
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   677
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   678
    val sequentials = replicate (length fun_names) false;
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   679
  in
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
   680
    fold_map2 (dissect_coeqn_ctr 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
   681
        (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
   682
      ctr_premss ctr_concls matchedsss
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   683
  end;
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   684
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   685
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
   686
    (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
   687
  let
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
   688
    val eqn = drop_All eqn0
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   689
      handle TERM _ => primcorec_error_eqn "malformed function equation" eqn0;
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   690
    val (prems, concl) = Logic.strip_horn eqn
53341
63015d035301 handle selector formulae with no corecursive calls
panny
parents: 53335
diff changeset
   691
      |> apfst (map HOLogic.dest_Trueprop) o apsnd HOLogic.dest_Trueprop;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   692
54065
e30e63d05e58 process code-style inputs
panny
parents: 54044
diff changeset
   693
    val head = concl
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   694
      |> 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
   695
      |> head_of;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   696
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   697
    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
   698
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   699
    val discs = maps (map #disc) basic_ctr_specss;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   700
    val sels = maps (maps #sels) basic_ctr_specss;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   701
    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
   702
  in
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   703
    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
   704
        is_some rhs_opt andalso
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   705
          member (op =) (filter (null o binder_types o fastype_of) ctrs) (the rhs_opt) 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
   706
      dissect_coeqn_disc fun_names sequentials basic_ctr_specss eqn_pos NONE NONE prems concl
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   707
        matchedsss
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   708
      |>> single
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   709
    else if member (op =) sels head then
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
   710
      ([dissect_coeqn_sel 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
   711
       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
   712
    else if is_Free head andalso member (op =) fun_names (fst (dest_Free head)) 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
   713
      if member (op =) ctrs (head_of (unfold_let (the rhs_opt))) 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
   714
        dissect_coeqn_ctr fun_names sequentials basic_ctr_specss eqn_pos eqn0
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
   715
          (if null prems then SOME eqn0 else NONE) prems 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
   716
      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
   717
        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
   718
        |>> 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
   719
      else
54956
80a1931267ce tuned error message
blanchet
parents: 54955
diff changeset
   720
        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
   721
    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
   722
      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
   723
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   724
54002
01c8f9d3b084 made SML/NJ happy
blanchet
parents: 54001
diff changeset
   725
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
   726
    ({fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   727
  if is_none (#pred (nth ctr_specs ctr_no)) then I else
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   728
    s_conjs prems
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   729
    |> curry subst_bounds (List.rev fun_args)
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   730
    |> HOLogic.tupled_lambda (HOLogic.mk_tuple fun_args)
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   731
    |> 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
   732
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   733
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
   734
  find_first (curry (op =) sel o #sel) sel_eqns
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   735
  |> try (fn SOME {fun_args, rhs_term, ...} => abs_tuple fun_args rhs_term)
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   736
  |> the_default undef_const
53411
ab4edf89992f support indirect corecursion
panny
parents: 53401
diff changeset
   737
  |> K;
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   738
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   739
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
   740
  (case find_first (curry (op =) sel o #sel) sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   741
    NONE => (I, I, I)
blanchet
parents: 54207
diff changeset
   742
  | SOME {fun_args, rhs_term, ... } =>
53876
fabf04d43a75 simplified code
panny
parents: 53875
diff changeset
   743
    let
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   744
      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
   745
      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
   746
      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
   747
      fun rewrite_cont bound_Ts t =
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   748
        if has_call t then mk_tuple1 bound_Ts (snd (strip_comb t)) else undef_const;
54102
82ada0a92dde tuned names
blanchet
parents: 54101
diff changeset
   749
      fun massage f _ = massage_mutual_corec_call lthy has_call f bound_Ts rhs_term
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   750
        |> abs_tuple fun_args;
53876
fabf04d43a75 simplified code
panny
parents: 53875
diff changeset
   751
    in
54207
9296ebf40db0 tuned names (to make them independent from temporary naming convention used in characteristic theorems)
blanchet
parents: 54206
diff changeset
   752
      (massage rewrite_stop, massage rewrite_end, massage rewrite_cont)
54208
blanchet
parents: 54207
diff changeset
   753
    end);
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   754
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   755
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
   756
  (case find_first (curry (op =) sel o #sel) sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   757
    NONE => I
blanchet
parents: 54207
diff changeset
   758
  | SOME {fun_args, rhs_term, ...} =>
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   759
    let
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   760
      val bound_Ts = List.rev (map fastype_of fun_args);
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   761
      fun rewrite bound_Ts U T (Abs (v, V, b)) = Abs (v, V, rewrite (V :: bound_Ts) U T b)
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   762
        | rewrite bound_Ts U T (t as _ $ _) =
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   763
          let val (u, vs) = strip_comb t in
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   764
            if is_Free u andalso has_call u then
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   765
              Inr_const U T $ mk_tuple1 bound_Ts vs
54271
blanchet
parents: 54246
diff changeset
   766
            else if try (fst o dest_Const) u = SOME @{const_name prod_case} then
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   767
              map (rewrite bound_Ts U T) vs |> chop 1 |>> HOLogic.mk_split o the_single |> list_comb
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   768
            else
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   769
              list_comb (rewrite bound_Ts U T u, map (rewrite bound_Ts U T) vs)
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   770
          end
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   771
        | rewrite _ U T t =
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   772
          if is_Free t andalso has_call t then Inr_const U T $ HOLogic.unit else t;
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   773
      fun massage t =
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
   774
        rhs_term
54102
82ada0a92dde tuned names
blanchet
parents: 54101
diff changeset
   775
        |> massage_nested_corec_call lthy has_call rewrite bound_Ts (range_type (fastype_of t))
53735
99331dac1e1c simplified code; eliminated some dummyTs
panny
parents: 53734
diff changeset
   776
        |> abs_tuple fun_args;
53899
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   777
    in
e55b634ff9fb simplified code
panny
parents: 53890
diff changeset
   778
      massage
54208
blanchet
parents: 54207
diff changeset
   779
    end);
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   780
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   781
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
   782
    (ctr_spec : corec_ctr_spec) =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   783
  (case filter (curry (op =) (#ctr ctr_spec) o #ctr) all_sel_eqns of
54208
blanchet
parents: 54207
diff changeset
   784
    [] => I
blanchet
parents: 54207
diff changeset
   785
  | sel_eqns =>
blanchet
parents: 54207
diff changeset
   786
    let
blanchet
parents: 54207
diff changeset
   787
      val sel_call_list = #sels ctr_spec ~~ #calls ctr_spec;
blanchet
parents: 54207
diff changeset
   788
      val no_calls' = map_filter (try (apsnd (fn No_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   789
      val mutual_calls' = map_filter (try (apsnd (fn Mutual_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   790
      val nested_calls' = map_filter (try (apsnd (fn Nested_Corec n => n))) sel_call_list;
blanchet
parents: 54207
diff changeset
   791
    in
blanchet
parents: 54207
diff changeset
   792
      I
blanchet
parents: 54207
diff changeset
   793
      #> fold (fn (sel, n) => nth_map n (build_corec_arg_no_call sel_eqns sel)) no_calls'
blanchet
parents: 54207
diff changeset
   794
      #> fold (fn (sel, (q, g, h)) =>
blanchet
parents: 54207
diff changeset
   795
        let val (fq, fg, fh) = build_corec_args_mutual_call lthy has_call sel_eqns sel in
blanchet
parents: 54207
diff changeset
   796
          nth_map q fq o nth_map g fg o nth_map h fh end) mutual_calls'
blanchet
parents: 54207
diff changeset
   797
      #> fold (fn (sel, n) => nth_map n
blanchet
parents: 54207
diff changeset
   798
        (build_corec_arg_nested_call lthy has_call sel_eqns sel)) nested_calls'
blanchet
parents: 54207
diff changeset
   799
    end);
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   800
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
   801
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
   802
    (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
   803
  let
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   804
    val corecs = map #corec corec_specs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   805
    val ctr_specss = map #ctr_specs corec_specs;
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   806
    val corec_args = hd corecs
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   807
      |> fst o split_last o binder_types o fastype_of
54806
a0f024caa04c pass auto-proved exhaustiveness properties to tactic;
panny
parents: 54628
diff changeset
   808
      |> map (fn T => if range_type T = @{typ bool}
a0f024caa04c pass auto-proved exhaustiveness properties to tactic;
panny
parents: 54628
diff changeset
   809
          then Abs (Name.uu_, domain_type T, @{term False})
a0f024caa04c pass auto-proved exhaustiveness properties to tactic;
panny
parents: 54628
diff changeset
   810
          else Const (@{const_name undefined}, T))
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   811
      |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   812
      |> 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
   813
    fun currys [] t = t
99331dac1e1c simplified code; eliminated some dummyTs
panny
parents: 53734
diff changeset
   814
      | currys Ts t = t $ mk_tuple1 (List.rev Ts) (map Bound (length Ts - 1 downto 0))
99331dac1e1c simplified code; eliminated some dummyTs
panny
parents: 53734
diff changeset
   815
          |> fold_rev (Term.abs o pair Name.uu) Ts;
53401
2101a97e6220 various refactoring;
panny
parents: 53360
diff changeset
   816
53856
54c8dee1295a commented out debugging output in "primcorec"
blanchet
parents: 53835
diff changeset
   817
(*
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   818
val _ = tracing ("corecursor arguments:\n    \<cdot> " ^
53411
ab4edf89992f support indirect corecursion
panny
parents: 53401
diff changeset
   819
 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
   820
*)
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   821
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   822
    val excludess' =
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   823
      disc_eqnss
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   824
      |> 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
   825
        #> 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
   826
        #> maps (uncurry (map o pair)
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   827
          #> map (fn ((fun_args, c, x, a), (_, c', y, a')) =>
54068
447354985f6a generate optimized DNF formula
blanchet
parents: 54067
diff changeset
   828
              ((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
   829
            ||> apfst (map HOLogic.mk_Trueprop) o apsnd HOLogic.mk_Trueprop
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   830
            ||> Logic.list_implies
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   831
            ||> 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
   832
  in
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   833
    map (list_comb o rpair corec_args) corecs
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   834
    |> 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
   835
    |> map2 currys arg_Tss
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   836
    |> Syntax.check_terms lthy
54155
b964fad0cbbd conceal more ugly constructions
blanchet
parents: 54154
diff changeset
   837
    |> 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
   838
      bs mxs
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   839
    |> rpair excludess'
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   840
  end;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   841
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   842
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
   843
    (sel_eqns : coeqn_data_sel list) (disc_eqns : coeqn_data_disc list) =
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   844
  let val num_disc_eqns = length disc_eqns in
54912
4ecdea61181e proper handling of corner case, take 2
blanchet
parents: 54911
diff changeset
   845
    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
   846
      disc_eqns
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   847
    else
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   848
      let
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   849
        val n = 0 upto length ctr_specs
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   850
          |> the o find_first (fn idx => not (exists (curry (op =) idx o #ctr_no) disc_eqns));
54958
4933165fd112 do not use wrong constructor in auto-generated proof goal
panny
parents: 54956
diff changeset
   851
        val {ctr, disc, ...} = nth ctr_specs n;
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   852
        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
   853
          |> 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
   854
        val sel_eqn_opt = find_first (equal ctr o #ctr) sel_eqns;
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   855
        val extra_disc_eqn = {
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   856
          fun_name = Binding.name_of fun_binding,
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   857
          fun_T = arg_Ts ---> body_type (fastype_of (#ctr (hd ctr_specs))),
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   858
          fun_args = fun_args,
54958
4933165fd112 do not use wrong constructor in auto-generated proof goal
panny
parents: 54956
diff changeset
   859
          ctr = ctr,
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   860
          ctr_no = n,
54958
4933165fd112 do not use wrong constructor in auto-generated proof goal
panny
parents: 54956
diff changeset
   861
          disc = disc,
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   862
          prems = maps (s_not_conj o #prems) disc_eqns,
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   863
          auto_gen = true,
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   864
          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
   865
          code_rhs_opt = Option.map #ctr_rhs_opt sel_eqn_opt |> the_default NONE,
54959
30ded82ff806 fixed 'disc_iff' tactic in the case where different equations use different variable names for the function arguments
blanchet
parents: 54958
diff changeset
   866
          eqn_pos = Option.map (curry (op +) 1 o #eqn_pos) sel_eqn_opt |> the_default 100000 (*###*),
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   867
          user_eqn = undef_const};
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   868
      in
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   869
        chop n disc_eqns ||> cons extra_disc_eqn |> (op @)
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   870
      end
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   871
  end;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   872
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54239
diff changeset
   873
fun find_corec_calls ctxt has_call basic_ctr_specs ({ctr, sel, rhs_term, ...} : coeqn_data_sel) =
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   874
  let
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   875
    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
   876
      |> find_index (curry (op =) sel) o #sels o the;
54970
891141de5672 only destruct cases equipped with the right stuff (in particular, 'sel_split')
blanchet
parents: 54969
diff changeset
   877
    fun find t = if has_call t then snd (fold_rev_let_if_case ctxt (K cons) [] t []) else [];
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   878
  in
a179353111db generate callssss
panny
parents: 54157
diff changeset
   879
    find rhs_term
a179353111db generate callssss
panny
parents: 54157
diff changeset
   880
    |> K |> nth_map sel_no |> AList.map_entry (op =) ctr
a179353111db generate callssss
panny
parents: 54157
diff changeset
   881
  end;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   882
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   883
fun applied_fun_of fun_name fun_T fun_args =
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   884
  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
   885
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
   886
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
   887
  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
   888
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   889
fun add_primcorec_ursive tac_opt 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
   890
  let
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   891
    val thy = Proof_Context.theory_of lthy;
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   892
53352
43a1cc050943 honor mixfix specifications
traytel
parents: 53341
diff changeset
   893
    val (bs, mxs) = map_split (apfst fst) fixes;
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   894
    val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> HOLogic.mk_tupleT) fixes |> split_list;
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   895
54272
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   896
    val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   897
        [] => ()
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
   898
      | (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
   899
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   900
    val actual_nn = length bs;
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   901
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   902
    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
   903
    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
   904
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   905
    val fun_names = map Binding.name_of bs;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   906
    val basic_ctr_specss = map (basic_corec_specs_of lthy) res_Ts;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   907
    val has_call = exists_subterm (map (fst #>> Binding.name_of #> Free) fixes |> member (op =));
a179353111db generate callssss
panny
parents: 54157
diff changeset
   908
    val eqns_data =
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   909
      fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss) (tag_list 0 (map snd specs))
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   910
        of_specs_opt []
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   911
      |> flat o fst;
a179353111db generate callssss
panny
parents: 54157
diff changeset
   912
a179353111db generate callssss
panny
parents: 54157
diff changeset
   913
    val callssss =
a179353111db generate callssss
panny
parents: 54157
diff changeset
   914
      map_filter (try (fn Sel x => x)) eqns_data
a179353111db generate callssss
panny
parents: 54157
diff changeset
   915
      |> partition_eq ((op =) o pairself #fun_name)
a179353111db generate callssss
panny
parents: 54157
diff changeset
   916
      |> fst o finds (fn (x, ({fun_name, ...} :: _)) => x = fun_name) fun_names
54161
panny
parents: 54160 54159
diff changeset
   917
      |> map (flat o snd)
54243
a596292be9a8 more robust n2m w.r.t. 'let's
blanchet
parents: 54239
diff changeset
   918
      |> map2 (fold o find_corec_calls lthy has_call) basic_ctr_specss
54160
a179353111db generate callssss
panny
parents: 54157
diff changeset
   919
      |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
a179353111db generate callssss
panny
parents: 54157
diff changeset
   920
        (ctr, map (K []) sels))) basic_ctr_specss);
a179353111db generate callssss
panny
parents: 54157
diff changeset
   921
a179353111db generate callssss
panny
parents: 54157
diff changeset
   922
(*
a179353111db generate callssss
panny
parents: 54157
diff changeset
   923
val _ = tracing ("callssss = " ^ @{make_string} callssss);
a179353111db generate callssss
panny
parents: 54157
diff changeset
   924
*)
53303
ae49b835ca01 moved files related to "primrec_new", "primcorec", and "datatype_compat" from bitbucket co-rec repository
blanchet
parents:
diff changeset
   925
53830
ed2eb7df2aac don't note more induction principles than there are functions + tuning
blanchet
parents: 53822
diff changeset
   926
    val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
53797
576f9637dc7a note coinduct theorems in "primcorec"
blanchet
parents: 53795
diff changeset
   927
          strong_coinduct_thms), lthy') =
53794
af7d1533a25b undid copy-paste
blanchet
parents: 53793
diff changeset
   928
      corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
   929
    val corec_specs = take actual_nn corec_specs';
54178
d6dc359426b7 more informative abort
blanchet
parents: 54177
diff changeset
   930
    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
   931
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   932
    val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   933
      |> partition_eq ((op =) o pairself #fun_name)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   934
      |> 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
   935
      |> map (sort ((op <) o pairself #ctr_no |> make_ord) o flat o snd);
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   936
    val _ = disc_eqnss' |> map (fn x =>
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   937
      let val d = duplicates ((op =) o pairself #ctr_no) x in null d 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
   938
        primcorec_error_eqns "excess discriminator formula in definition"
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
   939
          (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
   940
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   941
    val sel_eqnss = map_filter (try (fn Sel x => x)) eqns_data
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   942
      |> partition_eq ((op =) o pairself #fun_name)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
   943
      |> 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
   944
      |> map (flat o snd);
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   945
53360
7ffc4a746a73 handle direct corecursion
panny
parents: 53358
diff changeset
   946
    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
   947
    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
   948
      disc_eqnss';
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   949
    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
   950
      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
   951
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   952
    fun exclude_tac sequential (c, c', a) =
54901
0b8871677e0b use same name for feature internally as in user interface, to facilitate grepping
blanchet
parents: 54900
diff changeset
   953
      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
   954
        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
   955
      else
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   956
        tac_opt;
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   957
53856
54c8dee1295a commented out debugging output in "primcorec"
blanchet
parents: 53835
diff changeset
   958
(*
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   959
val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   960
 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
   961
*)
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
   962
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   963
    val excludess'' = map2 (fn sequential => map (fn (idx, goal) =>
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
   964
        (idx, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
54902
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   965
           (exclude_tac sequential idx), goal))))
a9291e4d2366 internally allow different values for 'sequential' for different constructors
blanchet
parents: 54901
diff changeset
   966
      sequentials excludess';
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   967
    val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
   968
    val (goal_idxss, goalss') = excludess''
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   969
      |> 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
   970
      |> split_list o map split_list;
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
   971
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
   972
    fun list_all_fun_args extras =
54910
0ec2cccbf8ad properly synchronize parallel lists
blanchet
parents: 54909
diff changeset
   973
      map2 (fn [] => I
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
   974
          | {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
   975
        disc_eqnss;
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54842
diff changeset
   976
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   977
    val syntactic_exhaustives =
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
   978
      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
   979
          orelse exists #auto_gen disc_eqns)
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   980
        disc_eqnss;
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   981
    val de_facto_exhaustives =
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   982
      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
   983
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   984
    fun map_prove_with_tac tac =
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
   985
      map (fn goal => Goal.prove_sorry lthy [] [] goal tac |> Thm.close_derivation);
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
   986
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
   987
    val nchotomy_goalss =
54904
5d965f17b0e4 detect syntactic exhaustiveness
blanchet
parents: 54903
diff changeset
   988
      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
   989
        de_facto_exhaustives disc_eqnss
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
   990
      |> list_all_fun_args []
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
   991
    val nchotomy_taut_thmss =
54972
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   992
      map3 (fn {disc_exhausts, ...} => fn syntactic_exhaustive =>
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   993
          if syntactic_exhaustive then
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   994
            map_prove_with_tac (fn {context = ctxt, ...} =>
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   995
              mk_primcorec_nchotomy_tac ctxt disc_exhausts)
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   996
          else
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   997
            (case tac_opt of
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   998
              SOME tac => map_prove_with_tac tac
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
   999
            | NONE => K []))
54924
44373f3560c7 refactoring
blanchet
parents: 54923
diff changeset
  1000
        corec_specs syntactic_exhaustives nchotomy_goalss;
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1001
    val goalss = goalss'
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1002
      |> (if is_none tac_opt then
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1003
          append (map2 (fn true => K [] | false => map (rpair [])) syntactic_exhaustives
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1004
            nchotomy_goalss)
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1005
        else
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1006
          I);
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54842
diff changeset
  1007
54613
985f8b49c050 more work towards "exhaustive"
panny
parents: 54591
diff changeset
  1008
    fun prove thmss'' def_thms' lthy =
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1009
      let
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1010
        val def_thms = map (snd o snd) def_thms';
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1011
54972
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
  1012
        val (nchotomy_thmss, exclude_thmss) =
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
  1013
          if is_none tac_opt then
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
  1014
            (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'')
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
  1015
          else
5747fdd4ad3b fix 'primcorec' (as opposed to 'primcorecursive') with 'exhaustive')
blanchet
parents: 54970
diff changeset
  1016
            (nchotomy_taut_thmss, thmss'');
54613
985f8b49c050 more work towards "exhaustive"
panny
parents: 54591
diff changeset
  1017
54927
a5a2598f0651 proper name generation to avoid clash with 'P' in user specification
blanchet
parents: 54926
diff changeset
  1018
        val ps =
a5a2598f0651 proper name generation to avoid clash with 'P' in user specification
blanchet
parents: 54926
diff changeset
  1019
          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
  1020
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1021
        val exhaust_thmss =
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1022
          map2 (fn false => K []
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1023
              | true => fn disc_eqns as {fun_args, ...} :: _ =>
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1024
                let
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1025
                  val p = Bound (length fun_args);
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1026
                  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
  1027
                in
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1028
                  [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
  1029
                end)
54904
5d965f17b0e4 detect syntactic exhaustiveness
blanchet
parents: 54903
diff changeset
  1030
            de_facto_exhaustives disc_eqnss
54927
a5a2598f0651 proper name generation to avoid clash with 'P' in user specification
blanchet
parents: 54926
diff changeset
  1031
          |> list_all_fun_args ps
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1032
          |> 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
  1033
              | [nchotomy_thm] => fn [goal] =>
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1034
                [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
  1035
                   (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
  1036
                 |> K |> Goal.prove_sorry lthy [] [] goal
54903
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1037
                 |> Thm.close_derivation])
c664bd02bf94 internally allow different values for 'exhaustive' for different constructors
blanchet
parents: 54902
diff changeset
  1038
            disc_eqnss nchotomy_thmss;
54921
862c36b6e57c avoid schematic variable in goal, which sometimes gets instantiated by tactic
blanchet
parents: 54917
diff changeset
  1039
        val nontriv_exhaust_thmss = map (filter_out is_trivial_implies) exhaust_thmss;
54844
630ba4d8a206 generate exhaust from nchotomy
blanchet
parents: 54842
diff changeset
  1040
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1041
        val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1042
        fun mk_excludesss excludes n =
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1043
          (excludes, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
53822
6304b12c7627 add "primcorec" command (cf. ae7f50e70c09)
panny
parents: 53811
diff changeset
  1044
          |-> fold (fn ((c, c', _), thm) => nth_map c (nth_map c' (K [thm])));
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1045
        val excludessss = (excludess' ~~ taut_thmss |> map (op @), fun_names ~~ corec_specs)
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1046
          |-> map2 (fn excludes => fn (_, {ctr_specs, ...}) =>
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1047
            mk_excludesss excludes (length ctr_specs));
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1048
54835
431133d07192 note manually proved exclusiveness property
blanchet
parents: 54834
diff changeset
  1049
        fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1050
            ({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
  1051
          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
  1052
            []
9d623cada37f avoid subtle failure in the presence of top sort
blanchet
parents: 54271
diff changeset
  1053
          else
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1054
            let
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1055
              val {disc, disc_corec, ...} = nth ctr_specs ctr_no;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1056
              val k = 1 + ctr_no;
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1057
              val m = length prems;
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1058
              val goal =
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1059
                applied_fun_of fun_name fun_T fun_args
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1060
                |> curry betapply disc
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1061
                |> HOLogic.mk_Trueprop
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1062
                |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1063
                |> curry Logic.list_all (map dest_Free fun_args);
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1064
            in
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1065
              if prems = [@{term False}] then
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1066
                []
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1067
              else
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1068
                mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
  1069
                |> K |> Goal.prove_sorry lthy [] [] goal
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1070
                |> Thm.close_derivation
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1071
                |> pair (#disc (nth ctr_specs ctr_no))
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1072
                |> pair eqn_pos
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1073
                |> single
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1074
            end;
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1075
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
  1076
        fun prove_sel ({nested_maps, nested_map_idents, nested_map_comps, ctr_specs, ...}
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
  1077
              : corec_spec) (disc_eqns : coeqn_data_disc list) excludesss
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1078
            ({fun_name, fun_T, fun_args, ctr, sel, rhs_term, eqn_pos, ...} : coeqn_data_sel) =
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1079
          let
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1080
            val SOME ctr_spec = find_first (curry (op =) ctr o #ctr) ctr_specs;
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1081
            val ctr_no = find_index (curry (op =) ctr o #ctr) ctr_specs;
54067
7be49e2bfccc rationalized negation code
blanchet
parents: 54065
diff changeset
  1082
            val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1083
              (find_first (curry (op =) ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1084
            val sel_corec = find_index (curry (op =) sel) (#sels ctr_spec)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1085
              |> nth (#sel_corecs ctr_spec);
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1086
            val k = 1 + ctr_no;
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1087
            val m = length prems;
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1088
            val goal =
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1089
              applied_fun_of fun_name fun_T fun_args
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1090
              |> curry betapply sel
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1091
              |> rpair (abstract (List.rev fun_args) rhs_term)
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1092
              |> HOLogic.mk_Trueprop o HOLogic.mk_eq
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1093
              |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1094
              |> curry Logic.list_all (map dest_Free fun_args);
53925
blanchet
parents: 53923
diff changeset
  1095
            val (distincts, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1096
          in
54955
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
  1097
            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
cf8d429dc24e reintroduce recursive calls under constructors, taken out in 8dd0e0316881 mainly and in subsequent changes
blanchet
parents: 54954
diff changeset
  1098
              nested_map_idents nested_map_comps sel_corec k m excludesss
54951
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
  1099
            |> K |> Goal.prove_sorry lthy [] [] goal
54176
8039bd7e98b1 systematically close derivations in BNF package
blanchet
parents: 54175
diff changeset
  1100
            |> Thm.close_derivation
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1101
            |> pair sel
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1102
            |> pair eqn_pos
53654
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1103
          end;
8b9ea4420f81 prove simp theorems for newly generated definitions
panny
parents: 53411
diff changeset
  1104
54153
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
  1105
        fun prove_ctr disc_alist sel_alist (disc_eqns : coeqn_data_disc list)
67487a607ce2 avoid 'co_' prefix with underscore meaning 'co', since it is our only possible identifier representation of '(co)'
blanchet
parents: 54145
diff changeset
  1106
            (sel_eqns : coeqn_data_sel list) ({ctr, disc, sels, collapse, ...} : corec_ctr_spec) =
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1107
          (* don't try to prove theorems when some sel_eqns are missing *)
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1108
          if not (exists (curry (op =) ctr o #ctr) disc_eqns)
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1109
              andalso not (exists (curry (op =) ctr o #ctr) sel_eqns)
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1110
            orelse
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1111
              filter (curry (op =) ctr o #ctr) sel_eqns
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1112
              |> fst o finds ((op =) o apsnd #sel) sels
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
  1113
              |> exists (null o snd) 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
  1114
            []
e25b4d22082b for code equations that coincide with ctr equations, make sure the usr's input is preserved for both
blanchet
parents: 54948
diff changeset
  1115
          else
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1116
            let
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1117
              val (fun_name, fun_T, fun_args, prems, rhs_opt, eqn_pos) =
54923
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1118
                (find_first (curry (op =) ctr o #ctr) disc_eqns,
ffed2452f5f6 instantiate schematics as projections to avoid HOU trouble
blanchet
parents: 54921
diff changeset
  1119
                 find_first (curry (op =) ctr o #ctr) sel_eqns)
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1120
                |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #prems x,
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1121
                  #ctr_rhs_opt x, #eqn_pos x))
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1122
                ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #ctr_rhs_opt x,
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1123
                  #eqn_pos x))
53722
e176d6d3345f generate more theorems (e.g. for types with only one constructor)
panny
parents: 53720
diff changeset
  1124
                |> the o merge_options;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1125
              val m = length prems;
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1126
              val goal =
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1127
                (case rhs_opt of
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1128
                  SOME rhs => rhs
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1129
                | NONE =>
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1130
                  filter (curry (op =) ctr o #ctr) sel_eqns
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1131
                  |> fst o finds ((op =) o apsnd #sel) sels
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1132
                  |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1133
                  |> curry list_comb ctr)
54900
136fe16e726a generate 'disc_iff' property in 'primcorec'
blanchet
parents: 54899
diff changeset
  1134
                |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1135
                |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1136
                |> curry Logic.list_all (map dest_Free fun_args);
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1137
              val disc_thm_opt = AList.lookup (op =) disc_alist disc;
53791
0ddf045113c9 tuned code
blanchet
parents: 53753
diff changeset
  1138
              val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist);
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1139
            in
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1140
              if prems = [@{term False}] then [] else
54954
a4ef9253a0b8 strengthened tactics w.r.t. 'lets' and tuples
blanchet
parents: 54951
diff changeset
  1141
                mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms
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
  1142
                |> K |> Goal.prove_sorry lthy [] [] goal
54176
8039bd7e98b1 systematically close derivations in BNF package
blanchet
parents: 54175
diff changeset
  1143
                |> Thm.close_derivation
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1144
                |> pair ctr
54948
516adecd99dd match order of generated theorems to user input;
panny
parents: 54927
diff changeset
  1145
                |> pair eqn_pos
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1146
                |> single
53876
fabf04d43a75 simplified code
panny
parents: 53875
diff changeset
  1147
            end;
53720
03fac7082137 generate constructor view theorems
panny
parents: 53699
diff changeset
  1148
54905
2fdec6c29eb7 don't generate any proof obligation for implicit (de facto) exclusiveness
blanchet
parents: 54904
diff changeset
  1149
        fun prove_code exhaustive disc_eqns sel_eqns nchotomys ctr_alist ctr_specs =
54098
07a8145aaeba pass the right theorems to tactic
panny
parents: 54097
diff changeset
  1150
          let
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1151
            val fun_data_opt =
54097
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1152
              (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
92c5bd3b342d prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
panny
parents: 54074
diff changeset
  1153
               find_first (member (op =) (map #ctr ctr_specs) o #ctr) sel_eqns)
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1154
              |>> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x))
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: 54925
diff changeset
  1155
              ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, #code_rhs_opt x))
54591
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
  1156
              |> merge_options;
c822230fd22b prevent exception when equations for a function are missing;
panny
parents: 54279
diff changeset
  1157
          in
54926
28b621fce2f9 more SML-ish (less Haskell-ish) naming convention
blanchet
parents: