QuotMain.thy
changeset 577 8dab8d82f26b
parent 576 33ff4b5f1806
child 578 070161f1996a
equal deleted inserted replaced
576:33ff4b5f1806 577:8dab8d82f26b
   267        if (length tys = length tys') 
   267        if (length tys = length tys') 
   268        then (List.all matches_typ (tys ~~ tys')) 
   268        then (List.all matches_typ (tys ~~ tys')) 
   269        else false
   269        else false
   270   | _ => false
   270   | _ => false
   271 *}
   271 *}
       
   272 
   272 ML {*
   273 ML {*
   273 fun matches_term (trm, trm') = 
   274 fun matches_term (trm, trm') = 
   274    case (trm, trm') of 
   275    case (trm, trm') of 
   275      (_, Var _) => true
   276      (_, Var _) => true
   276    | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
   277    | (Const (s, ty), Const (s', ty')) => s = s' andalso matches_typ (ty, ty')
   952 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
   953 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
   953 (case (bare_concl goal) of
   954 (case (bare_concl goal) of
   954     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
   955     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
   955   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
   956   ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
   956       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
   957       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
       
   958 
   957     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
   959     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
   958 | (Const (@{const_name "op ="},_) $
   960 | (Const (@{const_name "op ="},_) $
   959     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   961     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   960     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   962     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
   961       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
   963       => rtac @{thm ball_rsp} THEN' dtac @{thm QT_all}
       
   964 
   962     (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
   965     (* (R1 ===> op =) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Ball\<dots>x) = (Ball\<dots>y) *)
   963 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   966 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   964     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   967     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   965     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   968     (Const(@{const_name Ball},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   966       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
   969       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
       
   970 
   967     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
   971     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
   968 | Const (@{const_name "op ="},_) $
   972 | Const (@{const_name "op ="},_) $
   969     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   973     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   970     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   974     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   971       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
   975       => rtac @{thm bex_rsp} THEN' dtac @{thm QT_ex}
       
   976 
   972     (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
   977     (* (R1 ===> op =) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> (Bex\<dots>x) = (Bex\<dots>y) *)
   973 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   978 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   974     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   979     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
   975     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   980     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
   976       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
   981       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
   977 | Const (@{const_name "op ="},_) $ _ $ _ => 
   982 
   978     (* reflexivity of operators arising from Cong_tac *)
   983     (* reflexivity of operators arising from Cong_tac *)
   979     rtac @{thm refl} ORELSE'
   984 | Const (@{const_name "op ="},_) $ _ $ _ 
   980     (resolve_tac trans2 THEN' RANGE [
   985       => rtac @{thm refl} ORELSE'
   981       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
   986           (resolve_tac trans2 THEN' RANGE [
       
   987             quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
       
   988 
   982 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   989 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
   983     (Const (@{const_name fun_rel}, _) $ _ $ _) $
   990     (Const (@{const_name fun_rel}, _) $ _ $ _) $
   984     (Const (@{const_name fun_rel}, _) $ _ $ _)
   991     (Const (@{const_name fun_rel}, _) $ _ $ _)
   985     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
   992     => rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt
   986 | _ $ (Const _) $ (Const _) => (* fun_rel, list_rel, etc but not equality *)
   993 
   987     (* respectfulness of constants; in particular of a simple relation *)
   994    (* respectfulness of constants; in particular of a simple relation *)
   988     resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
   995 | _ $ (Const _) $ (Const _)  (* fun_rel, list_rel, etc but not equality *)
   989 | _ $ _ $ _ =>
   996     => resolve_tac (rsp_rules_get ctxt) THEN_ALL_NEW quotient_tac ctxt
       
   997 
   990     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
   998     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
   991     (* observe ---> *)
   999     (* observe ---> *)
   992     rep_abs_rsp_tac ctxt
  1000 | _ $ _ $ _ 
       
  1001     => rep_abs_rsp_tac ctxt
       
  1002 
   993 | _ => error "inj_repabs_tac not a relation"
  1003 | _ => error "inj_repabs_tac not a relation"
   994 ) i)
  1004 ) i)
   995 *}
  1005 *}
   996 
  1006 
   997 ML {*
  1007 ML {*