src/HOL/Tools/cnf_funcs.ML
changeset 32232 6c394343360f
parent 32231 95b8afcbb0ed
child 32283 3bebc195c124
     1.1 --- a/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 20:45:40 2009 +0200
     1.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Mon Jul 27 23:17:40 2009 +0200
     1.3 @@ -33,19 +33,20 @@
     1.4  
     1.5  signature CNF =
     1.6  sig
     1.7 -	val is_atom           : Term.term -> bool
     1.8 -	val is_literal        : Term.term -> bool
     1.9 -	val is_clause         : Term.term -> bool
    1.10 -	val clause_is_trivial : Term.term -> bool
    1.11 +	val is_atom: term -> bool
    1.12 +	val is_literal: term -> bool
    1.13 +	val is_clause: term -> bool
    1.14 +	val clause_is_trivial: term -> bool
    1.15  
    1.16 -	val clause2raw_thm : Thm.thm -> Thm.thm
    1.17 +	val clause2raw_thm: thm -> thm
    1.18  
    1.19 -	val weakening_tac : int -> Tactical.tactic  (* removes the first hypothesis of a subgoal *)
    1.20 +	val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
    1.21  
    1.22 -	val make_cnf_thm  : theory -> Term.term -> Thm.thm
    1.23 -	val make_cnfx_thm : theory -> Term.term ->  Thm.thm
    1.24 -	val cnf_rewrite_tac  : int -> Tactical.tactic  (* converts all prems of a subgoal to CNF *)
    1.25 -	val cnfx_rewrite_tac : int -> Tactical.tactic  (* converts all prems of a subgoal to (almost) definitional CNF *)
    1.26 +	val make_cnf_thm: theory -> term -> thm
    1.27 +	val make_cnfx_thm: theory -> term -> thm
    1.28 +	val cnf_rewrite_tac: Proof.context -> int -> tactic  (* converts all prems of a subgoal to CNF *)
    1.29 +	val cnfx_rewrite_tac: Proof.context -> int -> tactic
    1.30 +	  (* converts all prems of a subgoal to (almost) definitional CNF *)
    1.31  end;
    1.32  
    1.33  structure cnf : CNF =
    1.34 @@ -505,8 +506,6 @@
    1.35  (* weakening_tac: removes the first hypothesis of the 'i'-th subgoal         *)
    1.36  (* ------------------------------------------------------------------------- *)
    1.37  
    1.38 -(* int -> Tactical.tactic *)
    1.39 -
    1.40  fun weakening_tac i =
    1.41  	dtac weakening_thm i THEN atac (i+1);
    1.42  
    1.43 @@ -516,17 +515,16 @@
    1.44  (*      premise)                                                             *)
    1.45  (* ------------------------------------------------------------------------- *)
    1.46  
    1.47 -(* int -> Tactical.tactic *)
    1.48 -
    1.49 -fun cnf_rewrite_tac i =
    1.50 +fun cnf_rewrite_tac ctxt i =
    1.51  	(* cut the CNF formulas as new premises *)
    1.52 -	OldGoals.METAHYPS (fn prems =>
    1.53 +	FOCUS (fn {prems, ...} =>
    1.54  		let
    1.55 -			val cnf_thms = map (fn pr => make_cnf_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
    1.56 +		  val thy = ProofContext.theory_of ctxt
    1.57 +			val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
    1.58  			val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
    1.59  		in
    1.60  			cut_facts_tac cut_thms 1
    1.61 -		end) i
    1.62 +		end) ctxt i
    1.63  	(* remove the original premises *)
    1.64  	THEN SELECT_GOAL (fn thm =>
    1.65  		let
    1.66 @@ -540,17 +538,16 @@
    1.67  (*      (possibly introducing new literals)                                  *)
    1.68  (* ------------------------------------------------------------------------- *)
    1.69  
    1.70 -(* int -> Tactical.tactic *)
    1.71 -
    1.72 -fun cnfx_rewrite_tac i =
    1.73 +fun cnfx_rewrite_tac ctxt i =
    1.74  	(* cut the CNF formulas as new premises *)
    1.75 -	OldGoals.METAHYPS (fn prems =>
    1.76 +	FOCUS (fn {prems, ...} =>
    1.77  		let
    1.78 -			val cnfx_thms = map (fn pr => make_cnfx_thm (theory_of_thm pr) ((HOLogic.dest_Trueprop o prop_of) pr)) prems
    1.79 +		  val thy = ProofContext.theory_of ctxt;
    1.80 +			val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
    1.81  			val cut_thms  = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
    1.82  		in
    1.83  			cut_facts_tac cut_thms 1
    1.84 -		end) i
    1.85 +		end) ctxt i
    1.86  	(* remove the original premises *)
    1.87  	THEN SELECT_GOAL (fn thm =>
    1.88  		let