modernized setup;
authorwenzelm
Wed Oct 29 15:28:27 2014 +0100 (2014-10-29)
changeset 58824d480d1d7c544
parent 58823 513268cb2178
child 58825 2065f49da190
modernized setup;
src/HOL/Nat_Transfer.thy
src/HOL/Tools/legacy_transfer.ML
     1.1 --- a/src/HOL/Nat_Transfer.thy	Wed Oct 29 15:15:17 2014 +0100
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Wed Oct 29 15:28:27 2014 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4    by (simp add: transfer_morphism_def)
     1.5  
     1.6  ML_file "Tools/legacy_transfer.ML"
     1.7 -setup Legacy_Transfer.setup
     1.8  
     1.9  
    1.10  subsection {* Set up transfer from nat to int *}
     2.1 --- a/src/HOL/Tools/legacy_transfer.ML	Wed Oct 29 15:15:17 2014 +0100
     2.2 +++ b/src/HOL/Tools/legacy_transfer.ML	Wed Oct 29 15:28:27 2014 +0100
     2.3 @@ -14,7 +14,6 @@
     2.4    val add: thm -> bool -> entry -> Context.generic -> Context.generic
     2.5    val del: thm -> entry -> Context.generic -> Context.generic
     2.6    val drop: thm -> Context.generic -> Context.generic
     2.7 -  val setup: theory -> theory
     2.8  end;
     2.9  
    2.10  structure Legacy_Transfer : LEGACY_TRANSFER =
    2.11 @@ -112,7 +111,7 @@
    2.12      val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
    2.13      val T = Thm.typ_of (Thm.ctyp_of_term a);
    2.14      val (aT, bT) = (Term.range_type T, Term.domain_type T);
    2.15 -    
    2.16 +
    2.17      (* determine variables to transfer *)
    2.18      val ctxt3 = ctxt2
    2.19        |> Variable.declare_thm thm
    2.20 @@ -168,7 +167,7 @@
    2.21        cong = union Thm.eq_thm cong1 cong2, hints = union (op =) hints1 hints2 }
    2.22    end;
    2.23  
    2.24 -fun diminish_entry 
    2.25 +fun diminish_entry
    2.26      { inj = inj0, embed = embed0, return = return0, cong = cong0, hints = hints0 }
    2.27      { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
    2.28    { inj = subtract Thm.eq_thm inj0 inj2, embed = subtract Thm.eq_thm embed0 embed2,
    2.29 @@ -243,28 +242,23 @@
    2.30  
    2.31  in
    2.32  
    2.33 -val transfer_attribute = keyword delN >> K (Thm.declaration_attribute drop)
    2.34 -  || keyword addN |-- Scan.optional mode true -- entry_pair
    2.35 -    >> (fn (guess, (entry_add, entry_del)) => Thm.declaration_attribute
    2.36 -      (fn thm => add thm guess entry_add #> del thm entry_del))
    2.37 -  || keyword_colon keyN |-- Attrib.thm
    2.38 -    >> (fn key => Thm.declaration_attribute
    2.39 -      (fn thm => add key false
    2.40 -        { inj = [], embed = [], return = [thm], cong = [], hints = [] }));
    2.41 -
    2.42 -val transferred_attribute = selection -- these (keyword_colon leavingN |-- names)
    2.43 -  >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
    2.44 -      Conjunction.intr_balanced o transfer context selection leave));
    2.45 +val _ =
    2.46 +  Theory.setup
    2.47 +   (Attrib.setup @{binding transfer}
    2.48 +      (keyword delN >> K (Thm.declaration_attribute drop)
    2.49 +    || keyword addN |-- Scan.optional mode true -- entry_pair
    2.50 +      >> (fn (guess, (entry_add, entry_del)) =>
    2.51 +          Thm.declaration_attribute (fn thm => add thm guess entry_add #> del thm entry_del))
    2.52 +    || keyword_colon keyN |-- Attrib.thm
    2.53 +      >> (fn key => Thm.declaration_attribute (fn thm =>
    2.54 +            add key false { inj = [], embed = [], return = [thm], cong = [], hints = [] })))
    2.55 +    "install transfer data" #>
    2.56 +    Attrib.setup @{binding transferred}
    2.57 +      (selection -- these (keyword_colon leavingN |-- names)
    2.58 +        >> (fn (selection, leave) => Thm.rule_attribute (fn context =>
    2.59 +              Conjunction.intr_balanced o transfer context selection leave)))
    2.60 +    "transfer theorems");
    2.61  
    2.62  end;
    2.63  
    2.64 -
    2.65 -(* theory setup *)
    2.66 -
    2.67 -val setup =
    2.68 -  Attrib.setup @{binding transfer} transfer_attribute
    2.69 -    "Installs transfer data" #>
    2.70 -  Attrib.setup @{binding transferred} transferred_attribute
    2.71 -    "Transfers theorems";
    2.72 -
    2.73  end;