equal
deleted
inserted
replaced
1 (* Title: HOL/ex/svc_funcs.ML |
1 (* Title: HOL/ex/svc_funcs.ML |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson |
2 Author: Lawrence C Paulson |
4 Copyright 1999 University of Cambridge |
3 Copyright 1999 University of Cambridge |
5 |
4 |
6 Translation functions for the interface to SVC |
5 Translation functions for the interface to SVC. |
7 |
6 |
8 Based upon the work of Soren T. Heilmann |
7 Based upon the work of Soren T. Heilmann |
9 |
8 |
10 Integers and naturals are translated as follows: |
9 Integers and naturals are translated as follows: |
11 In a positive context, replace x<y by x+1<=y |
10 In a positive context, replace x<y by x+1<=y |
124 |
123 |
125 (*Translate an Isabelle formula into an SVC expression |
124 (*Translate an Isabelle formula into an SVC expression |
126 pos ["positive"]: true if an assumption, false if a goal*) |
125 pos ["positive"]: true if an assumption, false if a goal*) |
127 fun expr_of pos t = |
126 fun expr_of pos t = |
128 let |
127 let |
129 val params = rev (rename_wrt_term t (Term.strip_all_vars t)) |
128 val params = rev (Term.rename_wrt_term t (Term.strip_all_vars t)) |
130 and body = Term.strip_all_body t |
129 and body = Term.strip_all_body t |
131 val nat_vars = ref ([] : string list) |
130 val nat_vars = ref ([] : string list) |
132 (*translation of a variable: record all natural numbers*) |
131 (*translation of a variable: record all natural numbers*) |
133 fun trans_var (a,T,is) = |
132 fun trans_var (a,T,is) = |
134 (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars)) |
133 (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars)) |