# HG changeset patch
# User oheimb
# Date 873192332 -7200
# Node ID 4c484f03079cec900db680b27e3cf3abb2557cae
# Parent  5f6ab7fbd53b83124b77db1516e434eeb1a37076
added case_prover

diff -r 5f6ab7fbd53b -r 4c484f03079c src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Thu Aug 21 12:57:24 1997 +0200
+++ b/src/HOLCF/Fix.ML	Tue Sep 02 11:25:32 1997 +0200
@@ -391,21 +391,17 @@
 
 fun fix_tac5 thm i  = ((rtac trans i) THEN (rtac (thm RS fix_eq5) i)); 
 
-fun fix_prover thy fixdef thm = prove_goal thy thm
- (fn prems =>
-        [
+(* proves the unfolding theorem for function equations f = fix`... *)
+fun fix_prover thy fixeq s = prove_goal thy s (fn prems => [
         (rtac trans 1),
-        (rtac (fixdef RS fix_eq4) 1),
+        (rtac (fixeq RS fix_eq4) 1),
         (rtac trans 1),
         (rtac beta_cfun 1),
         (Simp_tac 1)
         ]);
 
-(* use this one for definitions! *)
-
-fun fix_prover2 thy fixdef thm = prove_goal thy thm
- (fn prems =>
-        [
+(* proves the unfolding theorem for function definitions f == fix`... *)
+fun fix_prover2 thy fixdef s = prove_goal thy s (fn prems => [
         (rtac trans 1),
         (rtac (fix_eq2) 1),
         (rtac fixdef 1),
@@ -413,6 +409,14 @@
         (Simp_tac 1)
         ]);
 
+(* proves an application case for a function from its unfolding thm *)
+fun case_prover thy unfold s = prove_goal thy s (fn prems => [
+	(cut_facts_tac prems 1),
+	(rtac trans 1),
+	(stac unfold 1),
+	(Auto_tac ())
+	]);
+
 (* ------------------------------------------------------------------------ *)
 (* better access to definitions                                             *)
 (* ------------------------------------------------------------------------ *)
@@ -875,10 +879,10 @@
         "!!P. [| adm(%x.~(P x)); adm Q |] ==> adm(%x.P x --> Q x)"
  (fn prems =>
         [
-        subgoal_tac "(%x.P x --> Q x) = (%x. ~P x | Q x)" 1,
-        (Asm_simp_tac 1),
-        (etac adm_disj 1),
-        (atac 1),
+        (subgoal_tac "(%x.P x --> Q x) = (%x. ~P x | Q x)" 1),
+         (Asm_simp_tac 1),
+         (etac adm_disj 1),
+         (atac 1),
         (rtac ext 1),
         (fast_tac HOL_cs 1)
         ]);