improved calculation of morphisms and rules
authorhaftmann
Sun Jan 18 10:11:12 2009 +0100 (2009-01-18)
changeset 29547f2587922591e
parent 29546 aa8a1ed95a57
child 29549 7187373c6cb1
improved calculation of morphisms and rules
src/Pure/Isar/class.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sat Jan 17 22:08:14 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sun Jan 18 10:11:12 2009 +0100
     1.3 @@ -24,91 +24,80 @@
     1.4  
     1.5  open Class_Target;
     1.6  
     1.7 -(** rule calculation **)
     1.8 -
     1.9 -fun calculate_axiom thy sups base_sort assm_axiom param_map class =
    1.10 -  case Locale.intros_of thy class
    1.11 -   of (_, NONE) => assm_axiom
    1.12 -    | (_, SOME intro) =>
    1.13 -      let
    1.14 -        fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.15 -          (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.16 -            (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
    1.17 -              Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
    1.18 -        val axiom_premises = map_filter (fst o rules thy) sups
    1.19 -          @ the_list assm_axiom;
    1.20 -      in intro
    1.21 -        |> instantiate thy [class]
    1.22 -        |> (fn thm => thm OF axiom_premises)
    1.23 -        |> Drule.standard'
    1.24 -        |> Thm.close_derivation
    1.25 -        |> SOME
    1.26 -      end;
    1.27 -
    1.28 -fun calculate_morphism thy class sups param_map some_axiom =
    1.29 -  let
    1.30 -    val ctxt = ProofContext.init thy;
    1.31 -    val (([props], [(_, morph1)], export_morph), _) = ctxt
    1.32 -      |> Expression.cert_goal_expression ([(class, (("", false),
    1.33 -           Expression.Named ((map o apsnd) Const param_map)))], []);
    1.34 -    val morph2 = morph1
    1.35 -      $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class));
    1.36 -    val morph3 = case props
    1.37 -     of [prop] => morph2
    1.38 -          $> Element.satisfy_morphism [(Element.prove_witness ctxt prop
    1.39 -               (ALLGOALS (ProofContext.fact_tac (the_list some_axiom))))]
    1.40 -        | [] => morph2;
    1.41 -    val morph4 = morph3 $> Element.eq_morphism thy (these_defs thy sups);
    1.42 -  in (morph3, morph4, export_morph) end;
    1.43 -
    1.44 -fun calculate_rules thy morph sups base_sort param_map axiom class =
    1.45 -  let
    1.46 -    fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
    1.47 -      (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
    1.48 -        (Var ((v, 0), map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty),
    1.49 -          Const (c, map_atyps (fn _ => TVar ((Name.aT, 0), sort)) ty))) param_map);
    1.50 -    val defs = these_defs thy sups;
    1.51 -    val assm_intro = Locale.intros_of thy class
    1.52 -      |> fst
    1.53 -      |> Option.map (instantiate thy base_sort)
    1.54 -      |> Option.map (MetaSimplifier.rewrite_rule defs)
    1.55 -      |> Option.map Thm.close_derivation;
    1.56 -    val fixate = Thm.instantiate
    1.57 -      (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
    1.58 -        (TVar ((Name.aT, 0), base_sort), TFree (Name.aT, base_sort))], [])
    1.59 -    val of_class_sups = if null sups
    1.60 -      then map (fixate o Thm.class_triv thy) base_sort
    1.61 -      else map (fixate o snd o rules thy) sups;
    1.62 -    val locale_dests = map Drule.standard' (Locale.axioms_of thy class);
    1.63 -    val num_trivs = case length locale_dests
    1.64 -     of 0 => if is_none axiom then 0 else 1
    1.65 -      | n => n;
    1.66 -    val pred_trivs = if num_trivs = 0 then []
    1.67 -      else the axiom
    1.68 -        |> Thm.prop_of
    1.69 -        |> (map_types o map_atyps o K) (TFree (Name.aT, base_sort))
    1.70 -        |> (Thm.assume o Thm.cterm_of thy)
    1.71 -        |> replicate num_trivs;
    1.72 -    val axclass_intro = (#intro o AxClass.get_info thy) class;
    1.73 -    val of_class = (fixate axclass_intro OF of_class_sups OF locale_dests OF pred_trivs)
    1.74 -      |> Drule.standard'
    1.75 -      |> Thm.close_derivation;
    1.76 -  in (assm_intro, of_class) end;
    1.77 -
    1.78 -
    1.79  (** define classes **)
    1.80  
    1.81  local
    1.82  
    1.83 +fun calculate thy class sups base_sort param_map assm_axiom =
    1.84 +  let
    1.85 +    val empty_ctxt = ProofContext.init thy;
    1.86 +
    1.87 +    (* instantiation of canonical interpretation *)
    1.88 +    (*FIXME inst_morph should be calculated manually and not instantiate constraint*)
    1.89 +    val aT = TFree ("'a", base_sort);
    1.90 +    val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
    1.91 +      |> Expression.cert_goal_expression ([(class, (("", false),
    1.92 +           Expression.Named ((map o apsnd) Const param_map)))], []);
    1.93 +
    1.94 +    (* witness for canonical interpretation *)
    1.95 +    val prop = try the_single props;
    1.96 +    val wit = Option.map (fn prop => let
    1.97 +        val sup_axioms = map_filter (fst o rules thy) sups;
    1.98 +        val loc_intro_tac = case Locale.intros_of thy class
    1.99 +          of (_, NONE) => all_tac
   1.100 +           | (_, SOME intro) => ALLGOALS (Tactic.rtac intro);
   1.101 +        val tac = loc_intro_tac
   1.102 +          THEN ALLGOALS (ProofContext.fact_tac (sup_axioms @ the_list assm_axiom))
   1.103 +      in Element.prove_witness empty_ctxt prop tac end) prop;
   1.104 +    val axiom = Option.map Element.conclude_witness wit;
   1.105 +
   1.106 +    (* canonical interpretation *)
   1.107 +    val base_morph = inst_morph
   1.108 +      $> Morphism.binding_morphism
   1.109 +           (Binding.add_prefix false (class_prefix class))
   1.110 +      $> Element.satisfy_morphism (the_list wit);
   1.111 +    val defs = these_defs thy sups;
   1.112 +    val eq_morph = Element.eq_morphism thy defs;
   1.113 +    val morph = base_morph $> eq_morph;
   1.114 +
   1.115 +    (* assm_intro *)
   1.116 +    fun prove_assm_intro thm = 
   1.117 +      let
   1.118 +        val prop = thm |> Thm.prop_of |> Logic.unvarify
   1.119 +          |> Morphism.term (inst_morph $> eq_morph) 
   1.120 +          |> (map_types o map_atyps) (K aT);
   1.121 +        fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME*)
   1.122 +          THEN ALLGOALS (ProofContext.fact_tac [thm]);
   1.123 +      in Goal.prove_global thy [] [] prop (tac o #context) end;
   1.124 +    val assm_intro = Option.map prove_assm_intro
   1.125 +      (fst (Locale.intros_of thy class));
   1.126 +
   1.127 +    (* of_class *)
   1.128 +    val of_class_prop_concl = Logic.mk_inclass (aT, class);
   1.129 +    val of_class_prop = case prop of NONE => of_class_prop_concl
   1.130 +      | SOME prop => Logic.mk_implies (Morphism.term inst_morph prop,
   1.131 +          of_class_prop_concl) |> (map_types o map_atyps) (K aT)
   1.132 +    val sup_of_classes = map (snd o rules thy) sups;
   1.133 +    val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
   1.134 +    val axclass_intro = #intro (AxClass.get_info thy class);
   1.135 +    val base_sort_trivs = Drule.sort_triv thy (aT, base_sort);
   1.136 +    val tac = REPEAT (SOMEGOAL
   1.137 +      (Tactic.match_tac (axclass_intro :: sup_of_classes
   1.138 +         @ loc_axiom_intros @ base_sort_trivs)
   1.139 +           ORELSE' Tactic.assume_tac));
   1.140 +    val of_class = Goal.prove_global thy [] [] of_class_prop (K tac);
   1.141 +
   1.142 +  in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
   1.143 +
   1.144  fun gen_class_spec prep_class process_decl thy raw_supclasses raw_elems =
   1.145    let
   1.146      (*FIXME 2009 simplify*)
   1.147      val supclasses = map (prep_class thy) raw_supclasses;
   1.148      val supsort = Sign.minimize_sort thy supclasses;
   1.149 -    val sups = filter (is_class thy) supsort;
   1.150 +    val (sups, bases) = List.partition (is_class thy) supsort;
   1.151      val base_sort = if null sups then supsort else
   1.152 -      foldr1 (Sorts.inter_sort (Sign.classes_of thy))
   1.153 -        (map (base_sort thy) sups);
   1.154 +      Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
   1.155 +        (map (base_sort thy) sups, bases);
   1.156      val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   1.157      val supparam_names = map fst supparams;
   1.158      val _ = if has_duplicates (op =) supparam_names
   1.159 @@ -163,7 +152,7 @@
   1.160        end;
   1.161    in
   1.162      thy
   1.163 -    |> Sign.add_path (Logic.const_of_class bname)
   1.164 +    |> Sign.add_path (class_prefix class)
   1.165      |> fold_map add_const raw_params
   1.166      ||> Sign.restore_naming thy
   1.167      |-> (fn params => pair (supconsts @ (map o apfst) fst params, params))
   1.168 @@ -205,14 +194,11 @@
   1.169      |> snd |> LocalTheory.exit_global
   1.170      |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
   1.171      |-> (fn (param_map, params, assm_axiom) =>
   1.172 -       `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)
   1.173 -    #-> (fn axiom =>
   1.174 -       `(fn thy => calculate_morphism thy class sups param_map axiom)
   1.175 -    #-> (fn (raw_morph, morph, export_morph) => Locale.add_registration (class, (morph, export_morph))
   1.176 -    #>  Locale.activate_global_facts (class, morph $> export_morph)
   1.177 -    #> `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
   1.178 -    #-> (fn (assm_intro, of_class) =>
   1.179 -        register class sups params base_sort raw_morph axiom assm_intro of_class))))
   1.180 +       `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
   1.181 +    #-> (fn (base_morph, morph, export_morph, axiom, assm_intro, of_class) =>
   1.182 +       Locale.add_registration (class, (morph, export_morph))
   1.183 +    #> Locale.activate_global_facts (class, morph $> export_morph)
   1.184 +    #> register class sups params base_sort base_morph axiom assm_intro of_class))
   1.185      |> TheoryTarget.init (SOME class)
   1.186      |> pair class
   1.187    end;
   1.188 @@ -286,6 +272,4 @@
   1.189  
   1.190  end; (*local*)
   1.191  
   1.192 -
   1.193  end;
   1.194 -