prove_goal.el
author paulson
Sat, 08 Feb 2003 16:05:33 +0100
changeset 13812 91713a1915ee
parent 0 a5a9c433f639
permissions -rw-r--r--
converting HOL/UNITY to use unconditional fairness
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
;; special function for Isabelle
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
; goalify.el
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
; Emacs command to change "goal" proofs to "prove_goal" proofs 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
; and reverse IN A REGION.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
;    [would be difficult in "sed" since replacements involve multiple lines]
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
;; origin is prove_goalify.el
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
;; enhanced by Franz Regensburger
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
;;    corrected some errors in regular expressions
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
;;    changed name prove_goalify --> goalify
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
;;    added inverse functions        ungoalify
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
; function goalify:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
; val PAT = goalARGS;$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
; COMMANDS;$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
; val ID = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
; to
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
; val ID = prove_goalARGS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
;  (fn PAT=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
;  [
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
;  COMMANDS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
;  ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
;; Note: PAT must be an identifier. _ as pattern is not supported.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
;;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
; function ungoalify:
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
; val ID = prove_goalARGS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
;  (fn PAT=>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
;  [
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
;  COMMANDS
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
;  ]);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
; to 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
; val PAT = goalARGS;$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
; COMMANDS;$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
; val ID = result();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
; 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
(defun ungoalify (alpha omega)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
 "Change well-formed prove_goal proofs to goal...result"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
  (interactive "r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
	       "*") 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  ; 0: restrict editing to region
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  (narrow-to-region alpha omega)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
  ; 1: insert delimiter ID 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
  (replace-regexp  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  "[ \t]*val[ \t]+\\([^ \t\n=]+\\)[ \t\n=]+prove_goal" "\\1")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
  ; 2: insertt delimiter ARGS  PAT  and  before first command   
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  (replace-regexp  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
  "[ \n\t]*(fn[ \t]+\\([^=]+\\)=>[^(]*" "\\1\n")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
  ; 3: shift  over all commands
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
  ; Note: only one line per command
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
  (goto-char (point-max))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
  (while (not (equal (point) (point-min)))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
    (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
    (replace-regexp  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
    "[ \t]*\\(.*\\),[ \t]*\n" "by \\1;\n"))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
    
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  ; 4: fix last 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
  (replace-regexp  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
    "[ \t]*\\(.*\\)[ \t\n]*\][ \t\n]*)[ \t\n]*;" "by \\1;")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
  ; 5: arange new val Pat = goal .. 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
  (replace-regexp  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
  "\\([^]*\\)\\([^]*\\)\\([^]*\\)\n\\([^]*\\)"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
  "val \\3= goal\\2;\n\\4\nval \\1 = result();")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
  ; widen again
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
  (widen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
(defun goalify (alpha omega)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
 "Change well-formed goal...result proofs to use prove_goal"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
  (interactive "r"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
               "*") 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
  ; 0: restrict editing to region
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
  (narrow-to-region alpha omega)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
  ; 1: delimit the identifier in "val ID = result()" using ^Q
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
  (replace-regexp  "val[ \t\n]+\\([^ \t\n=]+\\)[ \t\n=]+result();[ \t]*$"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
   "\\1")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
  ; 2: replace terminal \";  by  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
  (replace-regexp  "\";[ \t]*$" "")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
  ; 3: replace lines "by ...;" with "...,"
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
  (replace-regexp  "by[ \n\t]*\\([^;]*\\)[ \t\n]*;"  "\t\\1,")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
  ; 4: removing the extra commas, those followed by ^Q
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
  (replace-regexp  ",[ \n\t]*"  "")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   115
  ; 5: transforming goal... to prove_goal...
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   116
  (goto-char (point-min))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   117
  (replace-regexp
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   118
  "val[ \t\n]+\\([^ \n\t=]+\\)[ \t\n=]+goal\\([^]*\\)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   119
\\([^]*\\)\\([^]*\\)"  
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   120
  "val \\4 = prove_goal\\2\"\n (fn \\1 =>\n\t[\n\\3\n\t]);")
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   121
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   122
  ; 6: widen again
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   123
  (widen)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   124
)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   125