summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Pure/deriv.ML

changeset 1601 | 0ef6ea27ab15 |

parent 1593 | 69ed69a9c32a |

child 2042 | 33b4c1624e26 |

equal
deleted
inserted
replaced

1600:901579c25021 | 1601:0ef6ea27ab15 |
---|---|

11 (*Object-level rules*) |
11 (*Object-level rules*) |

12 datatype orule = Subgoal of cterm |
12 datatype orule = Subgoal of cterm |

13 | Asm of int |
13 | Asm of int |

14 | Res of deriv |
14 | Res of deriv |

15 | Equal of deriv |
15 | Equal of deriv |

16 | Thm of theory * string |
16 | Thm of string |

17 | Other of deriv; |
17 | Other of deriv; |

18 |
18 |

19 val size : deriv -> int |
19 val size : deriv -> int |

20 val drop : 'a mtree * int -> 'a mtree |
20 val drop : 'a mtree * int -> 'a mtree |

21 val linear : deriv -> deriv list |
21 val linear : deriv -> deriv list |

29 | size (Join(_, ders)) = foldl op+ (1, map size ders); |
29 | size (Join(_, ders)) = foldl op+ (1, map size ders); |

30 |
30 |

31 (*Conversion to linear format. Children of a node are the LIST of inferences |
31 (*Conversion to linear format. Children of a node are the LIST of inferences |

32 justifying ONE of the premises*) |
32 justifying ONE of the premises*) |

33 fun rev_deriv (Join (rl, [])) = [Join(rl,[])] |
33 fun rev_deriv (Join (rl, [])) = [Join(rl,[])] |

34 | rev_deriv (Join (Theorem arg, _)) = [Join(Theorem arg, [])] |
34 | rev_deriv (Join (Theorem name, _)) = [Join(Theorem name, [])] |

35 | rev_deriv (Join (Assumption arg, [der])) = |
35 | rev_deriv (Join (Assumption arg, [der])) = |

36 Join(Assumption arg,[]) :: rev_deriv der |
36 Join(Assumption arg,[]) :: rev_deriv der |

37 | rev_deriv (Join (Bicompose arg, [rder, sder])) = |
37 | rev_deriv (Join (Bicompose arg, [rder, sder])) = |

38 Join (Bicompose arg, linear rder) :: rev_deriv sder |
38 Join (Bicompose arg, linear rder) :: rev_deriv sder |

39 | rev_deriv (Join (_, [der])) = rev_deriv der |
39 | rev_deriv (Join (_, [der])) = rev_deriv der |

47 (*Object-level rules*) |
47 (*Object-level rules*) |

48 datatype orule = Subgoal of cterm |
48 datatype orule = Subgoal of cterm |

49 | Asm of int |
49 | Asm of int |

50 | Res of deriv |
50 | Res of deriv |

51 | Equal of deriv |
51 | Equal of deriv |

52 | Thm of theory * string |
52 | Thm of string |

53 | Other of deriv; |
53 | Other of deriv; |

54 |
54 |

55 (*At position i, splice in value x, removing ngoal elements*) |
55 (*At position i, splice in value x, removing ngoal elements*) |

56 fun splice (i,x,ngoal,prfs) = |
56 fun splice (i,x,ngoal,prfs) = |

57 let val prfs0 = take(i-1,prfs) |
57 let val prfs0 = take(i-1,prfs) |

62 (*Deletes trivial uses of Equal_elim; hides derivations of Theorems*) |
62 (*Deletes trivial uses of Equal_elim; hides derivations of Theorems*) |

63 fun simp_deriv (Join (Equal_elim, [Join (Rewrite_cterm _, []), der])) = |
63 fun simp_deriv (Join (Equal_elim, [Join (Rewrite_cterm _, []), der])) = |

64 simp_deriv der |
64 simp_deriv der |

65 | simp_deriv (Join (Equal_elim, [Join (Reflexive _, []), der])) = |
65 | simp_deriv (Join (Equal_elim, [Join (Reflexive _, []), der])) = |

66 simp_deriv der |
66 simp_deriv der |

67 | simp_deriv (Join (rule as Theorem arg, [_])) = Join (rule, []) |
67 | simp_deriv (Join (rule as Theorem name, [_])) = Join (rule, []) |

68 | simp_deriv (Join (rule, ders)) = Join (rule, map simp_deriv ders); |
68 | simp_deriv (Join (rule, ders)) = Join (rule, map simp_deriv ders); |

69 |
69 |

70 (*Proof term is an equality: first premise of equal_elim. |
70 (*Proof term is an equality: first premise of equal_elim. |

71 Attempt to decode proof terms made by Drule.goals_conv. |
71 Attempt to decode proof terms made by Drule.goals_conv. |

72 Subgoal numbers are returned; they are wrong if original subgoal |
72 Subgoal numbers are returned; they are wrong if original subgoal |

130 [der2, der3])]), prfs) |
130 [der2, der3])]), prfs) |

131 | tree_aux (Join (Bicompose (arg as (_,_,i,ngoal,_)), |
131 | tree_aux (Join (Bicompose (arg as (_,_,i,ngoal,_)), |

132 [rder, sder]), prfs) = |
132 [rder, sder]), prfs) = |

133 (*resolution with basic rule/assumption -- we hope!*) |
133 (*resolution with basic rule/assumption -- we hope!*) |

134 tree_aux (sder, splice (i, Res (simp_deriv rder), ngoal, prfs)) |
134 tree_aux (sder, splice (i, Res (simp_deriv rder), ngoal, prfs)) |

135 | tree_aux (Join (Theorem arg, _), prfs) = Join(Thm arg, prfs) |
135 | tree_aux (Join (Theorem name, _), prfs) = Join(Thm name, prfs) |

136 | tree_aux (Join (_, [der]), prfs) = tree_aux (der,prfs) |
136 | tree_aux (Join (_, [der]), prfs) = tree_aux (der,prfs) |

137 | tree_aux (der, prfs) = Join(Other (simp_deriv der), prfs); |
137 | tree_aux (der, prfs) = Join(Other (simp_deriv der), prfs); |

138 |
138 |

139 |
139 |

140 fun tree der = tree_aux (der,[]); |
140 fun tree der = tree_aux (der,[]); |