1473

1 
(* Title: FOL/ex/prolog.thy

0

2 
ID: $Id$

1473

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory

0

4 
Copyright 1992 University of Cambridge


5 
*)


6 

17245

7 
header {* FirstOrder Logic: PROLOG examples *}


8 


9 
theory Prolog


10 
imports FOL


11 
begin


12 


13 
typedecl 'a list


14 
arities list :: ("term") "term"


15 
consts


16 
Nil :: "'a list"


17 
Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60)


18 
app :: "['a list, 'a list, 'a list] => o"


19 
rev :: "['a list, 'a list] => o"


20 
axioms


21 
appNil: "app(Nil,ys,ys)"


22 
appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"


23 
revNil: "rev(Nil,Nil)"


24 
revCons: "[ rev(xs,ys); app(ys, x:Nil, zs) ] ==> rev(x:xs, zs)"


25 

19819

26 
lemma "app(a:b:c:Nil, d:e:Nil, ?x)"


27 
apply (rule appNil appCons)


28 
apply (rule appNil appCons)


29 
apply (rule appNil appCons)


30 
apply (rule appNil appCons)


31 
done


32 


33 
lemma "app(?x, c:d:Nil, a:b:c:d:Nil)"


34 
apply (rule appNil appCons)+


35 
done


36 


37 
lemma "app(?x, ?y, a:b:c:d:Nil)"


38 
apply (rule appNil appCons)+


39 
back


40 
back


41 
back


42 
back


43 
done


44 


45 
(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)


46 
(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)


47 


48 
lemmas rules = appNil appCons revNil revCons


49 


50 
lemma "rev(a:b:c:d:Nil, ?x)"


51 
apply (rule rules)+


52 
done


53 


54 
lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"


55 
apply (rule rules)+


56 
done


57 


58 
lemma "rev(?x, a:b:c:Nil)"


59 
apply (rule rules)+  {* does not solve it directly! *}


60 
back


61 
back


62 
done


63 


64 
(*backtracking version*)


65 
ML {*


66 
val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1)


67 
*}


68 


69 
lemma "rev(?x, a:b:c:Nil)"


70 
apply (tactic prolog_tac)


71 
done


72 


73 
lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)"


74 
apply (tactic prolog_tac)


75 
done


76 


77 
(*rev([a..p], ?w) requires 153 inferences *)


78 
lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"


79 
apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})


80 
done


81 


82 
(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences


83 
total inferences = 2 + 1 + 17 + 561 = 581*)


84 
lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"


85 
apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *})


86 
done

17245

87 

0

88 
end
