src/Pure/Isar/expression.ML
changeset 28898 530c7d28a962
parent 28895 4e2914c2f8c5
child 28902 2019bcc9d8bf
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Nov 27 21:25:16 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Nov 27 21:25:34 2008 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    type expression = string expr * (Name.binding * string option * mixfix) list;
     1.5    type expression_i = term expr * (Name.binding * typ option * mixfix) list;
     1.6  
     1.7 -  (* Processing of locale statements *)
     1.8 +  (* Processing of context statements *)
     1.9    val read_statement: Element.context list -> (string * string list) list list ->
    1.10      Proof.context ->  (term * term list) list list * Proof.context;
    1.11    val cert_statement: Element.context_i list -> (term * term list) list list ->
    1.12 @@ -499,7 +499,7 @@
    1.13           - Facts unchanged
    1.14         *)
    1.15  
    1.16 -  in ((parms, fors', deps, elems', concl), text) end
    1.17 +  in ((fors', deps, elems', concl), (parms, text)) end
    1.18  
    1.19  in
    1.20  
    1.21 @@ -512,41 +512,85 @@
    1.22  end;
    1.23  
    1.24  
    1.25 -(* full context statements: import + elements + conclusion *)
    1.26 +(* Context statement: elements + conclusion *)
    1.27  
    1.28  local
    1.29  
    1.30 -fun prep_context_statement prep_full_context_statement activate_elems
    1.31 -    strict do_close imprt elements raw_concl context =
    1.32 +fun prep_statement prep activate raw_elems raw_concl context =
    1.33 +  let
    1.34 +     val ((_, _, elems, concl), _) = prep true false context ([], []) raw_elems raw_concl;
    1.35 +     val (_, context') = activate elems (ProofContext.set_stmt true context);
    1.36 +  in (concl, context') end;
    1.37 +
    1.38 +in
    1.39 +
    1.40 +fun read_statement x = prep_statement read_full_context_statement Element.activate x;
    1.41 +fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x;
    1.42 +
    1.43 +end;
    1.44 +
    1.45 +
    1.46 +(* Locale declaration: import + elements *)
    1.47 +
    1.48 +local
    1.49 +
    1.50 +fun prep_declaration prep activate raw_import raw_elems context =
    1.51    let
    1.52      val thy = ProofContext.theory_of context;
    1.53  
    1.54 -    val ((parms, fixed, deps, elems, concl), (spec, (_, _, defs))) =
    1.55 -      prep_full_context_statement strict do_close context imprt elements raw_concl;
    1.56 -
    1.57 -    val (_, ctxt0) = ProofContext.add_fixes_i fixed context;
    1.58 -    val (_, ctxt) = fold (NewLocale.activate_facts thy) deps (NewLocale.empty, ctxt0);  
    1.59 -    val ((elems', _), ctxt') = activate_elems elems (ProofContext.set_stmt true ctxt);
    1.60 -  in
    1.61 -    (((fixed, deps), (ctxt', elems'), (parms, spec, defs)), concl)
    1.62 -  end;
    1.63 -
    1.64 -fun prep_statement prep_ctxt elems concl ctxt =
    1.65 -  let
    1.66 -    val (((_, (ctxt', _), _)), concl) = prep_ctxt true false ([], []) elems concl ctxt
    1.67 -  in (concl, ctxt') end;
    1.68 +    val ((fixed, deps, elems, _), (parms, (spec, (_, _, defs)))) =
    1.69 +      prep false true context raw_import raw_elems [];
    1.70 +    (* Declare parameters and imported facts *)
    1.71 +    val context' = context |>
    1.72 +      ProofContext.add_fixes_i fixed |> snd |>
    1.73 +      pair NewLocale.empty |> fold (NewLocale.activate_facts thy) deps |> snd;
    1.74 +    val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
    1.75 +  in ((fixed, deps, elems'), (parms, spec, defs)) end;
    1.76  
    1.77  in
    1.78  
    1.79 -fun read_statement body concl ctxt =
    1.80 -  prep_statement (prep_context_statement read_full_context_statement Element.activate) body concl ctxt;
    1.81 -fun cert_statement body concl ctxt =
    1.82 -  prep_statement (prep_context_statement cert_full_context_statement Element.activate_i) body concl ctxt;
    1.83 +fun read_declaration x = prep_declaration read_full_context_statement Element.activate x;
    1.84 +fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x;
    1.85 +
    1.86 +end;
    1.87 +
    1.88 +
    1.89 +(* Locale expression to set up a goal *)
    1.90 +
    1.91 +local
    1.92 +
    1.93 +fun props_of thy (name, morph) =
    1.94 +  let
    1.95 +    val (asm, defs) = NewLocale.specification_of thy name;
    1.96 +  in
    1.97 +    (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph)
    1.98 +  end;
    1.99 +
   1.100 +fun prep_goal_expression prep expression context =
   1.101 +  let
   1.102 +    val thy = ProofContext.theory_of context;
   1.103  
   1.104 -fun read_context strict imprt body ctxt =
   1.105 -  #1 (prep_context_statement read_full_context_statement Element.activate strict true imprt body [] ctxt);
   1.106 -fun cert_context strict imprt body ctxt =
   1.107 -  #1 (prep_context_statement cert_full_context_statement Element.activate_i strict true imprt body [] ctxt);
   1.108 +    val ((fixed, deps, _, _), _) = prep true true context expression [] [];
   1.109 +    (* proof obligations *)
   1.110 +    val propss = map (props_of thy) deps;
   1.111 +
   1.112 +    val goal_ctxt = context |>
   1.113 +      ProofContext.add_fixes_i fixed |> snd |>
   1.114 +      (fold o fold) Variable.auto_fixes propss;
   1.115 +
   1.116 +    val export = Variable.export_morphism goal_ctxt context;
   1.117 +    val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
   1.118 +(*    val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *)
   1.119 +    val exp_term = Drule.term_rule thy (singleton exp_fact);
   1.120 +    val exp_typ = Logic.type_map exp_term;
   1.121 +    val export' =
   1.122 +      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
   1.123 +  in ((propss, deps, export'), goal_ctxt) end;
   1.124 +    
   1.125 +in
   1.126 +
   1.127 +fun read_goal_expression x = prep_goal_expression read_full_context_statement x;
   1.128 +fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x;
   1.129  
   1.130  end;
   1.131  
   1.132 @@ -581,7 +625,7 @@
   1.133        Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
   1.134    else raise Match);
   1.135  
   1.136 -(* CB: define one predicate including its intro rule and axioms
   1.137 +(* define one predicate including its intro rule and axioms
   1.138     - bname: predicate name
   1.139     - parms: locale parameters
   1.140     - defs: thms representing substitutions from defines elements
   1.141 @@ -694,7 +738,7 @@
   1.142      end
   1.143    | defines_to_notes _ e defns = (e, defns);
   1.144  
   1.145 -fun gen_add_locale prep_context
   1.146 +fun gen_add_locale prep_decl
   1.147      bname predicate_name raw_imprt raw_body thy =
   1.148    let
   1.149      val thy_ctxt = ProofContext.init thy;
   1.150 @@ -702,8 +746,8 @@
   1.151      val _ = NewLocale.test_locale thy name andalso
   1.152        error ("Duplicate definition of locale " ^ quote name);
   1.153  
   1.154 -    val ((fixed, deps), (_, body_elems), text as (parms, ((_, exts'), _), defs)) =
   1.155 -      prep_context false raw_imprt raw_body thy_ctxt;
   1.156 +    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
   1.157 +      prep_decl raw_imprt raw_body thy_ctxt;
   1.158      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   1.159        define_preds predicate_name text thy;
   1.160  
   1.161 @@ -732,8 +776,8 @@
   1.162  
   1.163  in
   1.164  
   1.165 -val add_locale = gen_add_locale read_context;
   1.166 -val add_locale_i = gen_add_locale cert_context;
   1.167 +val add_locale = gen_add_locale read_declaration;
   1.168 +val add_locale_i = gen_add_locale cert_declaration;
   1.169  
   1.170  end;
   1.171  
   1.172 @@ -752,28 +796,17 @@
   1.173  
   1.174  local
   1.175  
   1.176 -fun store_dep target ((name, morph), thms) =
   1.177 -  NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms);
   1.178 -
   1.179  fun gen_sublocale prep_expr
   1.180      after_qed target expression thy =
   1.181    let
   1.182      val target_ctxt = NewLocale.init target thy;
   1.183      val target' = NewLocale.intern thy target;
   1.184  
   1.185 -    val ((_, fixed, deps, _, _), _) = prep_expr true true target_ctxt expression [] [];
   1.186 -    val (_, goal_ctxt) = ProofContext.add_fixes_i fixed target_ctxt;
   1.187 +    val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt;
   1.188 +    
   1.189 +    fun store_dep target ((name, morph), thms) =
   1.190 +      NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export');
   1.191  
   1.192 -    (* proof obligations from deps *)
   1.193 -    fun props_of (name, morph) =
   1.194 -    let
   1.195 -      val (asm, defs) = NewLocale.specification_of thy name;
   1.196 -    in
   1.197 -      (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph)
   1.198 -    end;
   1.199 -    
   1.200 -    val propss = map props_of deps;
   1.201 -    
   1.202      fun after_qed' results =
   1.203        fold (store_dep target') (deps ~~ prep_result propss results) #>
   1.204        after_qed results;
   1.205 @@ -786,8 +819,8 @@
   1.206  
   1.207  in
   1.208  
   1.209 -fun sublocale x = gen_sublocale read_full_context_statement x;
   1.210 -fun sublocale_i x = gen_sublocale cert_full_context_statement x;
   1.211 +fun sublocale x = gen_sublocale read_goal_expression x;
   1.212 +fun sublocale_i x = gen_sublocale cert_goal_expression x;
   1.213  
   1.214  end;
   1.215