src/Pure/Isar/expression.ML
changeset 29034 3dc51c01f9f3
parent 29033 721529248e31
parent 29032 3ad4cf50070d
child 29035 b0a0843dfd99
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 10 10:11:18 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 10 10:12:44 2008 +0100
     1.3 @@ -19,9 +19,11 @@
     1.4  
     1.5    (* Declaring locales *)
     1.6    val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory ->
     1.7 -    string * Proof.context
     1.8 +    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
     1.9 +    Proof.context
    1.10    val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory ->
    1.11 -    string * Proof.context
    1.12 +    (string * (string * (Attrib.binding * (thm list * Attrib.src list) list) list) list) *
    1.13 +    Proof.context
    1.14  
    1.15    (* Interpretation *)
    1.16    val sublocale_cmd: string -> expression -> theory -> Proof.state;
    1.17 @@ -72,6 +74,13 @@
    1.18        end;
    1.19  
    1.20      fun match_bind (n, b) = (n = Binding.base_name b);
    1.21 +    fun parm_eq ((b1, mx1), (b2, mx2)) =
    1.22 +      (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
    1.23 +      (Binding.base_name b1 = Binding.base_name b2) andalso
    1.24 +      (if mx1 = mx2 then true
    1.25 +      else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^
    1.26 +                    " in expression."));
    1.27 +      
    1.28      fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
    1.29        (* FIXME: cannot compare bindings for equality. *)
    1.30  
    1.31 @@ -103,12 +112,7 @@
    1.32              val (is', ps') = fold_map (fn i => fn ps =>
    1.33                let
    1.34                  val (ps', i') = params_inst i;
    1.35 -                val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) =>
    1.36 -                  (* FIXME: should check for bindings being the same.
    1.37 -                     Instead we check for equal name and syntax. *)
    1.38 -                  if mx1 = mx2 then mx1
    1.39 -                  else error ("Conflicting syntax for parameter" ^ quote (Binding.display p) ^
    1.40 -                    " in expression.")) (ps, ps')
    1.41 +                val ps'' = distinct parm_eq (ps @ ps');
    1.42                in (i', ps'') end) is []
    1.43            in (ps', is') end;
    1.44  
    1.45 @@ -268,21 +272,18 @@
    1.46  
    1.47  val norm_term = Envir.beta_norm oo Term.subst_atomic;
    1.48  
    1.49 -fun abstract_thm thy eq =
    1.50 -  Thm.assume (Thm.cterm_of thy eq) |> Drule.gen_all |> Drule.abs_def;
    1.51 -
    1.52 -fun bind_def ctxt eq (xs, env, ths) =
    1.53 +fun bind_def ctxt eq (xs, env, eqs) =
    1.54    let
    1.55 +    val _ = LocalDefs.cert_def ctxt eq;
    1.56      val ((y, T), b) = LocalDefs.abs_def eq;
    1.57      val b' = norm_term env b;
    1.58 -    val th = abstract_thm (ProofContext.theory_of ctxt) eq;
    1.59      fun err msg = error (msg ^ ": " ^ quote y);
    1.60    in
    1.61      exists (fn (x, _) => x = y) xs andalso
    1.62        err "Attempt to define previously specified variable";
    1.63      exists (fn (Free (y', _), _) => y = y' | _ => false) env andalso
    1.64        err "Attempt to redefine variable";
    1.65 -    (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
    1.66 +    (Term.add_frees b' xs, (Free (y, T), b') :: env, eq :: eqs)
    1.67    end;
    1.68  
    1.69  fun eval_text _ _ (Fixes _) text = text
    1.70 @@ -317,8 +318,11 @@
    1.71          (case elem of
    1.72            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
    1.73              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
    1.74 -        | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
    1.75 -            (a, (#2 (LocalDefs.cert_def ctxt (close_frees t)), no_binds ps))))
    1.76 +        | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
    1.77 +            let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
    1.78 +            in
    1.79 +              ((Binding.map_base (Thm.def_name_optional c) name, atts), (t', no_binds ps))
    1.80 +            end))
    1.81          | e => e)
    1.82        end;
    1.83  
    1.84 @@ -430,8 +434,7 @@
    1.85           env: list of term pairs encoding substitutions, where the first term
    1.86             is a free variable; substitutions represent defines elements and
    1.87             the rhs is normalised wrt. the previous env
    1.88 -         defs: theorems representing the substitutions from defines elements
    1.89 -           (thms are normalised wrt. env).
    1.90 +         defs: the equations from the defines elements
    1.91         elems is an updated version of raw_elems:
    1.92           - type info added to Fixes and modified in Constrains
    1.93           - axiom and definition statement replaced by corresponding one
    1.94 @@ -519,7 +522,6 @@
    1.95  
    1.96      val export = Variable.export_morphism goal_ctxt context;
    1.97      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
    1.98 -(*    val exp_term = TermSubst.zero_var_indexes o Morphism.term export; *)
    1.99      val exp_term = Drule.term_rule thy (singleton exp_fact);
   1.100      val exp_typ = Logic.type_map exp_term;
   1.101      val export' =
   1.102 @@ -623,6 +625,8 @@
   1.103  
   1.104  fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy =
   1.105    let
   1.106 +    val defs' = map (cterm_of thy #> Assumption.assume #> Drule.gen_all #> Drule.abs_def) defs;
   1.107 +
   1.108      val (a_pred, a_intro, a_axioms, thy'') =
   1.109        if null exts then (NONE, NONE, [], thy)
   1.110        else
   1.111 @@ -630,7 +634,7 @@
   1.112            val aname = if null ints then pname else pname ^ "_" ^ axiomsN;
   1.113            val ((statement, intro, axioms), thy') =
   1.114              thy
   1.115 -            |> def_pred aname parms defs exts exts';
   1.116 +            |> def_pred aname parms defs' exts exts';
   1.117            val (_, thy'') =
   1.118              thy'
   1.119              |> Sign.add_path aname
   1.120 @@ -645,7 +649,7 @@
   1.121          let
   1.122            val ((statement, intro, axioms), thy''') =
   1.123              thy''
   1.124 -            |> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred);
   1.125 +            |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
   1.126            val (_, thy'''') =
   1.127              thy'''
   1.128              |> Sign.add_path pname
   1.129 @@ -670,15 +674,10 @@
   1.130        |> apfst (curry Notes Thm.assumptionK)
   1.131    | assumes_to_notes e axms = (e, axms);
   1.132  
   1.133 -fun defines_to_notes thy (Defines defs) defns =
   1.134 -    let
   1.135 -      val defs' = map (fn (_, (def, _)) => def) defs
   1.136 -      val notes = map (fn (a, (def, _)) =>
   1.137 -        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs
   1.138 -    in
   1.139 -      (Notes (Thm.definitionK, notes), defns @ defs')
   1.140 -    end
   1.141 -  | defines_to_notes _ e defns = (e, defns);
   1.142 +fun defines_to_notes thy (Defines defs) =
   1.143 +      Notes (Thm.definitionK, map (fn (a, (def, _)) =>
   1.144 +        (a, [([Assumption.assume (cterm_of thy def)], [])])) defs)
   1.145 +  | defines_to_notes _ e = e;
   1.146  
   1.147  fun gen_add_locale prep_decl
   1.148      bname predicate_name raw_imprt raw_body thy =
   1.149 @@ -687,7 +686,7 @@
   1.150      val _ = NewLocale.test_locale thy name andalso
   1.151        error ("Duplicate definition of locale " ^ quote name);
   1.152  
   1.153 -    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), _)) =
   1.154 +    val ((fixed, deps, body_elems), text as (parms, ((_, exts'), _), defs)) =
   1.155        prep_decl raw_imprt raw_body (ProofContext.init thy);
   1.156      val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   1.157        define_preds predicate_name text thy;
   1.158 @@ -701,24 +700,30 @@
   1.159      val params = fixed @
   1.160        (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   1.161      val asm = if is_some b_statement then b_statement else a_statement;
   1.162 -    val (body_elems', defns) = fold_map (defines_to_notes thy') body_elems [];
   1.163 -    val notes = body_elems' |>
   1.164 -      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
   1.165 -      fst |> map (Element.morph_ctxt satisfy) |>
   1.166 -      map_filter (fn Notes notes => SOME notes | _ => NONE) |>
   1.167 -      (if is_some asm
   1.168 -        then cons (Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
   1.169 -          [([assume (cterm_of thy' (the asm))], [(Attrib.internal o K) NewLocale.witness_attrib])])])
   1.170 -        else I);
   1.171 +    val body_elems' = map (defines_to_notes thy') body_elems;
   1.172 +
   1.173 +    val notes =
   1.174 +        if is_some asm
   1.175 +        then [(Thm.internalK, [((Binding.name (bname ^ "_" ^ axiomsN), []),
   1.176 +          [([Assumption.assume (cterm_of thy' (the asm))],
   1.177 +            [(Attrib.internal o K) NewLocale.witness_attrib])])])]
   1.178 +        else [];
   1.179  
   1.180      val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
   1.181  
   1.182      val loc_ctxt = thy' |>
   1.183        NewLocale.register_locale bname (extraTs, params)
   1.184 -        (asm, defns) ([], [])
   1.185 +        (asm, rev defs) ([], [])
   1.186          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
   1.187 -      NewLocale.init name
   1.188 -  in (name, loc_ctxt) end;
   1.189 +      NewLocale.init name;
   1.190 +
   1.191 +    (* These will be added in the local theory. *)
   1.192 +    val notes' = body_elems' |>
   1.193 +      (fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness a_axioms)) |>
   1.194 +      fst |> map (Element.morph_ctxt satisfy) |>
   1.195 +      map_filter (fn Notes notes => SOME notes | _ => NONE);
   1.196 +
   1.197 +  in ((name, notes'), loc_ctxt) end;
   1.198  
   1.199  in
   1.200