src/CTT/ex/Synthesis.thy
author wenzelm
Wed, 17 May 2017 13:47:19 +0200
changeset 65851 c103358a5559
parent 65447 fae6051ec192
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     1
(*  Title:      CTT/ex/Synthesis.thy
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     3
    Copyright   1991  University of Cambridge
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     4
*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     5
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 36319
diff changeset
     6
section "Synthesis examples, using a crude form of narrowing"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     7
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     8
theory Synthesis
65447
fae6051ec192 clarified main CTT.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents: 61391
diff changeset
     9
imports "../CTT"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
begin
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    12
text "discovery of predecessor function"
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    13
schematic_goal "?a : \<Sum>pred:?A . Eq(N, pred`0, 0) \<times> (\<Prod>n:N. Eq(N, pred ` succ(n), n))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    14
apply intr
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    15
apply eqintr
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    16
apply (rule_tac [3] reduction_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    17
apply (rule_tac [5] comp_rls)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    18
apply rew
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    21
text "the function fst as an element of a function type"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 59498
diff changeset
    22
schematic_goal [folded basic_defs]:
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    23
  "A type \<Longrightarrow> ?a: \<Sum>f:?B . \<Prod>i:A. \<Prod>j:A. Eq(A, f ` <i,j>, i)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    24
apply intr
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    25
apply eqintr
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    26
apply (rule_tac [2] reduction_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    27
apply (rule_tac [4] comp_rls)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    28
apply typechk
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    29
txt "now put in A everywhere"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    30
apply assumption+
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    31
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
text "An interesting use of the eliminator, when"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    34
(*The early implementation of unification caused non-rigid path in occur check
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    35
  See following example.*)
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    36
schematic_goal "?a : \<Prod>i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    37
                   \<times> Eq(?A, ?b(inr(i)), <succ(0), i>)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    38
apply intr
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    39
apply eqintr
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    40
apply (rule comp_rls)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    41
apply rew
19774
5fe7731d0836 allow non-trivial schematic goals (via embedded term vars);
wenzelm
parents: 19761
diff changeset
    42
done
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    43
19774
5fe7731d0836 allow non-trivial schematic goals (via embedded term vars);
wenzelm
parents: 19761
diff changeset
    44
(*Here we allow the type to depend on i.
5fe7731d0836 allow non-trivial schematic goals (via embedded term vars);
wenzelm
parents: 19761
diff changeset
    45
 This prevents the cycle in the first unification (no longer needed).
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    46
 Requires flex-flex to preserve the dependence.
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    47
 Simpler still: make ?A into a constant type N \<times> N.*)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    48
schematic_goal "?a : \<Prod>i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    49
                  \<times>  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    50
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    51
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
text "A tricky combination of when and split"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    53
(*Now handled easily, but caused great problems once*)
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 59498
diff changeset
    54
schematic_goal [folded basic_defs]:
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    55
  "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A, ?b(inl(<i,j>)), i)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    56
                           \<times>  Eq(?A, ?b(inr(<i,j>)), j)"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    57
apply intr
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    58
apply eqintr
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    59
apply (rule PlusC_inl [THEN trans_elem])
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    60
apply (rule_tac [4] comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    61
apply (rule_tac [7] reduction_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    62
apply (rule_tac [10] comp_rls)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    63
apply typechk
19774
5fe7731d0836 allow non-trivial schematic goals (via embedded term vars);
wenzelm
parents: 19761
diff changeset
    64
done
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    65
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
(*similar but allows the type to depend on i and j*)
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    67
schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    68
                          \<times>   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    69
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    70
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    71
(*similar but specifying the type N simplifies the unification problems*)
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    72
schematic_goal "?a : \<Prod>i:N. \<Prod>j:N. Eq(N, ?b(inl(<i,j>)), i)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    73
                          \<times>   Eq(N, ?b(inr(<i,j>)), j)"
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    74
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    75
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    76
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    77
text "Deriving the addition operator"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 59498
diff changeset
    78
schematic_goal [folded arith_defs]:
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    79
  "?c : \<Prod>n:N. Eq(N, ?f(0,n), n)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    80
                  \<times>  (\<Prod>m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    81
apply intr
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    82
apply eqintr
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    83
apply (rule comp_rls)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    84
apply rew
19774
5fe7731d0836 allow non-trivial schematic goals (via embedded term vars);
wenzelm
parents: 19761
diff changeset
    85
done
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    86
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    87
text "The addition function -- using explicit lambdas"
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 59498
diff changeset
    88
schematic_goal [folded arith_defs]:
61391
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    89
  "?c : \<Sum>plus : ?A .
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    90
         \<Prod>x:N. Eq(N, plus`0`x, x)
2332d9be352b tuned syntax -- more symbols;
wenzelm
parents: 61337
diff changeset
    91
                \<times>  (\<Prod>y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    92
apply intr
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
    93
apply eqintr
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58977
diff changeset
    94
apply (tactic "resolve_tac @{context} [TSimp.split_eqn] 3")
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58889
diff changeset
    95
apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58977
diff changeset
    96
apply (tactic "resolve_tac @{context} [TSimp.split_eqn] 3")
58963
26bf09b95dda proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents: 58889
diff changeset
    97
apply (tactic "SELECT_GOAL (rew_tac @{context} []) 4")
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    98
apply (rule_tac [3] p = "y" in NC_succ)
59498
50b60f501b05 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents: 58977
diff changeset
    99
  (**  by (resolve_tac @{context} comp_rls 3);  caused excessive branching  **)
58972
5b026cfc5f04 more Isar proof methods;
wenzelm
parents: 58963
diff changeset
   100
apply rew
19761
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   101
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   102
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   103
end
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   104