src/Pure/deriv.ML
changeset 1593 69ed69a9c32a
child 1601 0ef6ea27ab15
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/deriv.ML	Wed Mar 20 18:42:31 1996 +0100
     1.3 @@ -0,0 +1,150 @@
     1.4 +(*  Title:      Pure/deriv.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1996  University of Cambridge
     1.8 +
     1.9 +Derivations (proof objects) and functions for examining them
    1.10 +*)
    1.11 +
    1.12 +signature DERIV = 
    1.13 +  sig
    1.14 +  (*Object-level rules*)
    1.15 +  datatype orule = Subgoal of cterm
    1.16 +		 | Asm of int
    1.17 +		 | Res of deriv
    1.18 +		 | Equal of deriv
    1.19 +		 | Thm   of theory * string
    1.20 +		 | Other of deriv;
    1.21 +
    1.22 +  val size : deriv -> int
    1.23 +  val drop : 'a mtree * int -> 'a mtree
    1.24 +  val linear : deriv -> deriv list
    1.25 +  val tree : deriv -> orule mtree
    1.26 +  end;  
    1.27 +
    1.28 +structure Deriv : DERIV =
    1.29 +struct
    1.30 +
    1.31 +fun size (Join(Theorem _, _)) = 1
    1.32 +  | size (Join(_, ders)) = foldl op+ (1, map size ders);
    1.33 +
    1.34 +(*Conversion to linear format.  Children of a node are the LIST of inferences
    1.35 +  justifying ONE of the premises*)
    1.36 +fun rev_deriv (Join (rl, [])) 	= [Join(rl,[])]
    1.37 +  | rev_deriv (Join (Theorem arg, _)) 	= [Join(Theorem arg, [])]
    1.38 +  | rev_deriv (Join (Assumption arg, [der])) = 
    1.39 +              Join(Assumption arg,[]) :: rev_deriv der
    1.40 +  | rev_deriv (Join (Bicompose arg, [rder, sder])) =
    1.41 +	Join (Bicompose arg, linear rder) :: rev_deriv sder
    1.42 +  | rev_deriv (Join (_, [der]))	= rev_deriv der
    1.43 +  | rev_deriv (Join (rl, der::ders)) =	(*catch-all case; doubtful?*)
    1.44 +        Join(rl, flat (map linear ders)) :: rev_deriv der
    1.45 +and linear der 	= rev (rev_deriv der);
    1.46 +
    1.47 +
    1.48 +(*** Conversion of object-level proof trees ***)
    1.49 +
    1.50 +(*Object-level rules*)
    1.51 +datatype orule = Subgoal of cterm
    1.52 +	       | Asm of int
    1.53 +               | Res of deriv
    1.54 +               | Equal of deriv
    1.55 +               | Thm   of theory * string
    1.56 +               | Other of deriv;
    1.57 +
    1.58 +(*At position i, splice in value x, removing ngoal elements*)
    1.59 +fun splice (i,x,ngoal,prfs) =
    1.60 +    let val prfs0 = take(i-1,prfs)
    1.61 +        and prfs1 = drop(i-1,prfs)
    1.62 +        val prfs2 = Join (x, take(ngoal, prfs1)) :: drop(ngoal, prfs1)
    1.63 +    in  prfs0 @ prfs2  end;
    1.64 +
    1.65 +(*Deletes trivial uses of Equal_elim; hides derivations of Theorems*)
    1.66 +fun simp_deriv (Join (Equal_elim, [Join (Rewrite_cterm _, []), der])) =
    1.67 +      simp_deriv der
    1.68 +  | simp_deriv (Join (Equal_elim, [Join (Reflexive _, []), der])) =
    1.69 +      simp_deriv der
    1.70 +  | simp_deriv (Join (rule as Theorem arg, [_])) = Join (rule, [])
    1.71 +  | simp_deriv (Join (rule, ders)) = Join (rule, map simp_deriv ders);
    1.72 +
    1.73 +(*Proof term is an equality: first premise of equal_elim.
    1.74 +  Attempt to decode proof terms made by Drule.goals_conv.
    1.75 +  Subgoal numbers are returned; they are wrong if original subgoal
    1.76 +	had flexflex pairs!
    1.77 +  NEGATIVE i means "could affect all subgoals starting from i"*)
    1.78 +fun scan_equals (i, Join (Combination, 
    1.79 +			   [Join (Combination, [_, der1]), der2])) =
    1.80 +    (case der1 of	(*ignore trivial cases*)
    1.81 +         Join (Reflexive _, _)      => scan_equals (i+1, der2)
    1.82 +       | Join (Rewrite_cterm _, []) => scan_equals (i+1, der2)
    1.83 +       | Join (Rewrite_cterm _, _)  => (i,der1) :: scan_equals (i+1, der2)
    1.84 +       | _ (*impossible in gconv*)  => [])
    1.85 +  | scan_equals (i, Join (Reflexive _, [])) = []
    1.86 +  | scan_equals (i, Join (Rewrite_cterm _, [])) = []
    1.87 +	(*Anything else could affect ALL following goals*)
    1.88 +  | scan_equals (i, der) = [(~i,der)];
    1.89 +
    1.90 +(*Record uses of equality reasoning on 1 or more subgoals*)
    1.91 +fun update_equals ((i,der), prfs) = 
    1.92 +      if i>0 then splice (i, Equal (simp_deriv der), 1, prfs)
    1.93 +      else take (~i-1, prfs) @
    1.94 +	   map (fn prf => Join (Equal (simp_deriv der), [prf])) 
    1.95 +	       (drop (~i-1, prfs));
    1.96 +
    1.97 +fun delift (Join (Lift_rule _, [der])) = der
    1.98 +  | delift der = der;
    1.99 +
   1.100 +(*Conversion to an object-level proof tree.
   1.101 +  Uses embedded Lift_rules to "annotate" the proof tree with subgoals;
   1.102 +    -- assumes that Lift_rule never occurs except with resolution
   1.103 +    -- may contain Vars that, in fact, are instantiated in that step*)
   1.104 +fun tree_aux (Join (Trivial ct, []), prfs) = Join(Subgoal ct, prfs)
   1.105 +  | tree_aux (Join (Assumption(i,_), [der]), prfs) = 
   1.106 +      tree_aux (der, splice (i, Asm i, 0, prfs))
   1.107 +  | tree_aux (Join (Equal_elim, [der1,der2]), prfs) = 
   1.108 +      tree_aux (der2, foldr update_equals (scan_equals (1, der1), prfs))
   1.109 +  | tree_aux (Join (Bicompose (match,true,i,ngoal,env), ders), prfs) =
   1.110 +		(*change eresolve_tac to proof by assumption*)
   1.111 +      tree_aux (Join (Assumption(i, Some env), 
   1.112 +			 [Join (Bicompose (match,false,i,ngoal,env), ders)]),
   1.113 +		   prfs)
   1.114 +  | tree_aux (Join (Lift_rule (ct,i), [der]), prfs) = 
   1.115 +      tree_aux (der, splice (i, Subgoal ct, 1, prfs))
   1.116 +  | tree_aux (Join (Bicompose arg, 
   1.117 +		       [Join (Instantiate _, [rder]), sder]), prfs) =
   1.118 +		(*Ignore Instantiate*)
   1.119 +      tree_aux (Join (Bicompose arg, [rder, sder]), prfs)
   1.120 +  | tree_aux (Join (Bicompose arg, 
   1.121 +		       [Join (Lift_rule larg, [rder]), sder]), prfs) =
   1.122 +		(*Move Lift_rule: to make a Subgoal on the result*)
   1.123 +      tree_aux (Join (Bicompose arg, [rder, 
   1.124 +					 Join(Lift_rule larg, [sder])]), prfs)
   1.125 +  | tree_aux (Join (Bicompose (match,ef,i,ngoal,env), 
   1.126 +		       [Join (Bicompose (match',ef',i',ngoal',env'),
   1.127 +			      [der1,der2]), 
   1.128 +			der3]), prfs) =
   1.129 +		(*associate resolutions to the right*)
   1.130 +      tree_aux (Join (Bicompose (match', ef', i'+i-1, ngoal', env'), 
   1.131 +			 [delift der1,	(*This Lift_rule would be wrong!*)
   1.132 +			  Join (Bicompose (match, ef, i, ngoal-ngoal'+1, env),
   1.133 +				[der2, der3])]), prfs)
   1.134 +  | tree_aux (Join (Bicompose (arg as (_,_,i,ngoal,_)), 
   1.135 +		       [rder, sder]), prfs) =
   1.136 +		(*resolution with basic rule/assumption -- we hope!*)
   1.137 +      tree_aux (sder, splice (i, Res (simp_deriv rder), ngoal, prfs))
   1.138 +  | tree_aux (Join (Theorem arg, _), prfs)	= Join(Thm arg, prfs)
   1.139 +  | tree_aux (Join (_, [der]), prfs)	= tree_aux (der,prfs)
   1.140 +  | tree_aux (der, prfs) = Join(Other (simp_deriv der), prfs);
   1.141 +
   1.142 +
   1.143 +fun tree der = tree_aux (der,[]);
   1.144 +
   1.145 +(*Currently declared at end, to avoid conflicting with library's drop
   1.146 +  Can put it after "size" once we switch to List.drop*)
   1.147 +fun drop (der,0) = der
   1.148 +  | drop (Join (_, der::_), n) = drop (der, n-1);
   1.149 +
   1.150 +end;
   1.151 +
   1.152 +
   1.153 +(*We do NOT open this structure*)