src/Pure/Isar/expression.ML
changeset 28903 b3fc3a62247a
parent 28902 2019bcc9d8bf
child 28936 f1647bf418f5
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Nov 28 12:26:14 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Nov 28 17:43:06 2008 +0100
     1.3 @@ -598,15 +598,17 @@
     1.4  
     1.5  (*** Locale declarations ***)
     1.6  
     1.7 +(* axiomsN: name of theorem set with destruct rules for locale predicates,
     1.8 +     also name suffix of delta predicates and assumptions. *)
     1.9 +
    1.10 +val axiomsN = "axioms";
    1.11 +
    1.12  local
    1.13  
    1.14  (* introN: name of theorems for introduction rules of locale and
    1.15 -     delta predicates;
    1.16 -   axiomsN: name of theorem set with destruct rules for locale predicates,
    1.17 -     also name suffix of delta predicates. *)
    1.18 +     delta predicates *)
    1.19  
    1.20  val introN = "intro";
    1.21 -val axiomsN = "axioms";
    1.22  
    1.23  fun atomize_spec thy ts =
    1.24    let
    1.25 @@ -695,7 +697,8 @@
    1.26              thy'
    1.27              |> Sign.add_path aname
    1.28              |> Sign.no_base_names
    1.29 -            |> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])]
    1.30 +            |> PureThy.note_thmss Thm.internalK
    1.31 +              [((Name.binding introN, []), [([intro], [NewLocale.unfold_attrib])])]
    1.32              ||> Sign.restore_naming thy';
    1.33            in (SOME statement, SOME intro, axioms, thy'') end;
    1.34      val (b_pred, b_intro, b_axioms, thy'''') =
    1.35 @@ -710,7 +713,7 @@
    1.36              |> Sign.add_path pname
    1.37              |> Sign.no_base_names
    1.38              |> PureThy.note_thmss Thm.internalK
    1.39 -                 [((Name.binding introN, []), [([intro], [])]),
    1.40 +                 [((Name.binding introN, []), [([intro], [NewLocale.intro_attrib])]),
    1.41                    ((Name.binding axiomsN, []),
    1.42                      [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
    1.43              ||> Sign.restore_naming thy''';
    1.44 @@ -757,20 +760,25 @@
    1.45        else warning ("Additional type variable(s) in locale specification " ^ quote bname);
    1.46  
    1.47      val satisfy = Element.satisfy_morphism b_axioms;
    1.48 +
    1.49      val params = fixed @
    1.50        (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
    1.51 -    val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems [];
    1.52 -
    1.53 +    val asm = if is_some b_statement then b_statement else a_statement;
    1.54 +    val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems [];
    1.55      val notes = body_elems' |>
    1.56        (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
    1.57        fst |> map (Element.morph_ctxt satisfy) |>
    1.58 -      map_filter (fn Notes notes => SOME notes | _ => NONE);
    1.59 +      map_filter (fn Notes notes => SOME notes | _ => NONE) |>
    1.60 +      (if is_some asm
    1.61 +        then cons (Thm.internalK, [((Name.binding (bname ^ "_" ^ axiomsN), []),
    1.62 +          [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
    1.63 +        else I);
    1.64  
    1.65      val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
    1.66  
    1.67      val loc_ctxt = thy' |>
    1.68        NewLocale.register_locale name (extraTs, params)
    1.69 -        (if is_some b_statement then b_statement else a_statement, map prop_of defs) ([], [])
    1.70 +        (asm, map prop_of defs) ([], [])
    1.71          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
    1.72        NewLocale.init name
    1.73    in (name, loc_ctxt) end;
    1.74 @@ -803,10 +811,10 @@
    1.75      val target = intern thy raw_target;
    1.76      val target_ctxt = NewLocale.init target thy;
    1.77  
    1.78 -    val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt;
    1.79 +    val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
    1.80      
    1.81      fun store_dep ((name, morph), thms) =
    1.82 -      NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export');
    1.83 +      NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
    1.84  
    1.85      fun after_qed' results =
    1.86        fold store_dep (deps ~~ prep_result propss results) #>
    1.87 @@ -827,3 +835,4 @@
    1.88  
    1.89  
    1.90  end;
    1.91 +