src/HOL/Integ/cooper_proof.ML
changeset 17985 d5d576b72371
parent 17959 8db36a108213
child 19233 77ca20b0ed77
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Sat Oct 22 01:22:10 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Tue Oct 25 18:18:49 2005 +0200
     1.3 @@ -189,47 +189,21 @@
     1.4  fun qe_get_terms th = let val (_$(Const("op =",Type ("fun",[Type ("bool", []),_])) $ A $ B )) = prop_of th in (A,B) end;
     1.5  
     1.6  (* ------------------------------------------------------------------------- *)
     1.7 -(* Modified version of the simple version with minimal amount of checking and postprocessing*)
     1.8 +(*This function proove elementar will be used to generate proofs at
     1.9 +  runtime*) (*It is thought to prove properties such as a dvd b
    1.10 +  (essentially) that are only to make at runtime.*)
    1.11  (* ------------------------------------------------------------------------- *)
    1.12 -
    1.13 -fun simple_prove_goal_cterm2 G tacs =
    1.14 -  let
    1.15 -    fun check NONE = error "prove_goal: tactic failed"
    1.16 -      | check (SOME (thm, _)) = (case nprems_of thm of
    1.17 -            0 => thm
    1.18 -          | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
    1.19 -  in check (Seq.pull (EVERY tacs (trivial G))) end;
    1.20 -
    1.21 -(*-------------------------------------------------------------*)
    1.22 -(*-------------------------------------------------------------*)
    1.23 -
    1.24 -fun cert_Trueprop sg t = cterm_of sg (HOLogic.mk_Trueprop t);
    1.25 -
    1.26 -(* ------------------------------------------------------------------------- *)
    1.27 -(*This function proove elementar will be used to generate proofs at runtime*)
    1.28 -(*It is is based on the isabelle function proove_goalw_cterm and is thought to *)
    1.29 -(*prove properties such as a dvd b (essentially) that are only to make at
    1.30 -runtime.*)
    1.31 -(* ------------------------------------------------------------------------- *)
    1.32 -fun prove_elementar sg s fm2 = case s of 
    1.33 +fun prove_elementar thy s fm2 =
    1.34 +  Goal.prove thy [] [] (HOLogic.mk_Trueprop fm2) (fn _ => EVERY
    1.35 +  (case s of
    1.36    (*"ss" like simplification with simpset*)
    1.37    "ss" =>
    1.38 -    let
    1.39 -      val ss = presburger_ss addsimps
    1.40 -        [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    1.41 -      val ct =  cert_Trueprop sg fm2
    1.42 -    in 
    1.43 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)] 
    1.44 -
    1.45 -    end
    1.46 +    let val ss = presburger_ss addsimps [zdvd_iff_zmod_eq_0,unity_coeff_ex]
    1.47 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
    1.48  
    1.49    (*"bl" like blast tactic*)
    1.50    (* Is only used in the harrisons like proof procedure *)
    1.51 -  | "bl" =>
    1.52 -     let val ct = cert_Trueprop sg fm2
    1.53 -     in
    1.54 -       simple_prove_goal_cterm2 ct [blast_tac HOL_cs 1]
    1.55 -     end
    1.56 +  | "bl" => [blast_tac HOL_cs 1]
    1.57  
    1.58    (*"ed" like Existence disjunctions ...*)
    1.59    (* Is only used in the harrisons like proof procedure *)
    1.60 @@ -244,51 +218,26 @@
    1.61            etac exE 1, REPEAT(EVERY[etac disjE 1, tac1]), tac1,
    1.62            REPEAT(EVERY[etac disjE 1, tac2]), tac2]
    1.63          end
    1.64 -
    1.65 -      val ct = cert_Trueprop sg fm2
    1.66 -    in 
    1.67 -      simple_prove_goal_cterm2 ct ex_disj_tacs
    1.68 -    end
    1.69 +    in ex_disj_tacs end
    1.70  
    1.71 -  | "fa" =>
    1.72 -    let val ct = cert_Trueprop sg fm2
    1.73 -    in simple_prove_goal_cterm2 ct [simple_arith_tac 1]  
    1.74 -
    1.75 -    end
    1.76 +  | "fa" => [simple_arith_tac 1]
    1.77  
    1.78    | "sa" =>
    1.79 -    let
    1.80 -      val ss = presburger_ss addsimps zadd_ac
    1.81 -      val ct = cert_Trueprop sg fm2
    1.82 -    in 
    1.83 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
    1.84 +    let val ss = presburger_ss addsimps zadd_ac
    1.85 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end
    1.86  
    1.87 -    end
    1.88    (* like Existance Conjunction *)
    1.89    | "ec" =>
    1.90 -    let
    1.91 -      val ss = presburger_ss addsimps zadd_ac
    1.92 -      val ct = cert_Trueprop sg fm2
    1.93 -    in 
    1.94 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (blast_tac HOL_cs 1)]
    1.95 -    end
    1.96 +    let val ss = presburger_ss addsimps zadd_ac
    1.97 +    in [simp_tac ss 1, TRY (blast_tac HOL_cs 1)] end
    1.98  
    1.99    | "ac" =>
   1.100 -    let
   1.101 -      val ss = HOL_basic_ss addsimps zadd_ac
   1.102 -      val ct = cert_Trueprop sg fm2
   1.103 -    in 
   1.104 -      simple_prove_goal_cterm2 ct [simp_tac ss 1]
   1.105 -    end
   1.106 +    let val ss = HOL_basic_ss addsimps zadd_ac
   1.107 +    in [simp_tac ss 1] end
   1.108  
   1.109    | "lf" =>
   1.110 -    let
   1.111 -      val ss = presburger_ss addsimps zadd_ac
   1.112 -      val ct = cert_Trueprop sg fm2
   1.113 -    in 
   1.114 -      simple_prove_goal_cterm2 ct [simp_tac ss 1, TRY (simple_arith_tac 1)]  
   1.115 -
   1.116 -    end;
   1.117 +    let val ss = presburger_ss addsimps zadd_ac
   1.118 +    in [simp_tac ss 1, TRY (simple_arith_tac 1)] end));
   1.119  
   1.120  (*=============================================================*)
   1.121  (*-------------------------------------------------------------*)