--- a/src/HOL/Quotient.thy Sat Aug 28 16:14:32 2010 +0200
+++ b/src/HOL/Quotient.thy Mon Aug 30 09:35:30 2010 +0200
@@ -651,6 +651,16 @@
shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
by auto
+lemma mem_rsp:
+ shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
+ by (simp add: mem_def)
+
+lemma mem_prs:
+ assumes a1: "Quotient R1 Abs1 Rep1"
+ and a2: "Quotient R2 Abs2 Rep2"
+ shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
+ by (simp add: expand_fun_eq mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
+
locale quot_type =
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
@@ -721,8 +731,8 @@
declare [[map "fun" = (fun_map, fun_rel)]]
lemmas [quot_thm] = fun_quotient
-lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp
-lemmas [quot_preserve] = if_prs o_prs let_prs
+lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp
+lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs
lemmas [quot_equiv] = identity_equivp
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Aug 28 16:14:32 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Mon Aug 30 09:35:30 2010 +0200
@@ -618,11 +618,18 @@
end
+(* Since we use Ball and Bex during the lifting and descending,
+ we cannot deal with lemmas containing them, unless we unfold
+ them by default. *)
+
+val default_unfolds = @{thms Ball_def Bex_def}
+
+
(** descending as tactic **)
fun descend_procedure_tac ctxt simps =
let
- val ss = (mk_minimal_ss ctxt) addsimps simps
+ val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
in
full_simp_tac ss
THEN' Object_Logic.full_atomize_tac
@@ -657,7 +664,7 @@
(* the tactic leaves three subgoals to be proved *)
fun lift_procedure_tac ctxt simps rthm =
let
- val ss = (mk_minimal_ss ctxt) addsimps simps
+ val ss = (mk_minimal_ss ctxt) addsimps (simps @ default_unfolds)
in
full_simp_tac ss
THEN' Object_Logic.full_atomize_tac
--- a/src/Tools/Code/code_haskell.ML Sat Aug 28 16:14:32 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Mon Aug 30 09:35:30 2010 +0200
@@ -483,7 +483,7 @@
Code_Target.add_target
(target, { serializer = isar_serializer, literals = literals,
check = { env_var = "EXEC_GHC", make_destination = I,
- make_command = fn ghc => fn p => fn module_name =>
+ make_command = fn ghc => fn module_name =>
ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_ml.ML Sat Aug 28 16:14:32 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Mon Aug 30 09:35:30 2010 +0200
@@ -966,11 +966,11 @@
Code_Target.add_target
(target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
- make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
+ make_command = fn isabelle => fn _ => isabelle ^ " -r -q -u Pure" } })
#> Code_Target.add_target
(target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
- make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
+ make_command = fn ocaml => fn _ => ocaml ^ " -w pu nums.cma ROOT.ocaml" } })
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_scala.ML Sat Aug 28 16:14:32 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Mon Aug 30 09:35:30 2010 +0200
@@ -521,9 +521,9 @@
Code_Target.add_target
(target, { serializer = isar_serializer, literals = literals,
check = { env_var = "SCALA_HOME", make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
- make_command = fn scala_home => fn p => fn _ =>
+ make_command = fn scala_home => fn _ =>
"export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
- ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " " ^ File.shell_path p } })
+ ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " ROOT.scala" } })
#> Code_Target.add_syntax_tyco target "fun"
(SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_target.ML Sat Aug 28 16:14:32 2010 +0200
+++ b/src/Tools/Code/code_target.ML Mon Aug 30 09:35:30 2010 +0200
@@ -13,7 +13,7 @@
type literals = Code_Printer.literals
val add_target: string * { serializer: serializer, literals: literals,
check: { env_var: string, make_destination: Path.T -> Path.T,
- make_command: string -> Path.T -> string -> string } } -> theory -> theory
+ make_command: string -> string -> string } } -> theory -> theory
val extend_target: string *
(string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
@@ -116,7 +116,7 @@
datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
check: { env_var: string, make_destination: Path.T -> Path.T,
- make_command: string -> Path.T -> string -> string } }
+ make_command: string -> string -> string } }
| Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
datatype target = Target of {
@@ -336,7 +336,7 @@
val destination = make_destination p;
val _ = file destination (serialize thy target (SOME 80)
(SOME module_name) args naming program names_cs);
- val cmd = make_command env_param destination module_name;
+ val cmd = make_command env_param module_name;
in if bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
then error ("Code check failed for " ^ target ^ ": " ^ cmd)
else ()