replaced sorry by oops; removed old debug functions in predicate compiler
authorbulwahn
Wed Sep 23 16:20:13 2009 +0200 (2009-09-23)
changeset 32673d5db9cf85401
parent 32672 90f3ce5d27ae
child 32674 b629fbcc5313
replaced sorry by oops; removed old debug functions in predicate compiler
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/ex/Predicate_Compile_ex.thy
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:13 2009 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Sep 23 16:20:13 2009 +0200
     1.3 @@ -125,12 +125,6 @@
     1.4  
     1.5  val do_proofs = ref true;
     1.6  
     1.7 -fun mycheat_tac thy i st =
     1.8 -  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
     1.9 -
    1.10 -fun remove_last_goal thy st =
    1.11 -  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
    1.12 -
    1.13  (* reference to preprocessing of InductiveSet package *)
    1.14  
    1.15  val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*)
    1.16 @@ -2119,7 +2113,7 @@
    1.17          THEN print_tac "proved one direction"
    1.18          THEN prove_other_direction thy modes pred mode moded_clauses
    1.19          THEN print_tac "proved other direction")
    1.20 -       else (fn _ => mycheat_tac thy 1))
    1.21 +      else (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy))
    1.22    end;
    1.23  
    1.24  (* composition of mode inference, definition, compilation and proof *)
     2.1 --- a/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:13 2009 +0200
     2.2 +++ b/src/HOL/ex/Predicate_Compile_ex.thy	Wed Sep 23 16:20:13 2009 +0200
     2.3 @@ -317,7 +317,6 @@
     2.4  | "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
     2.5  | "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
     2.6  
     2.7 -ML {* reset Predicate_Compile_Core.do_proofs *}
     2.8  (*
     2.9  code_pred (inductify_all) S\<^isub>3 .
    2.10  *)
    2.11 @@ -348,19 +347,19 @@
    2.12  theorem S\<^isub>4_sound:
    2.13  "w \<in> S\<^isub>4 \<longrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    2.14  quickcheck[generator = pred_compile, size=2, iterations=1]
    2.15 -sorry
    2.16 +oops
    2.17  
    2.18  theorem S\<^isub>4_complete:
    2.19  "length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] \<longrightarrow> w \<in> S\<^isub>4"
    2.20  quickcheck[generator = pred_compile, size=5, iterations=1]
    2.21 -sorry
    2.22 +oops
    2.23  
    2.24  theorem S\<^isub>4_A\<^isub>4_B\<^isub>4_sound_and_complete:
    2.25  "w \<in> S\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b]"
    2.26  "w \<in> A\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = a] = length [x \<leftarrow> w. x = b] + 1"
    2.27  "w \<in> B\<^isub>4 \<longleftrightarrow> length [x \<leftarrow> w. x = b] = length [x \<leftarrow> w. x = a] + 1"
    2.28  (*quickcheck[generator = pred_compile, size=5, iterations=1]*)
    2.29 -sorry
    2.30 +oops
    2.31  
    2.32  
    2.33  section {* Lambda *}
    2.34 @@ -432,8 +431,6 @@
    2.35  thm test.equation
    2.36  *)
    2.37  
    2.38 -ML {*set  Toplevel.debug *}
    2.39 -
    2.40  lemma filter_eq_ConsD:
    2.41   "filter P ys = x#xs \<Longrightarrow>
    2.42    \<exists>us vs. ys = ts @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"