src/HOL/Tools/Lifting/lifting_info.ML
author wenzelm
Mon, 18 Aug 2014 12:17:31 +0200
changeset 57978 8f4a332500e4
parent 57663 b590fcd03a4a
child 57961 10b2f60b70f0
permissions -rw-r--r--
Added tag Isabelle2014-RC4 for changeset 113b43b84412
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     1
(*  Title:      HOL/Tools/Lifting/lifting_info.ML
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     2
    Author:     Ondrej Kuncar
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     3
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     4
Context data for the lifting package.
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     5
*)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     6
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     7
signature LIFTING_INFO =
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
     8
sig
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
     9
  type quot_map = {rel_quot_thm: thm}
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    10
  val lookup_quot_maps: Proof.context -> string -> quot_map option
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    11
  val print_quot_maps: Proof.context -> unit
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    12
  
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    13
  type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    14
  type quotient = {quot_thm: thm, pcr_info: pcr option}
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    15
  val pcr_eq: pcr * pcr -> bool
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    16
  val quotient_eq: quotient * quotient -> bool
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    17
  val transform_quotient: morphism -> quotient -> quotient
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    18
  val lookup_quotients: Proof.context -> string -> quotient option
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    19
  val update_quotients: string -> quotient -> Context.generic -> Context.generic
53650
71a0a8687d6c make ML function for deleting quotients public
kuncar
parents: 53284
diff changeset
    20
  val delete_quotients: thm -> Context.generic -> Context.generic
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    21
  val print_quotients: Proof.context -> unit
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    22
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    23
  type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    24
  val lookup_restore_data: Proof.context -> string -> restore_data option
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    25
  val init_restore_data: string -> quotient -> Context.generic -> Context.generic
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    26
  val add_transfer_rules_in_restore_data: string -> thm Item_Net.T -> Context.generic -> Context.generic  
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    27
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
    28
  val get_relator_eq_onp_rules: Proof.context -> thm list
47936
756f30eac792 infrastructure that makes possible to prove that a relation is reflexive
kuncar
parents: 47784
diff changeset
    29
  
47982
7aa35601ff65 prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents: 47951
diff changeset
    30
  val get_reflexivity_rules: Proof.context -> thm list
7aa35601ff65 prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
kuncar
parents: 47951
diff changeset
    31
  val add_reflexivity_rule_attribute: attribute
47634
091bcd569441 hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents: 47308
diff changeset
    32
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
    33
  type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
    34
    pos_distr_rules: thm list, neg_distr_rules: thm list}
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
    35
  val lookup_relator_distr_data: Proof.context -> string -> relator_distr_data option
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    36
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    37
  val add_no_code_type: string -> Context.generic -> Context.generic
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    38
  val is_no_code_type: Proof.context -> string -> bool
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    39
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    40
  val get_quot_maps           : Proof.context -> quot_map Symtab.table
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    41
  val get_quotients           : Proof.context -> quotient Symtab.table
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    42
  val get_relator_distr_data  : Proof.context -> relator_distr_data Symtab.table
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    43
  val get_restore_data        : Proof.context -> restore_data Symtab.table
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    44
  val get_no_code_types       : Proof.context -> unit Symtab.table
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
    45
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    46
  val setup: theory -> theory
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    47
end
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    48
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    49
structure Lifting_Info: LIFTING_INFO =
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    50
struct
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
    51
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
    52
open Lifting_Util
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
    53
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    54
(** data container **)
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    55
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    56
type quot_map = {rel_quot_thm: thm}
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    57
type pcr = {pcrel_def: thm, pcr_cr_eq: thm}
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    58
type quotient = {quot_thm: thm, pcr_info: pcr option}
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    59
type relator_distr_data = {pos_mono_rule: thm, neg_mono_rule: thm, 
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    60
  pos_distr_rules: thm list, neg_distr_rules: thm list}
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    61
type restore_data = {quotient : quotient, transfer_rules: thm Item_Net.T}
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    62
53684
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    63
fun pcr_eq ({pcrel_def = pcrel_def1, pcr_cr_eq = pcr_cr_eq1},
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    64
           {pcrel_def = pcrel_def2, pcr_cr_eq = pcr_cr_eq2}) = 
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    65
           Thm.eq_thm (pcrel_def1, pcrel_def2) andalso Thm.eq_thm (pcr_cr_eq1, pcr_cr_eq2)
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    66
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    67
fun option_eq _ (NONE,NONE) = true
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    68
  | option_eq _ (NONE,_) = false
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    69
  | option_eq _ (_,NONE) = false
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    70
  | option_eq cmp (SOME x, SOME y) = cmp (x,y);
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    71
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    72
fun quotient_eq ({quot_thm = quot_thm1, pcr_info = pcr_info1},
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    73
                {quot_thm = quot_thm2, pcr_info = pcr_info2}) =
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    74
                Thm.eq_thm (quot_thm1, quot_thm2) andalso option_eq pcr_eq (pcr_info1, pcr_info2)
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    75
53754
124bb918f45f make SML/NJ happy
kuncar
parents: 53684
diff changeset
    76
fun join_restore_data key (rd1:restore_data, rd2) =
53684
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    77
  if pointer_eq (rd1, rd2) then raise Symtab.SAME else
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    78
  if not (quotient_eq (#quotient rd1, #quotient rd2)) then raise Symtab.DUP key else
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    79
    { quotient = #quotient rd1, 
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    80
      transfer_rules = Item_Net.merge (#transfer_rules rd1, #transfer_rules rd2)}
339aefeacb57 correct merging of restore data
kuncar
parents: 53651
diff changeset
    81
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    82
structure Data = Generic_Data
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    83
(
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    84
  type T = 
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    85
    { quot_maps : quot_map Symtab.table,
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    86
      quotients : quotient Symtab.table,
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    87
      reflexivity_rules : thm Item_Net.T,
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    88
      relator_distr_data : relator_distr_data Symtab.table,
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    89
      restore_data : restore_data Symtab.table,
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    90
      no_code_types : unit Symtab.table
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    91
    }
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    92
  val empty =
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    93
    { quot_maps = Symtab.empty,
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    94
      quotients = Symtab.empty,
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    95
      reflexivity_rules = Thm.full_rules,
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
    96
      relator_distr_data = Symtab.empty,
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    97
      restore_data = Symtab.empty,
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
    98
      no_code_types = Symtab.empty
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
    99
    }
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   100
  val extend = I
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   101
  fun merge
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   102
    ( { quot_maps = qm1, quotients = q1, reflexivity_rules = rr1, relator_distr_data = rdd1, 
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   103
        restore_data = rd1, no_code_types = nct1 },
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   104
      { quot_maps = qm2, quotients = q2, reflexivity_rules = rr2, relator_distr_data = rdd2,
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   105
        restore_data = rd2, no_code_types = nct2 } ) =
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   106
    { quot_maps = Symtab.merge (K true) (qm1, qm2),
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   107
      quotients = Symtab.merge (K true) (q1, q2),
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   108
      reflexivity_rules = Item_Net.merge (rr1, rr2),
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   109
      relator_distr_data = Symtab.merge (K true) (rdd1, rdd2),
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   110
      restore_data = Symtab.join join_restore_data (rd1, rd2),
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   111
      no_code_types = Symtab.merge (K true) (nct1, nct2)
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   112
    }
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   113
)
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   114
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   115
fun map_data f1 f2 f3 f4 f5 f6
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   116
  { quot_maps, quotients, reflexivity_rules, relator_distr_data, restore_data, no_code_types } =
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   117
  { quot_maps = f1 quot_maps,
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   118
    quotients = f2 quotients,
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   119
    reflexivity_rules = f3 reflexivity_rules,
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   120
    relator_distr_data = f4 relator_distr_data,
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   121
    restore_data = f5 restore_data,
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   122
    no_code_types = f6 no_code_types
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   123
  }
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   124
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   125
fun map_quot_maps           f = map_data f I I I I I
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   126
fun map_quotients           f = map_data I f I I I I
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   127
fun map_reflexivity_rules   f = map_data I I f I I I
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   128
fun map_relator_distr_data  f = map_data I I I f I I
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   129
fun map_restore_data        f = map_data I I I I f I
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   130
fun map_no_code_types       f = map_data I I I I I f
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   131
  
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   132
val get_quot_maps'           = #quot_maps o Data.get
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   133
val get_quotients'           = #quotients o Data.get
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   134
val get_reflexivity_rules'   = #reflexivity_rules o Data.get
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   135
val get_relator_distr_data'  = #relator_distr_data o Data.get
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   136
val get_restore_data'        = #restore_data o Data.get
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   137
val get_no_code_types'       = #no_code_types o Data.get
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   138
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   139
fun get_quot_maps          ctxt = get_quot_maps' (Context.Proof ctxt)
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   140
fun get_quotients          ctxt = get_quotients' (Context.Proof ctxt)
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   141
fun get_relator_distr_data ctxt = get_relator_distr_data' (Context.Proof ctxt)
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   142
fun get_restore_data       ctxt = get_restore_data' (Context.Proof ctxt)
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   143
fun get_no_code_types      ctxt = get_no_code_types' (Context.Proof ctxt)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   144
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   145
(* info about Quotient map theorems *)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   146
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   147
val lookup_quot_maps = Symtab.lookup o get_quot_maps
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   148
47784
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   149
fun quot_map_thm_sanity_check rel_quot_thm ctxt =
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   150
  let
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   151
    fun quot_term_absT ctxt quot_term = 
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   152
      let 
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   153
        val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) quot_term
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   154
          handle TERM (_, [t]) => error (Pretty.string_of (Pretty.block
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   155
            [Pretty.str "The Quotient map theorem is not in the right form.",
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   156
             Pretty.brk 1,
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   157
             Pretty.str "The following term is not the Quotient predicate:",
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   158
             Pretty.brk 1,
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   159
             Syntax.pretty_term ctxt t]))
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   160
      in
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   161
        fastype_of abs
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   162
      end
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   163
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   164
    val ((_, [rel_quot_thm_fixed]), ctxt') = Variable.importT [rel_quot_thm] ctxt
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   165
    val rel_quot_thm_prop = prop_of rel_quot_thm_fixed
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   166
    val rel_quot_thm_concl = Logic.strip_imp_concl rel_quot_thm_prop
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   167
    val rel_quot_thm_prems = Logic.strip_imp_prems rel_quot_thm_prop;
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   168
    val concl_absT = quot_term_absT ctxt' rel_quot_thm_concl
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   169
    val concl_tfrees = Term.add_tfree_namesT (concl_absT) []
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   170
    val prems_tfrees = fold (fn typ => fn list => Term.add_tfree_namesT (quot_term_absT ctxt' typ) list) 
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   171
                          rel_quot_thm_prems []
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   172
    val extra_prem_tfrees =
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   173
      case subtract (op =) concl_tfrees prems_tfrees of
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   174
        [] => []
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   175
      | extras => [Pretty.block ([Pretty.str "Extra type variables in the premises:",
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   176
                                 Pretty.brk 1] @ 
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   177
                                 ((Pretty.commas o map (Pretty.str o quote)) extras) @
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   178
                                 [Pretty.str "."])]
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   179
    val errs = extra_prem_tfrees 
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   180
  in
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   181
    if null errs then () else error (cat_lines (["Sanity check of the quotient map theorem failed:",""] 
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   182
                                                 @ (map Pretty.string_of errs)))
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   183
  end
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   184
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   185
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   186
fun add_quot_map rel_quot_thm ctxt = 
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   187
  let
47784
fe43977e434f added a basic sanity check for quot_map
kuncar
parents: 47777
diff changeset
   188
    val _ = Context.cases (K ()) (quot_map_thm_sanity_check rel_quot_thm) ctxt
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   189
    val rel_quot_thm_concl = (Logic.strip_imp_concl o prop_of) rel_quot_thm
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   190
    val (_, abs, _, _) = (dest_Quotient o HOLogic.dest_Trueprop) rel_quot_thm_concl
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   191
    val relatorT_name = (fst o dest_Type o fst o dest_funT o fastype_of) abs
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   192
    val minfo = {rel_quot_thm = rel_quot_thm}
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   193
  in
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   194
    Data.map (map_quot_maps (Symtab.update (relatorT_name, minfo))) ctxt
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   195
  end    
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   196
47951
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   197
val quot_map_attribute_setup =
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   198
  Attrib.setup @{binding quot_map} (Scan.succeed (Thm.declaration_attribute add_quot_map))
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   199
    "declaration of the Quotient map theorem"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   200
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   201
fun print_quot_maps ctxt =
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   202
  let
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   203
    fun prt_map (ty_name, {rel_quot_thm}) =
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   204
      Pretty.block (separate (Pretty.brk 2)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   205
         [Pretty.str "type:", 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   206
          Pretty.str ty_name,
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   207
          Pretty.str "quot. theorem:", 
47777
f29e7dcd7c40 use a quot_map theorem attribute instead of the complicated map attribute
kuncar
parents: 47634
diff changeset
   208
          Syntax.pretty_term ctxt (prop_of rel_quot_thm)])
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   209
  in
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   210
    map prt_map (Symtab.dest (get_quot_maps ctxt))
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   211
    |> Pretty.big_list "maps for type constructors:"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   212
    |> Pretty.writeln
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   213
  end
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   214
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   215
(* info about quotient types *)
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   216
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   217
fun transform_pcr_info phi {pcrel_def, pcr_cr_eq} =
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   218
  {pcrel_def = Morphism.thm phi pcrel_def, pcr_cr_eq = Morphism.thm phi pcr_cr_eq}
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   219
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   220
fun transform_quotient phi {quot_thm, pcr_info} =
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   221
  {quot_thm = Morphism.thm phi quot_thm, pcr_info = Option.map (transform_pcr_info phi) pcr_info}
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   222
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   223
fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   224
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   225
fun update_quotients type_name qinfo ctxt = 
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   226
  Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   227
47951
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   228
fun delete_quotients quot_thm ctxt =
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   229
  let
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   230
    val (_, qtyp) = quot_thm_rty_qty quot_thm
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   231
    val qty_full_name = (fst o dest_Type) qtyp
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   232
    val symtab = get_quotients' ctxt
53284
d0153a0a9b2b make SML/NJ happy
kuncar
parents: 53219
diff changeset
   233
    fun compare_data (_, data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
47951
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   234
  in
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   235
    if Symtab.member compare_data symtab (qty_full_name, quot_thm)
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   236
      then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   237
      else ctxt
47951
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   238
  end
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   239
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   240
fun print_quotients ctxt =
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   241
  let
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   242
    fun prt_quot (qty_name, {quot_thm, pcr_info}: quotient) =
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   243
      Pretty.block (separate (Pretty.brk 2)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   244
       [Pretty.str "type:", 
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   245
        Pretty.str qty_name,
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   246
        Pretty.str "quot. thm:",
50227
01d545993e8c generate a parameterized correspondence relation
kuncar
parents: 47982
diff changeset
   247
        Syntax.pretty_term ctxt (prop_of quot_thm),
01d545993e8c generate a parameterized correspondence relation
kuncar
parents: 47982
diff changeset
   248
        Pretty.str "pcrel_def thm:",
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   249
        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcrel_def) pcr_info,
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   250
        Pretty.str "pcr_cr_eq thm:",
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   251
        option_fold (Pretty.str "-") ((Syntax.pretty_term ctxt) o prop_of o #pcr_cr_eq) pcr_info])
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   252
  in
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   253
    map prt_quot (Symtab.dest (get_quotients ctxt))
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   254
    |> Pretty.big_list "quotients:"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   255
    |> Pretty.writeln
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   256
  end
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   257
47951
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   258
val quot_del_attribute_setup =
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   259
  Attrib.setup @{binding quot_del} (Scan.succeed (Thm.declaration_attribute delete_quotients))
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   260
    "deletes the Quotient theorem"
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   261
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   262
(* data for restoring Transfer/Lifting context *)
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   263
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   264
fun lookup_restore_data ctxt bundle_name = Symtab.lookup (get_restore_data ctxt) bundle_name
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   265
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   266
fun update_restore_data bundle_name restore_data ctxt = 
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   267
  Data.map (map_restore_data (Symtab.update (bundle_name, restore_data))) ctxt
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   268
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   269
fun init_restore_data bundle_name qinfo ctxt = 
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   270
  update_restore_data bundle_name { quotient = qinfo, transfer_rules = Thm.full_rules } ctxt
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   271
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   272
fun add_transfer_rules_in_restore_data bundle_name transfer_rules ctxt =
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   273
  case Symtab.lookup (get_restore_data' ctxt) bundle_name of
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   274
    SOME restore_data => update_restore_data bundle_name { quotient = #quotient restore_data, 
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   275
      transfer_rules = Item_Net.merge ((#transfer_rules restore_data), transfer_rules) } ctxt
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   276
    | NONE => error ("The restore data " ^ quote bundle_name ^ " is not defined.")
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   277
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   278
(* theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate *)
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   279
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   280
structure Relator_Eq_Onp = Named_Thms
47634
091bcd569441 hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents: 47308
diff changeset
   281
(
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   282
  val name = @{binding relator_eq_onp}
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   283
  val description = "theorems that a relator of an eq_onp is an eq_onp of the corresponding predicate"
47634
091bcd569441 hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents: 47308
diff changeset
   284
)
091bcd569441 hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents: 47308
diff changeset
   285
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   286
fun get_relator_eq_onp_rules ctxt = map safe_mk_meta_eq (Relator_Eq_Onp.get ctxt)
47634
091bcd569441 hide the invariant constant for relators: invariant_commute infrastracture
kuncar
parents: 47308
diff changeset
   287
51994
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51427
diff changeset
   288
(* info about reflexivity rules *)
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51427
diff changeset
   289
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   290
fun get_reflexivity_rules ctxt = Item_Net.content (get_reflexivity_rules' (Context.Proof ctxt))
51994
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51427
diff changeset
   291
55563
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   292
fun add_reflexivity_rule thm = Data.map (map_reflexivity_rules (Item_Net.update thm))
51994
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51427
diff changeset
   293
val add_reflexivity_rule_attribute = Thm.declaration_attribute add_reflexivity_rule
82cc2aeb7d13 stronger reflexivity prover
kuncar
parents: 51427
diff changeset
   294
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   295
(* info about relator distributivity theorems *)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   296
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   297
fun map_relator_distr_data' f1 f2 f3 f4
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   298
  {pos_mono_rule, neg_mono_rule, pos_distr_rules, neg_distr_rules} =
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   299
  {pos_mono_rule   = f1 pos_mono_rule, 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   300
   neg_mono_rule   = f2 neg_mono_rule,
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   301
   pos_distr_rules = f3 pos_distr_rules, 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   302
   neg_distr_rules = f4 neg_distr_rules}
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   303
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   304
fun map_pos_mono_rule f = map_relator_distr_data' f I I I
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   305
fun map_neg_mono_rule f = map_relator_distr_data' I f I I
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   306
fun map_pos_distr_rules f = map_relator_distr_data' I I f I 
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   307
fun map_neg_distr_rules f = map_relator_distr_data' I I I f
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   308
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   309
fun introduce_polarities rule =
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   310
  let
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   311
    val dest_less_eq = HOLogic.dest_bin @{const_name "less_eq"} dummyT
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   312
    val prems_pairs = map (dest_less_eq o HOLogic.dest_Trueprop) (prems_of rule)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   313
    val equal_prems = filter op= prems_pairs
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   314
    val _ = if null equal_prems then () 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   315
      else error "The rule contains reflexive assumptions."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   316
    val concl_pairs = rule 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   317
      |> concl_of
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   318
      |> HOLogic.dest_Trueprop
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   319
      |> dest_less_eq
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   320
      |> pairself (snd o strip_comb)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   321
      |> op~~
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   322
      |> filter_out op=
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   323
    
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   324
    val _ = if has_duplicates op= concl_pairs 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   325
      then error "The rule contains duplicated variables in the conlusion." else ()
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   326
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   327
    fun rewrite_prem prem_pair = 
51427
08bb00239652 proper use of "member", without embarking on delicate questions about SML equality types;
wenzelm
parents: 51426
diff changeset
   328
      if member op= concl_pairs prem_pair
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   329
      then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))
51427
08bb00239652 proper use of "member", without embarking on delicate questions about SML equality types;
wenzelm
parents: 51426
diff changeset
   330
      else if member op= concl_pairs (swap prem_pair)
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   331
        then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   332
      else error "The rule contains a non-relevant assumption."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   333
    
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   334
    fun rewrite_prems [] = Conv.all_conv
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   335
      | rewrite_prems (x::xs) = Conv.implies_conv (rewrite_prem x) (rewrite_prems xs)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   336
    
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   337
    val rewrite_prems_conv = rewrite_prems prems_pairs
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   338
    val rewrite_concl_conv = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   339
      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def})))
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   340
  in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   341
    (Conv.fconv_rule (rewrite_prems_conv then_conv rewrite_concl_conv)) rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   342
  end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   343
  handle 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   344
    TERM _ => error "The rule has a wrong format."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   345
    | CTERM _ => error "The rule has a wrong format."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   346
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   347
fun negate_mono_rule mono_rule = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   348
  let
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   349
    val rewr_conv = HOLogic.Trueprop_conv (Conv.rewrs_conv [@{thm POS_NEG}, @{thm NEG_POS}])
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   350
  in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   351
    Conv.fconv_rule (Conv.prems_conv ~1 rewr_conv then_conv Conv.concl_conv ~1 rewr_conv) mono_rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   352
  end;
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   353
55563
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   354
fun add_reflexivity_rules mono_rule ctxt =
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   355
  let
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   356
    fun find_eq_rule thm ctxt =
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   357
      let
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   358
        val concl_rhs = (hd o get_args 1 o HOLogic.dest_Trueprop o concl_of) thm;
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   359
        val rules = Item_Net.retrieve (Transfer.get_relator_eq_item_net ctxt) concl_rhs;
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   360
      in
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   361
        find_first (fn thm => Pattern.matches (Proof_Context.theory_of ctxt) (concl_rhs, 
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   362
          (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.concl_of) thm)) rules
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   363
      end
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   364
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   365
    val eq_rule = find_eq_rule mono_rule (Context.proof_of ctxt);
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   366
    val eq_rule = if is_some eq_rule then the eq_rule else error 
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   367
      "No corresponding rule that the relator preserves equality was found."
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   368
  in
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   369
    ctxt
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   370
    |> add_reflexivity_rule (Drule.zero_var_indexes (@{thm ord_le_eq_trans} OF [mono_rule, eq_rule]))
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   371
    |> add_reflexivity_rule 
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   372
      (Drule.zero_var_indexes (@{thm ord_eq_le_trans} OF [sym OF [eq_rule], mono_rule]))
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   373
  end
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   374
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   375
fun add_mono_rule mono_rule ctxt = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   376
  let
55563
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   377
    val pol_mono_rule = introduce_polarities mono_rule
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   378
    val mono_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
55563
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   379
      dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) pol_mono_rule
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   380
    val _ = if Symtab.defined (get_relator_distr_data' ctxt) mono_ruleT_name 
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   381
      then error ("Monotocity rule for type " ^ quote mono_ruleT_name ^ " is already_defined.")
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   382
      else ()
55563
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   383
    val neg_mono_rule = negate_mono_rule pol_mono_rule
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   384
    val relator_distr_data = {pos_mono_rule = pol_mono_rule, neg_mono_rule = neg_mono_rule, 
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   385
      pos_distr_rules = [], neg_distr_rules = []}
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   386
  in
55563
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   387
    ctxt 
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   388
    |> Data.map (map_relator_distr_data (Symtab.update (mono_ruleT_name, relator_distr_data)))
a64d49f49ca3 implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
kuncar
parents: 53754
diff changeset
   389
    |> add_reflexivity_rules mono_rule
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   390
  end;
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   391
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   392
local 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   393
  fun add_distr_rule update_entry distr_rule ctxt =
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   394
    let
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   395
      val distr_ruleT_name = (fst o dest_Type o fst o relation_types o fst o relation_types o snd o 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   396
        dest_Const o head_of o HOLogic.dest_Trueprop o concl_of) distr_rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   397
    in
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   398
      if Symtab.defined (get_relator_distr_data' ctxt) distr_ruleT_name then 
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   399
        Data.map (map_relator_distr_data (Symtab.map_entry distr_ruleT_name (update_entry distr_rule))) 
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   400
          ctxt
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   401
      else error "The monoticity rule is not defined."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   402
    end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   403
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   404
    fun rewrite_concl_conv thm ctm = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   405
      Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric thm))) ctm
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   406
      handle CTERM _ => error "The rule has a wrong format."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   407
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   408
in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   409
  fun add_pos_distr_rule distr_rule ctxt = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   410
    let
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   411
      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm POS_def}) distr_rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   412
      fun update_entry distr_rule data = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   413
        map_pos_distr_rules (cons (@{thm POS_trans} OF [distr_rule, #pos_mono_rule data])) data
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   414
    in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   415
      add_distr_rule update_entry distr_rule ctxt
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   416
    end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   417
    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   418
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   419
  
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   420
  fun add_neg_distr_rule distr_rule ctxt = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   421
    let
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   422
      val distr_rule = Conv.fconv_rule (rewrite_concl_conv @{thm NEG_def}) distr_rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   423
      fun update_entry distr_rule data = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   424
        map_neg_distr_rules (cons (@{thm NEG_trans} OF [distr_rule, #neg_mono_rule data])) data
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   425
    in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   426
      add_distr_rule update_entry distr_rule ctxt
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   427
    end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   428
    handle THM _ => error "Combining of the distr. rule and the monotonicity rule together has failed."
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   429
end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   430
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   431
local 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   432
  val eq_refl2 = sym RS @{thm eq_refl}
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   433
in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   434
  fun add_eq_distr_rule distr_rule ctxt =
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   435
    let 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   436
      val pos_distr_rule = @{thm eq_refl} OF [distr_rule]
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   437
      val neg_distr_rule = eq_refl2 OF [distr_rule]
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   438
    in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   439
      ctxt 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   440
      |> add_pos_distr_rule pos_distr_rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   441
      |> add_neg_distr_rule neg_distr_rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   442
    end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   443
end;
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   444
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   445
local
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   446
  fun sanity_check rule =
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   447
    let
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   448
      val assms = map (perhaps (try HOLogic.dest_Trueprop)) (prems_of rule)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   449
      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of rule);
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   450
      val (lhs, rhs) =
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   451
        (case concl of
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   452
          Const (@{const_name less_eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   453
            (lhs, rhs)
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   454
        | Const (@{const_name less_eq}, _) $ rhs $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) =>
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   455
            (lhs, rhs)
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   456
        | Const (@{const_name HOL.eq}, _) $ (lhs as Const (@{const_name relcompp},_) $ _ $ _) $ rhs =>
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   457
            (lhs, rhs)
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   458
        | _ => error "The rule has a wrong format.")
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   459
      
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   460
      val lhs_vars = Term.add_vars lhs []
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   461
      val rhs_vars = Term.add_vars rhs []
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   462
      val assms_vars = fold Term.add_vars assms [];
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   463
      val _ =
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   464
        if has_duplicates op= lhs_vars
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   465
        then error "Left-hand side has variable duplicates" else ()
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   466
      val _ =
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   467
        if subset op= (rhs_vars, lhs_vars) then () 
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   468
        else error "Extra variables in the right-hand side of the rule"
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   469
      val _ =
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   470
        if subset op= (assms_vars, lhs_vars) then () 
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   471
        else error "Extra variables in the assumptions of the rule"
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   472
      val rhs_args = (snd o strip_comb) rhs;
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   473
      fun check_comp t =
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   474
        (case t of
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   475
          Const (@{const_name relcompp}, _) $ Var _ $ Var _ => ()
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   476
        | _ => error "There is an argument on the rhs that is not a composition.")
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   477
      val _ = map check_comp rhs_args
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   478
    in () end
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   479
in
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   480
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   481
  fun add_distr_rule distr_rule ctxt = 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   482
    let
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   483
      val _ = sanity_check distr_rule
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   484
      val concl = (perhaps (try HOLogic.dest_Trueprop)) (concl_of distr_rule)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   485
    in
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   486
      (case concl of
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   487
        Const (@{const_name less_eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   488
          add_pos_distr_rule distr_rule ctxt
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   489
      | Const (@{const_name less_eq}, _) $ _ $ (Const (@{const_name relcompp},_) $ _ $ _) =>
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   490
          add_neg_distr_rule distr_rule ctxt
56257
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   491
      | Const (@{const_name HOL.eq}, _) $ (Const (@{const_name relcompp},_) $ _ $ _) $ _ =>
589fafcc7cb6 more antiquotations;
wenzelm
parents: 55731
diff changeset
   492
          add_eq_distr_rule distr_rule ctxt)
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   493
    end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   494
end
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   495
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   496
fun get_distr_rules_raw ctxt = Symtab.fold 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   497
  (fn (_, {pos_distr_rules, neg_distr_rules, ...}) => fn rules => pos_distr_rules @ neg_distr_rules @ rules) 
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   498
    (get_relator_distr_data' ctxt) []
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   499
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   500
fun get_mono_rules_raw ctxt = Symtab.fold 
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   501
  (fn (_, {pos_mono_rule, neg_mono_rule, ...}) => fn rules => [pos_mono_rule, neg_mono_rule] @ rules) 
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   502
    (get_relator_distr_data' ctxt) []
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   503
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   504
val lookup_relator_distr_data = Symtab.lookup o get_relator_distr_data
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   505
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   506
val relator_distr_attribute_setup =
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   507
  Attrib.setup @{binding relator_mono} (Scan.succeed (Thm.declaration_attribute add_mono_rule))
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   508
    "declaration of relator's monoticity"
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   509
  #> Attrib.setup @{binding relator_distr} (Scan.succeed (Thm.declaration_attribute add_distr_rule))
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   510
    "declaration of relator's distributivity over OO"
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   511
  #> Global_Theory.add_thms_dynamic
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   512
     (@{binding relator_distr_raw}, get_distr_rules_raw)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   513
  #> Global_Theory.add_thms_dynamic
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   514
     (@{binding relator_mono_raw}, get_mono_rules_raw)
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   515
57663
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   516
(* no_code types *)
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   517
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   518
fun add_no_code_type type_name ctxt = 
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   519
  Data.map (map_no_code_types (Symtab.update (type_name, ()))) ctxt;
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   520
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   521
fun is_no_code_type ctxt type_name = (Symtab.defined o get_no_code_types) ctxt type_name
b590fcd03a4a store explicitly quotient types with no_code => more precise registration of code equations
kuncar
parents: 56519
diff changeset
   522
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   523
(* theory setup *)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   524
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   525
val setup =
47951
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   526
  quot_map_attribute_setup
8c8a03765de7 quot_del attribute, it allows us to deregister quotient types
kuncar
parents: 47936
diff changeset
   527
  #> quot_del_attribute_setup
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   528
  #> Relator_Eq_Onp.setup
51374
84d01fd733cf lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
kuncar
parents: 50227
diff changeset
   529
  #> relator_distr_attribute_setup
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   530
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   531
(* setup fixed eq_onp rules *)
55731
66df76dd2640 rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents: 55563
diff changeset
   532
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   533
val _ = Context.>> (fold (Relator_Eq_Onp.add_thm o Transfer.prep_transfer_domain_thm @{context}) 
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   534
  @{thms composed_equiv_rel_eq_onp composed_equiv_rel_eq_eq_onp})
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56257
diff changeset
   535
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56257
diff changeset
   536
(* setup fixed reflexivity rules *)
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56257
diff changeset
   537
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56257
diff changeset
   538
val _ = Context.>> (fold add_reflexivity_rule 
56519
c1048f5bbb45 more appropriate name (Lifting.invariant -> eq_onp)
kuncar
parents: 56518
diff changeset
   539
  @{thms order_refl[of "op="] eq_onp_le_eq Quotient_composition_le_eq Quotient_composition_ge_eq
56518
beb3b6851665 left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
kuncar
parents: 56257
diff changeset
   540
    bi_unique_OO bi_total_OO right_unique_OO right_total_OO left_unique_OO left_total_OO})
55731
66df76dd2640 rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
kuncar
parents: 55563
diff changeset
   541
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   542
(* outer syntax commands *)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   543
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   544
val _ =
53219
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   545
  Outer_Syntax.improper_command @{command_spec "print_quot_maps"} "print quotient map functions"
ca237b9e4542 use only one data slot; rename print_quotmaps to print_quot_maps; tuned
kuncar
parents: 51994
diff changeset
   546
    (Scan.succeed (Toplevel.keep (print_quot_maps o Toplevel.context_of)))
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   547
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   548
val _ =
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   549
  Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   550
    (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
9caab698dbe4 new package Lifting - initial commit
kuncar
parents:
diff changeset
   551
53651
ee90c67502c9 restoring Transfer/Lifting context
kuncar
parents: 53650
diff changeset
   552
end