isabelle: comparison src/HOL/Import/shuffler.ML

equal deleted inserted replaced

-:a3561bfe0ada
+:cd0dc678a205
 fun if_debug f x = if !debug then f x else ()
 val message = if_debug writeln
 (*Prints exceptions readably to users*)
 fun print_sign_exn_unit sign e =
 case e of
 THM (msg,i,thms) =>
-	 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
+(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg);
-	  List.app print_thm thms)
+List.app print_thm thms)
 | THEORY (msg,thys) =>
-	 (writeln ("Exception THEORY raised:\n" ^ msg);
+(writeln ("Exception THEORY raised:\n" ^ msg);
-	  List.app (writeln o Context.str_of_thy) thys)
+List.app (writeln o Context.str_of_thy) thys)
 | TERM (msg,ts) =>
-	 (writeln ("Exception TERM raised:\n" ^ msg);
+(writeln ("Exception TERM raised:\n" ^ msg);
-	  List.app (writeln o Sign.string_of_term sign) ts)
+List.app (writeln o Sign.string_of_term sign) ts)
 | TYPE (msg,Ts,ts) =>
-	 (writeln ("Exception TYPE raised:\n" ^ msg);
+(writeln ("Exception TYPE raised:\n" ^ msg);
-	  List.app (writeln o Sign.string_of_typ sign) Ts;
+List.app (writeln o Sign.string_of_typ sign) Ts;
-	  List.app (writeln o Sign.string_of_term sign) ts)
+List.app (writeln o Sign.string_of_term sign) ts)
 | e => raise e
 (*Prints an exception, then fails*)
 fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
 val string_of_thm = Library.setmp print_mode [] string_of_thm;
 val string_of_cterm = Library.setmp print_mode [] string_of_cterm;
 fun mk_meta_eq th =
 (case concl_of th of
-	 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
+Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th RS eq_reflection
 | Const("==",_) $ _ $ _ => th
 | _ => raise THM("Not an equality",0,[th]))
 handle _ => raise THM("Couldn't make meta equality",0,[th])
 fun mk_obj_eq th =
 (case concl_of th of
-	 Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
+Const("Trueprop",_) $ (Const("op =",_) $ _ $ _) => th
 | Const("==",_) $ _ $ _ => th RS meta_eq_to_obj_eq
 | _ => raise THM("Not an equality",0,[th]))
 handle _ => raise THM("Couldn't make object equality",0,[th])
 structure ShuffleDataArgs: THEORY_DATA_ARGS =
 val copy = I
 val extend = I
 fun merge _ = Library.gen_union Thm.eq_thm
 fun print _ thms =
 Pretty.writeln (Pretty.big_list "Shuffle theorems:"
-				    (map Display.pretty_thm thms))
+(map Display.pretty_thm thms))
 end
 structure ShuffleData = TheoryDataFun(ShuffleDataArgs)
 val weaken =
 let
-	val cert = cterm_of ProtoPure.thy
+val cert = cterm_of ProtoPure.thy
-	val P = Free("P",propT)
+val P = Free("P",propT)
-	val Q = Free("Q",propT)
+val Q = Free("Q",propT)
-	val PQ = Logic.mk_implies(P,Q)
+val PQ = Logic.mk_implies(P,Q)
-	val PPQ = Logic.mk_implies(P,PQ)
+val PPQ = Logic.mk_implies(P,PQ)
-	val cP = cert P
+val cP = cert P
-	val cQ = cert Q
+val cQ = cert Q
-	val cPQ = cert PQ
+val cPQ = cert PQ
-	val cPPQ = cert PPQ
+val cPPQ = cert PPQ
-	val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
+val th1 = assume cPQ |> implies_intr_list [cPQ,cP]
-	val th3 = assume cP
+val th3 = assume cP
-	val th4 = implies_elim_list (assume cPPQ) [th3,th3]
+val th4 = implies_elim_list (assume cPPQ) [th3,th3]
-				    |> implies_intr_list [cPPQ,cP]
+|> implies_intr_list [cPPQ,cP]
 in
-	equal_intr th4 th1 |> standard
+equal_intr th4 th1 |> standard
 end
 val imp_comm =
 let
-	val cert = cterm_of ProtoPure.thy
+val cert = cterm_of ProtoPure.thy
-	val P = Free("P",propT)
+val P = Free("P",propT)
-	val Q = Free("Q",propT)
+val Q = Free("Q",propT)
-	val R = Free("R",propT)
+val R = Free("R",propT)
-	val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
+val PQR = Logic.mk_implies(P,Logic.mk_implies(Q,R))
-	val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
+val QPR = Logic.mk_implies(Q,Logic.mk_implies(P,R))
-	val cP = cert P
+val cP = cert P
-	val cQ = cert Q
+val cQ = cert Q
-	val cPQR = cert PQR
+val cPQR = cert PQR
-	val cQPR = cert QPR
+val cQPR = cert QPR
-	val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
+val th1 = implies_elim_list (assume cPQR) [assume cP,assume cQ]
-				    |> implies_intr_list [cPQR,cQ,cP]
+|> implies_intr_list [cPQR,cQ,cP]
-	val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
+val th2 = implies_elim_list (assume cQPR) [assume cQ,assume cP]
-				    |> implies_intr_list [cQPR,cP,cQ]
+|> implies_intr_list [cQPR,cP,cQ]
 in
-	equal_intr th1 th2 |> standard
+equal_intr th1 th2 |> standard
 end
 val def_norm =
 let
-	val cert = cterm_of ProtoPure.thy
+val cert = cterm_of ProtoPure.thy
-	val aT = TFree("'a",[])
+val aT = TFree("'a",[])
-	val bT = TFree("'b",[])
+val bT = TFree("'b",[])
-	val v = Free("v",aT)
+val v = Free("v",aT)
-	val P = Free("P",aT-->bT)
+val P = Free("P",aT-->bT)
-	val Q = Free("Q",aT-->bT)
+val Q = Free("Q",aT-->bT)
-	val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
+val cvPQ = cert (list_all ([("v",aT)],Logic.mk_equals(P $ Bound 0,Q $ Bound 0)))
-	val cPQ = cert (Logic.mk_equals(P,Q))
+val cPQ = cert (Logic.mk_equals(P,Q))
-	val cv = cert v
+val cv = cert v
-	val rew = assume cvPQ
+val rew = assume cvPQ
-			 |> forall_elim cv
+|> forall_elim cv
-			 |> abstract_rule "v" cv
+|> abstract_rule "v" cv
-	val (lhs,rhs) = Logic.dest_equals(concl_of rew)
+val (lhs,rhs) = Logic.dest_equals(concl_of rew)
-	val th1 = transitive (transitive
+val th1 = transitive (transitive
-				  (eta_conversion (cert lhs) |> symmetric)
+(eta_conversion (cert lhs) |> symmetric)
-				  rew)
+rew)
-			     (eta_conversion (cert rhs))
+(eta_conversion (cert rhs))
-			     |> implies_intr cvPQ
+|> implies_intr cvPQ
-	val th2 = combination (assume cPQ) (reflexive cv)
+val th2 = combination (assume cPQ) (reflexive cv)
-			      |> forall_intr cv
+|> forall_intr cv
-			      |> implies_intr cPQ
+|> implies_intr cPQ
 in
-	equal_intr th1 th2 |> standard
+equal_intr th1 th2 |> standard
 end
 val all_comm =
 let
-	val cert = cterm_of ProtoPure.thy
+val cert = cterm_of ProtoPure.thy
-	val xT = TFree("'a",[])
+val xT = TFree("'a",[])
-	val yT = TFree("'b",[])
+val yT = TFree("'b",[])
-	val P = Free("P",xT-->yT-->propT)
+val P = Free("P",xT-->yT-->propT)
-	val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
+val lhs = all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))
-	val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
+val rhs = all yT $ (Abs("y",yT,all xT $ (Abs("x",xT,P $ Bound 0 $ Bound 1))))
-	val cl = cert lhs
+val cl = cert lhs
-	val cr = cert rhs
+val cr = cert rhs
-	val cx = cert (Free("x",xT))
+val cx = cert (Free("x",xT))
-	val cy = cert (Free("y",yT))
+val cy = cert (Free("y",yT))
-	val th1 = assume cr
+val th1 = assume cr
-			 |> forall_elim_list [cy,cx]
+|> forall_elim_list [cy,cx]
-			 |> forall_intr_list [cx,cy]
+|> forall_intr_list [cx,cy]
-			 |> implies_intr cr
+|> implies_intr cr
-	val th2 = assume cl
+val th2 = assume cl
-			 |> forall_elim_list [cx,cy]
+|> forall_elim_list [cx,cy]
-			 |> forall_intr_list [cy,cx]
+|> forall_intr_list [cy,cx]
-			 |> implies_intr cl
+|> implies_intr cl
 in
-	equal_intr th1 th2 |> standard
+equal_intr th1 th2 |> standard
 end
 val equiv_comm =
 let
-	val cert = cterm_of ProtoPure.thy
+val cert = cterm_of ProtoPure.thy
-	val T    = TFree("'a",[])
+val T    = TFree("'a",[])
-	val t    = Free("t",T)
+val t    = Free("t",T)
-	val u    = Free("u",T)
+val u    = Free("u",T)
-	val ctu  = cert (Logic.mk_equals(t,u))
+val ctu  = cert (Logic.mk_equals(t,u))
-	val cut  = cert (Logic.mk_equals(u,t))
+val cut  = cert (Logic.mk_equals(u,t))
-	val th1  = assume ctu |> symmetric |> implies_intr ctu
+val th1  = assume ctu |> symmetric |> implies_intr ctu
-	val th2  = assume cut |> symmetric |> implies_intr cut
+val th2  = assume cut |> symmetric |> implies_intr cut
 in
-	equal_intr th1 th2 |> standard
+equal_intr th1 th2 |> standard
 end
 (* This simplification procedure rewrites !!x y. P x y
 deterministicly, in order for the normalization function, defined
 below, to handle nested quantifiers robustly *)
 local
 exception RESULT of int
 fun find_bound n (Bound i) = if i = n then raise RESULT 0
-			     else if i = n+1 then raise RESULT 1
+else if i = n+1 then raise RESULT 1
-			     else ()
+else ()
 | find_bound n (t $ u) = (find_bound n t; find_bound n u)
 | find_bound n (Abs(_,_,t)) = find_bound (n+1) t
 | find_bound _ _ = ()
 fun swap_bound n (Bound i) = if i = n then Bound (n+1)
-			     else if i = n+1 then Bound n
+else if i = n+1 then Bound n
-			     else Bound i
+else Bound i
 | swap_bound n (t $ u) = (swap_bound n t $ swap_bound n u)
 | swap_bound n (Abs(x,xT,t)) = Abs(x,xT,swap_bound (n+1) t)
 | swap_bound n t = t
 fun rew_th thy (xv as (x,xT)) (yv as (y,yT)) t =
 let
-	val lhs = list_all ([xv,yv],t)
+val lhs = list_all ([xv,yv],t)
-	val rhs = list_all ([yv,xv],swap_bound 0 t)
+val rhs = list_all ([yv,xv],swap_bound 0 t)
-	val rew = Logic.mk_equals (lhs,rhs)
+val rew = Logic.mk_equals (lhs,rhs)
-	val init = trivial (cterm_of thy rew)
+val init = trivial (cterm_of thy rew)
 in
-	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
+(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
 end
 fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
 let
-	val res = (find_bound 0 body;2) handle RESULT i => i
+val res = (find_bound 0 body;2) handle RESULT i => i
 in
-	case res of
+case res of
-	    0 => SOME (rew_th thy (x,xT) (y,yT) body)
+0 => SOME (rew_th thy (x,xT) (y,yT) body)
-	  | 1 => if string_ord(y,x) = LESS
+| 1 => if string_ord(y,x) = LESS
-		 then
+then
-		     let
+let
-			 val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
+val newt = Const("all",T1) $ (Abs(y,xT,Const("all",T2) $ Abs(x,yT,body)))
-			 val t_th    = reflexive (cterm_of thy t)
+val t_th    = reflexive (cterm_of thy t)
-			 val newt_th = reflexive (cterm_of thy newt)
+val newt_th = reflexive (cterm_of thy newt)
-		     in
+in
-			 SOME (transitive t_th newt_th)
+SOME (transitive t_th newt_th)
-		     end
+end
-		 else NONE
+else NONE
-	  | _ => error "norm_term (quant_rewrite) internal error"
+| _ => error "norm_term (quant_rewrite) internal error"
 end
 | quant_rewrite _ _ _ = (warning "quant_rewrite: Unknown lhs"; NONE)
 fun freeze_thaw_term t =
 let
-	val tvars = term_tvars t
+val tvars = term_tvars t
-	val tfree_names = add_term_tfree_names(t,[])
+val tfree_names = add_term_tfree_names(t,[])
-	val (type_inst,_) =
+val (type_inst,_) =
-	    Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
+Library.foldl (fn ((inst,used),(w as (v,_),S)) =>
-		      let
+let
-			  val v' = Name.variant used v
+val v' = Name.variant used v
-		      in
+in
-			  ((w,TFree(v',S))::inst,v'::used)
+((w,TFree(v',S))::inst,v'::used)
-		      end)
+end)
-		  (([],tfree_names),tvars)
+(([],tfree_names),tvars)
-	val t' = subst_TVars type_inst t
+val t' = subst_TVars type_inst t
 in
-	(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
+(t',map (fn (w,TFree(v,S)) => (v,TVar(w,S))
-		  | _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
+| _ => error "Internal error in Shuffler.freeze_thaw") type_inst)
 end
 fun inst_tfrees thy [] thm = thm
 | inst_tfrees thy ((name,U)::rest) thm =
 let
-	val cU = ctyp_of thy U
+val cU = ctyp_of thy U
-	val tfrees = add_term_tfrees (prop_of thm,[])
+val tfrees = add_term_tfrees (prop_of thm,[])
-	val (rens, thm') = Thm.varifyT'
+val (rens, thm') = Thm.varifyT'
 (remove (op = o apsnd fst) name tfrees) thm
-	val mid =
+val mid =
-	    case rens of
+case rens of
-		[] => thm'
+[] => thm'
-	      | [((_, S), idx)] => instantiate
+| [((_, S), idx)] => instantiate
 ([(ctyp_of thy (TVar (idx, S)), cU)], []) thm'
-	      | _ => error "Shuffler.inst_tfrees internal error"
+| _ => error "Shuffler.inst_tfrees internal error"
 in
-	inst_tfrees thy rest mid
+inst_tfrees thy rest mid
 end
 fun is_Abs (Abs _) = true
 | is_Abs _ = false
 fun eta_redex (t $ Bound 0) =
 let
-	fun free n (Bound i) = i = n
+fun free n (Bound i) = i = n
-	  | free n (t $ u) = free n t orelse free n u
+| free n (t $ u) = free n t orelse free n u
-	  | free n (Abs(_,_,t)) = free (n+1) t
+| free n (Abs(_,_,t)) = free (n+1) t
-	  | free n _ = false
+| free n _ = false
 in
-	not (free 0 t)
+not (free 0 t)
 end
 | eta_redex _ = false
 fun eta_contract thy assumes origt =
 let
-	val (typet,Tinst) = freeze_thaw_term origt
+val (typet,Tinst) = freeze_thaw_term origt
-	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
-	val final = inst_tfrees thy Tinst o thaw
+val final = inst_tfrees thy Tinst o thaw
-	val t = #1 (Logic.dest_equals (prop_of init))
+val t = #1 (Logic.dest_equals (prop_of init))
-	val _ =
+val _ =
-	    let
+let
-		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
+val lhs = #1 (Logic.dest_equals (prop_of (final init)))
-	    in
+in
-		if not (lhs aconv origt)
+if not (lhs aconv origt)
-		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
+then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
-		      writeln (string_of_cterm (cterm_of thy origt));
+writeln (string_of_cterm (cterm_of thy origt));
-		      writeln (string_of_cterm (cterm_of thy lhs));
+writeln (string_of_cterm (cterm_of thy lhs));
-		      writeln (string_of_cterm (cterm_of thy typet));
+writeln (string_of_cterm (cterm_of thy typet));
-		      writeln (string_of_cterm (cterm_of thy t));
+writeln (string_of_cterm (cterm_of thy t));
-		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
+app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
-		      writeln "done")
+writeln "done")
-		else ()
+else ()
-	    end
+end
 in
-	case t of
+case t of
-	    Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
+Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
-	    ((if eta_redex P andalso eta_redex Q
+((if eta_redex P andalso eta_redex Q
-	      then
+then
-		  let
+let
-		      val cert = cterm_of thy
+val cert = cterm_of thy
-		      val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
+val v = Free(Name.variant (add_term_free_names(t,[])) "v",xT)
-		      val cv = cert v
+val cv = cert v
-		      val ct = cert t
+val ct = cert t
-		      val th = (assume ct)
+val th = (assume ct)
-				   |> forall_elim cv
+|> forall_elim cv
-				   |> abstract_rule x cv
+|> abstract_rule x cv
-		      val ext_th = eta_conversion (cert (Abs(x,xT,P)))
+val ext_th = eta_conversion (cert (Abs(x,xT,P)))
-		      val th' = transitive (symmetric ext_th) th
+val th' = transitive (symmetric ext_th) th
-		      val cu = cert (prop_of th')
+val cu = cert (prop_of th')
-		      val uth = combination (assume cu) (reflexive cv)
+val uth = combination (assume cu) (reflexive cv)
-		      val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
+val uth' = (beta_conversion false (cert (Abs(x,xT,Q) $ v)))
-				     |> transitive uth
+|> transitive uth
-				     |> forall_intr cv
+|> forall_intr cv
-				     |> implies_intr cu
+|> implies_intr cu
-		      val rew_th = equal_intr (th' |> implies_intr ct) uth'
+val rew_th = equal_intr (th' |> implies_intr ct) uth'
-		      val res = final rew_th
+val res = final rew_th
-		      val lhs = (#1 (Logic.dest_equals (prop_of res)))
+val lhs = (#1 (Logic.dest_equals (prop_of res)))
-		  in
+in
-		       SOME res
+SOME res
-		  end
+end
-	      else NONE)
+else NONE)
-	     handle e => OldGoals.print_exn e)
+handle e => OldGoals.print_exn e)
-	  | _ => NONE
+| _ => NONE
 end
 fun beta_fun thy assume t =
 SOME (beta_conversion true (cterm_of thy t))
 val meta_sym_rew = thm "refl"
 fun equals_fun thy assume t =
 case t of
-	Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
+Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
 | _ => NONE
 fun eta_expand thy assumes origt =
 let
-	val (typet,Tinst) = freeze_thaw_term origt
+val (typet,Tinst) = freeze_thaw_term origt
-	val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
+val (init,thaw) = freeze_thaw (reflexive (cterm_of thy typet))
-	val final = inst_tfrees thy Tinst o thaw
+val final = inst_tfrees thy Tinst o thaw
-	val t = #1 (Logic.dest_equals (prop_of init))
+val t = #1 (Logic.dest_equals (prop_of init))
-	val _ =
+val _ =
-	    let
+let
-		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
+val lhs = #1 (Logic.dest_equals (prop_of (final init)))
-	    in
+in
-		if not (lhs aconv origt)
+if not (lhs aconv origt)
-		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
+then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
-		      writeln (string_of_cterm (cterm_of thy origt));
+writeln (string_of_cterm (cterm_of thy origt));
-		      writeln (string_of_cterm (cterm_of thy lhs));
+writeln (string_of_cterm (cterm_of thy lhs));
-		      writeln (string_of_cterm (cterm_of thy typet));
+writeln (string_of_cterm (cterm_of thy typet));
-		      writeln (string_of_cterm (cterm_of thy t));
+writeln (string_of_cterm (cterm_of thy t));
-		      app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
+app (fn (n,T) => writeln (n ^ ": " ^ (string_of_ctyp (ctyp_of thy T)))) Tinst;
-		      writeln "done")
+writeln "done")
-		else ()
+else ()
-	    end
+end
 in
-	case t of
+case t of
-	    Const("==",T) $ P $ Q =>
+Const("==",T) $ P $ Q =>
-	    if is_Abs P orelse is_Abs Q
+if is_Abs P orelse is_Abs Q
-	    then (case domain_type T of
+then (case domain_type T of
-		      Type("fun",[aT,bT]) =>
+Type("fun",[aT,bT]) =>
-		      let
+let
-			  val cert = cterm_of thy
+val cert = cterm_of thy
-			  val vname = Name.variant (add_term_free_names(t,[])) "v"
+val vname = Name.variant (add_term_free_names(t,[])) "v"
-			  val v = Free(vname,aT)
+val v = Free(vname,aT)
-			  val cv = cert v
+val cv = cert v
-			  val ct = cert t
+val ct = cert t
-			  val th1 = (combination (assume ct) (reflexive cv))
+val th1 = (combination (assume ct) (reflexive cv))
-					|> forall_intr cv
+|> forall_intr cv
-					|> implies_intr ct
+|> implies_intr ct
-			  val concl = cert (concl_of th1)
+val concl = cert (concl_of th1)
-			  val th2 = (assume concl)
+val th2 = (assume concl)
-					|> forall_elim cv
+|> forall_elim cv
-					|> abstract_rule vname cv
+|> abstract_rule vname cv
-			  val (lhs,rhs) = Logic.dest_equals (prop_of th2)
+val (lhs,rhs) = Logic.dest_equals (prop_of th2)
-			  val elhs = eta_conversion (cert lhs)
+val elhs = eta_conversion (cert lhs)
-			  val erhs = eta_conversion (cert rhs)
+val erhs = eta_conversion (cert rhs)
-			  val th2' = transitive
+val th2' = transitive
-					 (transitive (symmetric elhs) th2)
+(transitive (symmetric elhs) th2)
-					 erhs
+erhs
-			  val res = equal_intr th1 (th2' |> implies_intr concl)
+val res = equal_intr th1 (th2' |> implies_intr concl)
-			  val res' = final res
+val res' = final res
-		      in
+in
-			  SOME res'
+SOME res'
-		      end
+end
-		    | _ => NONE)
+| _ => NONE)
-	    else NONE
+else NONE
-	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
+| _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of thy t))); NONE)
 end
 handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
 fun mk_tfree s = TFree("'"^s,[])
 fun mk_free s t = Free (s,t)
 val R  = mk_free "R" (xT-->yT)
 val S  = mk_free "S" xT
 val S'  = mk_free "S'" xT
 in
 fun beta_simproc thy = Simplifier.simproc_i
-		      thy
+thy
-		      "Beta-contraction"
+"Beta-contraction"
-		      [Abs("x",xT,Q) $ S]
+[Abs("x",xT,Q) $ S]
-		      beta_fun
+beta_fun
 fun equals_simproc thy = Simplifier.simproc_i
-		      thy
+thy
-		      "Ordered rewriting of meta equalities"
+"Ordered rewriting of meta equalities"
-		      [Const("op ==",xT) $ S $ S']
+[Const("op ==",xT) $ S $ S']
-		      equals_fun
+equals_fun
 fun quant_simproc thy = Simplifier.simproc_i
-			   thy
+thy
-			   "Ordered rewriting of nested quantifiers"
+"Ordered rewriting of nested quantifiers"
-			   [all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
+[all xT $ (Abs("x",xT,all yT $ (Abs("y",yT,P $ Bound 1 $ Bound 0))))]
-			   quant_rewrite
+quant_rewrite
 fun eta_expand_simproc thy = Simplifier.simproc_i
-			 thy
+thy
-			 "Smart eta-expansion by equivalences"
+"Smart eta-expansion by equivalences"
-			 [Logic.mk_equals(Q,R)]
+[Logic.mk_equals(Q,R)]
-			 eta_expand
+eta_expand
 fun eta_contract_simproc thy = Simplifier.simproc_i
-			 thy
+thy
-			 "Smart handling of eta-contractions"
+"Smart handling of eta-contractions"
-			 [all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
+[all xT $ (Abs("x",xT,Logic.mk_equals(Q $ Bound 0,R $ Bound 0)))]
-			 eta_contract
+eta_contract
 end
 (* Disambiguates the names of bound variables in a term, returning t
 == t' where all the names of bound variables in t' are unique *)
 fun disamb_bound thy t =
 let
-	fun F (t $ u,idx) =
+fun F (t $ u,idx) =
-	    let
+let
-		val (t',idx') = F (t,idx)
+val (t',idx') = F (t,idx)
-		val (u',idx'') = F (u,idx')
+val (u',idx'') = F (u,idx')
-	    in
+in
-		(t' $ u',idx'')
+(t' $ u',idx'')
-	    end
+end
-	  | F (Abs(x,xT,t),idx) =
+| F (Abs(x,xT,t),idx) =
-	    let
+let
-		val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
+val x' = "x" ^ (LargeInt.toString idx) (* amazing *)
-		val (t',idx') = F (t,idx+1)
+val (t',idx') = F (t,idx+1)
-	    in
+in
-		(Abs(x',xT,t'),idx')
+(Abs(x',xT,t'),idx')
-	    end
+end
-	  | F arg = arg
+| F arg = arg
-	val (t',_) = F (t,0)
+val (t',_) = F (t,0)
-	val ct = cterm_of thy t
+val ct = cterm_of thy t
-	val ct' = cterm_of thy t'
+val ct' = cterm_of thy t'
-	val res = transitive (reflexive ct) (reflexive ct')
+val res = transitive (reflexive ct) (reflexive ct')
-	val _ = message ("disamb_term: " ^ (string_of_thm res))
+val _ = message ("disamb_term: " ^ (string_of_thm res))
 in
-	res
+res
 end
 (* Transforms a term t to some normal form t', returning the theorem t
 == t'.  This is originally a help function for make_equal, but might
 be handy in its own right, for example for indexing terms. *)
 fun norm_term thy t =
 let
-	val norms = ShuffleData.get thy
+val norms = ShuffleData.get thy
-	val ss = Simplifier.theory_context thy empty_ss
+val ss = Simplifier.theory_context thy empty_ss
 setmksimps single
-	  addsimps (map (Thm.transfer thy) norms)
+addsimps (map (Thm.transfer thy) norms)
 addsimprocs [quant_simproc thy, eta_expand_simproc thy,eta_contract_simproc thy]
-	fun chain f th =
+fun chain f th =
-	    let
+let
 val rhs = snd (dest_equals (cprop_of th))
-	    in
+in
-		transitive th (f rhs)
+transitive th (f rhs)
-	    end
+end
-	val th =
+val th =
 t |> disamb_bound thy
-	      |> chain (Simplifier.full_rewrite ss)
+|> chain (Simplifier.full_rewrite ss)
 |> chain eta_conversion
-	      |> strip_shyps
+|> strip_shyps
-	val _ = message ("norm_term: " ^ (string_of_thm th))
+val _ = message ("norm_term: " ^ (string_of_thm th))
 in
-	th
+th
 end
 handle e => (writeln "norm_term internal error"; print_sign_exn thy e)
 (* Closes a theorem with respect to free and schematic variables (does
 not touch type variables, though). *)
 fun close_thm th =
 let
-	val thy = sign_of_thm th
+val thy = sign_of_thm th
-	val c = prop_of th
+val c = prop_of th
-	val vars = add_term_frees (c,add_term_vars(c,[]))
+val vars = add_term_frees (c,add_term_vars(c,[]))
 in
-	Drule.forall_intr_list (map (cterm_of thy) vars) th
+Drule.forall_intr_list (map (cterm_of thy) vars) th
 end
 handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
 (* Normalizes a theorem's conclusion using norm_term. *)
 fun norm_thm thy th =
 let
-	val c = prop_of th
+val c = prop_of th
 in
-	equal_elim (norm_term thy c) th
+equal_elim (norm_term thy c) th
 end
 (* make_equal thy t u tries to construct the theorem t == u under the
 signature thy.  If it succeeds, SOME (t == u) is returned, otherwise
 NONE is returned. *)
 fun make_equal thy t u =
 let
-	val t_is_t' = norm_term thy t
+val t_is_t' = norm_term thy t
-	val u_is_u' = norm_term thy u
+val u_is_u' = norm_term thy u
-	val th = transitive t_is_t' (symmetric u_is_u')
+val th = transitive t_is_t' (symmetric u_is_u')
-	val _ = message ("make_equal: SOME " ^ (string_of_thm th))
+val _ = message ("make_equal: SOME " ^ (string_of_thm th))
 in
-	SOME th
+SOME th
 end
 handle e as THM _ => (message "make_equal: NONE";NONE)
 fun match_consts ignore t (* th *) =
 let
-	fun add_consts (Const (c, _), cs) =
+fun add_consts (Const (c, _), cs) =
-	    if c mem_string ignore
+if c mem_string ignore
-	    then cs
+then cs
-	    else insert (op =) c cs
+else insert (op =) c cs
-	  | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
+| add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
-	  | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
+| add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
-	  | add_consts (_, cs) = cs
+| add_consts (_, cs) = cs
-	val t_consts = add_consts(t,[])
+val t_consts = add_consts(t,[])
 in
 fn (name,th) =>
-	let
+let
-	    val th_consts = add_consts(prop_of th,[])
+val th_consts = add_consts(prop_of th,[])
-	in
+in
-	    eq_set(t_consts,th_consts)
+eq_set(t_consts,th_consts)
-	end
+end
 end
 val collect_ignored =
 fold_rev (fn thm => fn cs =>
-	      let
+let
-		  val (lhs,rhs) = Logic.dest_equals (prop_of thm)
+val (lhs,rhs) = Logic.dest_equals (prop_of thm)
-		  val ignore_lhs = term_consts lhs \\ term_consts rhs
+val ignore_lhs = term_consts lhs \\ term_consts rhs
-		  val ignore_rhs = term_consts rhs \\ term_consts lhs
+val ignore_rhs = term_consts rhs \\ term_consts lhs
-	      in
+in
-		  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
+fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
-	      end)
+end)
 (* set_prop t thms tries to make a theorem with the proposition t from
 one of the theorems thms, by shuffling the propositions around.  If it
 succeeds, SOME theorem is returned, otherwise NONE.  *)
 fun set_prop thy t =
 let
-	val vars = add_term_frees (t,add_term_vars (t,[]))
+val vars = add_term_frees (t,add_term_vars (t,[]))
-	val closed_t = Library.foldr (fn (v, body) =>
+val closed_t = Library.foldr (fn (v, body) =>
 let val vT = type_of v in all vT $ (Abs ("x", vT, abstract_over (v, body))) end) (vars, t)
-	val rew_th = norm_term thy closed_t
+val rew_th = norm_term thy closed_t
-	val rhs = snd (dest_equals (cprop_of rew_th))
+val rhs = snd (dest_equals (cprop_of rew_th))
-	val shuffles = ShuffleData.get thy
+val shuffles = ShuffleData.get thy
-	fun process [] = NONE
+fun process [] = NONE
-	  | process ((name,th)::thms) =
+| process ((name,th)::thms) =
-	    let
+let
-		val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
+val norm_th = Thm.varifyT (norm_thm thy (close_thm (Thm.transfer thy th)))
-		val triv_th = trivial rhs
+val triv_th = trivial rhs
-		val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
+val _ = message ("Shuffler.set_prop: Gluing together " ^ (string_of_thm norm_th) ^ " and " ^ (string_of_thm triv_th))
-		val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
+val mod_th = case Seq.pull (bicompose false (*true*) (false,norm_th,0) 1 triv_th) of
-				 SOME(th,_) => SOME th
+SOME(th,_) => SOME th
-			       | NONE => NONE
+| NONE => NONE
-	    in
+in
-		case mod_th of
+case mod_th of
-		    SOME mod_th =>
+SOME mod_th =>
-		    let
+let
-			val closed_th = equal_elim (symmetric rew_th) mod_th
+val closed_th = equal_elim (symmetric rew_th) mod_th
-		    in
+in
-			message ("Shuffler.set_prop succeeded by " ^ name);
+message ("Shuffler.set_prop succeeded by " ^ name);
-			SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
+SOME (name,forall_elim_list (map (cterm_of thy) vars) closed_th)
-		    end
+end
-		  | NONE => process thms
+| NONE => process thms
-	    end
+end
-	    handle e as THM _ => process thms
+handle e as THM _ => process thms
 in
-	fn thms =>
+fn thms =>
-	   case process thms of
+case process thms of
-	       res as SOME (name,th) => if (prop_of th) aconv t
+res as SOME (name,th) => if (prop_of th) aconv t
-					then res
+then res
-					else error "Internal error in set_prop"
+else error "Internal error in set_prop"
-	     | NONE => NONE
+| NONE => NONE
 end
 handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
 fun find_potential thy t =
 let
-	val shuffles = ShuffleData.get thy
+val shuffles = ShuffleData.get thy
-	val ignored = collect_ignored shuffles []
+val ignored = collect_ignored shuffles []
-	val rel_consts = term_consts t \\ ignored
+val rel_consts = term_consts t \\ ignored
-	val pot_thms = PureThy.thms_containing_consts thy rel_consts
+val pot_thms = PureThy.thms_containing_consts thy rel_consts
 in
-	List.filter (match_consts ignored t) pot_thms
+List.filter (match_consts ignored t) pot_thms
 end
 fun gen_shuffle_tac thy search thms i st =
 let
-	val _ = message ("Shuffling " ^ (string_of_thm st))
+val _ = message ("Shuffling " ^ (string_of_thm st))
-	val t = List.nth(prems_of st,i-1)
+val t = List.nth(prems_of st,i-1)
-	val set = set_prop thy t
+val set = set_prop thy t
-	fun process_tac thms st =
+fun process_tac thms st =
-	    case set thms of
+case set thms of
-		SOME (_,th) => Seq.of_list (compose (th,i,st))
+SOME (_,th) => Seq.of_list (compose (th,i,st))
-	      | NONE => Seq.empty
+| NONE => Seq.empty
 in
-	(process_tac thms APPEND (if search
+(process_tac thms APPEND (if search
-				  then process_tac (find_potential thy t)
+then process_tac (find_potential thy t)
-				  else no_tac)) st
+else no_tac)) st
 end
 fun shuffle_tac thms i st =
 gen_shuffle_tac (the_context()) false thms i st
 fun search_tac thms i st =
 gen_shuffle_tac (the_context()) true thms i st
 fun shuffle_meth (thms:thm list) ctxt =
 let
-	val thy = ProofContext.theory_of ctxt
+val thy = ProofContext.theory_of ctxt
 in
-	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy false (map (pair "") thms))
+Method.SIMPLE_METHOD' (gen_shuffle_tac thy false (map (pair "") thms))
 end
 fun search_meth ctxt =
 let
-	val thy = ProofContext.theory_of ctxt
+val thy = ProofContext.theory_of ctxt
-	val prems = Assumption.prems_of ctxt
+val prems = Assumption.prems_of ctxt
 in
-	Method.SIMPLE_METHOD' HEADGOAL (gen_shuffle_tac thy true (map (pair "premise") prems))
+Method.SIMPLE_METHOD' (gen_shuffle_tac thy true (map (pair "premise") prems))
 end
 val print_shuffles = ShuffleData.print
 fun add_shuffle_rule thm thy =
 let
-	val shuffles = ShuffleData.get thy
+val shuffles = ShuffleData.get thy
 in
-	if exists (curry Thm.eq_thm thm) shuffles
+if exists (curry Thm.eq_thm thm) shuffles
-	then (warning ((string_of_thm thm) ^ " already known to the shuffler");
+then (warning ((string_of_thm thm) ^ " already known to the shuffler");
-	      thy)
+thy)
-	else ShuffleData.put (thm::shuffles) thy
+else ShuffleData.put (thm::shuffles) thy
 end
 val shuffle_attr = Thm.declaration_attribute (fn th => Context.mapping (add_shuffle_rule th) I);
 val setup =

changeset 21588	cd0dc678a205
parent 21078	101aefd61aac
child 22578	b0eb5652f210