summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/CTT/ex/synth.ML

author | paulson |

Tue Apr 30 11:08:09 1996 +0200 (1996-04-30) | |

changeset 1702 | 4aa538e82f76 |

parent 1459 | d12da312eff4 |

child 9251 | bd57acd44fc1 |

permissions | -rw-r--r-- |

Cosmetic re-ordering of declarations

1 (* Title: CTT/ex/synth

2 ID: $Id$

3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Copyright 1991 University of Cambridge

5 *)

7 writeln"Synthesis examples, using a crude form of narrowing";

10 writeln"discovery of predecessor function";

11 goal CTT.thy

12 "?a : SUM pred:?A . Eq(N, pred`0, 0) \

13 \ * (PROD n:N. Eq(N, pred ` succ(n), n))";

14 by (intr_tac[]);

15 by eqintr_tac;

16 by (resolve_tac reduction_rls 3);

17 by (resolve_tac comp_rls 5);

18 by (rew_tac[]);

19 result();

21 writeln"the function fst as an element of a function type";

22 val prems = goal CTT.thy

23 "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";

24 by (intr_tac prems);

25 by eqintr_tac;

26 by (resolve_tac reduction_rls 2);

27 by (resolve_tac comp_rls 4);

28 by (typechk_tac prems);

29 writeln"now put in A everywhere";

30 by (REPEAT (resolve_tac prems 1));

31 by (fold_tac basic_defs);

32 result();

34 writeln"An interesting use of the eliminator, when";

35 (*The early implementation of unification caused non-rigid path in occur check

36 See following example.*)

37 goal CTT.thy

38 "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) \

39 \ * Eq(?A, ?b(inr(i)), <succ(0), i>)";

40 by (intr_tac[]);

41 by eqintr_tac;

42 by (resolve_tac comp_rls 1);

43 by (rew_tac[]);

44 uresult();

46 (*Here we allow the type to depend on i.

47 This prevents the cycle in the first unification (no longer needed).

48 Requires flex-flex to preserve the dependence.

49 Simpler still: make ?A into a constant type N*N.*)

50 goal CTT.thy

51 "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) \

52 \ * Eq(?A(i), ?b(inr(i)), <succ(0),i>)";

54 writeln"A tricky combination of when and split";

55 (*Now handled easily, but caused great problems once*)

56 goal CTT.thy

57 "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i) \

58 \ * Eq(?A, ?b(inr(<i,j>)), j)";

59 by (intr_tac[]);

60 by eqintr_tac;

61 by (resolve_tac [ PlusC_inl RS trans_elem ] 1);

62 by (resolve_tac comp_rls 4);

63 by (resolve_tac reduction_rls 7);

64 by (resolve_tac comp_rls 10);

65 by (typechk_tac[]); (*2 secs*)

66 by (fold_tac basic_defs);

67 uresult();

69 (*similar but allows the type to depend on i and j*)

70 goal CTT.thy

71 "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \

72 \ * Eq(?A(i,j), ?b(inr(<i,j>)), j)";

74 (*similar but specifying the type N simplifies the unification problems*)

75 goal CTT.thy

76 "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i) \

77 \ * Eq(N, ?b(inr(<i,j>)), j)";

80 writeln"Deriving the addition operator";

81 goal Arith.thy

82 "?c : PROD n:N. Eq(N, ?f(0,n), n) \

83 \ * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";

84 by (intr_tac[]);

85 by eqintr_tac;

86 by (resolve_tac comp_rls 1);

87 by (rew_tac[]);

88 by (fold_tac arith_defs);

89 result();

91 writeln"The addition function -- using explicit lambdas";

92 goal Arith.thy

93 "?c : SUM plus : ?A . \

94 \ PROD x:N. Eq(N, plus`0`x, x) \

95 \ * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";

96 by (intr_tac[]);

97 by eqintr_tac;

98 by (resolve_tac [TSimp.split_eqn] 3);

99 by (SELECT_GOAL (rew_tac[]) 4);

100 by (resolve_tac [TSimp.split_eqn] 3);

101 by (SELECT_GOAL (rew_tac[]) 4);

102 by (res_inst_tac [("p","y")] NC_succ 3);

103 (** by (resolve_tac comp_rls 3); caused excessive branching **)

104 by (rew_tac[]);

105 by (fold_tac arith_defs);

106 result();

108 writeln"Reached end of file.";