1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Thu Nov 27 21:25:16 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Thu Nov 27 21:25:34 2008 +0100
     1.3 @@ -216,4 +216,47 @@
     1.4  print_locale! rgrp
     1.5  print_locale! lgrp
     1.6  
     1.7 +
     1.8 +(* locale with many parameters ---
     1.9 +   interpretations generate alternating group A5 *)
    1.10 +
    1.11 +locale A5 =
    1.12 +  fixes A and B and C and D and E
    1.13 +  assumes eq: "A <-> B <-> C <-> D <-> E"
    1.14 +
    1.15 +sublocale A5 < 1: A5 _ _ D E C
    1.16 +print_facts
    1.17 +  using eq apply (blast intro: A5.intro) done
    1.18 +
    1.19 +sublocale A5 < 2: A5 C _ E _ A
    1.20 +print_facts
    1.21 +  using eq apply (blast intro: A5.intro) done
    1.22 +
    1.23 +sublocale A5 < 3: A5 B C A _ _
    1.24 +print_facts
    1.25 +  using eq apply (blast intro: A5.intro) done
    1.26 +
    1.27 +(* Any even permutation of parameters is subsumed by the above. *)
    1.28 +
    1.29 +print_locale! A5
    1.30 +
    1.31 +
    1.32 +(* Free arguments of instance *)
    1.33 +
    1.34 +locale trivial =
    1.35 +  fixes P and Q :: o
    1.36 +  assumes Q: "P <-> P <-> Q"
    1.37 +begin
    1.38 +
    1.39 +lemma Q_triv: "Q" using Q by fast
    1.40 +
    1.41  end
    1.42 +
    1.43 +sublocale trivial < x: trivial x _
    1.44 +  apply (intro trivial.intro) using Q by fast
    1.45 +
    1.46 +print_locale! trivial
    1.47 +
    1.48 +context trivial begin thm x.Q [where ?x = True] end
    1.49 +
    1.50 +end

     2.1 --- a/src/Pure/Isar/expression.ML	Thu Nov 27 21:25:16 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Thu Nov 27 21:25:34 2008 +0100
     2.3 @@ -12,7 +12,7 @@
     2.4    type expression = string expr * (Name.binding * string option * mixfix) list;
     2.5    type expression_i = term expr * (Name.binding * typ option * mixfix) list;
     2.6  
     2.7 -  (* Processing of locale statements *)
     2.8 +  (* Processing of context statements *)
     2.9    val read_statement: Element.context list -> (string * string list) list list ->
    2.10      Proof.context ->  (term * term list) list list * Proof.context;
    2.11    val cert_statement: Element.context_i list -> (term * term list) list list ->
    2.12 @@ -499,7 +499,7 @@
    2.13           - Facts unchanged
    2.14         *)
    2.15  
    2.16 -  in ((parms, fors', deps, elems', concl), text) end
    2.17 +  in ((fors', deps, elems', concl), (parms, text)) end
    2.18  
    2.19  in
    2.20  
    2.21 @@ -512,41 +512,85 @@
    2.22  end;
    2.23  
    2.24  
    2.25 -(* full context statements: import + elements + conclusion *)
    2.26 +(* Context statement: elements + conclusion *)
    2.27  
    2.28  local
    2.29  
    2.30 -fun prep_context_statement prep_full_context_statement activate_elems
    2.31 -    strict do_close imprt elements raw_concl context =
    2.32 +fun prep_statement prep activate raw_elems raw_concl context =
    2.33 +  let
    2.34 +     val ((_, _, elems, concl), _) = prep true false context ([], []) raw_elems raw_concl;
    2.35 +     val (_, context') = activate elems (ProofContext.set_stmt true context);
    2.36 +  in (concl, context') end;
    2.37 +
    2.38 +in
    2.39 +
    2.40 +fun read_statement x = prep_statement read_full_context_statement Element.activate x;
    2.41 +fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
    2.42 +
    2.43 +end;
    2.44 +
    2.45 +
    2.46 +(* Locale declaration: import + elements *)
    2.47 +
    2.48 +local
    2.49 +
    2.50 +fun prep_declaration prep activate raw_import raw_elems context =
    2.51    let
    2.52      val thy = ProofContext.theory_of context;
    2.53  
    2.54 -    val ((parms, fixed, deps, elems, concl), (spec, (_, _, defs))) =
    2.55 -      prep_full_context_statement strict do_close context imprt elements raw_concl;
    2.56 -
    2.57 -    val (_, ctxt0) = ProofContext.add_fixes_i fixed context;
    2.58 -    val (_, ctxt) = fold (NewLocale.activate_facts thy) deps (NewLocale.empty, ctxt0);  
    2.59 -    val ((elems', _), ctxt') = activate_elems elems (ProofContext.set_stmt true ctxt);
    2.60 -  in
    2.61 -    (((fixed, deps), (ctxt', elems'), (parms, spec, defs)), concl)
    2.62 -  end;
    2.63 -
    2.64 -fun prep_statement prep_ctxt elems concl ctxt =
    2.65 -  let
    2.66 -    val (((_, (ctxt', _), _)), concl) = prep_ctxt true false ([], []) elems concl ctxt
    2.67 -  in (concl, ctxt') end;
    2.68 +    val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) =
    2.69 +      prep false true context raw_import raw_elems [];
    2.70 +    (* Declare parameters and imported facts *)
    2.71 +    val context' = context |>
    2.72 +      ProofContext.add_fixes_i fixed |> snd |>
    2.73 +      pair NewLocale.empty |> fold (NewLocale.activate_facts thy) deps |> snd;
    2.74 +    val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
    2.75 +  in ((fixed, deps, elems'), (parms, spec, defs)) end;
    2.76  
    2.77  in
    2.78  
    2.79 -fun read_statement body concl ctxt =
    2.80 -  prep_statement (prep_context_statement read_full_context_statement Element.activate) body concl ctxt;
    2.81 -fun cert_statement body concl ctxt =
    2.82 -  prep_statement (prep_context_statement cert_full_context_statement Element.activate_i) body concl ctxt;
    2.83 +fun read_declaration x = prep_declaration read_full_context_statement Element.activate x;
    2.84 +fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
    2.85  
    2.86 -fun read_context strict imprt body ctxt =
    2.87 -  #1 (prep_context_statement read_full_context_statement Element.activate strict true imprt body [] ctxt);
    2.88 -fun cert_context strict imprt body ctxt =
    2.89 -  #1 (prep_context_statement cert_full_context_statement Element.activate_i strict true imprt body [] ctxt);
    2.90 +end;
    2.91 +
    2.92 +
    2.93 +(* Locale expression to set up a goal *)
    2.94 +
    2.95 +local
    2.96 +
    2.97 +fun props_of thy (name, morph) =
    2.98 +  let
    2.99 +    val (asm, defs) = NewLocale.specification_of thy name;
   2.100 +  in
   2.101 +    (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph)
   2.102 +  end;
   2.103 +
   2.104 +fun prep_goal_expression prep expression context =
   2.105 +  let
   2.106 +    val thy = ProofContext.theory_of context;
   2.107 +
   2.108 +    val ((fixed, deps, _, _), _) = prep true true context expression [] [];
   2.109 +    (* proof obligations *)
   2.110 +    val propss = map (props_of thy) deps;
   2.111 +
   2.112 +    val goal_ctxt = context |>
   2.113 +      ProofContext.add_fixes_i fixed |> snd |>
   2.114 +      (fold o fold) Variable.auto_fixes propss;
   2.115 +
   2.116 +    val export = Variable.export_morphism goal_ctxt context;
   2.117 +    val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
   2.118 +(*    val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *)
   2.119 +    val exp_term = Drule.term_rule thy (singleton exp_fact);
   2.120 +    val exp_typ = Logic.type_map exp_term;
   2.121 +    val export' =
   2.122 +      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   2.123 +  in ((propss, deps, export'), goal_ctxt) end;
   2.124 +    
   2.125 +in
   2.126 +
   2.127 +fun read_goal_expression x = prep_goal_expression read_full_context_statement x;
   2.128 +fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
   2.129  
   2.130  end;
   2.131  
   2.132 @@ -581,7 +625,7 @@
   2.133        Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
   2.134    else raise Match);
   2.135  
   2.136 -(* CB: define one predicate including its intro rule and axioms
   2.137 +(* define one predicate including its intro rule and axioms
   2.138     - bname: predicate name
   2.139     - parms: locale parameters
   2.140     - defs: thms representing substitutions from defines elements
   2.141 @@ -694,7 +738,7 @@
   2.142      end
   2.143    | defines_to_notes _ e defns = (e, defns);
   2.144  
   2.145 -fun gen_add_locale prep_context
   2.146 +fun gen_add_locale prep_decl
   2.147      bname predicate_name raw_imprt raw_body thy =
   2.148    let
   2.149      val thy_ctxt = ProofContext.init thy;
   2.150 @@ -702,8 +746,8 @@
   2.151      val _ = NewLocale.test_locale thy name andalso
   2.152        error ("Duplicate definition of locale " ^ quote name);
   2.153  
   2.154 -    val ((fixed, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) =
   2.155 -      prep_context false raw_imprt raw_body thy_ctxt;
   2.156 +    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
   2.157 +      prep_decl raw_imprt raw_body thy_ctxt;
   2.158      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   2.159        define_preds predicate_name text thy;
   2.160  
   2.161 @@ -732,8 +776,8 @@
   2.162  
   2.163  in
   2.164  
   2.165 -val add_locale = gen_add_locale read_context;
   2.166 -val add_locale_i = gen_add_locale cert_context;
   2.167 +val add_locale = gen_add_locale read_declaration;
   2.168 +val add_locale_i = gen_add_locale cert_declaration;
   2.169  
   2.170  end;
   2.171  
   2.172 @@ -752,28 +796,17 @@
   2.173  
   2.174  local
   2.175  
   2.176 -fun store_dep target ((name, morph), thms) =
   2.177 -  NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms);
   2.178 -
   2.179  fun gen_sublocale prep_expr
   2.180      after_qed target expression thy =
   2.181    let
   2.182      val target_ctxt = NewLocale.init target thy;
   2.183      val target' = NewLocale.intern thy target;
   2.184  
   2.185 -    val ((_, fixed, deps, _, _), _) = prep_expr true true target_ctxt expression [] [];
   2.186 -    val (_, goal_ctxt) = ProofContext.add_fixes_i fixed target_ctxt;
   2.187 +    val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt;
   2.188 +    
   2.189 +    fun store_dep target ((name, morph), thms) =
   2.190 +      NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export');
   2.191  
   2.192 -    (* proof obligations from deps *)
   2.193 -    fun props_of (name, morph) =
   2.194 -    let
   2.195 -      val (asm, defs) = NewLocale.specification_of thy name;
   2.196 -    in
   2.197 -      (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph)
   2.198 -    end;
   2.199 -    
   2.200 -    val propss = map props_of deps;
   2.201 -    
   2.202      fun after_qed' results =
   2.203        fold (store_dep target') (deps ~~ prep_result propss results) #>
   2.204        after_qed results;
   2.205 @@ -786,8 +819,8 @@
   2.206  
   2.207  in
   2.208  
   2.209 -fun sublocale x = gen_sublocale read_full_context_statement x;
   2.210 -fun sublocale_i x = gen_sublocale cert_full_context_statement x;
   2.211 +fun sublocale x = gen_sublocale read_goal_expression x;
   2.212 +fun sublocale_i x = gen_sublocale cert_goal_expression x;
   2.213  
   2.214  end;
   2.215