separated the lifting and descending procedures in the quotient package
authorChristian Urban <urbanc@in.tum.de>
Tue Jun 29 01:38:29 2010 +0100 (2010-06-29)
changeset 375932505feaf2d70
parent 37592 e16495cfdde0
child 37594 32ad67684ee7
separated the lifting and descending procedures in the quotient package
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_tacs.ML
     1.1 --- a/src/HOL/Quotient.thy	Mon Jun 28 16:20:39 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Tue Jun 29 01:38:29 2010 +0100
     1.3 @@ -764,13 +764,23 @@
     1.4  subsection {* Methods / Interface *}
     1.5  
     1.6  method_setup lifting =
     1.7 -  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
     1.8 +  {* Attrib.thms >> (fn thms => fn ctxt => 
     1.9 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
    1.10    {* lifts theorems to quotient types *}
    1.11  
    1.12  method_setup lifting_setup =
    1.13 -  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
    1.14 +  {* Attrib.thm >> (fn thm => fn ctxt => 
    1.15 +       SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt thm))) *}
    1.16    {* sets up the three goals for the quotient lifting procedure *}
    1.17  
    1.18 +method_setup descending =
    1.19 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt))) *}
    1.20 +  {* decends theorems to the raw level *}
    1.21 +
    1.22 +method_setup descending_setup =
    1.23 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt))) *}
    1.24 +  {* sets up the three goals for the decending theorems *}
    1.25 +
    1.26  method_setup regularize =
    1.27    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
    1.28    {* proves the regularization goals from the quotient lifting procedure *}
     2.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Jun 28 16:20:39 2010 +0100
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Jun 29 01:38:29 2010 +0100
     2.3 @@ -11,10 +11,13 @@
     2.4    val injection_tac: Proof.context -> int -> tactic
     2.5    val all_injection_tac: Proof.context -> int -> tactic
     2.6    val clean_tac: Proof.context -> int -> tactic
     2.7 -  val procedure_tac: Proof.context -> thm list -> int -> tactic
     2.8 +  
     2.9 +  val descend_procedure_tac: Proof.context -> int -> tactic
    2.10 +  val descend_tac: Proof.context -> int -> tactic
    2.11 + 
    2.12 +  val lift_procedure_tac: Proof.context -> thm -> int -> tactic
    2.13    val lift_tac: Proof.context -> thm list -> int -> tactic
    2.14 -  val quotient_tac: Proof.context -> int -> tactic
    2.15 -  val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic
    2.16 +
    2.17    val lifted: typ list -> Proof.context -> thm -> thm
    2.18    val lifted_attrib: attribute
    2.19  end;
    2.20 @@ -615,55 +618,64 @@
    2.21       SOME (cterm_of thy inj_goal)] lifting_procedure_thm
    2.22  end
    2.23  
    2.24 -(* the tactic leaves three subgoals to be proved *)
    2.25 -fun procedure_tac ctxt rthm =
    2.26 +
    2.27 +(** descending as tactic **)
    2.28 +
    2.29 +fun descend_procedure_tac ctxt =
    2.30    Object_Logic.full_atomize_tac
    2.31    THEN' gen_frees_tac ctxt
    2.32    THEN' SUBGOAL (fn (goal, i) =>
    2.33 -    case rthm of
    2.34 -      [] =>
    2.35          let
    2.36            val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
    2.37            val rtrm = derive_rtrm qtys goal ctxt
    2.38 -          val rule = procedure_inst ctxt rtrm goal
    2.39 +          val rule = procedure_inst ctxt rtrm  goal
    2.40          in
    2.41            rtac rule i
    2.42 -        end
    2.43 -    | [rthm'] =>
    2.44 -        let
    2.45 -          val rthm'' = atomize_thm rthm'
    2.46 -          val rule = procedure_inst ctxt (prop_of rthm'') goal
    2.47 -        in
    2.48 -          (rtac rule THEN' rtac rthm'') i
    2.49 -        end
    2.50 -    | _ => error "more than one raw theorem given")
    2.51 +        end)
    2.52 +
    2.53 +fun descend_tac ctxt =
    2.54 +let
    2.55 +  val mk_tac_raw =
    2.56 +    descend_procedure_tac ctxt
    2.57 +    THEN' RANGE
    2.58 +      [Object_Logic.rulify_tac THEN' (K all_tac),
    2.59 +       regularize_tac ctxt,
    2.60 +       all_injection_tac ctxt,
    2.61 +       clean_tac ctxt]
    2.62 +in
    2.63 +  Goal.conjunction_tac THEN_ALL_NEW mk_tac_raw
    2.64 +end
    2.65  
    2.66  
    2.67 -(* Automatic Proofs *)
    2.68 +(** lifting as tactic **)
    2.69 +
    2.70 +(* the tactic leaves three subgoals to be proved *)
    2.71 +fun lift_procedure_tac ctxt rthm =
    2.72 +  Object_Logic.full_atomize_tac
    2.73 +  THEN' gen_frees_tac ctxt
    2.74 +  THEN' SUBGOAL (fn (goal, i) =>
    2.75 +    let
    2.76 +      val rthm' = atomize_thm rthm
    2.77 +      val rule = procedure_inst ctxt (prop_of rthm') goal
    2.78 +    in
    2.79 +      (rtac rule THEN' rtac rthm') i
    2.80 +    end)
    2.81  
    2.82  fun lift_tac ctxt rthms =
    2.83  let
    2.84    fun mk_tac rthm =
    2.85 -    procedure_tac ctxt [rthm]
    2.86 -    THEN' RANGE
    2.87 -      [regularize_tac ctxt,
    2.88 -       all_injection_tac ctxt,
    2.89 -       clean_tac ctxt];
    2.90 -  val mk_tac_raw =
    2.91 -    procedure_tac ctxt []
    2.92 +    lift_procedure_tac ctxt rthm
    2.93      THEN' RANGE
    2.94 -      [fn _ => all_tac,
    2.95 -       regularize_tac ctxt,
    2.96 -       all_injection_tac ctxt,
    2.97 -       clean_tac ctxt]
    2.98 +      [ regularize_tac ctxt,
    2.99 +        all_injection_tac ctxt,
   2.100 +        clean_tac ctxt ]
   2.101  in
   2.102 -  simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *)
   2.103 -  THEN'
   2.104 -    (case rthms of
   2.105 -      [] => mk_tac_raw
   2.106 -    | _ => RANGE (map mk_tac rthms))
   2.107 +  Goal.conjunction_tac THEN' RANGE (map mk_tac rthms)
   2.108  end
   2.109  
   2.110 +
   2.111 +(** lifting as attribute **)
   2.112 +
   2.113  fun lifted qtys ctxt thm =
   2.114  let
   2.115    (* When the theorem is atomized, eta redexes are contracted,
   2.116 @@ -676,15 +688,12 @@
   2.117    |> singleton (ProofContext.export ctxt' ctxt)
   2.118  end;
   2.119  
   2.120 -(* An attribute which automatically constructs the qthm 
   2.121 -   using all quotients defined so far.
   2.122 -*)
   2.123  val lifted_attrib = Thm.rule_attribute (fn context => 
   2.124 -       let
   2.125 -         val ctxt = Context.proof_of context
   2.126 -         val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
   2.127 -       in
   2.128 -         lifted qtys ctxt
   2.129 -       end)
   2.130 +  let
   2.131 +    val ctxt = Context.proof_of context
   2.132 +    val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
   2.133 +  in
   2.134 +    lifted qtys ctxt
   2.135 +  end)
   2.136  
   2.137  end; (* structure *)