diff -r a7462e442e35 -r 6d19301074cf src/HOL/Tools/type_lifting.ML --- a/src/HOL/Tools/type_lifting.ML Mon Jan 10 22:03:24 2011 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,256 +0,0 @@ -(* Title: HOL/Tools/type_lifting.ML - Author: Florian Haftmann, TU Muenchen - -Functorial structure of types. -*) - -signature TYPE_LIFTING = -sig - val find_atomic: Proof.context -> typ -> (typ * (bool * bool)) list - val construct_mapper: Proof.context -> (string * bool -> term) - -> bool -> typ -> typ -> term - val type_lifting: string option -> term -> local_theory -> Proof.state - type entry - val entries: Proof.context -> entry list Symtab.table -end; - -structure Type_Lifting : TYPE_LIFTING = -struct - -(* bookkeeping *) - -val compN = "comp"; -val idN = "id"; -val compositionalityN = "compositionality"; -val identityN = "identity"; - -type entry = { mapper: term, variances: (sort * (bool * bool)) list, - comp: thm, id: thm }; - -structure Data = Generic_Data -( - type T = entry list Symtab.table - val empty = Symtab.empty - val extend = I - fun merge data = Symtab.merge (K true) data -); - -val entries = Data.get o Context.Proof; - - -(* type analysis *) - -fun term_with_typ ctxt T t = Envir.subst_term_types - (Type.typ_match (ProofContext.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t; - -fun find_atomic ctxt T = - let - val variances_of = Option.map #variances o try hd o Symtab.lookup_list (entries ctxt); - fun add_variance is_contra T = - AList.map_default (op =) (T, (false, false)) - ((if is_contra then apsnd else apfst) (K true)); - fun analyze' is_contra (_, (co, contra)) T = - (if co then analyze is_contra T else I) - #> (if contra then analyze (not is_contra) T else I) - and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco - of NONE => add_variance is_contra T - | SOME variances => fold2 (analyze' is_contra) variances Ts) - | analyze is_contra T = add_variance is_contra T; - in analyze false T [] end; - -fun construct_mapper ctxt atomic = - let - val lookup = hd o Symtab.lookup_list (entries ctxt); - fun constructs is_contra (_, (co, contra)) T T' = - (if co then [construct is_contra T T'] else []) - @ (if contra then [construct (not is_contra) T T'] else []) - and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) = - let - val { mapper = raw_mapper, variances, ... } = lookup tyco; - val args = maps (fn (arg_pattern, (T, T')) => - constructs is_contra arg_pattern T T') - (variances ~~ (Ts ~~ Ts')); - val (U, U') = if is_contra then (T', T) else (T, T'); - val mapper = term_with_typ ctxt (map fastype_of args ---> U --> U') raw_mapper; - in list_comb (mapper, args) end - | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra); - in construct end; - - -(* mapper properties *) - -val compositionality_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm comp_def}) HOL_basic_ss; - -fun make_comp_prop ctxt variances (tyco, mapper) = - let - val sorts = map fst variances - val (((vs3, vs2), vs1), _) = ctxt - |> Variable.invent_types sorts - ||>> Variable.invent_types sorts - ||>> Variable.invent_types sorts - val (Ts1, Ts2, Ts3) = (map TFree vs1, map TFree vs2, map TFree vs3); - fun mk_argT ((T, T'), (_, (co, contra))) = - (if co then [(T --> T')] else []) - @ (if contra then [(T' --> T)] else []); - val contras = maps (fn (_, (co, contra)) => - (if co then [false] else []) @ (if contra then [true] else [])) variances; - val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances); - val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances); - fun invents n k nctxt = - let - val names = Name.invents nctxt n k; - in (names, fold Name.declare names nctxt) end; - val ((names21, names32), nctxt) = Variable.names_of ctxt - |> invents "f" (length Ts21) - ||>> invents "f" (length Ts32); - val T1 = Type (tyco, Ts1); - val T2 = Type (tyco, Ts2); - val T3 = Type (tyco, Ts3); - val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32); - val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) => - if not is_contra then - HOLogic.mk_comp (Free (f21, T21), Free (f32, T32)) - else - HOLogic.mk_comp (Free (f32, T32), Free (f21, T21)) - ) contras (args21 ~~ args32) - fun mk_mapper T T' args = list_comb - (term_with_typ ctxt (map fastype_of args ---> T --> T') mapper, args); - val mapper21 = mk_mapper T2 T1 (map Free args21); - val mapper32 = mk_mapper T3 T2 (map Free args32); - val mapper31 = mk_mapper T3 T1 args31; - val eq1 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) - (HOLogic.mk_comp (mapper21, mapper32), mapper31); - val x = Free (the_single (Name.invents nctxt (Long_Name.base_name tyco) 1), T3) - val eq2 = (HOLogic.mk_Trueprop o HOLogic.mk_eq) - (mapper21 $ (mapper32 $ x), mapper31 $ x); - val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1; - val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2; - fun prove_compositionality ctxt comp_thm = Skip_Proof.prove ctxt [] [] compositionality_prop - (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]] - THEN' Simplifier.asm_lr_simp_tac compositionality_ss - THEN_ALL_NEW (Goal.assume_rule_tac ctxt)))); - in (comp_prop, prove_compositionality) end; - -val identity_ss = Simplifier.add_simp (Simpdata.mk_eq @{thm id_def}) HOL_basic_ss; - -fun make_id_prop ctxt variances (tyco, mapper) = - let - val (vs, ctxt') = Variable.invent_types (map fst variances) ctxt; - val Ts = map TFree vs; - fun bool_num b = if b then 1 else 0; - fun mk_argT (T, (_, (co, contra))) = - replicate (bool_num co + bool_num contra) T - val arg_Ts = maps mk_argT (Ts ~~ variances) - val T = Type (tyco, Ts); - val head = term_with_typ ctxt (map (fn T => T --> T) arg_Ts ---> T --> T) mapper; - val lhs1 = list_comb (head, map (HOLogic.id_const) arg_Ts); - val lhs2 = list_comb (head, map (fn arg_T => Abs ("x", arg_T, Bound 0)) arg_Ts); - val rhs = HOLogic.id_const T; - val (id_prop, identity_prop) = pairself - (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2); - fun prove_identity ctxt id_thm = Skip_Proof.prove ctxt [] [] identity_prop - (K (ALLGOALS (Method.insert_tac [id_thm] THEN' Simplifier.asm_lr_simp_tac identity_ss))); - in (id_prop, prove_identity) end; - - -(* analyzing and registering mappers *) - -fun consume eq x [] = (false, []) - | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys); - -fun split_mapper_typ "fun" T = - let - val (Ts', T') = strip_type T; - val (Ts'', T'') = split_last Ts'; - val (Ts''', T''') = split_last Ts''; - in (Ts''', T''', T'' --> T') end - | split_mapper_typ tyco T = - let - val (Ts', T') = strip_type T; - val (Ts'', T'') = split_last Ts'; - in (Ts'', T'', T') end; - -fun analyze_variances ctxt tyco T = - let - fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T); - val (Ts, T1, T2) = split_mapper_typ tyco T - handle List.Empty => bad_typ (); - val _ = pairself - ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2) - handle TYPE _ => bad_typ (); - val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2) - handle TYPE _ => bad_typ (); - val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2) - then bad_typ () else (); - fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) = - let - val coT = TFree var1 --> TFree var2; - val contraT = TFree var2 --> TFree var1; - val sort = Sign.inter_sort (ProofContext.theory_of ctxt) (sort1, sort2); - in - consume (op =) coT - ##>> consume (op =) contraT - #>> pair sort - end; - val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts; - val _ = if null left_variances then () else bad_typ (); - in variances end; - -fun gen_type_lifting prep_term some_prfx raw_mapper lthy = - let - val input_mapper = prep_term lthy raw_mapper; - val T = fastype_of input_mapper; - val _ = Type.no_tvars T; - val mapper = singleton (Variable.polymorphic lthy) input_mapper; - val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then () - else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T); - fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts - | add_tycos _ = I; - val tycos = add_tycos T []; - val tyco = if tycos = ["fun"] then "fun" - else case remove (op =) "fun" tycos - of [tyco] => tyco - | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ lthy T); - val prfx = the_default (Long_Name.base_name tyco) some_prfx; - val variances = analyze_variances lthy tyco T; - val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper); - val (id_prop, prove_identity) = make_id_prop lthy variances (tyco, mapper); - val qualify = Binding.qualify true prfx o Binding.name; - fun mapper_declaration comp_thm id_thm phi context = - let - val typ_instance = Type.typ_instance (ProofContext.tsig_of (Context.proof_of context)); - val mapper' = Morphism.term phi mapper; - val T_T' = pairself fastype_of (mapper, mapper'); - in if typ_instance T_T' andalso typ_instance (swap T_T') - then (Data.map o Symtab.cons_list) (tyco, - { mapper = mapper', variances = variances, - comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context - else context - end; - fun after_qed [single_comp_thm, single_id_thm] lthy = - lthy - |> Local_Theory.note ((qualify compN, []), single_comp_thm) - ||>> Local_Theory.note ((qualify idN, []), single_id_thm) - |-> (fn ((_, [comp_thm]), (_, [id_thm])) => fn lthy => - lthy - |> Local_Theory.note ((qualify compositionalityN, []), - [prove_compositionality lthy comp_thm]) - |> snd - |> Local_Theory.note ((qualify identityN, []), - [prove_identity lthy id_thm]) - |> snd - |> Local_Theory.declaration false (mapper_declaration comp_thm id_thm)) - in - lthy - |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop]) - end - -val type_lifting = gen_type_lifting Syntax.check_term; -val type_lifting_cmd = gen_type_lifting Syntax.read_term; - -val _ = Outer_Syntax.local_theory_to_proof "type_lifting" - "register operations managing the functorial structure of a type" - Keyword.thy_goal (Scan.option (Parse.name --| Parse.$$$ ":") -- Parse.term - >> (fn (prfx, t) => type_lifting_cmd prfx t)); - -end;