src/HOL/Matrix/conv.ML
author obua
Fri Sep 03 17:10:36 2004 +0200 (2004-09-03)
changeset 15178 5f621aa35c25
permissions -rw-r--r--
Matrix theory, linear programming
obua@15178
     1
exception Fail_conv;
obua@15178
     2
obua@15178
     3
fun orelsec conv1 conv2 ct = conv1 ct handle Fail_conv => conv2 ct
obua@15178
     4
obua@15178
     5
val allc = Thm.reflexive
obua@15178
     6
obua@15178
     7
fun thenc conv1 conv2 ct = 
obua@15178
     8
    let 
obua@15178
     9
	fun rhs_of t = snd (Thm.dest_comb (strip_imp_concl (cprop_of t)))
obua@15178
    10
	    
obua@15178
    11
	val eq = conv1 ct
obua@15178
    12
    in
obua@15178
    13
	Thm.transitive eq (conv2 (rhs_of eq))
obua@15178
    14
    end
obua@15178
    15
obua@15178
    16
fun subc conv ct = 
obua@15178
    17
    case term_of ct of
obua@15178
    18
	_ $ _ => 
obua@15178
    19
	let 
obua@15178
    20
	    val (ct1, ct2) = Thm.dest_comb ct
obua@15178
    21
	in
obua@15178
    22
	    Thm.combination (conv ct1) (conv ct2)
obua@15178
    23
	end
obua@15178
    24
      | _ => allc ct
obua@15178
    25
obua@15178
    26
fun botc conv ct = thenc (subc (botc conv)) (orelsec conv allc) ct