8 theory Synthesis |
8 theory Synthesis |
9 imports "../Arith" |
9 imports "../Arith" |
10 begin |
10 begin |
11 |
11 |
12 text "discovery of predecessor function" |
12 text "discovery of predecessor function" |
13 schematic_lemma "?a : SUM pred:?A . Eq(N, pred`0, 0) |
13 schematic_goal "?a : SUM pred:?A . Eq(N, pred`0, 0) |
14 * (PROD n:N. Eq(N, pred ` succ(n), n))" |
14 * (PROD n:N. Eq(N, pred ` succ(n), n))" |
15 apply intr |
15 apply intr |
16 apply eqintr |
16 apply eqintr |
17 apply (rule_tac [3] reduction_rls) |
17 apply (rule_tac [3] reduction_rls) |
18 apply (rule_tac [5] comp_rls) |
18 apply (rule_tac [5] comp_rls) |
19 apply rew |
19 apply rew |
20 done |
20 done |
21 |
21 |
22 text "the function fst as an element of a function type" |
22 text "the function fst as an element of a function type" |
23 schematic_lemma [folded basic_defs]: |
23 schematic_goal [folded basic_defs]: |
24 "A type \<Longrightarrow> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)" |
24 "A type \<Longrightarrow> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)" |
25 apply intr |
25 apply intr |
26 apply eqintr |
26 apply eqintr |
27 apply (rule_tac [2] reduction_rls) |
27 apply (rule_tac [2] reduction_rls) |
28 apply (rule_tac [4] comp_rls) |
28 apply (rule_tac [4] comp_rls) |
32 done |
32 done |
33 |
33 |
34 text "An interesting use of the eliminator, when" |
34 text "An interesting use of the eliminator, when" |
35 (*The early implementation of unification caused non-rigid path in occur check |
35 (*The early implementation of unification caused non-rigid path in occur check |
36 See following example.*) |
36 See following example.*) |
37 schematic_lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) |
37 schematic_goal "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0 , i>) |
38 * Eq(?A, ?b(inr(i)), <succ(0), i>)" |
38 * Eq(?A, ?b(inr(i)), <succ(0), i>)" |
39 apply intr |
39 apply intr |
40 apply eqintr |
40 apply eqintr |
41 apply (rule comp_rls) |
41 apply (rule comp_rls) |
42 apply rew |
42 apply rew |
44 |
44 |
45 (*Here we allow the type to depend on i. |
45 (*Here we allow the type to depend on i. |
46 This prevents the cycle in the first unification (no longer needed). |
46 This prevents the cycle in the first unification (no longer needed). |
47 Requires flex-flex to preserve the dependence. |
47 Requires flex-flex to preserve the dependence. |
48 Simpler still: make ?A into a constant type N*N.*) |
48 Simpler still: make ?A into a constant type N*N.*) |
49 schematic_lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) |
49 schematic_goal "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0 , i>) |
50 * Eq(?A(i), ?b(inr(i)), <succ(0),i>)" |
50 * Eq(?A(i), ?b(inr(i)), <succ(0),i>)" |
51 oops |
51 oops |
52 |
52 |
53 text "A tricky combination of when and split" |
53 text "A tricky combination of when and split" |
54 (*Now handled easily, but caused great problems once*) |
54 (*Now handled easily, but caused great problems once*) |
55 schematic_lemma [folded basic_defs]: |
55 schematic_goal [folded basic_defs]: |
56 "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i) |
56 "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i) |
57 * Eq(?A, ?b(inr(<i,j>)), j)" |
57 * Eq(?A, ?b(inr(<i,j>)), j)" |
58 apply intr |
58 apply intr |
59 apply eqintr |
59 apply eqintr |
60 apply (rule PlusC_inl [THEN trans_elem]) |
60 apply (rule PlusC_inl [THEN trans_elem]) |
63 apply (rule_tac [10] comp_rls) |
63 apply (rule_tac [10] comp_rls) |
64 apply typechk |
64 apply typechk |
65 done |
65 done |
66 |
66 |
67 (*similar but allows the type to depend on i and j*) |
67 (*similar but allows the type to depend on i and j*) |
68 schematic_lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) |
68 schematic_goal "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) |
69 * Eq(?A(i,j), ?b(inr(<i,j>)), j)" |
69 * Eq(?A(i,j), ?b(inr(<i,j>)), j)" |
70 oops |
70 oops |
71 |
71 |
72 (*similar but specifying the type N simplifies the unification problems*) |
72 (*similar but specifying the type N simplifies the unification problems*) |
73 schematic_lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i) |
73 schematic_goal "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i) |
74 * Eq(N, ?b(inr(<i,j>)), j)" |
74 * Eq(N, ?b(inr(<i,j>)), j)" |
75 oops |
75 oops |
76 |
76 |
77 |
77 |
78 text "Deriving the addition operator" |
78 text "Deriving the addition operator" |
79 schematic_lemma [folded arith_defs]: |
79 schematic_goal [folded arith_defs]: |
80 "?c : PROD n:N. Eq(N, ?f(0,n), n) |
80 "?c : PROD n:N. Eq(N, ?f(0,n), n) |
81 * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))" |
81 * (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))" |
82 apply intr |
82 apply intr |
83 apply eqintr |
83 apply eqintr |
84 apply (rule comp_rls) |
84 apply (rule comp_rls) |
85 apply rew |
85 apply rew |
86 done |
86 done |
87 |
87 |
88 text "The addition function -- using explicit lambdas" |
88 text "The addition function -- using explicit lambdas" |
89 schematic_lemma [folded arith_defs]: |
89 schematic_goal [folded arith_defs]: |
90 "?c : SUM plus : ?A . |
90 "?c : SUM plus : ?A . |
91 PROD x:N. Eq(N, plus`0`x, x) |
91 PROD x:N. Eq(N, plus`0`x, x) |
92 * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))" |
92 * (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))" |
93 apply intr |
93 apply intr |
94 apply eqintr |
94 apply eqintr |