# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 1f990689349fff8849aa917d8b42bffa7d2f3749 # Parent eb91ec1ef6f03b87f74b5d91f1488e653ea5fe8f further cleaning up diff -r eb91ec1ef6f0 -r 1f990689349f src/HOL/MicroJava/J/Eval.thy --- a/src/HOL/MicroJava/J/Eval.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/MicroJava/J/Eval.thy Sat Oct 24 16:55:42 2009 +0200 @@ -40,7 +40,7 @@ ("_ \ _ -_[\]_-> _" [51,82,60,51,82] 81) and exec :: "[java_mb prog,xstate,stmt, xstate] => bool " ("_ \ _ -_-> _" [51,82,60,82] 81) - for G :: "java_mb prog" + (*for G :: "java_mb prog"*) where -- "evaluation of expressions" diff -r eb91ec1ef6f0 -r 1f990689349f src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 24 16:55:42 2009 +0200 @@ -171,7 +171,8 @@ end fun flat_intro intro (new_defs, thy) = let - val constname = "dummy" + val constname = fst (dest_Const (fst (strip_comb + (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro)))))) val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy) val th = setmp quick_and_dirty true (SkipProof.make_thm thy) intro_ts in diff -r eb91ec1ef6f0 -r 1f990689349f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 @@ -293,8 +293,6 @@ error "Trying to instantiate another predicate" else () val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty - val _ = tracing (commas (map (fn ((x, i), (s, T)) => x ^ " instantiate to " ^ (Syntax.string_of_typ ctxt' T)) - (Vartab.dest subst))) val subst' = map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) in Thm.certify_instantiate (subst', []) th end; @@ -567,23 +565,21 @@ fun preprocess_elim thy nparams elimrule = let - val _ = tracing ("Preprocessing elimination rule " - ^ (Display.string_of_thm_global thy elimrule)) fun replace_eqs (Const ("Trueprop", _) $ (Const ("op =", T) $ lhs $ rhs)) = HOLogic.mk_Trueprop (Const (@{const_name Predicate.eq}, T) $ lhs $ rhs) | replace_eqs t = t - val ctxt = ProofContext.init thy - val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt - val prems = Thm.prems_of elimrule + val ctxt = ProofContext.init thy + val ((_, [elimrule]), ctxt') = Variable.import false [elimrule] ctxt + val prems = Thm.prems_of elimrule val nargs = length (snd (strip_comb (HOLogic.dest_Trueprop (hd prems)))) - nparams fun preprocess_case t = - let + let val params = Logic.strip_params t val (assums1, assums2) = chop nargs (Logic.strip_assums_hyp t) val assums_hyp' = assums1 @ (map replace_eqs assums2) - in + in list_all (params, Logic.list_implies (assums_hyp', Logic.strip_assums_concl t)) - end + end val cases' = map preprocess_case (tl prems) val elimrule' = Logic.list_implies ((hd prems) :: cases', Thm.concl_of elimrule) val bigeq = (Thm.symmetric (Conv.implies_concl_conv @@ -591,7 +587,6 @@ (cterm_of thy elimrule'))) val tac = (fn _ => setmp quick_and_dirty true (SkipProof.cheat_tac thy)) val eq = Goal.prove ctxt' [] [] (Logic.mk_equals ((Thm.prop_of elimrule), elimrule')) tac - val _ = tracing "Preprocessed elimination rule" in Thm.equal_elim eq elimrule |> singleton (Variable.export ctxt' ctxt) end; @@ -729,8 +724,6 @@ fun constname_of_intro intr = fst (dest_Const (fst (strip_intro_concl 0 (prop_of intr)))) val _ = if not (forall (fn intr => constname_of_intro intr = c) pre_intros) then error "register_intros: Introduction rules of different constants are used" else () - val _ = tracing ("Registering introduction rules of " ^ c ^ "...") - val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros)) val nparams = guess_nparams T val pre_elim = (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy))) @@ -1124,10 +1117,7 @@ (select_mode_prem thy modes' (vs union generator_vs) ps)) all_generator_vs) of SOME generator_vs => check_mode_prems ((map (generator vTs) generator_vs) @ acc_ps) (vs union generator_vs) ps - | NONE => let - val _ = tracing ("ps:" ^ (commas - (map (fn p => string_of_moded_prem thy (p, Mode (([], []), [], []))) ps))) - in (*error "mode analysis failed"*)NONE end + | NONE => NONE end) else NONE) @@ -1950,14 +1940,14 @@ | select_sup _ 1 = [rtac @{thm supI1}] | select_sup n i = (rtac @{thm supI2})::(select_sup (n - 1) (i - 1)); -fun prove_one_direction thy clauses preds modes pred mode moded_clauses = +fun prove_one_direction options thy clauses preds modes pred mode moded_clauses = let val T = the (AList.lookup (op =) preds pred) val nargs = length (binder_types T) - nparams_of thy pred val pred_case_rule = the_elim_of thy pred in REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) - THEN print_tac "before applying elim rule" + THEN print_tac' options "before applying elim rule" THEN etac (predfun_elim_of thy pred mode) 1 THEN etac pred_case_rule 1 THEN (EVERY (map @@ -2150,7 +2140,7 @@ (fn _ => rtac @{thm pred_iffI} 1 THEN print_tac' options "after pred_iffI" - THEN prove_one_direction thy clauses preds modes pred mode moded_clauses + THEN prove_one_direction options thy clauses preds modes pred mode moded_clauses THEN print_tac' options "proved one direction" THEN prove_other_direction thy modes pred mode moded_clauses THEN print_tac' options "proved other direction") @@ -2285,8 +2275,6 @@ val elim' = (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy))) (mk_casesrule (ProofContext.init thy) nparams intros) - val _ = Output.tracing (Display.string_of_thm_global thy elim) - val _ = Output.tracing (Display.string_of_thm_global thy elim') in if not (Thm.equiv_thm (elim, elim')) then error "Introduction and elimination rules do not match!" diff -r eb91ec1ef6f0 -r 1f990689349f src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 @@ -55,8 +55,6 @@ subsection {* Tricky case with alternative rules *} -text {* This cannot be handled correctly yet *} -(* inductive append2 where "append2 [] xs xs" @@ -72,7 +70,7 @@ case append2 from append2.cases[OF append2(1)] append2(2-3) show thesis by blast qed -*) + subsection {* Tricky cases with tuples *} inductive tupled_append :: "'a list \ 'a list \ 'a list \ bool" @@ -560,15 +558,15 @@ "[]\i\ = None" | "(x # xs)\i\ = (case i of 0 \ Some x | Suc j \ xs \j\)" -(* + inductive nth_el' :: "'a list \ nat \ 'a \ bool" where "nth_el' (x # xs) 0 x" | "nth_el' xs i y \ nth_el' (x # xs) (Suc i) y" -*) + inductive typing :: "type list \ dB \ type \ bool" ("_ \ _ : _" [50, 50, 50] 50) where - Var [intro!]: "nth_el env x = Some T \ env \ Var x : T" + Var [intro!]: "nth_el' env x T \ env \ Var x : T" | Abs [intro!]: "T # env \ t : U \ env \ Abs T t : (T \ U)" (* | App [intro!]: "env \ s : T \ U \ env \ t : T \ env \ (s \ t) : U" *) | App [intro!]: "env \ s : U \ T \ env \ t : T \ env \ (s \ t) : U" @@ -596,7 +594,7 @@ | abs [simp, intro!]: "s \\<^sub>\ t ==> Abs T s \\<^sub>\ Abs T t" lemma "Gamma \ t : T \ t \\<^sub>\ t' \ Gamma \ t' : T" -quickcheck[generator = pred_compile, size = 10, iterations = 100] +quickcheck[generator = pred_compile, size = 10, iterations = 1] oops lemma filter_eq_ConsD: