src/CTT/ex/Synthesis.thy
author wenzelm
Fri, 02 Jun 2006 18:15:38 +0200
changeset 19761 5cd82054c2c6
child 19774 5fe7731d0836
permissions -rw-r--r--
removed obsolete ML files;
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
    ID:         $Id$
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     5
*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     6
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     7
header "Synthesis examples, using a crude form of narrowing"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     8
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
     9
theory Synthesis
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
imports Arith
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
begin
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    12
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    13
text "discovery of predecessor function"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    14
lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)    
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    15
                  *  (PROD n:N. Eq(N, pred ` succ(n), n))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    16
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    17
apply (tactic eqintr_tac)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    18
apply (rule_tac [3] reduction_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
apply (rule_tac [5] comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    21
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    22
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    23
text "the function fst as an element of a function type"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    24
lemma [folded basic_defs]:
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    25
  "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    26
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    27
apply (tactic eqintr_tac)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    28
apply (rule_tac [2] reduction_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    29
apply (rule_tac [4] comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    30
apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    31
txt "now put in A everywhere"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
apply assumption+
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    34
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    35
text "An interesting use of the eliminator, when"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    36
(*The early implementation of unification caused non-rigid path in occur check
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    37
  See following example.*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    38
lemma "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)   
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    39
                   * Eq(?A, ?b(inr(i)), <succ(0), i>)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    40
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    41
apply (tactic eqintr_tac)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    42
apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    43
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    44
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    45
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    46
(*Here we allow the type to depend on i.  
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    47
 This prevents the cycle in the first unification (no longer needed).  
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    48
 Requires flex-flex to preserve the dependence.
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    49
 Simpler still: make ?A into a constant type N*N.*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    50
lemma "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    51
                  *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    53
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    54
text "A tricky combination of when and split"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    55
(*Now handled easily, but caused great problems once*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    56
lemma [folded basic_defs]:
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    57
  "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)    
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    58
                           *  Eq(?A, ?b(inr(<i,j>)), j)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    59
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    60
apply (tactic eqintr_tac)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    61
apply (rule PlusC_inl [THEN trans_elem])
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    62
apply (rule_tac [4] comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    63
apply (rule_tac [7] reduction_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    64
apply (rule_tac [10] comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    65
apply (tactic "typechk_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    67
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    68
(*similar but allows the type to depend on i and j*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    69
lemma "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i)  
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    70
                          *   Eq(?A(i,j), ?b(inr(<i,j>)), j)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    71
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    72
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    73
(*similar but specifying the type N simplifies the unification problems*)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    74
lemma "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)   
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    75
                          *   Eq(N, ?b(inr(<i,j>)), j)"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    76
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    77
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    78
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    79
text "Deriving the addition operator"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    80
lemma [folded arith_defs]:
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    81
  "?c : PROD n:N. Eq(N, ?f(0,n), n)   
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    82
                  *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    83
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    84
apply (tactic eqintr_tac)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    85
apply (rule comp_rls)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    86
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    87
oops
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    88
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    89
text "The addition function -- using explicit lambdas"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    90
lemma [folded arith_defs]:
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    91
  "?c : SUM plus : ?A .   
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    92
         PROD x:N. Eq(N, plus`0`x, x)   
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    93
                *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    94
apply (tactic "intr_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    95
apply (tactic eqintr_tac)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    96
apply (tactic "resolve_tac [TSimp.split_eqn] 3")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    97
apply (tactic "SELECT_GOAL (rew_tac []) 4")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    98
apply (tactic "resolve_tac [TSimp.split_eqn] 3")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
    99
apply (tactic "SELECT_GOAL (rew_tac []) 4")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   100
apply (rule_tac [3] p = "y" in NC_succ)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   101
  (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   102
apply (tactic "rew_tac []")
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   103
done
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   104
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   105
end
5cd82054c2c6 removed obsolete ML files;
wenzelm
parents:
diff changeset
   106