1(* Title: Pure/morphism.ML 2 Author: Makarius 3 4Abstract morphisms on formal entities. 5*) 6 7infix 1 $> 8 9signature BASIC_MORPHISM = 10sig 11 type morphism 12 type declaration = morphism -> Context.generic -> Context.generic 13 val $> : morphism * morphism -> morphism 14end 15 16signature MORPHISM = 17sig 18 include BASIC_MORPHISM 19 exception MORPHISM of string * exn 20 val morphism: string -> 21 {binding: (binding -> binding) list, 22 typ: (typ -> typ) list, 23 term: (term -> term) list, 24 fact: (thm list -> thm list) list} -> morphism 25 val pretty: morphism -> Pretty.T 26 val binding: morphism -> binding -> binding 27 val binding_prefix: morphism -> (string * bool) list 28 val typ: morphism -> typ -> typ 29 val term: morphism -> term -> term 30 val fact: morphism -> thm list -> thm list 31 val thm: morphism -> thm -> thm 32 val cterm: morphism -> cterm -> cterm 33 val identity: morphism 34 val compose: morphism -> morphism -> morphism 35 val transform: morphism -> (morphism -> 'a) -> morphism -> 'a 36 val form: (morphism -> 'a) -> 'a 37 val binding_morphism: string -> (binding -> binding) -> morphism 38 val typ_morphism: string -> (typ -> typ) -> morphism 39 val term_morphism: string -> (term -> term) -> morphism 40 val fact_morphism: string -> (thm list -> thm list) -> morphism 41 val thm_morphism: string -> (thm -> thm) -> morphism 42 val transfer_morphism: theory -> morphism 43 val transfer_morphism': Proof.context -> morphism 44 val transfer_morphism'': Context.generic -> morphism 45 val trim_context_morphism: morphism 46 val instantiate_frees_morphism: 47 ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism 48 val instantiate_morphism: 49 ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism 50end; 51 52structure Morphism: MORPHISM = 53struct 54 55(* named functions *) 56 57type 'a funs = (string * ('a -> 'a)) list; 58 59exception MORPHISM of string * exn; 60 61fun app (name, f) x = f x 62 handle exn => 63 if Exn.is_interrupt exn then Exn.reraise exn else raise MORPHISM (name, exn); 64 65fun apply fs = fold_rev app fs; 66 67 68(* type morphism *) 69 70datatype morphism = Morphism of 71 {names: string list, 72 binding: binding funs, 73 typ: typ funs, 74 term: term funs, 75 fact: thm list funs}; 76 77type declaration = morphism -> Context.generic -> Context.generic; 78 79fun morphism a {binding, typ, term, fact} = 80 Morphism { 81 names = if a = "" then [] else [a], 82 binding = map (pair a) binding, 83 typ = map (pair a) typ, 84 term = map (pair a) term, 85 fact = map (pair a) fact}; 86 87fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names)); 88 89val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty); 90 91fun binding (Morphism {binding, ...}) = apply binding; 92fun binding_prefix morph = Binding.name "x" |> binding morph |> Binding.prefix_of; 93fun typ (Morphism {typ, ...}) = apply typ; 94fun term (Morphism {term, ...}) = apply term; 95fun fact (Morphism {fact, ...}) = apply fact; 96val thm = singleton o fact; 97val cterm = Drule.cterm_rule o thm; 98 99 100(* morphism combinators *) 101 102val identity = morphism "" {binding = [], typ = [], term = [], fact = []}; 103 104fun compose 105 (Morphism {names = names1, binding = binding1, typ = typ1, term = term1, fact = fact1}) 106 (Morphism {names = names2, binding = binding2, typ = typ2, term = term2, fact = fact2}) = 107 Morphism { 108 names = names1 @ names2, 109 binding = binding1 @ binding2, 110 typ = typ1 @ typ2, 111 term = term1 @ term2, 112 fact = fact1 @ fact2}; 113 114fun phi1 $> phi2 = compose phi2 phi1; 115 116fun transform phi f = fn psi => f (phi $> psi); 117fun form f = f identity; 118 119 120(* concrete morphisms *) 121 122fun binding_morphism a binding = morphism a {binding = [binding], typ = [], term = [], fact = []}; 123fun typ_morphism a typ = morphism a {binding = [], typ = [typ], term = [], fact = []}; 124fun term_morphism a term = morphism a {binding = [], typ = [], term = [term], fact = []}; 125fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]}; 126fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]}; 127 128val transfer_morphism = thm_morphism "transfer" o Thm.join_transfer; 129val transfer_morphism' = transfer_morphism o Proof_Context.theory_of; 130val transfer_morphism'' = transfer_morphism o Context.theory_of; 131 132val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context; 133 134 135(* instantiate *) 136 137fun instantiate_frees_morphism ([], []) = identity 138 | instantiate_frees_morphism (cinstT, cinst) = 139 let 140 val instT = map (apsnd Thm.typ_of) cinstT; 141 val inst = map (apsnd Thm.term_of) cinst; 142 in 143 morphism "instantiate_frees" 144 {binding = [], 145 typ = if null instT then [] else [Term_Subst.instantiateT_frees instT], 146 term = [Term_Subst.instantiate_frees (instT, inst)], 147 fact = [map (Thm.instantiate_frees (cinstT, cinst))]} 148 end; 149 150fun instantiate_morphism ([], []) = identity 151 | instantiate_morphism (cinstT, cinst) = 152 let 153 val instT = map (apsnd Thm.typ_of) cinstT; 154 val inst = map (apsnd Thm.term_of) cinst; 155 in 156 morphism "instantiate" 157 {binding = [], 158 typ = if null instT then [] else [Term_Subst.instantiateT instT], 159 term = [Term_Subst.instantiate (instT, inst)], 160 fact = [map (Thm.instantiate (cinstT, cinst))]} 161 end; 162 163end; 164 165structure Basic_Morphism: BASIC_MORPHISM = Morphism; 166open Basic_Morphism; 167