src/Pure/deriv.ML
 author wenzelm Mon Nov 09 15:40:26 1998 +0100 (1998-11-09) changeset 5838 a4122945d638 parent 2672 85d7e800d754 child 6085 3d8dcb09dbfb permissions -rw-r--r--
```     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*)
```