# HG changeset patch # User huffman # Date 1333489764 -7200 # Node ID b4490e1a07323eb926b8810dabea60aecdb3d6bc # Parent ec6187036495467db663240db281598395df8eef# Parent 365521737b6aa0c792bb5118a4736caf1021ebce merged diff -r ec6187036495 -r b4490e1a0732 Admin/isatest/settings/at-poly --- a/Admin/isatest/settings/at-poly Tue Apr 03 22:31:00 2012 +0200 +++ b/Admin/isatest/settings/at-poly Tue Apr 03 23:49:24 2012 +0200 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-5.3.0" - ML_SYSTEM="polyml-5.3.0" + POLYML_HOME="/home/polyml/polyml-5.2.1" + ML_SYSTEM="polyml-5.2.1" ML_PLATFORM="x86-linux" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 500" diff -r ec6187036495 -r b4490e1a0732 Admin/isatest/settings/at-poly-e --- a/Admin/isatest/settings/at-poly-e Tue Apr 03 22:31:00 2012 +0200 +++ b/Admin/isatest/settings/at-poly-e Tue Apr 03 23:49:24 2012 +0200 @@ -1,7 +1,7 @@ # -*- shell-script -*- :mode=shellscript: - POLYML_HOME="/home/polyml/polyml-5.2.1" - ML_SYSTEM="polyml-5.2.1" + POLYML_HOME="/home/polyml/polyml-5.3.0" + ML_SYSTEM="polyml-5.3.0" ML_PLATFORM="x86-linux" ML_HOME="$POLYML_HOME/$ML_PLATFORM" ML_OPTIONS="-H 500" diff -r ec6187036495 -r b4490e1a0732 doc-src/Dirs --- a/doc-src/Dirs Tue Apr 03 22:31:00 2012 +0200 +++ b/doc-src/Dirs Tue Apr 03 23:49:24 2012 +0200 @@ -1,1 +1,1 @@ -Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer +Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer ProgProve diff -r ec6187036495 -r b4490e1a0732 doc-src/ProgProve/IsaMakefile --- a/doc-src/ProgProve/IsaMakefile Tue Apr 03 22:31:00 2012 +0200 +++ b/doc-src/ProgProve/IsaMakefile Tue Apr 03 23:49:24 2012 +0200 @@ -20,7 +20,15 @@ HOL-ProgProve: $(LOG)/HOL-ProgProve.gz -$(LOG)/HOL-ProgProve.gz: Thys/*.thy Thys/ROOT.ML +$(LOG)/HOL-ProgProve.gz: \ + Thys/Basics.thy \ + Thys/Bool_nat_list.thy \ + Thys/Isar.thy \ + Thys/LaTeXsugar.thy \ + Thys/Logic.thy \ + Thys/MyList.thy \ + Thys/Types_and_funs.thy \ + Thys/ROOT.ML @$(USEDIR) -s ProgProve HOL Thys @rm -f Thys/document/MyList.tex @rm -f Thys/document/isabelle.sty diff -r ec6187036495 -r b4490e1a0732 doc/Contents --- a/doc/Contents Tue Apr 03 22:31:00 2012 +0200 +++ b/doc/Contents Tue Apr 03 23:49:24 2012 +0200 @@ -1,7 +1,6 @@ Miscellaneous tutorials + prog-prove Programming and Proving in Isabelle/HOL tutorial Tutorial on Isabelle/HOL - main What's in Main - isar-overview Tutorial on Isar locales Tutorial on Locales classes Tutorial on Type Classes functions Tutorial on Function Definitions @@ -10,7 +9,8 @@ sledgehammer User's Guide to Sledgehammer sugar LaTeX Sugar for Isabelle documents -Main Reference Manuals +Reference Manuals + main What's in Main isar-ref The Isabelle/Isar Reference Manual implementation The Isabelle/Isar Implementation Manual system The Isabelle System Manual diff -r ec6187036495 -r b4490e1a0732 src/HOL/Isar_Examples/Group_Context.thy --- a/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 22:31:00 2012 +0200 +++ b/src/HOL/Isar_Examples/Group_Context.thy Tue Apr 03 23:49:24 2012 +0200 @@ -14,9 +14,9 @@ fixes prod :: "'a \ 'a \ 'a" (infixl "**" 70) and one :: "'a" and inverse :: "'a => 'a" - assumes assoc: "\x y z. (x ** y) ** z = x ** (y ** z)" - and left_one: "\x. one ** x = x" - and left_inverse: "\x. inverse x ** x = one" + assumes assoc: "(x ** y) ** z = x ** (y ** z)" + and left_one: "one ** x = x" + and left_inverse: "inverse x ** x = one" begin text {* some consequences *} diff -r ec6187036495 -r b4490e1a0732 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Tue Apr 03 22:31:00 2012 +0200 +++ b/src/Pure/Isar/bundle.ML Tue Apr 03 23:49:24 2012 +0200 @@ -91,10 +91,16 @@ let val decls = maps (the_bundle ctxt o prep ctxt) args in #2 (Attrib.local_notes "" [((Binding.empty, []), decls)] ctxt) end; -fun gen_context prep_bundle prep_stmt raw_incls raw_elems gthy = +fun gen_context prep_bundle prep_decl raw_incls raw_elems gthy = let val lthy = Context.cases Named_Target.theory_init Local_Theory.assert gthy; - val augment = gen_includes prep_bundle raw_incls #> prep_stmt raw_elems [] #> snd; + fun augment ctxt = + let + val ((_, _, _, ctxt'), _) = ctxt + |> Context_Position.restore_visible lthy + |> gen_includes prep_bundle raw_incls + |> prep_decl ([], []) I raw_elems; + in ctxt' |> Context_Position.restore_visible ctxt end; in (case gthy of Context.Theory _ => Local_Theory.target augment lthy |> Local_Theory.restore @@ -115,8 +121,8 @@ fun including bs = Proof.assert_backward #> Proof.map_context (includes bs); fun including_cmd bs = Proof.assert_backward #> Proof.map_context (includes_cmd bs); -val context = gen_context (K I) Expression.cert_statement; -val context_cmd = gen_context check Expression.read_statement; +val context = gen_context (K I) Expression.cert_declaration; +val context_cmd = gen_context check Expression.read_declaration; end; diff -r ec6187036495 -r b4490e1a0732 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Tue Apr 03 22:31:00 2012 +0200 +++ b/src/Pure/Isar/class_declaration.ML Tue Apr 03 23:49:24 2012 +0200 @@ -157,7 +157,7 @@ fold (Proof_Context.add_const_constraint o apsnd SOME) base_constraints #> Class.redeclare_operations thy sups #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate)); - val ((raw_supparams, _, raw_inferred_elems), _) = + val ((raw_supparams, _, raw_inferred_elems, _), _) = Proof_Context.init_global thy |> Context.proof_map (Syntax_Phases.term_check 0 "after_infer_fixate" (K after_infer_fixate)) |> prep_decl raw_supexpr init_class_body raw_elems; @@ -221,7 +221,7 @@ (* process elements as class specification *) val class_ctxt = Class.begin sups base_sort thy_ctxt; - val ((_, _, syntax_elems), _) = class_ctxt + val ((_, _, syntax_elems, _), _) = class_ctxt |> Expression.cert_declaration supexpr I inferred_elems; fun check_vars e vs = if null vs then diff -r ec6187036495 -r b4490e1a0732 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Apr 03 22:31:00 2012 +0200 +++ b/src/Pure/Isar/expression.ML Tue Apr 03 23:49:24 2012 +0200 @@ -21,14 +21,14 @@ (* Declaring locales *) val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list - * Element.context_i list) * ((string * typ) list * Proof.context) + * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list - * Element.context_i list) * ((string * typ) list * Proof.context) + * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) (*FIXME*) val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list - * Element.context_i list) * ((string * typ) list * Proof.context) + * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val add_locale: (local_theory -> local_theory) -> binding -> binding -> expression_i -> Element.context_i list -> theory -> string * local_theory val add_locale_cmd: (local_theory -> local_theory) -> binding -> binding -> @@ -357,17 +357,19 @@ Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global); val inst'' = map2 Type.constraint parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; - val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt; + val (insts'', _, _, _) = check_autofix insts' [] [] ctxt; val inst''' = insts'' |> List.last |> snd |> snd; val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt; val ctxt'' = Locale.activate_declarations (loc, morph) ctxt; in (i + 1, insts', ctxt'') end; - fun prep_elem insts raw_elem (elems, ctxt) = + fun prep_elem insts raw_elem ctxt = let - val ctxt' = declare_elem prep_vars_elem raw_elem ctxt; - val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem]; - val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt'; + val ctxt' = ctxt + |> Context_Position.set_visible false + |> declare_elem prep_vars_elem raw_elem + |> Context_Position.restore_visible ctxt; + val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem; in (elems', ctxt') end; fun prep_concl raw_concl (insts, elems, ctxt) = @@ -388,7 +390,7 @@ commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); val ctxt4 = init_body ctxt3; - val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4); + val (elems, ctxt5) = fold_map (prep_elem insts') raw_elems ctxt4; val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5); (* Retrieve parameter types *) @@ -458,10 +460,10 @@ val context' = context |> fix_params fixed |> fold (Context.proof_map o Locale.activate_facts NONE) deps; - val (elems', _) = context' |> + val (elems', context'') = context' |> Proof_Context.set_stmt true |> fold_map activate elems; - in ((fixed, deps, elems'), (parms, ctxt')) end; + in ((fixed, deps, elems', context''), (parms, ctxt')) end; in @@ -735,7 +737,7 @@ val _ = Locale.defined thy name andalso error ("Duplicate definition of locale " ^ quote name); - val ((fixed, deps, body_elems), (parms, ctxt')) = + val ((fixed, deps, body_elems, _), (parms, ctxt')) = prep_decl raw_import I raw_body (Proof_Context.init_global thy); val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; diff -r ec6187036495 -r b4490e1a0732 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Tue Apr 03 22:31:00 2012 +0200 +++ b/src/Pure/Isar/generic_target.ML Tue Apr 03 23:49:24 2012 +0200 @@ -121,7 +121,7 @@ (*export assumes/defines*) val th = Goal.norm_result raw_th; val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; - val asms' = map (Raw_Simplifier.rewrite_rule defs) asms; + val asms' = map (Raw_Simplifier.rewrite_rule (Drule.norm_hhf_eqs @ defs)) asms; (*export fixes*) val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);