src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
author blanchet
Tue, 05 Jul 2016 17:52:08 +0200
changeset 63391 6840e808fe44
parent 63352 4eaf35781b23
child 63801 83841a5c0897
permissions -rw-r--r--
tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     1
(*  Title:      HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     2
    Author:     Aymeric Bouzy, Ecole polytechnique
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, Inria, LORIA, MPII
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     4
    Author:     Dmitriy Traytel, ETH Z├╝rich
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     5
    Copyright   2015, 2016
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     6
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     7
Generalized corecursor sugar ("corec" and friends).
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     8
*)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
     9
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    10
signature BNF_GFP_GREC_SUGAR =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    11
sig
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    12
  datatype corec_option =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    13
    Plugins_Option of Proof.context -> Plugin_Name.filter |
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    14
    Friend_Option |
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    15
    Transfer_Option
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    16
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    17
  val parse_corec_equation: Proof.context -> term list -> term -> term list * term
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    18
  val explore_corec_equation: Proof.context -> bool -> bool -> string -> term ->
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    19
    BNF_GFP_Grec_Sugar_Util.s_parse_info -> typ -> term list * term -> term list * term
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    20
  val build_corecUU_arg_and_goals: bool -> term -> term list * term -> local_theory ->
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    21
    (((thm list * thm list * thm list) * term list) * term) * local_theory
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    22
  val derive_eq_corecUU: Proof.context -> BNF_GFP_Grec.corec_info -> term -> term -> thm -> thm
62746
blanchet
parents: 62743
diff changeset
    23
  val derive_unique: Proof.context -> morphism -> term -> BNF_GFP_Grec.corec_info -> string ->
blanchet
parents: 62743
diff changeset
    24
    thm -> thm
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    25
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    26
  val corec_cmd: corec_option list -> (binding * string option * mixfix) list * string ->
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    27
    local_theory -> local_theory
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    28
  val corecursive_cmd: corec_option list -> (binding * string option * mixfix) list * string ->
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    29
    local_theory -> Proof.state
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    30
  val friend_of_corec_cmd: (string * string option) * string -> local_theory -> Proof.state
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    31
  val coinduction_upto_cmd: string * string -> local_theory -> local_theory
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    32
end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    33
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    34
structure BNF_GFP_Grec_Sugar : BNF_GFP_GREC_SUGAR =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    35
struct
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    36
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    37
open Ctr_Sugar
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    38
open BNF_Util
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    39
open BNF_Tactics
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    40
open BNF_Def
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    41
open BNF_Comp
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    42
open BNF_FP_Util
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    43
open BNF_FP_Def_Sugar
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    44
open BNF_FP_N2M_Sugar
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    45
open BNF_GFP_Rec_Sugar
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    46
open BNF_GFP_Util
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    47
open BNF_GFP_Grec
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    48
open BNF_GFP_Grec_Sugar_Util
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    49
open BNF_GFP_Grec_Sugar_Tactics
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    50
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    51
val cong_N = "cong_";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    52
val baseN = "base";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    53
val reflN = "refl";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    54
val symN = "sym";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    55
val transN = "trans";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    56
val cong_introsN = prefix cong_N "intros";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    57
val codeN = "code";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    58
val coinductN = "coinduct";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    59
val coinduct_uptoN = "coinduct_upto";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    60
val corecN = "corec";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    61
val ctrN = "ctr";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    62
val discN = "disc";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    63
val disc_iffN = "disc_iff";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    64
val eq_algrhoN = "eq_algrho";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    65
val eq_corecUUN = "eq_corecUU";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    66
val friendN = "friend";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    67
val inner_elimN = "inner_elim";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    68
val inner_inductN = "inner_induct";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    69
val inner_simpN = "inner_simp";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    70
val rhoN = "rho";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    71
val selN = "sel";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    72
val uniqueN = "unique";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    73
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    74
val inner_fp_suffix = "_inner_fp";
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    75
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    76
val nitpicksimp_attrs = @{attributes [nitpick_simp]};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    77
val simp_attrs = @{attributes [simp]};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    78
val transfer_rule_attrs = @{attributes [transfer_rule]};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    79
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    80
val unfold_id_thms1 =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    81
  map (fn thm => thm RS eq_reflection) @{thms id_bnf_o o_id_bnf id_apply o_apply} @
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    82
  @{thms fst_def[abs_def, symmetric] snd_def[abs_def, symmetric]};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    83
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    84
fun unfold_id_bnf_etc lthy =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    85
  let val thy = Proof_Context.theory_of lthy in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    86
    Raw_Simplifier.rewrite_term thy unfold_id_thms1 []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    87
    #> Raw_Simplifier.rewrite_term thy @{thms BNF_Composition.id_bnf_def} []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    88
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    89
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    90
fun unexpected_corec_call ctxt eqns t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    91
  error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    92
fun unsupported_case_around_corec_call ctxt eqns t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    93
  error_at ctxt eqns ("Unsupported corecursive call under case expression " ^
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    94
    quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    95
    quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    96
    " with  discriminators and selectors to circumvent this limitation.)");
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    97
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    98
datatype corec_option =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
    99
  Plugins_Option of Proof.context -> Plugin_Name.filter |
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   100
  Friend_Option |
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   101
  Transfer_Option;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   102
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   103
val corec_option_parser = Parse.group (K "option")
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   104
  (Plugin_Name.parse_filter >> Plugins_Option
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   105
   || Parse.reserved "friend" >> K Friend_Option
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   106
   || Parse.reserved "transfer" >> K Transfer_Option);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   107
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   108
type codatatype_extra =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   109
  {case_dtor: thm,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   110
   case_trivial: thm,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   111
   abs_rep_transfers: thm list};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   112
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   113
fun morph_codatatype_extra phi ({case_dtor, case_trivial, abs_rep_transfers} : codatatype_extra) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   114
  {case_dtor = Morphism.thm phi case_dtor, case_trivial = Morphism.thm phi case_trivial,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   115
   abs_rep_transfers = map (Morphism.thm phi) abs_rep_transfers};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   116
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   117
val transfer_codatatype_extra = morph_codatatype_extra o Morphism.transfer_morphism;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   118
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   119
type coinduct_extra =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   120
  {coinduct: thm,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   121
   coinduct_attrs: Token.src list,
62743
f9a65b48f5e2 more natural order for 'cong_intros'
blanchet
parents: 62741
diff changeset
   122
   cong_intro_pairs: (string * thm) list};
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   123
62743
f9a65b48f5e2 more natural order for 'cong_intros'
blanchet
parents: 62741
diff changeset
   124
fun morph_coinduct_extra phi ({coinduct, coinduct_attrs, cong_intro_pairs} : coinduct_extra) =
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   125
  {coinduct = Morphism.thm phi coinduct, coinduct_attrs = coinduct_attrs,
62743
f9a65b48f5e2 more natural order for 'cong_intros'
blanchet
parents: 62741
diff changeset
   126
   cong_intro_pairs = map (apsnd (Morphism.thm phi)) cong_intro_pairs};
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   127
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   128
val transfer_coinduct_extra = morph_coinduct_extra o Morphism.transfer_morphism;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   129
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   130
type friend_extra =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   131
  {eq_algrhos: thm list,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   132
   algrho_eqs: thm list};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   133
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   134
val empty_friend_extra = {eq_algrhos = [], algrho_eqs = []};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   135
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   136
fun merge_friend_extras ({eq_algrhos = eq_algrhos1, algrho_eqs = algrho_eqs1},
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   137
    {eq_algrhos = eq_algrhos2, algrho_eqs = algrho_eqs2}) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   138
  {eq_algrhos = union Thm.eq_thm_prop eq_algrhos1 eq_algrhos2,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   139
   algrho_eqs = union Thm.eq_thm_prop algrho_eqs1 algrho_eqs2};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   140
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   141
type corec_sugar_data =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   142
  codatatype_extra Symtab.table * coinduct_extra Symtab.table * friend_extra Symtab.table;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   143
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   144
structure Data = Generic_Data
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   145
(
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   146
  type T = corec_sugar_data;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   147
  val empty = (Symtab.empty, Symtab.empty, Symtab.empty);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   148
  val extend = I;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   149
  fun merge data : T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   150
    (Symtab.merge (K true) (apply2 #1 data), Symtab.merge (K true) (apply2 #2 data),
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   151
     Symtab.join (K merge_friend_extras) (apply2 #3 data));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   152
);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   153
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   154
fun register_codatatype_extra fpT_name extra =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   155
  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   156
    Data.map (@{apply 3(1)} (Symtab.update (fpT_name, morph_codatatype_extra phi extra))));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   157
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   158
fun codatatype_extra_of ctxt =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   159
  Symtab.lookup (#1 (Data.get (Context.Proof ctxt)))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   160
  #> Option.map (transfer_codatatype_extra (Proof_Context.theory_of ctxt));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   161
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   162
fun all_codatatype_extras_of ctxt =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   163
  Symtab.dest (#1 (Data.get (Context.Proof ctxt)));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   164
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   165
fun register_coinduct_extra fpT_name extra =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   166
  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   167
    Data.map (@{apply 3(2)} (Symtab.update (fpT_name, morph_coinduct_extra phi extra))));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   168
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   169
fun coinduct_extra_of ctxt =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   170
  Symtab.lookup (#2 (Data.get (Context.Proof ctxt)))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   171
  #> Option.map (transfer_coinduct_extra (Proof_Context.theory_of ctxt));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   172
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   173
fun register_friend_extra fun_name eq_algrho algrho_eq =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   174
  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   175
    Data.map (@{apply 3(3)} (Symtab.map_default (fun_name, empty_friend_extra)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   176
      (fn {eq_algrhos, algrho_eqs} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   177
        {eq_algrhos = Morphism.thm phi eq_algrho :: eq_algrhos,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   178
         algrho_eqs = Morphism.thm phi algrho_eq :: algrho_eqs}))));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   179
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   180
fun all_friend_extras_of ctxt =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   181
  Symtab.dest (#3 (Data.get (Context.Proof ctxt)));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   182
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   183
fun coinduct_extras_of_generic context =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   184
  corec_infos_of_generic context
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   185
  #> map (#corecUU #> dest_Const #> fst #> Symtab.lookup (#2 (Data.get context)) #> the
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   186
    #> transfer_coinduct_extra (Context.theory_of context));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   187
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   188
fun get_coinduct_uptos fpT_name context =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   189
  coinduct_extras_of_generic context fpT_name |> map #coinduct;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   190
fun get_cong_all_intros fpT_name context =
62743
f9a65b48f5e2 more natural order for 'cong_intros'
blanchet
parents: 62741
diff changeset
   191
  coinduct_extras_of_generic context fpT_name |> maps (#cong_intro_pairs #> map snd);
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   192
fun get_cong_intros fpT_name name context =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   193
  coinduct_extras_of_generic context fpT_name
62743
f9a65b48f5e2 more natural order for 'cong_intros'
blanchet
parents: 62741
diff changeset
   194
  |> map_filter (#cong_intro_pairs #> (fn ps => AList.lookup (op =) ps name));
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   195
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   196
fun ctr_names_of_fp_name lthy fpT_name =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   197
  fpT_name |> fp_sugar_of lthy |> the |> #fp_ctr_sugar |> #ctr_sugar |> #ctrs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   198
  |> map (Long_Name.base_name o name_of_ctr);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   199
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   200
fun register_coinduct_dynamic_base fpT_name lthy =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   201
  let val fp_b = Binding.name (Long_Name.base_name fpT_name) in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   202
    lthy
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   203
    |> fold Local_Theory.add_thms_dynamic
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   204
      ((mk_fp_binding fp_b coinduct_uptoN, get_coinduct_uptos fpT_name) ::
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   205
        map (fn N =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   206
          let val N = cong_N ^ N in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   207
            (mk_fp_binding fp_b N, get_cong_intros fpT_name N)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   208
          end)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   209
        ([baseN, reflN, symN, transN] @ ctr_names_of_fp_name lthy fpT_name))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   210
    |> Local_Theory.add_thms_dynamic
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   211
      (mk_fp_binding fp_b cong_introsN, get_cong_all_intros fpT_name)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   212
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   213
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   214
fun register_coinduct_dynamic_friend fpT_name friend_name =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   215
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   216
    val fp_b = Binding.name (Long_Name.base_name fpT_name);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   217
    val friend_base_name = cong_N ^ Long_Name.base_name friend_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   218
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   219
    Local_Theory.add_thms_dynamic
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   220
      (mk_fp_binding fp_b friend_base_name, get_cong_intros fpT_name friend_base_name)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   221
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   222
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   223
fun derive_case_dtor ctxt fpT_name =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   224
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   225
    val thy = Proof_Context.theory_of ctxt;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   226
62699
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   227
    val SOME ({fp_res_index, fp_res = {dtors = dtors0, dtor_ctors, ...},
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   228
        absT_info = {rep = rep0, abs_inverse, ...},
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   229
        fp_ctr_sugar = {ctr_defs, ctr_sugar = {casex, exhaust, case_thms, ...}, ...}, ...}) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   230
      fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   231
62699
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   232
    val (f_Ts, Type (_, [fpT as Type (_, As), _])) = strip_fun_type (fastype_of casex);
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   233
    val x_Tss = map binder_types f_Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   234
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   235
    val (((u, fs), xss), _) = ctxt
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   236
      |> yield_singleton (mk_Frees "y") fpT
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   237
      ||>> mk_Frees "f" f_Ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   238
      ||>> mk_Freess "x" x_Tss;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   239
62699
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   240
    val dtor0 = nth dtors0 fp_res_index;
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   241
    val dtor = mk_dtor As dtor0;
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   242
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   243
    val u' = dtor $ u;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   244
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   245
    val absT = fastype_of u';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   246
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   247
    val rep = mk_rep absT rep0;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   248
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   249
    val goal = mk_Trueprop_eq (list_comb (casex, fs) $ u,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   250
        mk_case_absumprod absT rep fs xss xss $ u')
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   251
      |> Raw_Simplifier.rewrite_term thy @{thms comp_def[THEN eq_reflection]} [];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   252
    val vars = map (fst o dest_Free) (u :: fs);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   253
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   254
    val dtor_ctor = nth dtor_ctors fp_res_index;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   255
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   256
    Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   257
      mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust case_thms)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   258
    |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   259
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   260
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   261
fun derive_case_trivial ctxt fpT_name =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   262
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   263
    val SOME {casex, exhaust, case_thms, ...} = ctr_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   264
62746
blanchet
parents: 62743
diff changeset
   265
    val Type (_, As0) = domain_type (body_fun_type (fastype_of casex));
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   266
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   267
    val (As, _) = ctxt
62699
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   268
      |> mk_TFrees' (map Type.sort_of_atyp As0);
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   269
    val fpT = Type (fpT_name, As);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   270
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   271
    val (var_name, ()) = singleton (Variable.variant_frees ctxt []) ("x", ());
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   272
    val var = Free (var_name, fpT);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   273
    val goal = mk_Trueprop_eq (expand_to_ctr_term ctxt fpT var, var);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   274
62727
blanchet
parents: 62724
diff changeset
   275
    val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt var)] exhaust;
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   276
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   277
    Goal.prove_sorry ctxt [var_name] [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   278
      HEADGOAL (rtac ctxt exhaust') THEN ALLGOALS (hyp_subst_tac ctxt) THEN
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   279
      unfold_thms_tac ctxt case_thms THEN ALLGOALS (rtac ctxt refl))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   280
    |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   281
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   282
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   283
fun mk_abs_rep_transfers ctxt fpT_name =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   284
  [mk_abs_transfer ctxt fpT_name, mk_rep_transfer ctxt fpT_name]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   285
  handle Fail _ => [];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   286
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   287
fun set_transfer_rule_attrs thms =
63352
4eaf35781b23 tuned signature;
wenzelm
parents: 63285
diff changeset
   288
  snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])];
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   289
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   290
fun ensure_codatatype_extra fpT_name ctxt =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   291
  (case codatatype_extra_of ctxt fpT_name of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   292
    NONE =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   293
    let val abs_rep_transfers = mk_abs_rep_transfers ctxt fpT_name in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   294
      ctxt
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   295
      |> register_codatatype_extra fpT_name
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   296
        {case_dtor = derive_case_dtor ctxt fpT_name,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   297
         case_trivial = derive_case_trivial ctxt fpT_name,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   298
         abs_rep_transfers = abs_rep_transfers}
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   299
      |> set_transfer_rule_attrs abs_rep_transfers
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   300
    end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   301
  | SOME {abs_rep_transfers, ...} => ctxt |> set_transfer_rule_attrs abs_rep_transfers);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   302
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   303
fun setup_base fpT_name =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   304
  register_coinduct_dynamic_base fpT_name
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   305
  #> ensure_codatatype_extra fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   306
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   307
fun is_set ctxt (const_name, T) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   308
  (case T of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   309
    Type (@{type_name fun}, [Type (fpT_name, _), Type (@{type_name set}, [_])]) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   310
    (case bnf_of ctxt fpT_name of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   311
      SOME bnf => exists (fn Const (s, _) => s = const_name | _ => false) (sets_of_bnf bnf)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   312
    | NONE => false)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   313
  | _ => false);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   314
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   315
fun case_eq_if_thms_of_term ctxt t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   316
  let val ctr_sugars = map_filter (ctr_sugar_of_case ctxt o fst) (Term.add_consts t []) in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   317
    maps #case_eq_ifs ctr_sugars
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   318
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   319
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   320
fun all_algrho_eqs_of ctxt =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   321
  maps (#algrho_eqs o snd) (all_friend_extras_of ctxt);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   322
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   323
fun derive_code ctxt inner_fp_simps goal
62746
blanchet
parents: 62743
diff changeset
   324
    {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs, corecUU_thm, ...} fun_t
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   325
    fun_def =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   326
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   327
    val fun_T = fastype_of fun_t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   328
    val (arg_Ts, Type (fpT_name, _)) = strip_type fun_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   329
    val num_args = length arg_Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   330
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   331
    val SOME {pre_bnf, fp_bnf, absT_info, fp_nesting_bnfs, live_nesting_bnfs, fp_ctr_sugar, ...} =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   332
      fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   333
    val SOME {case_trivial, ...} = codatatype_extra_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   334
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   335
    val ctr_sugar = #ctr_sugar fp_ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   336
    val pre_map_def = map_def_of_bnf pre_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   337
    val abs_inverse = #abs_inverse absT_info;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   338
    val ctr_defs = #ctr_defs fp_ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   339
    val case_eq_ifs = #case_eq_ifs ctr_sugar @ case_eq_if_thms_of_term ctxt goal;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   340
    val all_sig_map_thms = maps (#map_thms o #fp_bnf_sugar) sig_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   341
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   342
    val fp_map_ident = map_ident_of_bnf fp_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   343
    val fpsig_nesting_bnfs = fp_nesting_bnfs @ maps #live_nesting_bnfs sig_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   344
    val fpsig_nesting_T_names = map (fst o dest_Type o T_of_bnf) fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   345
    val fpsig_nesting_fp_sugars = map_filter (fp_sugar_of ctxt) fpsig_nesting_T_names;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   346
    val fpsig_nesting_fp_bnf_sugars = map #fp_bnf_sugar fpsig_nesting_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   347
    val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   348
    val ssig_bnf = #fp_bnf ssig_fp_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   349
    val ssig_map = map_of_bnf ssig_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   350
    val fpsig_nesting_maps = map map_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   351
    val fpsig_nesting_map_ident0s = map map_ident0_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   352
    val fpsig_nesting_map_comps = map map_comp_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   353
    val fpsig_nesting_map_thms = maps #map_thms fpsig_nesting_fp_bnf_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   354
    val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   355
    val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   356
    val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   357
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   358
    Variable.add_free_names ctxt goal []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   359
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   360
      mk_code_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   361
        fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   362
        live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs corecUU_thm
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   363
        all_sig_map_thms ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   364
        inner_fp_simps fun_def))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   365
    |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   366
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   367
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   368
fun derive_unique ctxt phi code_goal
62746
blanchet
parents: 62743
diff changeset
   369
    {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs, corecUU_unique, ...} fpT_name
blanchet
parents: 62743
diff changeset
   370
    eq_corecUU =
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   371
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   372
    val SOME {pre_bnf, fp_bnf, absT_info, fp_nesting_bnfs, live_nesting_bnfs, fp_ctr_sugar, ...} =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   373
      fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   374
    val SOME {case_trivial, ...} = codatatype_extra_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   375
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   376
    val ctr_sugar = #ctr_sugar fp_ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   377
    val pre_map_def = map_def_of_bnf pre_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   378
    val abs_inverse = #abs_inverse absT_info;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   379
    val ctr_defs = #ctr_defs fp_ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   380
    val case_eq_ifs = #case_eq_ifs ctr_sugar @ case_eq_if_thms_of_term ctxt code_goal;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   381
    val all_sig_map_thms = maps (#map_thms o #fp_bnf_sugar) sig_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   382
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   383
    val fp_map_ident = map_ident_of_bnf fp_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   384
    val fpsig_nesting_bnfs = fp_nesting_bnfs @ maps #live_nesting_bnfs sig_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   385
    val fpsig_nesting_T_names = map (fst o dest_Type o T_of_bnf) fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   386
    val fpsig_nesting_fp_sugars = map_filter (fp_sugar_of ctxt) fpsig_nesting_T_names;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   387
    val fpsig_nesting_fp_bnf_sugars = map #fp_bnf_sugar fpsig_nesting_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   388
    val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   389
    val ssig_bnf = #fp_bnf ssig_fp_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   390
    val ssig_map = map_of_bnf ssig_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   391
    val fpsig_nesting_maps = map map_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   392
    val fpsig_nesting_map_ident0s = map map_ident0_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   393
    val fpsig_nesting_map_comps = map map_comp_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   394
    val fpsig_nesting_map_thms = maps #map_thms fpsig_nesting_fp_bnf_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   395
    val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   396
    val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   397
    val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   398
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   399
    val @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ rhs) = code_goal;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   400
    val (fun_t, args) = strip_comb lhs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   401
    val closed_rhs = fold_rev lambda args rhs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   402
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   403
    val fun_T = fastype_of fun_t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   404
    val num_args = num_binder_types fun_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   405
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   406
    val f = Free (singleton (Variable.variant_frees ctxt []) ("f", fun_T));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   407
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   408
    val is_self_call = curry (op aconv) fun_t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   409
    val has_self_call = exists_subterm is_self_call;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   410
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   411
    fun fify args (t $ u) = fify (u :: args) t $ fify [] u
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   412
      | fify _ (Abs (s, T, t)) = Abs (s, T, fify [] t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   413
      | fify args t = if t = fun_t andalso not (exists has_self_call args) then f else t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   414
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   415
    val goal = Logic.mk_implies (mk_Trueprop_eq (f, fify [] closed_rhs), mk_Trueprop_eq (f, fun_t))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   416
      |> Morphism.term phi;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   417
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   418
    Goal.prove_sorry ctxt [fst (dest_Free f)] [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   419
      mk_unique_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   420
        fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   421
        live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_map_thms
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   422
        ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps corecUU_unique
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   423
        eq_corecUU)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   424
    |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   425
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   426
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   427
fun derive_last_disc ctxt fcT_name =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   428
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   429
    val SOME {T = fcT, discs, exhaust, disc_thmss, ...} = ctr_sugar_of ctxt fcT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   430
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   431
    val (u, _) = ctxt
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   432
      |> yield_singleton (mk_Frees "x") fcT;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   433
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   434
    val udiscs = map (rapp u) discs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   435
    val (not_udiscs, last_udisc) = split_last udiscs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   436
      |>> map HOLogic.mk_not;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   437
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   438
    val goal = mk_Trueprop_eq (last_udisc, foldr1 HOLogic.mk_conj not_udiscs);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   439
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   440
    Goal.prove_sorry ctxt [fst (dest_Free u)] [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   441
      mk_last_disc_tac ctxt u exhaust (flat disc_thmss))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   442
    |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   443
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   444
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   445
fun derive_eq_algrho ctxt {sig_fp_sugars, ssig_fp_sugar, eval, eval_simps, all_algLam_algs,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   446
      corecUU_unique, ...}
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   447
    ({algrho = algrho0, dtor_algrho, ...} : friend_info) fun_t k_T code_goal const_transfers rho_def
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   448
    eq_corecUU =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   449
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   450
    val fun_T = fastype_of fun_t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   451
    val (arg_Ts, Type (fpT_name, Ts)) = strip_type fun_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   452
    val num_args = length arg_Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   453
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   454
    val SOME {fp_res_index, fp_res, pre_bnf, fp_bnf, absT_info, fp_nesting_bnfs, live_nesting_bnfs,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   455
        fp_ctr_sugar, ...} =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   456
      fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   457
    val SOME {case_dtor, ...} = codatatype_extra_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   458
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   459
    val fp_nesting_Ts = map T_of_bnf fp_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   460
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   461
    fun is_nullary_disc_def (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   462
          $ (Const (@{const_name HOL.eq}, _) $ _ $ _))) = true
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   463
      | is_nullary_disc_def (Const (@{const_name Pure.eq}, _) $ _
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   464
          $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   465
      | is_nullary_disc_def _ = false;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   466
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   467
    val dtor_ctor = nth (#dtor_ctors fp_res) fp_res_index;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   468
    val ctor_iff_dtor = #ctor_iff_dtor fp_ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   469
    val ctr_sugar = #ctr_sugar fp_ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   470
    val pre_map_def = map_def_of_bnf pre_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   471
    val abs_inverse = #abs_inverse absT_info;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   472
    val ctr_defs = #ctr_defs fp_ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   473
    val nullary_disc_defs = filter (is_nullary_disc_def o Thm.prop_of) (#disc_defs ctr_sugar);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   474
    val disc_sel_eq_cases = #disc_eq_cases ctr_sugar @ #sel_defs ctr_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   475
    val case_eq_ifs = #case_eq_ifs ctr_sugar @ case_eq_if_thms_of_term ctxt code_goal;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   476
    val all_sig_map_thms = maps (#map_thms o #fp_bnf_sugar) sig_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   477
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   478
    fun add_tnameT (Type (s, Ts)) = insert (op =) s #> fold add_tnameT Ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   479
      | add_tnameT _ = I;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   480
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   481
    fun map_disc_sels'_of s =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   482
      (case fp_sugar_of ctxt s of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   483
        SOME {fp_bnf_sugar = {map_disc_iffs, map_selss, ...}, ...} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   484
        let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   485
          val map_selss' =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   486
            if length map_selss <= 1 then map_selss
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   487
            else map (map (unfold_thms ctxt (no_refl [derive_last_disc ctxt s]))) map_selss;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   488
        in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   489
          map_disc_iffs @ flat map_selss'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   490
        end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   491
      | NONE => []);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   492
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   493
    fun mk_const_pointful_natural const_transfer =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   494
      SOME (mk_pointful_natural_from_transfer ctxt const_transfer)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   495
      handle UNNATURAL () => NONE;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   496
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   497
    val const_pointful_natural_opts = map mk_const_pointful_natural const_transfers;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   498
    val const_pointful_naturals = map_filter I const_pointful_natural_opts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   499
    val fp_nesting_k_T_names = fold add_tnameT (k_T :: fp_nesting_Ts) [];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   500
    val fp_nesting_k_map_disc_sels' = maps map_disc_sels'_of fp_nesting_k_T_names;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   501
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   502
    val fp_map_ident = map_ident_of_bnf fp_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   503
    val fpsig_nesting_bnfs = fp_nesting_bnfs @ maps #live_nesting_bnfs sig_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   504
    val fpsig_nesting_T_names = map (fst o dest_Type o T_of_bnf) fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   505
    val fpsig_nesting_fp_sugars = map_filter (fp_sugar_of ctxt) fpsig_nesting_T_names;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   506
    val fpsig_nesting_fp_bnf_sugars = map #fp_bnf_sugar fpsig_nesting_fp_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   507
    val ssig_fp_bnf_sugar = #fp_bnf_sugar ssig_fp_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   508
    val ssig_bnf = #fp_bnf ssig_fp_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   509
    val ssig_map = map_of_bnf ssig_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   510
    val fpsig_nesting_maps = map map_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   511
    val fpsig_nesting_map_ident0s = map map_ident0_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   512
    val fpsig_nesting_map_comps = map map_comp_of_bnf fpsig_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   513
    val fpsig_nesting_map_thms = maps #map_thms fpsig_nesting_fp_bnf_sugars;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   514
    val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   515
    val ssig_map_thms = #map_thms ssig_fp_bnf_sugar;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   516
    val all_algLam_alg_pointfuls = map (mk_pointful ctxt) all_algLam_algs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   517
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   518
    val ctor = nth (#ctors fp_res) fp_res_index;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   519
    val abs = #abs absT_info;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   520
    val rep = #rep absT_info;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   521
    val algrho = mk_ctr Ts algrho0;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   522
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   523
    val goal = mk_Trueprop_eq (fun_t, abs_curried_balanced arg_Ts algrho);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   524
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   525
    fun const_of_transfer thm =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   526
      (case Thm.prop_of thm of @{const Trueprop} $ (_ $ cst $ _) => cst);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   527
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   528
    val eq_algrho =
62729
b0bf94ccc59f avoid 'prove_sorry' for unreliable tactics
blanchet
parents: 62728
diff changeset
   529
      Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   530
        mk_eq_algrho_tac ctxt fpsig_nesting_maps abs rep ctor ssig_map eval pre_map_def abs_inverse
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   531
          fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   532
          live_nesting_map_ident0s fp_map_ident dtor_ctor ctor_iff_dtor ctr_defs nullary_disc_defs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   533
          disc_sel_eq_cases case_dtor case_eq_ifs const_pointful_naturals
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   534
          fp_nesting_k_map_disc_sels' rho_def dtor_algrho corecUU_unique eq_corecUU all_sig_map_thms
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   535
          ssig_map_thms all_algLam_alg_pointfuls (all_algrho_eqs_of ctxt) eval_simps)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   536
      |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   537
      handle e as ERROR _ =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   538
        (case filter (is_none o snd) (const_transfers ~~ const_pointful_natural_opts) of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   539
          [] => Exn.reraise e
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   540
        | thm_nones =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   541
          error ("Failed to state naturality property for " ^
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   542
            commas (map (Syntax.string_of_term ctxt o const_of_transfer o fst) thm_nones)));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   543
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   544
    val algrho_eq = eq_algrho RS (mk_curry_uncurryN_balanced ctxt num_args RS iffD2) RS sym;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   545
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   546
    (eq_algrho, algrho_eq)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   547
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   548
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   549
fun prime_rho_transfer_goal ctxt fpT_name rho_def goal =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   550
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   551
    val thy = Proof_Context.theory_of ctxt;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   552
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   553
    val SOME {pre_bnf, ...} = fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   554
    val SOME {abs_rep_transfers, ...} = codatatype_extra_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   555
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   556
    val simps = rel_def_of_bnf pre_bnf :: rho_transfer_simps;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   557
    val fold_rho = unfold_thms ctxt [rho_def RS @{thm symmetric}];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   558
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   559
    fun derive_unprimed rho_transfer' =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   560
      Variable.add_free_names ctxt goal []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   561
      |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   562
        unfold_thms_tac ctxt simps THEN HEADGOAL (rtac ctxt rho_transfer')))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   563
      |> Thm.close_derivation;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   564
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   565
    val goal' = Raw_Simplifier.rewrite_term thy simps [] goal;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   566
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   567
    if null abs_rep_transfers then (goal', derive_unprimed #> fold_rho)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   568
    else (goal, fold_rho)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   569
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   570
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   571
fun derive_rho_transfer_folded ctxt fpT_name const_transfers rho_def goal =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   572
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   573
    val SOME {pre_bnf, ...} = fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   574
    val SOME {abs_rep_transfers, ...} = codatatype_extra_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   575
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   576
    Variable.add_free_names ctxt goal []
62729
b0bf94ccc59f avoid 'prove_sorry' for unreliable tactics
blanchet
parents: 62728
diff changeset
   577
    |> (fn vars => Goal.prove (*no sorry*) ctxt vars [] goal (fn {context = ctxt, prems = _} =>
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   578
      mk_rho_transfer_tac ctxt (null abs_rep_transfers) (rel_def_of_bnf pre_bnf)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   579
      const_transfers))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   580
    |> unfold_thms ctxt [rho_def RS @{thm symmetric}]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   581
    |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   582
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   583
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   584
fun mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong alg =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   585
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   586
    val xy_Ts = binder_types (fastype_of alg);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   587
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   588
    val ((xs, ys), _) = ctxt
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   589
      |> mk_Frees "x" xy_Ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   590
      ||>> mk_Frees "y" xy_Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   591
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   592
    fun mk_prem xy_T x y =
62746
blanchet
parents: 62743
diff changeset
   593
      build_rel [] ctxt [fpT] (fn (T, _) => if T = fpT then Rcong else HOLogic.eq_const T)
blanchet
parents: 62743
diff changeset
   594
        (xy_T, xy_T) $ x $ y;
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   595
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   596
    val prems = @{map 3} mk_prem xy_Ts xs ys;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   597
    val concl = Rcong $ list_comb (alg, xs) $ list_comb (alg, ys);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   598
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   599
    Logic.list_implies (map HOLogic.mk_Trueprop prems, HOLogic.mk_Trueprop concl)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   600
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   601
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   602
fun derive_cong_ctr_intros ctxt cong_ctor_intro =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   603
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   604
    val @{const Pure.imp} $ _ $ (@{const Trueprop} $ ((Rcong as _ $ _) $ _ $ (ctor $ _))) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   605
      Thm.prop_of cong_ctor_intro;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   606
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   607
    val fpT as Type (fpT_name, fp_argTs) = range_type (fastype_of ctor);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   608
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   609
    val SOME {pre_bnf, absT_info = {abs_inverse, ...},
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   610
        fp_ctr_sugar = {ctr_defs, ctr_sugar = {ctrs = ctrs0, ...}, ...}, ...} =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   611
      fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   612
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   613
    val ctrs = map (mk_ctr fp_argTs) ctrs0;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   614
    val pre_rel_def = rel_def_of_bnf pre_bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   615
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   616
    fun prove ctr_def goal =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   617
      Variable.add_free_names ctxt goal []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   618
      |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   619
        mk_cong_intro_ctr_or_friend_tac ctxt ctr_def [pre_rel_def, abs_inverse] cong_ctor_intro))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   620
      |> Thm.close_derivation;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   621
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   622
    val goals = map (mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong) ctrs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   623
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   624
    map2 prove ctr_defs goals
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   625
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   626
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   627
fun derive_cong_friend_intro ctxt cong_algrho_intro =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   628
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   629
    val @{const Pure.imp} $ _ $ (@{const Trueprop} $ ((Rcong as _ $ _) $ _
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   630
        $ ((algrho as Const (algrho_name, _)) $ _))) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   631
      Thm.prop_of cong_algrho_intro;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   632
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   633
    val fpT as Type (_, fp_argTs) = range_type (fastype_of algrho);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   634
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   635
    fun has_algrho (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ rhs)) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   636
      fst (dest_Const (head_of (strip_abs_body rhs))) = algrho_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   637
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   638
    val eq_algrho :: _ =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   639
      maps (filter (has_algrho o Thm.prop_of) o #eq_algrhos o snd) (all_friend_extras_of ctxt);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   640
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   641
    val @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ friend0 $ _) = Thm.prop_of eq_algrho;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   642
    val friend = mk_ctr fp_argTs friend0;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   643
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   644
    val goal = mk_cong_intro_ctr_or_friend_goal ctxt fpT Rcong friend;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   645
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   646
    Variable.add_free_names ctxt goal []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   647
    |> (fn vars => Goal.prove_sorry ctxt vars [] goal (fn {context = ctxt, prems = _} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   648
      mk_cong_intro_ctr_or_friend_tac ctxt eq_algrho [] cong_algrho_intro))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   649
    |> Thm.close_derivation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   650
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   651
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   652
fun derive_cong_intros lthy ctr_names friend_names
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   653
    ({cong_base, cong_refl, cong_sym, cong_trans, cong_alg_intros, ...} : dtor_coinduct_info) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   654
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   655
    val cong_ctor_intro :: cong_algrho_intros = rev cong_alg_intros;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   656
    val names = map (prefix cong_N) ([baseN, reflN, symN, transN] @ ctr_names @ friend_names);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   657
    val thms = [cong_base, cong_refl, cong_sym, cong_trans] @
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   658
      derive_cong_ctr_intros lthy cong_ctor_intro @
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   659
      map (derive_cong_friend_intro lthy) cong_algrho_intros;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   660
  in
62743
f9a65b48f5e2 more natural order for 'cong_intros'
blanchet
parents: 62741
diff changeset
   661
    names ~~ thms
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   662
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   663
62699
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   664
fun derive_coinduct ctxt (fpT as Type (fpT_name, fpT_args)) dtor_coinduct =
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   665
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   666
    val thy = Proof_Context.theory_of ctxt;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   667
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   668
    val @{const Pure.imp} $ (@{const Trueprop} $ (_ $ Abs (_, _, _ $
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   669
        Abs (_, _, @{const implies} $ _ $ (_ $ (cong0 $ _) $ _ $ _))))) $ _ =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   670
      Thm.prop_of dtor_coinduct;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   671
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   672
    val SOME {X as TVar ((X_s, _), _), fp_res = {dtor_ctors, ...}, pre_bnf,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   673
        absT_info = {abs_inverse, ...}, live_nesting_bnfs,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   674
        fp_ctr_sugar = {ctrXs_Tss, ctr_defs,
62699
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   675
          ctr_sugar = ctr_sugar0 as {T = Type (_, T0_args), ctrs = ctrs0, discs = discs0, ...},
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   676
            ...}, ...} =
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   677
      fp_sugar_of ctxt fpT_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   678
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   679
    val n = length ctrXs_Tss;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   680
    val ms = map length ctrXs_Tss;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   681
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   682
    val X' = TVar ((X_s, maxidx_of_typ fpT + 1), @{sort type});
62699
add334b71e16 sorted out type issue with sort constraints
blanchet
parents: 62692
diff changeset
   683
    val As_rho = tvar_subst thy T0_args fpT_args;
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   684
    val substXAT = Term.typ_subst_TVars As_rho o Tsubst X X';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   685
    val substXA = Term.subst_TVars As_rho o substT X X';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   686
    val phi = Morphism.typ_morphism "BNF" substXAT $> Morphism.term_morphism "BNF" substXA;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   687
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   688
    fun mk_applied_cong arg =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   689
      enforce_type ctxt domain_type (fastype_of arg) cong0 $ arg;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   690
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   691
    val thm = derive_coinduct_thms_for_types false mk_applied_cong [pre_bnf] dtor_coinduct
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   692
        dtor_ctors live_nesting_bnfs [fpT] [substXAT X] [map (map substXAT) ctrXs_Tss] [n]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   693
        [abs_inverse] [abs_inverse] I [ctr_defs] [morph_ctr_sugar phi ctr_sugar0] ctxt
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   694
      |> map snd |> the_single;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   695
    val (attrs, _) = mk_coinduct_attrs [fpT] [ctrs0] [discs0] [ms];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   696
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   697
    (thm, attrs)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   698
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   699
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   700
type explore_parameters =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   701
  {bound_Us: typ list,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   702
   bound_Ts: typ list,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   703
   U: typ,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   704
   T: typ};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   705
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   706
fun update_UT {bound_Us, bound_Ts, ...} U T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   707
  {bound_Us = bound_Us, bound_Ts = bound_Ts, U = U, T = T};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   708
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   709
fun explore_nested lthy explore {bound_Us, bound_Ts, U, T} t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   710
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   711
    fun build_simple (T, U) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   712
      if T = U then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   713
        @{term "%y. y"}
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   714
      else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   715
        Bound 0
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   716
        |> explore {bound_Us = T :: bound_Us, bound_Ts = T :: bound_Ts, U = U, T = T}
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   717
        |> (fn t => Abs (Name.uu, T, t));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   718
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   719
    betapply (build_map lthy [] build_simple (T, U), t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   720
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   721
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   722
fun add_boundvar t = betapply (incr_boundvars 1 t, Bound 0);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   723
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   724
fun explore_fun (arg_U :: arg_Us) explore {bound_Us, bound_Ts, U, T} t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   725
    let val arg_name = the_default Name.uu (try (fn (Abs (s, _, _)) => s) t) in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   726
      add_boundvar t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   727
      |> explore_fun arg_Us explore
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   728
        {bound_Us = arg_U :: bound_Us, bound_Ts = domain_type T :: bound_Ts, U = range_type U,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   729
         T = range_type T}
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   730
      |> (fn t => Abs (arg_name, arg_U, t))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   731
    end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   732
  | explore_fun [] explore params t = explore params t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   733
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   734
fun massage_fun explore (params as {T, U, ...}) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   735
  if can dest_funT T then explore_fun [domain_type U] explore params else explore params;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   736
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   737
fun massage_star massages explore =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   738
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   739
    fun after_massage massages' t params t' =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   740
      if t aconv t' then massage_any massages' params t else massage_any massages params t'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   741
    and massage_any [] params t = explore params t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   742
      | massage_any (massage :: massages') params t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   743
        massage (after_massage massages' t) params t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   744
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   745
    massage_any massages
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   746
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   747
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   748
fun massage_let explore params t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   749
  (case strip_comb t of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   750
    (Const (@{const_name Let}, _), [_, _]) => unfold_lets_splits t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   751
  | _ => t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   752
  |> explore params;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   753
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   754
fun check_corec_equation ctxt fun_frees (lhs, rhs) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   755
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   756
    val (fun_t, arg_ts) = strip_comb lhs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   757
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   758
    fun check_fun_name () =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   759
      null fun_frees orelse member (op aconv) fun_frees fun_t orelse
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   760
      error (quote (Syntax.string_of_term ctxt fun_t) ^
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   761
        " is not the function currently being defined");
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   762
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   763
    fun check_args_are_vars () =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   764
      let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   765
        fun is_ok_Free_or_Var (Free (s, _)) = not (String.isSuffix inner_fp_suffix s)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   766
          | is_ok_Free_or_Var (Var _) = true
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   767
          | is_ok_Free_or_Var _ = false;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   768
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   769
        fun is_valid arg =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   770
          (is_ok_Free_or_Var arg andalso not (member (op aconv) fun_frees arg)) orelse
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   771
          error ("Argument " ^ quote (Syntax.string_of_term ctxt arg) ^ " is not free");
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   772
      in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   773
        forall is_valid arg_ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   774
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   775
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   776
    fun check_no_duplicate_arg () =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   777
      (case duplicates (op =) arg_ts of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   778
        [] => ()
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   779
      | arg :: _ => error ("Repeated argument: " ^ quote (Syntax.string_of_term ctxt arg)));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   780
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   781
    fun check_no_other_frees () =
62724
2b317e347b9b more reliable check for rhs variables
blanchet
parents: 62699
diff changeset
   782
      (case Term.add_frees rhs [] |> map Free |> subtract (op =) (fun_frees @ arg_ts)
2b317e347b9b more reliable check for rhs variables
blanchet
parents: 62699
diff changeset
   783
          |> filter_out (Variable.is_fixed ctxt o fst o dest_Free) of
2b317e347b9b more reliable check for rhs variables
blanchet
parents: 62699
diff changeset
   784
        [] => ()
2b317e347b9b more reliable check for rhs variables
blanchet
parents: 62699
diff changeset
   785
      | Free (s, _) :: _ => error ("Extra variable on right-hand side: " ^ quote s));
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   786
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   787
    check_no_duplicate_arg ();
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   788
    check_fun_name ();
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   789
    check_args_are_vars ();
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   790
    check_no_other_frees ()
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   791
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   792
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   793
fun parse_corec_equation ctxt fun_frees eq =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   794
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   795
    val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (drop_all eq))
63188
38d6aabec460 more flexible parsing (towards type class support)
blanchet
parents: 63182
diff changeset
   796
      handle TERM _ => error "Expected HOL equation";
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   797
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   798
    val _ = check_corec_equation ctxt fun_frees (lhs, rhs);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   799
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   800
    val (fun_t, arg_ts) = strip_comb lhs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   801
    val (arg_Ts, _) = strip_type (fastype_of fun_t);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   802
    val added_Ts = drop (length arg_ts) arg_Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   803
    val free_names = mk_names (length added_Ts) "x" ~~ added_Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   804
    val free_args = Variable.variant_frees ctxt [rhs, lhs] free_names |> map Free;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   805
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   806
    (arg_ts @ free_args, list_comb (rhs, free_args))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   807
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   808
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   809
fun morph_views phi (code, ctrs, discs, disc_iffs, sels) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   810
  (Morphism.term phi code, map (Morphism.term phi) ctrs, map (Morphism.term phi) discs,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   811
   map (Morphism.term phi) disc_iffs, map (Morphism.term phi) sels);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   812
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   813
fun generate_views ctxt eq fun_t (lhs_free_args, rhs) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   814
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   815
    val lhs = list_comb (fun_t, lhs_free_args);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   816
    val T as Type (T_name, Ts) = fastype_of rhs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   817
    val SOME {fp_ctr_sugar = {ctr_sugar = {ctrs = ctrs0, discs = discs0, selss = selss0, ...}, ...},
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   818
        ...} =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   819
      fp_sugar_of ctxt T_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   820
    val ctrs = map (mk_ctr Ts) ctrs0;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   821
    val discs = map (mk_disc_or_sel Ts) discs0;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   822
    val selss = map (map (mk_disc_or_sel Ts)) selss0;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   823
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   824
    val code_view = drop_all eq;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   825
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   826
    fun can_case_expand t = not (can (dest_ctr ctxt T_name) t);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   827
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   828
    fun generate_raw_views conds t raw_views =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   829
      let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   830
        fun analyse (ctr :: ctrs) (disc :: discs) ctr' =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   831
          if ctr = ctr' then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   832
            (conds, disc, ctr)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   833
          else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   834
            analyse ctrs discs ctr';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   835
      in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   836
        (analyse ctrs discs (fst (strip_comb t))) :: raw_views
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   837
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   838
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   839
    fun generate_disc_views raw_views =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   840
      if length discs = 1 then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   841
        ([], [])
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   842
      else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   843
        let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   844
          fun collect_condss_disc condss [] _ = condss
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   845
            | collect_condss_disc condss ((conds, disc', _) :: raw_views) disc =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   846
              collect_condss_disc (condss |> disc = disc' ? cons conds) raw_views disc;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   847
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   848
          val grouped_disc_views = discs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   849
            |> map (collect_condss_disc [] raw_views)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   850
            |> curry (op ~~) (map (fn disc => disc $ lhs) discs);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   851
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   852
          fun mk_disc_iff_props props [] = props
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   853
            | mk_disc_iff_props _ ((lhs, @{const HOL.True}) :: _) = [lhs]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   854
            | mk_disc_iff_props props ((lhs, rhs) :: views) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   855
              mk_disc_iff_props ((HOLogic.mk_eq (lhs, rhs)) :: props) views;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   856
        in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   857
          (grouped_disc_views
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   858
           |> map swap,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   859
           grouped_disc_views
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   860
           |> map (apsnd (s_dnf #> mk_conjs))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   861
           |> mk_disc_iff_props []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   862
           |> map (fn eq => ([[]], eq)))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   863
        end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   864
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   865
    fun generate_ctr_views raw_views =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   866
      let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   867
        fun collect_condss_ctr condss [] _ = condss
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   868
          | collect_condss_ctr condss ((conds, _, ctr') :: raw_views) ctr =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   869
            collect_condss_ctr (condss |> ctr = ctr' ? cons conds) raw_views ctr;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   870
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   871
        fun mk_ctr_eq ctr_sels ctr =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   872
          let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   873
            fun extract_arg n sel _(*bound_Ts*) fun_t arg_ts =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   874
              if ctr = fun_t then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   875
                nth arg_ts n
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   876
              else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   877
                let val t = list_comb (fun_t, arg_ts) in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   878
                  if can_case_expand t then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   879
                    sel $ t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   880
                  else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   881
                    Term.dummy_pattern (range_type (fastype_of sel))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   882
                end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   883
          in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   884
            ctr_sels
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   885
            |> map_index (uncurry extract_arg)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   886
            |> map (fn extract => massage_corec_code_rhs ctxt extract [] rhs)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   887
            |> curry list_comb ctr
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   888
            |> curry HOLogic.mk_eq lhs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   889
          end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   890
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   891
          fun remove_condss_if_alone [(_, concl)] = [([[]], concl)]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   892
            | remove_condss_if_alone views = views;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   893
      in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   894
        ctrs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   895
        |> `(map (collect_condss_ctr [] raw_views))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   896
        ||> map2 mk_ctr_eq selss
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   897
        |> op ~~
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   898
        |> filter_out (null o fst)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   899
        |> remove_condss_if_alone
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   900
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   901
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   902
    fun generate_sel_views raw_views only_one_ctr =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   903
      let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   904
        fun mk_sel_positions sel =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   905
          let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   906
            fun get_sel_position _ [] = NONE
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   907
              | get_sel_position i (sel' :: sels) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   908
                if sel = sel' then SOME i else get_sel_position (i + 1) sels;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   909
          in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   910
            ctrs ~~ map (get_sel_position 0) selss
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   911
            |> map_filter (fn (ctr, pos_opt) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   912
              if is_some pos_opt then SOME (ctr, the pos_opt) else NONE)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   913
          end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   914
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   915
        fun collect_sel_condss0 condss [] _ = condss
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   916
          | collect_sel_condss0 condss ((conds, _, ctr) :: raw_views) sel_positions =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   917
            let val condss' = condss |> is_some (AList.lookup (op =) sel_positions ctr) ? cons conds
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   918
            in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   919
              collect_sel_condss0 condss' raw_views sel_positions
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   920
            end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   921
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   922
        val collect_sel_condss =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   923
          if only_one_ctr then K [[]] else collect_sel_condss0 [] raw_views;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   924
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   925
        fun mk_sel_rhs sel_positions sel =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   926
          let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   927
            val sel_T = range_type (fastype_of sel);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   928
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   929
            fun extract_sel_value _(*bound_Ts*) fun_t arg_ts =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   930
              (case AList.lookup (op =) sel_positions fun_t of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   931
                SOME n => nth arg_ts n
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   932
              | NONE =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   933
                let val t = list_comb (fun_t, arg_ts) in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   934
                  if can_case_expand t then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   935
                    sel $ t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   936
                  else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   937
                    Term.dummy_pattern sel_T
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   938
                end);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   939
          in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   940
            massage_corec_code_rhs ctxt extract_sel_value [] rhs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   941
          end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   942
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   943
        val ordered_sels = distinct (op =) (flat selss);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   944
        val sel_positionss = map mk_sel_positions ordered_sels;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   945
        val sel_rhss = map2 mk_sel_rhs sel_positionss ordered_sels;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   946
        val sel_lhss = map (rapp lhs o mk_disc_or_sel Ts) ordered_sels;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   947
        val sel_condss = map collect_sel_condss sel_positionss;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   948
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   949
        fun is_undefined (Const (@{const_name undefined}, _)) = true
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   950
          | is_undefined _ = false;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   951
      in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   952
        sel_condss ~~ (sel_lhss ~~ sel_rhss)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   953
        |> filter_out (is_undefined o snd o snd)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   954
        |> map (apsnd HOLogic.mk_eq)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   955
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   956
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   957
    fun mk_atomic_prop fun_args (condss, concl) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   958
      (Logic.list_all (map dest_Free fun_args, abstract_over_list fun_args
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   959
        (Logic.list_implies (map HOLogic.mk_Trueprop (s_dnf condss), HOLogic.mk_Trueprop concl))));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   960
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   961
    val raw_views = rhs
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   962
      |> massage_let_if_case ctxt (K false) (fn _(*bound_Ts*) => fn t => t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   963
          |> can_case_expand t ? expand_to_ctr_term ctxt T) (K (K ())) (K I) []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   964
      |> (fn expanded_rhs => fold_rev_let_if_case ctxt generate_raw_views [] expanded_rhs [])
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   965
      |> rev;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   966
    val (disc_views, disc_iff_views) = generate_disc_views raw_views;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   967
    val ctr_views = generate_ctr_views raw_views;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   968
    val sel_views = generate_sel_views raw_views (length ctr_views = 1);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   969
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   970
    val mk_props = filter_out (null o fst) #> map (mk_atomic_prop lhs_free_args);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   971
  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   972
    (code_view, mk_props ctr_views, mk_props disc_views, mk_props disc_iff_views,
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   973
     mk_props sel_views)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   974
  end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   975
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   976
fun find_all_associated_types [] _ = []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   977
  | find_all_associated_types ((Type (_, Ts1), Type (_, Ts2)) :: TTs) T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   978
    find_all_associated_types ((Ts1 ~~ Ts2) @ TTs) T
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   979
  | find_all_associated_types ((T1, T2) :: TTs) T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   980
    find_all_associated_types TTs T |> T1 = T ? cons T2;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   981
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   982
fun as_member_of tab = try dest_Const #> Option.mapPartial (fst #> Symtab.lookup tab);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   983
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   984
fun extract_rho_from_equation
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   985
    ({ctr_guards, inner_buffer = {Oper, VLeaf, CLeaf, ctr_wrapper, friends}, ...},
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   986
     {pattern_ctrs, discs, sels, it, mk_case})
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   987
    b version Y preT ssig_T friend_tm (lhs_args, rhs) lthy =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   988
  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   989
    val thy = Proof_Context.theory_of lthy;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   990
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   991
    val res_T = fastype_of rhs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   992
    val YpreT = HOLogic.mk_prodT (Y, preT);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   993
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   994
    fun fpT_to new_T T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   995
      if T = res_T then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   996
        new_T
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   997
      else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   998
        (case T of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
   999
          Type (s, Ts) => Type (s, map (fpT_to new_T) Ts)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1000
        | _ => T);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1001
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1002
    fun build_params bound_Us bound_Ts T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1003
      {bound_Us = bound_Us, bound_Ts = bound_Ts, U = T, T = T};
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1004
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1005
    fun typ_before explore {bound_Us, bound_Ts, ...} t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1006
      explore (build_params bound_Us bound_Ts (fastype_of1 (bound_Ts, t))) t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1007
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1008
    val is_self_call = curry (op aconv) friend_tm;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1009
    val has_self_call = Term.exists_subterm is_self_call;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1010
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1011
    fun has_res_T bound_Ts t = fastype_of1 (bound_Ts, t) = res_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1012
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1013
    fun contains_res_T (Type (s, Ts)) = s = fst (dest_Type res_T) orelse exists contains_res_T Ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1014
      | contains_res_T _ = false;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1015
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1016
    val is_lhs_arg = member (op =) lhs_args;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1017
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1018
    fun is_constant t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1019
      not (Term.exists_subterm is_lhs_arg t orelse has_self_call t orelse loose_bvar (t, 0));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1020
    fun is_nested_type T = T <> res_T andalso T <> YpreT andalso T <> ssig_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1021
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1022
    val is_valid_case_argumentT = not o member (op =) [Y, ssig_T];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1023
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1024
    fun is_same_type_constr (Type (s, _)) (Type (s', _)) = (s = s')
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1025
      | is_same_type_constr _ _ = false;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1026
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1027
    exception NO_ENCAPSULATION of unit;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1028
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1029
    val parametric_consts = Unsynchronized.ref [];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1030
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1031
    (* We are assuming that set functions are marked with "[transfer_rule]" (cf. the "transfer"
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1032
       plugin). Otherwise, the "eq_algrho" tactic might fail. *)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1033
    fun is_special_parametric_const (x as (s, _)) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1034
      s = @{const_name id} orelse is_set lthy x;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1035
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1036
    fun add_parametric_const s general_T T U =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1037
      let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1038
        fun tupleT_of_funT T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1039
          let val (Ts, T) = strip_type T in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1040
            mk_tupleT_balanced (Ts @ [T])
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1041
          end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1042
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1043
        fun funT_of_tupleT n =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1044
          dest_tupleT_balanced (n + 1)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1045
          #> split_last
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1046
          #> op --->;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1047
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1048
        val m = num_binder_types general_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1049
        val param1_T = Type_Infer.paramify_vars general_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1050
        val param2_T = Type_Infer.paramify_vars param1_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1051
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1052
        val deadfixed_T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1053
          build_map lthy [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1054
          |> singleton (Type_Infer_Context.infer_types lthy)
62958
b41c1cb5e251 Type_Infer.object_logic controls improvement of type inference result;
wenzelm
parents: 62746
diff changeset
  1055
          |> singleton (Type_Infer.fixate lthy false)
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1056
          |> type_of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1057
          |> dest_funT
62746
blanchet
parents: 62743
diff changeset
  1058
          |-> generalize_types 1
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1059
          |> funT_of_tupleT m;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1060
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1061
        val j = maxidx_of_typ deadfixed_T + 1;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1062
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1063
        fun varifyT (Type (s, Ts)) = Type (s, map varifyT Ts)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1064
          | varifyT (TFree (s, T)) = TVar ((s, j), T)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1065
          | varifyT T = T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1066
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1067
        val dedvarified_T = varifyT deadfixed_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1068
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1069
        val new_vars = Sign.typ_match thy (dedvarified_T, T) Vartab.empty
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1070
          |> Vartab.dest
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1071
          |> filter (curry (op =) j o snd o fst)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1072
          |> Vartab.make;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1073
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1074
        val deadinstantiated_T = map_atyps (Type.devar new_vars) dedvarified_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1075
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1076
        val final_T =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1077
          if Sign.typ_instance thy (U, deadinstantiated_T) then deadfixed_T else general_T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1078
      in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1079
        parametric_consts := insert (op =) (s, final_T) (!parametric_consts)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1080
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1081
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1082
    fun encapsulate (params as {U, T, ...}) t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1083
      if U = T then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1084
        t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1085
      else if T = Y then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1086
        VLeaf $ t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1087
      else if T = res_T then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1088
        CLeaf $ t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1089
      else if T = YpreT then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1090
        it $ t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1091
      else if is_nested_type T andalso is_same_type_constr T U then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1092
        explore_nested lthy encapsulate params t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1093
      else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1094
        raise NO_ENCAPSULATION ();
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1095
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1096
    fun build_function_after_encapsulation fun_t fun_t' (params as {bound_Us, ...}) arg_ts arg_ts' =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1097
      let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1098
        val arg_Us' = fst (strip_typeN (length arg_ts) (fastype_of1 (bound_Us, fun_t')));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1099
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1100
        fun the_or_error arg NONE =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1101
            error ("Illegal argument " ^ quote (Syntax.string_of_term lthy arg) ^
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1102
              " to " ^ quote (Syntax.string_of_term lthy fun_t))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1103
          | the_or_error _ (SOME arg') = arg';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1104
      in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1105
        arg_ts'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1106
        |> `(map (curry fastype_of1 bound_Us))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1107
        |>> map2 (update_UT params) arg_Us'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1108
        |> op ~~
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1109
        |> map (try (uncurry encapsulate))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1110
        |> map2 the_or_error arg_ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1111
        |> curry list_comb fun_t'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1112
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1113
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1114
    fun rebuild_function_after_exploration old_fn new_fn explore params arg_ts =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1115
      arg_ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1116
      |> map (typ_before explore params)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1117
      |> build_function_after_encapsulation old_fn new_fn params arg_ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1118
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1119
    fun update_case Us U casex =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1120
      let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1121
        val Type (T_name, _) = domain_type (snd (strip_fun_type (fastype_of casex)));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1122
        val SOME {fp_ctr_sugar = {ctr_sugar = {T = Type (_, Ts), casex, ...}, ...}, ...} =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1123
          fp_sugar_of lthy T_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1124
        val T = body_type (fastype_of casex);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1125
      in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1126
        Term.subst_atomic_types ((T :: Ts) ~~ (U :: Us)) casex
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1127
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1128
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1129
    fun deduce_according_type default_T [] = default_T
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1130
      | deduce_according_type default_T Ts = (case distinct (op =) Ts of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1131
          U :: [] => U
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1132
        | _ => fpT_to ssig_T default_T);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1133
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1134
    fun massage_if explore_cond explore (params as {bound_Us, bound_Ts, ...}) t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1135
      (case strip_comb t of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1136
        (const as Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1137
        (case List.partition Term.is_dummy_pattern (map (explore params) branches) of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1138
          (dummy_branch' :: _, []) => dummy_branch'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1139
        | (_, [branch']) => branch'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1140
        | (_, branches') =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1141
          let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1142
            val brancheUs = map (curry fastype_of1 bound_Us) branches';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1143
            val U = deduce_according_type (fastype_of1 (bound_Ts, hd branches)) brancheUs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1144
            val const_obj' = (If_const U, obj)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1145
              ||> explore_cond (update_UT params @{typ bool} @{typ bool})
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1146
              |> op $;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1147
          in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1148
            build_function_after_encapsulation (const $ obj) const_obj' params branches branches'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1149
          end)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1150
      | _ => explore params t);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1151
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1152
    fun massage_map explore (params as {bound_Us, bound_Ts, T = Type (T_name, Ts), ...})
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1153
          (t as func $ mapped_arg) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1154
        if is_self_call (head_of func) then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1155
          explore params t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1156
        else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1157
          (case try (dest_map lthy T_name) func of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1158
            SOME (map_tm, fs) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1159
            let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1160
              val n = length fs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1161
              val mapped_arg' = mapped_arg
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1162
                |> `(curry fastype_of1 bound_Ts)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1163
                |>> build_params bound_Us bound_Ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1164
                |-> explore;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1165
              val Us = map (fpT_to ssig_T) (snd (dest_Type (fastype_of1 (bound_Us, mapped_arg'))));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1166
              val temporary_map = map_tm
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1167
                |> mk_map n Us Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1168
              val map_fn_Ts = fastype_of #> strip_fun_type #> fst;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1169
              val binder_Uss = map_fn_Ts temporary_map
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1170
                |> map (map (fpT_to ssig_T) o binder_types);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1171
              val fun_paramss = map_fn_Ts (head_of func)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1172
                |> map (build_params bound_Us bound_Ts);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1173
              val fs' = fs |> @{map 4} explore_fun binder_Uss (replicate n explore) fun_paramss;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1174
              val SOME bnf = bnf_of lthy T_name;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1175
              val Type (_, bnf_Ts) = T_of_bnf bnf;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1176
              val typ_alist =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1177
                lives_of_bnf bnf ~~ map (curry fastype_of1 bound_Us #> range_type) fs';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1178
              val Us' = map2 the_default Us (map (AList.lookup (op =) typ_alist) bnf_Ts);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1179
              val map_tm' = map_tm |> mk_map n Us Us';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1180
            in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1181
              build_function_after_encapsulation func (list_comb (map_tm', fs')) params [mapped_arg]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1182
                [mapped_arg']
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1183
            end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1184
          | NONE => explore params t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1185
      | massage_map explore params t = explore params t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1186
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1187
    fun massage_comp explore (params as {bound_Us, ...}) t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1188
      (case strip_comb t of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1189
        (Const (@{const_name comp}, _), f1 :: f2 :: args) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1190
        let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1191
          val args' = map (typ_before explore params) args;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1192
          val f2' = typ_before (explore_fun (map (curry fastype_of1 bound_Us) args') explore) params
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1193
            f2;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1194
          val f1' = typ_before (explore_fun [range_type (fastype_of1 (bound_Us, f2'))] explore)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1195
            params f1;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1196
        in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1197
          betapply (f1', list_comb (f2', args'))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1198
        end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1199
      | _ => explore params t);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1200
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1201
    fun massage_ctr explore (params as {T = T as Type (s, Ts), bound_Us, ...}) t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1202
        if T <> res_T then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1203
          (case try (dest_ctr lthy s) t of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1204
            SOME (ctr, args) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1205
            let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1206
              val args' = map (typ_before explore params) args;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1207
              val SOME {T = Type (_, ctr_Ts), ...} = ctr_sugar_of lthy s;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1208
              val temp_ctr = mk_ctr ctr_Ts ctr;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1209
              val argUs = map (curry fastype_of1 bound_Us) args';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1210
              val typ_alist = binder_types (fastype_of temp_ctr) ~~ argUs;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1211
              val Us = ctr_Ts
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1212
                |> map (find_all_associated_types typ_alist)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1213
                |> map2 deduce_according_type Ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1214
              val ctr' = mk_ctr Us ctr;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1215
            in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1216
              build_function_after_encapsulation ctr ctr' params args args'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1217
            end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1218
          | NONE => explore params t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1219
        else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1220
          explore params t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1221
      | massage_ctr explore params t = explore params t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1222
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1223
    fun const_of [] _ = NONE
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1224
      | const_of ((sel as Const (s1, _)) :: r) (const as Const (s2, _)) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1225
        if s1 = s2 then SOME sel else const_of r const
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1226
      | const_of _ _ = NONE;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1227
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1228
    fun massage_disc explore (params as {T, bound_Us, bound_Ts, ...}) t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1229
      (case (strip_comb t, T = @{typ bool}) of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1230
        ((fun_t, arg :: []), true) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1231
        let val arg_T = fastype_of1 (bound_Ts, arg) in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1232
          if arg_T <> res_T then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1233
            (case arg_T |> try (fst o dest_Type) |> Option.mapPartial (ctr_sugar_of lthy) of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1234
              SOME {discs, T = Type (_, Ts), ...} =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1235
              (case const_of discs fun_t of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1236
                SOME disc =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1237
                let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1238
                  val arg' = arg |> typ_before explore params;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1239
                  val Type (_, Us) = fastype_of1 (bound_Us, arg');
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1240
                  val disc' = disc |> Term.subst_TVars (map (fst o dest_TVar) Ts ~~ Us);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1241
                in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1242
                  disc' $ arg'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1243
                end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1244
              | NONE => explore params t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1245
            | NONE => explore params t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1246
          else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1247
            explore params t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1248
        end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1249
      | _ => explore params t);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1250
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1251
    fun massage_sel explore (params as {bound_Us, bound_Ts, ...}) t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1252
      let val (fun_t, args) = strip_comb t in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1253
        if args = [] then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1254
          explore params t
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1255
        else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1256
          let val T = fastype_of1 (bound_Ts, hd args) in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1257
            (case (Option.mapPartial (ctr_sugar_of lthy) (try (fst o dest_Type) T), T <> res_T) of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1258
              (SOME {selss, T = Type (_, Ts), ...}, true) =>
63391
blanchet
parents: 63352
diff changeset
  1259
              (case const_of (flat selss) fun_t of
62692
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1260
                SOME sel =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1261
                let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1262
                  val args' = args |> map (typ_before explore params);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1263
                  val Type (_, Us) = fastype_of1 (bound_Us, hd args');
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1264
                  val sel' = sel |> Term.subst_TVars (map (fst o dest_TVar) Ts ~~ Us);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1265
                in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1266
                  build_function_after_encapsulation sel sel' params args args'
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1267
                end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1268
              | NONE => explore params t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1269
            | _ => explore params t)
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1270
          end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1271
      end;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1272
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1273
    fun massage_equality explore (params as {bound_Us, bound_Ts, ...})
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1274
          (t as Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1275
        let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1276
          val check_is_VLeaf =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1277
            not o (Term.exists_subterm (fn t => t aconv CLeaf orelse t aconv Oper));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1278
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1279
          fun try_pattern_matching (fun_t, arg_ts) t =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1280
            (case as_member_of pattern_ctrs fun_t of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1281
              SOME (disc, sels) =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1282
              let val t' = typ_before explore params t in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1283
                if fastype_of1 (bound_Us, t') = YpreT then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1284
                  let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1285
                    val arg_ts' = map (typ_before explore params) arg_ts;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1286
                    val sels_t' = map (fn sel => betapply (sel, t')) sels;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1287
                    val Ts = map (curry fastype_of1 bound_Us) arg_ts';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1288
                    val Us = map (curry fastype_of1 bound_Us) sels_t';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1289
                    val arg_ts' = map2 encapsulate (map2 (update_UT params) Us Ts) arg_ts';
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1290
                  in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1291
                    if forall check_is_VLeaf arg_ts' then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1292
                      SOME (Library.foldl1 HOLogic.mk_conj
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1293
                        (betapply (disc, t') :: (map HOLogic.mk_eq (arg_ts' ~~ sels_t'))))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1294
                    else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1295
                      NONE
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1296
                  end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1297
                else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1298
                  NONE
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1299
              end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1300
            | NONE => NONE);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1301
        in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1302
          (case try_pattern_matching (strip_comb t1) t2 of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1303
            SOME cond => cond
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1304
          | NONE => (case try_pattern_matching (strip_comb t2) t1 of
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1305
              SOME cond => cond
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1306
            | NONE =>
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1307
              let
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1308
                val T = fastype_of1 (bound_Ts, t1);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1309
                val params' = build_params bound_Us bound_Ts T;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1310
                val t1' = explore params' t1;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1311
                val t2' = explore params' t2;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1312
              in
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1313
                if fastype_of1 (bound_Us, t1') = T andalso fastype_of1 (bound_Us, t2') = T then
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1314
                  HOLogic.mk_eq (t1', t2')
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1315
                else
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1316
                  error ("Unsupported condition: " ^ quote (Syntax.string_of_term lthy t))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1317
              end))
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1318
        end
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1319
      | massage_equality explore params t = explore params t;
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1320
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1321
    fun infer_types (TVar _) (TVar _) = []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1322
      | infer_types (U as TVar _) T = [(U, T)]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1323
      | infer_types (Type (s', Us)) (Type (s, Ts)) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1324
        if s' = s then flat (map2 infer_types Us Ts) else []
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1325
      | infer_types _ _ = [];
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1326
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1327
    fun group_by_fst associations [] = associations
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1328
      | group_by_fst associations ((a, b) :: r) = group_by_fst (add_association a b associations) r
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1329
    and add_association a b [] = [(a, [b])]
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1330
      | add_association a b ((c, d) :: r) =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1331
        if a = c then (c, b :: d) :: r
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1332
        else (c, d) :: (add_association a b r);
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1333
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1334
    fun new_TVar known_TVars =
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1335
      Name.invent_list (map (fst o fst o dest_TVar) known_TVars) "x" 1
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff changeset
  1336
      |> (fn [s] => TVar ((s, 0), []));
0701f25fac39 moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff