Fixed "axiom" generation for mixed locales with and without predicates.
authorballarin
Wed Jun 08 16:11:09 2005 +0200 (2005-06-08)
changeset 16325a6431098a929
parent 16324 059caec54d91
child 16326 50a613925c4e
Fixed "axiom" generation for mixed locales with and without predicates.
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/Lattice.thy
src/Pure/Isar/locale.ML
src/Pure/tactic.ML
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Jun 08 15:14:09 2005 +0200
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Wed Jun 08 16:11:09 2005 +0200
     1.3 @@ -22,12 +22,10 @@
     1.4  
     1.5  locale (open) S = var mult +
     1.6    assumes "mult(x, y) = mult(y, x)"
     1.7 -(* Making this declaration (open) reveals a problem when mixing open and
     1.8 -   closed locales. *)
     1.9  
    1.10  print_locale S
    1.11  
    1.12 -locale (open) S' = S mult (infixl "**" 60)
    1.13 +locale S' = S mult (infixl "**" 60)
    1.14  
    1.15  print_locale S'
    1.16  
     2.1 --- a/src/HOL/Algebra/Lattice.thy	Wed Jun 08 15:14:09 2005 +0200
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Jun 08 16:11:09 2005 +0200
     2.3 @@ -58,7 +58,7 @@
     2.4    join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
     2.5    "x \<squnion> y == sup L {x, y}"
     2.6  
     2.7 -  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 65)
     2.8 +  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
     2.9    "x \<sqinter> y == inf L {x, y}"
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/locale.ML	Wed Jun 08 15:14:09 2005 +0200
     3.2 +++ b/src/Pure/Isar/locale.ML	Wed Jun 08 16:11:09 2005 +0200
     3.3 @@ -21,7 +21,6 @@
     3.4  (* TODO:
     3.5  - beta-eta normalisation of interpretation parameters
     3.6  - no beta reduction of interpretation witnesses
     3.7 -- mix of locales with and without open in activate_elems
     3.8  - dangling type frees in locales
     3.9  *)
    3.10  
    3.11 @@ -855,7 +854,6 @@
    3.12      (* thy used for retrieval of locale info,
    3.13         ctxt for error messages, parameter unification and instantiation
    3.14         of axioms *)
    3.15 -    (* TODO: consider err_in_locale with thy argument *)
    3.16  
    3.17      fun renaming (SOME x :: xs) (y :: ys) = (y, x) :: renaming xs ys
    3.18        | renaming (NONE :: xs) (y :: ys) = renaming xs ys
    3.19 @@ -1740,7 +1738,7 @@
    3.20          Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]
    3.21        |> Drule.conj_elim_precise (length ts);
    3.22      val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) =>
    3.23 -      Tactic.prove defs_sign [] [] t (fn _ =>
    3.24 +      Tactic.prove_plain defs_sign [] [] t (fn _ =>
    3.25          Tactic.rewrite_goals_tac defs THEN
    3.26          Tactic.compose_tac (false, ax, 0) 1));
    3.27    in (defs_thy, (statement, intro, axioms)) end;
    3.28 @@ -1777,7 +1775,7 @@
    3.29            val aname = if null ints then bname else bname ^ "_" ^ axiomsN;
    3.30            val (def_thy, (statement, intro, axioms)) =
    3.31              thy |> def_pred aname parms defs exts exts';
    3.32 -          val elemss' = change_elemss axioms elemss @
    3.33 +          val elemss' = change_elemss (map (Drule.zero_var_indexes o Drule.gen_all) axioms) elemss @
    3.34              [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
    3.35          in
    3.36            def_thy |> note_thmss_qualified "" aname
     4.1 --- a/src/Pure/tactic.ML	Wed Jun 08 15:14:09 2005 +0200
     4.2 +++ b/src/Pure/tactic.ML	Wed Jun 08 16:11:09 2005 +0200
     4.3 @@ -111,10 +111,13 @@
     4.4    val simplify: bool -> thm list -> thm -> thm
     4.5    val conjunction_tac: tactic
     4.6    val smart_conjunction_tac: int -> tactic
     4.7 +  val prove_multi_plain: Sign.sg -> string list -> term list -> term list ->
     4.8 +    (thm list -> tactic) -> thm list
     4.9    val prove_multi: Sign.sg -> string list -> term list -> term list ->
    4.10      (thm list -> tactic) -> thm list
    4.11    val prove_multi_standard: Sign.sg -> string list -> term list -> term list ->
    4.12      (thm list -> tactic) -> thm list
    4.13 +  val prove_plain: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    4.14    val prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm
    4.15    val prove_standard: Sign.sg -> string list -> term list -> term ->
    4.16      (thm list -> tactic) -> thm
    4.17 @@ -659,7 +662,7 @@
    4.18  
    4.19  (** minimal goal interface for programmed proofs *)
    4.20  
    4.21 -fun prove_multi sign xs asms props tac =
    4.22 +fun gen_prove_multi finish_thm sign xs asms props tac =
    4.23    let
    4.24      val prop = Logic.mk_conjunction_list props;
    4.25      val statement = Logic.list_implies (asms, prop);
    4.26 @@ -700,14 +703,19 @@
    4.27      |> map (fn res => res
    4.28        |> Drule.implies_intr_list casms
    4.29        |> Drule.forall_intr_list cparams
    4.30 -      |> norm_hhf_rule
    4.31 -      |> (#1 o Thm.varifyT' fixed_tfrees)
    4.32 -      |> Drule.zero_var_indexes)
    4.33 +      |> finish_thm fixed_tfrees)
    4.34    end;
    4.35  
    4.36 +fun prove_multi_plain sign xs asms prop tac =
    4.37 +  gen_prove_multi (K norm_hhf_plain) sign xs asms prop tac;
    4.38 +fun prove_multi sign xs asms prop tac =
    4.39 +  gen_prove_multi (fn fixed_tfrees => Drule.zero_var_indexes o
    4.40 +      (#1 o Thm.varifyT' fixed_tfrees) o norm_hhf_rule)
    4.41 +    sign xs asms prop tac;
    4.42  fun prove_multi_standard sign xs asms prop tac =
    4.43    map Drule.standard (prove_multi sign xs asms prop tac);
    4.44  
    4.45 +fun prove_plain sign xs asms prop tac = hd (prove_multi_plain sign xs asms [prop] tac);
    4.46  fun prove sign xs asms prop tac = hd (prove_multi sign xs asms [prop] tac);
    4.47  fun prove_standard sign xs asms prop tac = Drule.standard (prove sign xs asms prop tac);
    4.48