19761

1 
(* Title: CTT/ex/Synthesis.thy


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1991 University of Cambridge


5 
*)


6 


7 
header "Synthesis examples, using a crude form of narrowing"


8 


9 
theory Synthesis


10 
imports Arith


11 
begin


12 


13 
text "discovery of predecessor function"


14 
lemma "?a : SUM pred:?A . Eq(N, pred`0, 0)


15 
* (PROD n:N. Eq(N, pred ` succ(n), n))"


16 
apply (tactic "intr_tac []")


17 
apply (tactic eqintr_tac)


18 
apply (rule_tac [3] reduction_rls)


19 
apply (rule_tac [5] comp_rls)


20 
apply (tactic "rew_tac []")


21 
done


22 


23 
text "the function fst as an element of a function type"


24 
lemma [folded basic_defs]:


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


26 
apply (tactic "intr_tac []")


27 
apply (tactic eqintr_tac)


28 
apply (rule_tac [2] reduction_rls)


29 
apply (rule_tac [4] comp_rls)


30 
apply (tactic "typechk_tac []")


31 
txt "now put in A everywhere"


32 
apply assumption+


33 
done


34 


35 
text "An interesting use of the eliminator, when"


36 
(*The early implementation of unification caused nonrigid path in occur check


37 
See following example.*)


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


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


40 
apply (tactic "intr_tac []")


41 
apply (tactic eqintr_tac)


42 
apply (rule comp_rls)


43 
apply (tactic "rew_tac []")


44 
oops


45 


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


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


48 
Requires flexflex to preserve the dependence.


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


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


51 
* Eq(?A(i), ?b(inr(i)), <succ(0),i>)"


52 
oops


53 


54 
text "A tricky combination of when and split"


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


56 
lemma [folded basic_defs]:


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


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


59 
apply (tactic "intr_tac []")


60 
apply (tactic eqintr_tac)


61 
apply (rule PlusC_inl [THEN trans_elem])


62 
apply (rule_tac [4] comp_rls)


63 
apply (rule_tac [7] reduction_rls)


64 
apply (rule_tac [10] comp_rls)


65 
apply (tactic "typechk_tac []")


66 
oops


67 


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


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


70 
* Eq(?A(i,j), ?b(inr(<i,j>)), j)"


71 
oops


72 


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


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


75 
* Eq(N, ?b(inr(<i,j>)), j)"


76 
oops


77 


78 


79 
text "Deriving the addition operator"


80 
lemma [folded arith_defs]:


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


82 
* (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"


83 
apply (tactic "intr_tac []")


84 
apply (tactic eqintr_tac)


85 
apply (rule comp_rls)


86 
apply (tactic "rew_tac []")


87 
oops


88 


89 
text "The addition function  using explicit lambdas"


90 
lemma [folded arith_defs]:


91 
"?c : SUM plus : ?A .


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


93 
* (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))"


94 
apply (tactic "intr_tac []")


95 
apply (tactic eqintr_tac)


96 
apply (tactic "resolve_tac [TSimp.split_eqn] 3")


97 
apply (tactic "SELECT_GOAL (rew_tac []) 4")


98 
apply (tactic "resolve_tac [TSimp.split_eqn] 3")


99 
apply (tactic "SELECT_GOAL (rew_tac []) 4")


100 
apply (rule_tac [3] p = "y" in NC_succ)


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


102 
apply (tactic "rew_tac []")


103 
done


104 


105 
end


106 
