author paulson Wed Mar 20 18:42:31 1996 +0100 (1996-03-20) changeset 1593 69ed69a9c32a parent 1592 d89d5ff2397f child 1594 b776e3223dd6
New module for proof objects (deriviations)
 src/Pure/deriv.ML file | annotate | diff | revisions
```     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.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*)
```