src/HOLCF/Tools/Domain/domain_take_proofs.ML
author haftmann
Wed, 05 May 2010 18:25:34 +0200
changeset 36692 54b64d4ad524
parent 36241 2a4cec6bcae2
child 37078 a1656804fcad
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     1
(*  Title:      HOLCF/Tools/domain/domain_take_proofs.ML
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     3
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     4
Defines take functions for the given domain equation
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     5
and proves related theorems.
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     6
*)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     7
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     8
signature DOMAIN_TAKE_PROOFS =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
     9
sig
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    10
  type iso_info =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    11
    {
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    12
      absT : typ,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    13
      repT : typ,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    14
      abs_const : term,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    15
      rep_const : term,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    16
      abs_inverse : thm,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    17
      rep_inverse : thm
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    18
    }
35651
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    19
  type take_info =
35659
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    20
    {
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    21
      take_consts : term list,
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    22
      take_defs : thm list,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    23
      chain_take_thms : thm list,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    24
      take_0_thms : thm list,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    25
      take_Suc_thms : thm list,
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
    26
      deflation_take_thms : thm list,
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
    27
      finite_consts : term list,
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
    28
      finite_defs : thm list
35651
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    29
    }
35656
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
    30
  type take_induct_info =
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
    31
    {
35659
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    32
      take_consts         : term list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    33
      take_defs           : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    34
      chain_take_thms     : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    35
      take_0_thms         : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    36
      take_Suc_thms       : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    37
      deflation_take_thms : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    38
      finite_consts       : term list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    39
      finite_defs         : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    40
      lub_take_thms       : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    41
      reach_thms          : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    42
      take_lemma_thms     : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    43
      is_finite           : bool,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    44
      take_induct_thms    : thm list
35656
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
    45
    }
35651
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    46
  val define_take_functions :
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    47
    (binding * iso_info) list -> theory -> take_info * theory
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    48
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
    49
  val add_lub_take_theorems :
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
    50
    (binding * iso_info) list -> take_info -> thm list ->
35656
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
    51
    theory -> take_induct_info * theory
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
    52
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    53
  val map_of_typ :
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    54
    theory -> (typ * term) list -> typ -> term
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    55
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    56
  val add_map_function :
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    57
    (string * string * thm) -> theory -> theory
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    58
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    59
  val get_map_tab : theory -> string Symtab.table
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    60
  val get_deflation_thms : theory -> thm list
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    61
end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    62
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    63
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    64
struct
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    65
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    66
type iso_info =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    67
  {
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    68
    absT : typ,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    69
    repT : typ,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    70
    abs_const : term,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    71
    rep_const : term,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    72
    abs_inverse : thm,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    73
    rep_inverse : thm
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    74
  };
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
    75
35651
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    76
type take_info =
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    77
  { take_consts : term list,
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    78
    take_defs : thm list,
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    79
    chain_take_thms : thm list,
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    80
    take_0_thms : thm list,
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    81
    take_Suc_thms : thm list,
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    82
    deflation_take_thms : thm list,
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    83
    finite_consts : term list,
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    84
    finite_defs : thm list
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    85
  };
5dd352a85464 add type take_info
huffman
parents: 35650
diff changeset
    86
35656
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
    87
type take_induct_info =
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
    88
  {
35659
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    89
    take_consts         : term list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    90
    take_defs           : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    91
    chain_take_thms     : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    92
    take_0_thms         : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    93
    take_Suc_thms       : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    94
    deflation_take_thms : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    95
    finite_consts       : term list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    96
    finite_defs         : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    97
    lub_take_thms       : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    98
    reach_thms          : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
    99
    take_lemma_thms     : thm list,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   100
    is_finite           : bool,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   101
    take_induct_thms    : thm list
35656
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
   102
  };
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
   103
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   104
val beta_ss =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   105
  HOL_basic_ss
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   106
    addsimps simp_thms
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   107
    addsimps [@{thm beta_cfun}]
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   108
    addsimprocs [@{simproc cont_proc}];
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   109
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   110
val beta_tac = simp_tac beta_ss;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   111
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   112
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   113
(******************************** theory data *********************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   114
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   115
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   116
structure MapData = Theory_Data
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   117
(
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   118
  (* constant names like "foo_map" *)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   119
  type T = string Symtab.table;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   120
  val empty = Symtab.empty;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   121
  val extend = I;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   122
  fun merge data = Symtab.merge (K true) data;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   123
);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   124
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   125
structure DeflMapData = Theory_Data
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   126
(
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   127
  (* theorems like "deflation a ==> deflation (foo_map$a)" *)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   128
  type T = thm list;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   129
  val empty = [];
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   130
  val extend = I;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   131
  val merge = Thm.merge_thms;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   132
);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   133
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   134
fun add_map_function (tname, map_name, deflation_map_thm) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   135
    MapData.map (Symtab.insert (K true) (tname, map_name))
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   136
    #> DeflMapData.map (Thm.add_thm deflation_map_thm);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   137
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   138
val get_map_tab = MapData.get;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   139
val get_deflation_thms = DeflMapData.get;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   140
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   141
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   142
(************************** building types and terms **************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   143
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   144
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   145
open HOLCF_Library;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   146
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   147
infixr 6 ->>;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   148
infix -->>;
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   149
infix 9 `;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   150
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   151
fun mapT (T as Type (_, Ts)) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   152
    (map (fn T => T ->> T) Ts) -->> (T ->> T)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   153
  | mapT T = T ->> T;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   154
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   155
fun mk_deflation t =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   156
  Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   157
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   158
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   159
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   160
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   161
(****************************** isomorphism info ******************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   162
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   163
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   164
fun deflation_abs_rep (info : iso_info) : thm =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   165
  let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   166
    val abs_iso = #abs_inverse info;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   167
    val rep_iso = #rep_inverse info;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   168
    val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   169
  in
36241
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   170
    Drule.zero_var_indexes thm
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   171
  end
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   172
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   173
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   174
(********************* building map functions over types **********************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   175
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   176
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   177
fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   178
  let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   179
    val map_tab = get_map_tab thy;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   180
    fun auto T = T ->> T;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   181
    fun map_of T =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   182
        case AList.lookup (op =) sub T of
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   183
          SOME m => (m, true) | NONE => map_of' T
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   184
    and map_of' (T as (Type (c, Ts))) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   185
        (case Symtab.lookup map_tab c of
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   186
          SOME map_name =>
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   187
          let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   188
            val map_type = map auto Ts -->> auto T;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   189
            val (ms, bs) = map_split map_of Ts;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   190
          in
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   191
            if exists I bs
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   192
            then (list_ccomb (Const (map_name, map_type), ms), true)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   193
            else (mk_ID T, false)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   194
          end
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   195
        | NONE => (mk_ID T, false))
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   196
      | map_of' T = (mk_ID T, false);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   197
  in
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   198
    fst (map_of T)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   199
  end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   200
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   201
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   202
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   203
(********************* declaring definitions and theorems *********************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   204
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   205
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   206
fun add_qualified_def name (dbind, eqn) =
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   207
    yield_singleton (PureThy.add_defs false)
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   208
     ((Binding.qualified true name dbind, eqn), []);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   209
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   210
fun add_qualified_thm name (dbind, thm) =
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   211
    yield_singleton PureThy.add_thms
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   212
      ((Binding.qualified true name dbind, thm), []);
35650
64fff18d7f08 add function add_qualified_def
huffman
parents: 35594
diff changeset
   213
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   214
fun add_qualified_simp_thm name (dbind, thm) =
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   215
    yield_singleton PureThy.add_thms
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   216
      ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]);
35573
bd8b50e76e94 add function add_qualified_simp_thm
huffman
parents: 35572
diff changeset
   217
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   218
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   219
(************************** defining take functions ***************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   220
(******************************************************************************)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   221
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   222
fun define_take_functions
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   223
    (spec : (binding * iso_info) list)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   224
    (thy : theory) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   225
  let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   226
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   227
    (* retrieve components of spec *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   228
    val dbinds = map fst spec;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   229
    val iso_infos = map snd spec;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   230
    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   231
    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   232
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   233
    (* get table of map functions *)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   234
    val map_tab = MapData.get thy;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   235
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   236
    fun mk_projs []      t = []
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   237
      | mk_projs (x::[]) t = [(x, t)]
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   238
      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   239
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   240
    fun mk_cfcomp2 ((rep_const, abs_const), f) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   241
        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   242
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   243
    (* define take functional *)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   244
    val newTs : typ list = map fst dom_eqns;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   245
    val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   246
    val copy_arg = Free ("f", copy_arg_type);
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   247
    val copy_args = map snd (mk_projs dbinds copy_arg);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   248
    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   249
      let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   250
        val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   251
      in
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   252
        mk_cfcomp2 (rep_abs, body)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   253
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   254
    val take_functional =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   255
        big_lambda copy_arg
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   256
          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   257
    val take_rhss =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   258
      let
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   259
        val n = Free ("n", HOLogic.natT);
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   260
        val rhs = mk_iterate (n, take_functional);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   261
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   262
        map (lambda n o snd) (mk_projs dbinds rhs)
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   263
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   264
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   265
    (* define take constants *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   266
    fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   267
      let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   268
        val take_type = HOLogic.natT --> lhsT ->> lhsT;
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   269
        val take_bind = Binding.suffix_name "_take" dbind;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   270
        val (take_const, thy) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   271
          Sign.declare_const ((take_bind, take_type), NoSyn) thy;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   272
        val take_eqn = Logic.mk_equals (take_const, take_rhs);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   273
        val (take_def_thm, thy) =
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   274
            add_qualified_def "take_def" (dbind, take_eqn) thy;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   275
      in ((take_const, take_def_thm), thy) end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   276
    val ((take_consts, take_defs), thy) = thy
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   277
      |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns)
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   278
      |>> ListPair.unzip;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   279
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   280
    (* prove chain_take lemmas *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   281
    fun prove_chain_take (take_const, dbind) thy =
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   282
      let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   283
        val goal = mk_trp (mk_chain take_const);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   284
        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   285
        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   286
        val thm = Goal.prove_global thy [] [] goal (K tac);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   287
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   288
        add_qualified_simp_thm "chain_take" (dbind, thm) thy
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   289
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   290
    val (chain_take_thms, thy) =
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   291
      fold_map prove_chain_take (take_consts ~~ dbinds) thy;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   292
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   293
    (* prove take_0 lemmas *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   294
    fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   295
      let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   296
        val lhs = take_const $ @{term "0::nat"};
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   297
        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   298
        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   299
        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   300
        val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   301
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   302
        add_qualified_thm "take_0" (dbind, take_0_thm) thy
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   303
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   304
    val (take_0_thms, thy) =
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   305
      fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   306
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   307
    (* prove take_Suc lemmas *)
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   308
    val n = Free ("n", natT);
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   309
    val take_is = map (fn t => t $ n) take_consts;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   310
    fun prove_take_Suc
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   311
          (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   312
      let
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   313
        val lhs = take_const $ (@{term Suc} $ n);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   314
        val body = map_of_typ thy (newTs ~~ take_is) rhsT;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   315
        val rhs = mk_cfcomp2 (rep_abs, body);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   316
        val goal = mk_eqs (lhs, rhs);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   317
        val simps = @{thms iterate_Suc fst_conv snd_conv}
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   318
        val rules = take_defs @ simps;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   319
        val tac = simp_tac (beta_ss addsimps rules) 1;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   320
        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   321
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   322
        add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   323
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   324
    val (take_Suc_thms, thy) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   325
      fold_map prove_take_Suc
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   326
        (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   327
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   328
    (* prove deflation theorems for take functions *)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   329
    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   330
    val deflation_take_thm =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   331
      let
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   332
        val n = Free ("n", natT);
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   333
        fun mk_goal take_const = mk_deflation (take_const $ n);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   334
        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   335
        val adm_rules =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   336
          @{thms adm_conj adm_subst [OF _ adm_deflation]
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   337
                 cont2cont_fst cont2cont_snd cont_id};
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   338
        val bottom_rules =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   339
          take_0_thms @ @{thms deflation_UU simp_thms};
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   340
        val deflation_rules =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   341
          @{thms conjI deflation_ID}
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   342
          @ deflation_abs_rep_thms
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   343
          @ DeflMapData.get thy;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   344
      in
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   345
        Goal.prove_global thy [] [] goal (fn _ =>
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   346
         EVERY
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   347
          [rtac @{thm nat.induct} 1,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   348
           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   349
           asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   350
           REPEAT (etac @{thm conjE} 1
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   351
                   ORELSE resolve_tac deflation_rules 1
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   352
                   ORELSE atac 1)])
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   353
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   354
    fun conjuncts [] thm = []
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   355
      | conjuncts (n::[]) thm = [(n, thm)]
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   356
      | conjuncts (n::ns) thm = let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   357
          val thmL = thm RS @{thm conjunct1};
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   358
          val thmR = thm RS @{thm conjunct2};
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   359
        in (n, thmL):: conjuncts ns thmR end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   360
    val (deflation_take_thms, thy) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   361
      fold_map (add_qualified_thm "deflation_take")
36241
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   362
        (map (apsnd Drule.zero_var_indexes)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   363
          (conjuncts dbinds deflation_take_thm)) thy;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   364
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   365
    (* prove strictness of take functions *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   366
    fun prove_take_strict (deflation_take, dbind) thy =
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   367
      let
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   368
        val take_strict_thm =
36241
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   369
            Drule.zero_var_indexes
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   370
              (@{thm deflation_strict} OF [deflation_take]);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   371
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   372
        add_qualified_thm "take_strict" (dbind, take_strict_thm) thy
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   373
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   374
    val (take_strict_thms, thy) =
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   375
      fold_map prove_take_strict
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   376
        (deflation_take_thms ~~ dbinds) thy;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   377
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   378
    (* prove take/take rules *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   379
    fun prove_take_take ((chain_take, deflation_take), dbind) thy =
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   380
      let
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   381
        val take_take_thm =
36241
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   382
            Drule.zero_var_indexes
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   383
              (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   384
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   385
        add_qualified_thm "take_take" (dbind, take_take_thm) thy
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   386
      end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   387
    val (take_take_thms, thy) =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   388
      fold_map prove_take_take
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   389
        (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy;
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   390
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   391
    (* prove take_below rules *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   392
    fun prove_take_below (deflation_take, dbind) thy =
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   393
      let
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   394
        val take_below_thm =
36241
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   395
            Drule.zero_var_indexes
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   396
              (@{thm deflation.below} OF [deflation_take]);
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   397
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   398
        add_qualified_thm "take_below" (dbind, take_below_thm) thy
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   399
      end;
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   400
    val (take_below_thms, thy) =
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   401
      fold_map prove_take_below
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   402
        (deflation_take_thms ~~ dbinds) thy;
35572
44eeda8cb708 generate lemma take_below, declare chain_take [simp]
huffman
parents: 35557
diff changeset
   403
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   404
    (* define finiteness predicates *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   405
    fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   406
      let
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   407
        val finite_type = lhsT --> boolT;
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   408
        val finite_bind = Binding.suffix_name "_finite" dbind;
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   409
        val (finite_const, thy) =
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   410
          Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   411
        val x = Free ("x", lhsT);
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   412
        val n = Free ("n", natT);
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   413
        val finite_rhs =
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   414
          lambda x (HOLogic.exists_const natT $
35557
5da670d57118 uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
huffman
parents: 35555
diff changeset
   415
            (lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   416
        val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   417
        val (finite_def_thm, thy) =
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   418
            add_qualified_def "finite_def" (dbind, finite_eqn) thy;
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   419
      in ((finite_const, finite_def_thm), thy) end;
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   420
    val ((finite_consts, finite_defs), thy) = thy
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   421
      |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns)
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   422
      |>> ListPair.unzip;
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   423
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   424
    val result =
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   425
      {
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   426
        take_consts = take_consts,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   427
        take_defs = take_defs,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   428
        chain_take_thms = chain_take_thms,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   429
        take_0_thms = take_0_thms,
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   430
        take_Suc_thms = take_Suc_thms,
35515
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   431
        deflation_take_thms = deflation_take_thms,
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   432
        finite_consts = finite_consts,
d631dc53ede0 move definition of finiteness predicate into domain_take_proofs.ML
huffman
parents: 35514
diff changeset
   433
        finite_defs = finite_defs
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   434
      };
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   435
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   436
  in
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   437
    (result, thy)
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   438
  end;
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   439
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   440
fun prove_finite_take_induct
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   441
    (spec : (binding * iso_info) list)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   442
    (take_info : take_info)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   443
    (lub_take_thms : thm list)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   444
    (thy : theory) =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   445
  let
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   446
    val dbinds = map fst spec;
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   447
    val iso_infos = map snd spec;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   448
    val absTs = map #absT iso_infos;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   449
    val {take_consts, ...} = take_info;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   450
    val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   451
    val {finite_consts, finite_defs, ...} = take_info;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   452
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   453
    val decisive_lemma =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   454
      let
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   455
        fun iso_locale info =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   456
            @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   457
        val iso_locale_thms = map iso_locale iso_infos;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   458
        val decisive_abs_rep_thms =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   459
            map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   460
        val n = Free ("n", @{typ nat});
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   461
        fun mk_decisive t =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   462
            Const (@{const_name decisive}, fastype_of t --> boolT) $ t;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   463
        fun f take_const = mk_decisive (take_const $ n);
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   464
        val goal = mk_trp (foldr1 mk_conj (map f take_consts));
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   465
        val rules0 = @{thm decisive_bottom} :: take_0_thms;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   466
        val rules1 =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   467
            take_Suc_thms @ decisive_abs_rep_thms
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   468
            @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   469
        val tac = EVERY [
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   470
            rtac @{thm nat.induct} 1,
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   471
            simp_tac (HOL_ss addsimps rules0) 1,
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   472
            asm_simp_tac (HOL_ss addsimps rules1) 1];
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   473
      in Goal.prove_global thy [] [] goal (K tac) end;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   474
    fun conjuncts 1 thm = [thm]
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   475
      | conjuncts n thm = let
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   476
          val thmL = thm RS @{thm conjunct1};
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   477
          val thmR = thm RS @{thm conjunct2};
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   478
        in thmL :: conjuncts (n-1) thmR end;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   479
    val decisive_thms = conjuncts (length spec) decisive_lemma;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   480
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   481
    fun prove_finite_thm (absT, finite_const) =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   482
      let
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   483
        val goal = mk_trp (finite_const $ Free ("x", absT));
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   484
        val tac =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   485
            EVERY [
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   486
            rewrite_goals_tac finite_defs,
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   487
            rtac @{thm lub_ID_finite} 1,
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   488
            resolve_tac chain_take_thms 1,
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   489
            resolve_tac lub_take_thms 1,
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   490
            resolve_tac decisive_thms 1];
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   491
      in
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   492
        Goal.prove_global thy [] [] goal (K tac)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   493
      end;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   494
    val finite_thms =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   495
        map prove_finite_thm (absTs ~~ finite_consts);
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   496
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   497
    fun prove_take_induct ((ch_take, lub_take), decisive) =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   498
        Drule.export_without_context
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   499
          (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]);
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   500
    val take_induct_thms =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   501
        map prove_take_induct
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   502
          (chain_take_thms ~~ lub_take_thms ~~ decisive_thms);
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   503
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   504
    val thy = thy
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   505
        |> fold (snd oo add_qualified_thm "finite")
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   506
            (dbinds ~~ finite_thms)
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   507
        |> fold (snd oo add_qualified_thm "take_induct")
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   508
            (dbinds ~~ take_induct_thms);
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   509
  in
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   510
    ((finite_thms, take_induct_thms), thy)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   511
  end;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   512
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   513
fun add_lub_take_theorems
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   514
    (spec : (binding * iso_info) list)
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   515
    (take_info : take_info)
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   516
    (lub_take_thms : thm list)
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   517
    (thy : theory) =
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   518
  let
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   519
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   520
    (* retrieve components of spec *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   521
    val dbinds = map fst spec;
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   522
    val iso_infos = map snd spec;
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   523
    val absTs = map #absT iso_infos;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   524
    val repTs = map #repT iso_infos;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   525
    val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info;
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   526
    val {chain_take_thms, deflation_take_thms, ...} = take_info;
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   527
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   528
    (* prove take lemmas *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   529
    fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   530
      let
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   531
        val take_lemma =
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   532
            Drule.export_without_context
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   533
              (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]);
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   534
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   535
        add_qualified_thm "take_lemma" (dbind, take_lemma) thy
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   536
      end;
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   537
    val (take_lemma_thms, thy) =
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   538
      fold_map prove_take_lemma
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   539
        (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   540
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   541
    (* prove reach lemmas *)
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   542
    fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   543
      let
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   544
        val thm =
36241
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   545
            Drule.zero_var_indexes
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   546
              (@{thm lub_ID_reach} OF [chain_take, lub_take]);
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   547
      in
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   548
        add_qualified_thm "reach" (dbind, thm) thy
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   549
      end;
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   550
    val (reach_thms, thy) =
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   551
      fold_map prove_reach_lemma
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   552
        (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   553
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   554
    (* test for finiteness of domain definitions *)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   555
    local
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   556
      val types = [@{type_name ssum}, @{type_name sprod}];
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36241
diff changeset
   557
      fun finite d T = if member (op =) absTs T then d else finite' d T
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   558
      and finite' d (Type (c, Ts)) =
36692
54b64d4ad524 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
haftmann
parents: 36241
diff changeset
   559
          let val d' = d andalso member (op =) types c;
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   560
          in forall (finite d') Ts end
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   561
        | finite' d _ = true;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   562
    in
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   563
      val is_finite = forall (finite true) repTs;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   564
    end;
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   565
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   566
    val ((finite_thms, take_induct_thms), thy) =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   567
      if is_finite
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   568
      then
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   569
        let
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   570
          val ((finites, take_inducts), thy) =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   571
              prove_finite_take_induct spec take_info lub_take_thms thy;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   572
        in
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   573
          ((SOME finites, take_inducts), thy)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   574
        end
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   575
      else
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   576
        let
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   577
          fun prove_take_induct (chain_take, lub_take) =
36241
2a4cec6bcae2 replace many uses of Drule.export_without_context with Drule.zero_var_indexes
huffman
parents: 35773
diff changeset
   578
              Drule.zero_var_indexes
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   579
                (@{thm lub_ID_take_induct} OF [chain_take, lub_take]);
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   580
          val take_inducts =
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   581
              map prove_take_induct (chain_take_thms ~~ lub_take_thms);
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   582
          val thy = fold (snd oo add_qualified_thm "take_induct")
35773
cae4f840d15d more consistent use of qualified bindings
huffman
parents: 35659
diff changeset
   583
                         (dbinds ~~ take_inducts) thy;
35655
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   584
        in
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   585
          ((NONE, take_inducts), thy)
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   586
        end;
e8e4af6da819 generate take_induct lemmas
huffman
parents: 35654
diff changeset
   587
35656
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
   588
    val result =
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
   589
      {
35659
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   590
        take_consts         = #take_consts take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   591
        take_defs           = #take_defs take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   592
        chain_take_thms     = #chain_take_thms take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   593
        take_0_thms         = #take_0_thms take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   594
        take_Suc_thms       = #take_Suc_thms take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   595
        deflation_take_thms = #deflation_take_thms take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   596
        finite_consts       = #finite_consts take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   597
        finite_defs         = #finite_defs take_info,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   598
        lub_take_thms       = lub_take_thms,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   599
        reach_thms          = reach_thms,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   600
        take_lemma_thms     = take_lemma_thms,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   601
        is_finite           = is_finite,
a78bc1930a7a include take_info within take_induct_info type
huffman
parents: 35656
diff changeset
   602
        take_induct_thms    = take_induct_thms
35656
b62731352812 add type take_induct_info
huffman
parents: 35655
diff changeset
   603
      };
35654
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   604
  in
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   605
    (result, thy)
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   606
  end;
7a15e181bf3b move proofs of reach and take lemmas to domain_take_proofs.ML
huffman
parents: 35651
diff changeset
   607
35514
a2cfa413eaab move take-related definitions and proofs to new module; simplify map_of_typ functions
huffman
parents:
diff changeset
   608
end;