src/Pure/deriv.ML
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 2672 85d7e800d754
child 6085 3d8dcb09dbfb
permissions -rw-r--r--
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
     1 (*  Title:      Pure/deriv.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1996  University of Cambridge
     5 
     6 Derivations (proof objects) and functions for examining them
     7 *)
     8 
     9 signature DERIV = 
    10   sig
    11   (*Object-level rules*)
    12   datatype orule = Subgoal of cterm
    13 		 | Asm of int
    14 		 | Res of deriv
    15 		 | Equal of deriv
    16 		 | Thm   of string
    17 		 | Other of deriv;
    18 
    19   val size : deriv -> int
    20   val drop : 'a mtree * int -> 'a mtree
    21   val linear : deriv -> deriv list
    22   val tree : deriv -> orule mtree
    23   end;  
    24 
    25 structure Deriv : DERIV =
    26 struct
    27 
    28 fun size (Join(Theorem _, _)) = 1
    29   | size (Join(_, ders)) = foldl op+ (1, map size ders);
    30 
    31 (*Conversion to linear format.  Children of a node are the LIST of inferences
    32   justifying ONE of the premises*)
    33 fun rev_deriv (Join (rl, [])) 	= [Join(rl,[])]
    34   | rev_deriv (Join (Theorem name, _)) 	= [Join(Theorem name, [])]
    35   | rev_deriv (Join (Assumption arg, [der])) = 
    36               Join(Assumption arg,[]) :: rev_deriv der
    37   | rev_deriv (Join (Bicompose arg, [rder, sder])) =
    38 	Join (Bicompose arg, linear rder) :: rev_deriv sder
    39   | rev_deriv (Join (_, [der]))	= rev_deriv der
    40   | rev_deriv (Join (rl, der::ders)) =	(*catch-all case; doubtful?*)
    41         Join(rl, List.concat (map linear ders)) :: rev_deriv der
    42 and linear der 	= rev (rev_deriv der);
    43 
    44 
    45 (*** Conversion of object-level proof trees ***)
    46 
    47 (*Object-level rules*)
    48 datatype orule = Subgoal of cterm
    49 	       | Asm of int
    50                | Res of deriv
    51                | Equal of deriv
    52                | Thm   of string
    53                | Other of deriv;
    54 
    55 (*At position i, splice in value x, removing ngoal elements*)
    56 fun splice (i,x,ngoal,prfs) =
    57     let val prfs0 = take(i-1,prfs)
    58         and prfs1 = drop(i-1,prfs)
    59         val prfs2 = Join (x, take(ngoal, prfs1)) :: drop(ngoal, prfs1)
    60     in  prfs0 @ prfs2  end;
    61 
    62 (*Deletes trivial uses of Equal_elim; hides derivations of Theorems*)
    63 fun simp_deriv (Join (Equal_elim, [Join (Rewrite_cterm _, []), der])) =
    64       simp_deriv der
    65   | simp_deriv (Join (Equal_elim, [Join (Reflexive _, []), der])) =
    66       simp_deriv der
    67   | simp_deriv (Join (rule as Theorem name, [_])) = Join (rule, [])
    68   | simp_deriv (Join (rule, ders)) = Join (rule, map simp_deriv ders);
    69 
    70 (*Proof term is an equality: first premise of equal_elim.
    71   Attempt to decode proof terms made by Drule.goals_conv.
    72   Subgoal numbers are returned; they are wrong if original subgoal
    73 	had flexflex pairs!
    74   NEGATIVE i means "could affect all subgoals starting from i"*)
    75 fun scan_equals (i, Join (Combination, 
    76 			   [Join (Combination, [_, der1]), der2])) =
    77     (case der1 of	(*ignore trivial cases*)
    78          Join (Reflexive _, _)      => scan_equals (i+1, der2)
    79        | Join (Rewrite_cterm _, []) => scan_equals (i+1, der2)
    80        | Join (Rewrite_cterm _, _)  => (i,der1) :: scan_equals (i+1, der2)
    81        | _ (*impossible in gconv*)  => [])
    82   | scan_equals (i, Join (Reflexive _, [])) = []
    83   | scan_equals (i, Join (Rewrite_cterm _, [])) = []
    84 	(*Anything else could affect ALL following goals*)
    85   | scan_equals (i, der) = [(~i,der)];
    86 
    87 (*Record uses of equality reasoning on 1 or more subgoals*)
    88 fun update_equals ((i,der), prfs) = 
    89       if i>0 then splice (i, Equal (simp_deriv der), 1, prfs)
    90       else take (~i-1, prfs) @
    91 	   map (fn prf => Join (Equal (simp_deriv der), [prf])) 
    92 	       (drop (~i-1, prfs));
    93 
    94 fun delift (Join (Lift_rule _, [der])) = der
    95   | delift der = der;
    96 
    97 (*Conversion to an object-level proof tree.
    98   Uses embedded Lift_rules to "annotate" the proof tree with subgoals;
    99     -- assumes that Lift_rule never occurs except with resolution
   100     -- may contain Vars that, in fact, are instantiated in that step*)
   101 fun tree_aux (Join (Trivial ct, []), prfs) = Join(Subgoal ct, prfs)
   102   | tree_aux (Join (Assumption(i,_), [der]), prfs) = 
   103       tree_aux (der, splice (i, Asm i, 0, prfs))
   104   | tree_aux (Join (Equal_elim, [der1,der2]), prfs) = 
   105       tree_aux (der2, foldr update_equals (scan_equals (1, der1), prfs))
   106   | tree_aux (Join (Bicompose (match,true,i,ngoal,env), ders), prfs) =
   107 		(*change eresolve_tac to proof by assumption*)
   108       tree_aux (Join (Assumption(i, Some env), 
   109 			 [Join (Bicompose (match,false,i,ngoal,env), ders)]),
   110 		   prfs)
   111   | tree_aux (Join (Lift_rule (ct,i), [der]), prfs) = 
   112       tree_aux (der, splice (i, Subgoal ct, 1, prfs))
   113   | tree_aux (Join (Bicompose arg, 
   114 		       [Join (Instantiate _, [rder]), sder]), prfs) =
   115 		(*Ignore Instantiate*)
   116       tree_aux (Join (Bicompose arg, [rder, sder]), prfs)
   117   | tree_aux (Join (Bicompose arg, 
   118 		       [Join (Lift_rule larg, [rder]), sder]), prfs) =
   119 		(*Move Lift_rule: to make a Subgoal on the result*)
   120       tree_aux (Join (Bicompose arg, [rder, 
   121 					 Join(Lift_rule larg, [sder])]), prfs)
   122   | tree_aux (Join (Bicompose (match,ef,i,ngoal,env), 
   123 		       [Join (Bicompose (match',ef',i',ngoal',env'),
   124 			      [der1,der2]), 
   125 			der3]), prfs) =
   126 		(*associate resolutions to the right*)
   127       tree_aux (Join (Bicompose (match', ef', i'+i-1, ngoal', env'), 
   128 			 [delift der1,	(*This Lift_rule would be wrong!*)
   129 			  Join (Bicompose (match, ef, i, ngoal-ngoal'+1, env),
   130 				[der2, der3])]), prfs)
   131   | tree_aux (Join (Bicompose (arg as (_,_,i,ngoal,_)), 
   132 		       [rder, sder]), prfs) =
   133 		(*resolution with basic rule/assumption -- we hope!*)
   134       tree_aux (sder, splice (i, Res (simp_deriv rder), ngoal, prfs))
   135   | tree_aux (Join (Theorem name, _), prfs)	= Join(Thm name, prfs)
   136   | tree_aux (Join (_, [der]), prfs)	= tree_aux (der,prfs)
   137   | tree_aux (der, prfs) = Join(Other (simp_deriv der), prfs);
   138 
   139 
   140 fun tree der = tree_aux (der,[]);
   141 
   142 (*Currently declared at end, to avoid conflicting with library's drop
   143   Can put it after "size" once we switch to List.drop*)
   144 fun drop (der,0) = der
   145   | drop (Join (_, der::_), n) = drop (der, n-1)
   146   | drop (der,_) = der;
   147 
   148 end;
   149 
   150 
   151 (*We do NOT open this structure*)